diff options
Diffstat (limited to '')
| -rw-r--r-- | compiler/InterpreterLoopsFixedPoint.mli | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/compiler/InterpreterLoopsFixedPoint.mli b/compiler/InterpreterLoopsFixedPoint.mli index 7c3f6199..d727e9bd 100644 --- a/compiler/InterpreterLoopsFixedPoint.mli +++ b/compiler/InterpreterLoopsFixedPoint.mli @@ -60,7 +60,7 @@ val cleanup_fresh_values_and_abs : config -> ids_sets -> Cps.cm_fun we only introduce a fresh abstraction for [l1]. *) -val prepare_ashared_loans : loop_id option -> Cps.cm_fun +val prepare_ashared_loans : Meta.meta -> loop_id option -> Cps.cm_fun (** Compute a fixed-point for the context at the entry of the loop. We also return: @@ -77,6 +77,7 @@ val prepare_ashared_loans : loop_id option -> Cps.cm_fun the values which are read or modified (some symbolic values may be ignored). *) val compute_loop_entry_fixed_point : + Meta.meta -> config -> loop_id -> Cps.st_cm_fun -> @@ -160,7 +161,7 @@ val compute_loop_entry_fixed_point : through the loan [l1] is actually the value which has to be given back to [l0]. *) val compute_fixed_point_id_correspondance : - ids_sets -> eval_ctx -> eval_ctx -> borrow_loan_corresp + Meta.meta -> ids_sets -> eval_ctx -> eval_ctx -> borrow_loan_corresp (** Compute the set of "quantified" symbolic value ids in a fixed-point context. @@ -169,4 +170,4 @@ val compute_fixed_point_id_correspondance : - the list of input symbolic values *) val compute_fp_ctx_symbolic_values : - eval_ctx -> eval_ctx -> symbolic_value_id_set * symbolic_value list + Meta.meta -> eval_ctx -> eval_ctx -> symbolic_value_id_set * symbolic_value list |