Merge pull request #175 from AeneasVerif/afromher/meta

Rename meta into span

2 files changed, 78 insertions, 78 deletions

diff --git a/compiler/InterpreterLoopsFixedPoint.ml b/compiler/InterpreterLoopsFixedPoint.ml
index 329abcf3..6c87f1c8 100644
--- a/compiler/InterpreterLoopsFixedPoint.ml
+++ b/compiler/InterpreterLoopsFixedPoint.ml
@@ -23,7 +23,7 @@ exception FoundAbsId of AbstractionId.id
    - end the borrows which appear in fresh anonymous values and don't contain loans
    - end the fresh region abstractions which can be ended (no loans)
 *)
-let rec end_useless_fresh_borrows_and_abs (config : config) (meta : Meta.meta)
+let rec end_useless_fresh_borrows_and_abs (config : config) (span : Meta.span)
     (fixed_ids : ids_sets) : cm_fun =
  fun ctx ->
   let rec explore_env (env : env) : unit =
@@ -56,7 +56,7 @@ let rec end_useless_fresh_borrows_and_abs (config : config) (meta : Meta.meta)
     | EAbs abs :: env when not (AbstractionId.Set.mem abs.abs_id fixed_ids.aids)
       -> (
         (* Check if it is possible to end the abstraction: if yes, raise an exception *)
-        let opt_loan = get_first_non_ignored_aloan_in_abstraction meta abs in
+        let opt_loan = get_first_non_ignored_aloan_in_abstraction span abs in
         match opt_loan with
         | None ->
             (* No remaining loans: we can end the abstraction *)
@@ -66,7 +66,7 @@ let rec end_useless_fresh_borrows_and_abs (config : config) (meta : Meta.meta)
             explore_env env)
     | _ :: env -> explore_env env
   in
-  let rec_call = end_useless_fresh_borrows_and_abs config meta fixed_ids in
+  let rec_call = end_useless_fresh_borrows_and_abs config span fixed_ids in
   try
     (* Explore the environment *)
     explore_env ctx.env;
@@ -74,10 +74,10 @@ let rec end_useless_fresh_borrows_and_abs (config : config) (meta : Meta.meta)
     (ctx, fun e -> e)
   with
   | FoundAbsId abs_id ->
-      let ctx, cc = end_abstraction config meta abs_id ctx in
+      let ctx, cc = end_abstraction config span abs_id ctx in
       comp cc (rec_call ctx)
   | FoundBorrowId bid ->
-      let ctx, cc = end_borrow config meta bid ctx in
+      let ctx, cc = end_borrow config span bid ctx in
       comp cc (rec_call ctx)
 
 (* Explore the fresh anonymous values and replace all the values which are not
@@ -119,10 +119,10 @@ let cleanup_fresh_values (fixed_ids : ids_sets) (ctx : eval_ctx) : eval_ctx =
    - also end the borrows which appear in fresh anonymous values and don't contain loans
    - end the fresh region abstractions which can be ended (no loans)
 *)
-let cleanup_fresh_values_and_abs (config : config) (meta : Meta.meta)
+let cleanup_fresh_values_and_abs (config : config) (span : Meta.span)
     (fixed_ids : ids_sets) : cm_fun =
  fun ctx ->
-  let ctx, cc = end_useless_fresh_borrows_and_abs config meta fixed_ids ctx in
+  let ctx, cc = end_useless_fresh_borrows_and_abs config span fixed_ids ctx in
   let ctx = cleanup_fresh_values fixed_ids ctx in
   (ctx, cc)
 
@@ -133,7 +133,7 @@ let cleanup_fresh_values_and_abs (config : config) (meta : Meta.meta)
     called typically after we merge abstractions together (see {!collapse_ctx}
     for instance).
  *)
-let reorder_loans_borrows_in_fresh_abs (meta : Meta.meta)
+let reorder_loans_borrows_in_fresh_abs (span : Meta.span)
     (old_abs_ids : AbstractionId.Set.t) (ctx : eval_ctx) : eval_ctx =
   let reorder_in_fresh_abs (abs : abs) : abs =
     (* Split between the loans and borrows *)
@@ -141,7 +141,7 @@ let reorder_loans_borrows_in_fresh_abs (meta : Meta.meta)
       match av.value with
       | ABorrow _ -> true
       | ALoan _ -> false
-      | _ -> craise __FILE__ __LINE__ meta "Unexpected"
+      | _ -> craise __FILE__ __LINE__ span "Unexpected"
     in
     let aborrows, aloans = List.partition is_borrow abs.avalues in
 
@@ -154,13 +154,13 @@ let reorder_loans_borrows_in_fresh_abs (meta : Meta.meta)
     let get_borrow_id (av : typed_avalue) : BorrowId.id =
       match av.value with
       | ABorrow (AMutBorrow (bid, _) | ASharedBorrow bid) -> bid
-      | _ -> craise __FILE__ __LINE__ meta "Unexpected"
+      | _ -> craise __FILE__ __LINE__ span "Unexpected"
     in
     let get_loan_id (av : typed_avalue) : BorrowId.id =
       match av.value with
       | ALoan (AMutLoan (lid, _)) -> lid
       | ALoan (ASharedLoan (lids, _, _)) -> BorrowId.Set.min_elt lids
-      | _ -> craise __FILE__ __LINE__ meta "Unexpected"
+      | _ -> craise __FILE__ __LINE__ span "Unexpected"
     in
     (* We use ordered maps to reorder the borrows and loans *)
     let reorder (get_bid : typed_avalue -> BorrowId.id)
@@ -184,7 +184,7 @@ let reorder_loans_borrows_in_fresh_abs (meta : Meta.meta)
 
   { ctx with env }
 
-let prepare_ashared_loans (meta : Meta.meta) (loop_id : LoopId.id option) :
+let prepare_ashared_loans (span : Meta.span) (loop_id : LoopId.id option) :
     cm_fun =
  fun ctx0 ->
   let ctx = ctx0 in
@@ -213,7 +213,7 @@ let prepare_ashared_loans (meta : Meta.meta) (loop_id : LoopId.id option) :
     (* Remove the shared loans *)
     let v = value_remove_shared_loans v in
     (* Substitute the symbolic values and the region *)
-    Substitute.typed_value_subst_ids meta
+    Substitute.typed_value_subst_ids span
       (fun r -> if RegionId.Set.mem r rids then nrid else r)
       (fun x -> x)
       (fun x -> x)
@@ -265,32 +265,32 @@ let prepare_ashared_loans (meta : Meta.meta) (loop_id : LoopId.id option) :
     borrow_substs := (lid, nlid) :: !borrow_substs;
 
     (* Rem.: the below sanity checks are not really necessary *)
-    sanity_check __FILE__ __LINE__ (AbstractionId.Set.is_empty abs.parents) meta;
-    sanity_check __FILE__ __LINE__ (abs.original_parents = []) meta;
+    sanity_check __FILE__ __LINE__ (AbstractionId.Set.is_empty abs.parents) span;
+    sanity_check __FILE__ __LINE__ (abs.original_parents = []) span;
     sanity_check __FILE__ __LINE__
       (RegionId.Set.is_empty abs.ancestors_regions)
-      meta;
+      span;
 
     (* Introduce the new abstraction for the shared values *)
-    cassert __FILE__ __LINE__ (ty_no_regions sv.ty) meta
+    cassert __FILE__ __LINE__ (ty_no_regions sv.ty) span
       "Nested borrows are not supported yet";
     let rty = sv.ty in
 
     (* Create the shared loan child *)
     let child_rty = rty in
-    let child_av = mk_aignored meta child_rty in
+    let child_av = mk_aignored span child_rty in
 
     (* Create the shared loan *)
     let loan_rty = TRef (RFVar nrid, rty, RShared) in
     let loan_value =
       ALoan (ASharedLoan (BorrowId.Set.singleton nlid, nsv, child_av))
     in
-    let loan_value = mk_typed_avalue meta loan_rty loan_value in
+    let loan_value = mk_typed_avalue span loan_rty loan_value in
 
     (* Create the shared borrow *)
     let borrow_rty = loan_rty in
     let borrow_value = ABorrow (ASharedBorrow lid) in
-    let borrow_value = mk_typed_avalue meta borrow_rty borrow_value in
+    let borrow_value = mk_typed_avalue span borrow_rty borrow_value in
 
     (* Create the abstraction *)
     let avalues = [ borrow_value; loan_value ] in
@@ -324,7 +324,7 @@ let prepare_ashared_loans (meta : Meta.meta) (loop_id : LoopId.id option) :
   let collect_shared_values_in_abs (abs : abs) : unit =
     let collect_shared_value lids (sv : typed_value) =
       (* Sanity check: we don't support nested borrows for now *)
-      sanity_check __FILE__ __LINE__ (not (value_has_borrows ctx sv.value)) meta;
+      sanity_check __FILE__ __LINE__ (not (value_has_borrows ctx sv.value)) span;
 
       (* Filter the loan ids whose corresponding borrows appear in abstractions
          (see the documentation of the function) *)
@@ -360,7 +360,7 @@ let prepare_ashared_loans (meta : Meta.meta) (loop_id : LoopId.id option) :
         method! visit_symbolic_value env sv =
           cassert __FILE__ __LINE__
             (not (symbolic_value_has_borrows ctx sv))
-            meta
+            span
             "There should be no symbolic values with borrows inside the \
              abstraction";
           super#visit_symbolic_value env sv
@@ -441,11 +441,11 @@ let prepare_ashared_loans (meta : Meta.meta) (loop_id : LoopId.id option) :
   in
   (ctx, cf)
 
-let prepare_ashared_loans_no_synth (meta : Meta.meta) (loop_id : LoopId.id)
+let prepare_ashared_loans_no_synth (span : Meta.span) (loop_id : LoopId.id)
     (ctx : eval_ctx) : eval_ctx =
-  fst (prepare_ashared_loans meta (Some loop_id) ctx)
+  fst (prepare_ashared_loans span (Some loop_id) ctx)
 
-let compute_loop_entry_fixed_point (config : config) (meta : Meta.meta)
+let compute_loop_entry_fixed_point (config : config) (span : Meta.span)
     (loop_id : LoopId.id) (eval_loop_body : stl_cm_fun) (ctx0 : eval_ctx) :
     eval_ctx * ids_sets * abs RegionGroupId.Map.t =
   (* Introduce "reborrows" for the shared values in the abstractions, so that
@@ -455,16 +455,16 @@ let compute_loop_entry_fixed_point (config : config) (meta : Meta.meta)
 
      For more details, see the comments for {!prepare_ashared_loans}
   *)
-  let ctx = prepare_ashared_loans_no_synth meta loop_id ctx0 in
+  let ctx = prepare_ashared_loans_no_synth span loop_id ctx0 in
 
   (* Debug *)
   log#ldebug
     (lazy
       ("compute_loop_entry_fixed_point: after prepare_ashared_loans:"
      ^ "\n\n- ctx0:\n"
-      ^ eval_ctx_to_string_no_filter ~meta:(Some meta) ctx0
+      ^ eval_ctx_to_string_no_filter ~span:(Some span) ctx0
       ^ "\n\n- ctx1:\n"
-      ^ eval_ctx_to_string_no_filter ~meta:(Some meta) ctx
+      ^ eval_ctx_to_string_no_filter ~span:(Some span) ctx
       ^ "\n\n"));
 
   (* The fixed ids. They are the ids of the original ctx, after we ended
@@ -496,10 +496,10 @@ let compute_loop_entry_fixed_point (config : config) (meta : Meta.meta)
           (* End those borrows and abstractions *)
           let end_borrows_abs blids aids ctx =
             let ctx =
-              InterpreterBorrows.end_borrows_no_synth config meta blids ctx
+              InterpreterBorrows.end_borrows_no_synth config span blids ctx
             in
             let ctx =
-              InterpreterBorrows.end_abstractions_no_synth config meta aids ctx
+              InterpreterBorrows.end_abstractions_no_synth config span aids ctx
             in
             ctx
           in
@@ -530,7 +530,7 @@ let compute_loop_entry_fixed_point (config : config) (meta : Meta.meta)
 
     (* Join the context with the context at the loop entry *)
     let (_, _), ctx2 =
-      loop_join_origin_with_continue_ctxs config meta loop_id fixed_ids ctx1
+      loop_join_origin_with_continue_ctxs config span loop_id fixed_ids ctx1
         ctxs
     in
     ctx2
@@ -560,15 +560,15 @@ let compute_loop_entry_fixed_point (config : config) (meta : Meta.meta)
     log#ldebug (lazy "compute_fixed_point: equiv_ctx:");
     let fixed_ids = compute_fixed_ids [ ctx1; ctx2 ] in
     let check_equivalent = true in
-    let lookup_shared_value _ = craise __FILE__ __LINE__ meta "Unreachable" in
+    let lookup_shared_value _ = craise __FILE__ __LINE__ span "Unreachable" in
     Option.is_some
-      (match_ctxs meta check_equivalent fixed_ids lookup_shared_value
+      (match_ctxs span check_equivalent fixed_ids lookup_shared_value
          lookup_shared_value ctx1 ctx2)
   in
   let max_num_iter = Config.loop_fixed_point_max_num_iters in
   let rec compute_fixed_point (ctx : eval_ctx) (i0 : int) (i : int) : eval_ctx =
     if i = 0 then
-      craise __FILE__ __LINE__ meta
+      craise __FILE__ __LINE__ span
         ("Could not compute a loop fixed point in " ^ string_of_int i0
        ^ " iterations")
     else
@@ -582,15 +582,15 @@ let compute_loop_entry_fixed_point (config : config) (meta : Meta.meta)
         | Return | Panic | Break _ -> None
         | Unit ->
             (* See the comment in {!eval_loop} *)
-            craise __FILE__ __LINE__ meta "Unreachable"
+            craise __FILE__ __LINE__ span "Unreachable"
         | Continue i ->
             (* For now we don't support continues to outer loops *)
-            cassert __FILE__ __LINE__ (i = 0) meta
+            cassert __FILE__ __LINE__ (i = 0) span
               "Continues to outer loops not supported yet";
             Some ctx
         | LoopReturn _ | EndEnterLoop _ | EndContinue _ ->
             (* We don't support nested loops for now *)
-            craise __FILE__ __LINE__ meta
+            craise __FILE__ __LINE__ span
               "Nested loops are not supported for now"
       in
       let continue_ctxs = List.filter_map keep_continue_ctx ctx_resl in
@@ -602,9 +602,9 @@ let compute_loop_entry_fixed_point (config : config) (meta : Meta.meta)
       log#ldebug
         (lazy
           ("compute_fixed_point:" ^ "\n\n- ctx0:\n"
-          ^ eval_ctx_to_string_no_filter ~meta:(Some meta) ctx
+          ^ eval_ctx_to_string_no_filter ~span:(Some span) ctx
           ^ "\n\n- ctx1:\n"
-          ^ eval_ctx_to_string_no_filter ~meta:(Some meta) ctx1
+          ^ eval_ctx_to_string_no_filter ~span:(Some span) ctx1
           ^ "\n\n"));
 
       (* Check if we reached a fixed point: if not, iterate *)
@@ -617,7 +617,7 @@ let compute_loop_entry_fixed_point (config : config) (meta : Meta.meta)
     (lazy
       ("compute_fixed_point: fixed point computed before matching with input \
         region groups:" ^ "\n\n- fp:\n"
-      ^ eval_ctx_to_string_no_filter ~meta:(Some meta) fp
+      ^ eval_ctx_to_string_no_filter ~span:(Some span) fp
       ^ "\n\n"));
 
   (* Make sure we have exactly one loop abstraction per function region (merge
@@ -639,10 +639,10 @@ let compute_loop_entry_fixed_point (config : config) (meta : Meta.meta)
         method! visit_abs _ abs =
           match abs.kind with
           | Loop (loop_id', _, kind) ->
-              sanity_check __FILE__ __LINE__ (loop_id' = loop_id) meta;
-              sanity_check __FILE__ __LINE__ (kind = LoopSynthInput) meta;
+              sanity_check __FILE__ __LINE__ (loop_id' = loop_id) span;
+              sanity_check __FILE__ __LINE__ (kind = LoopSynthInput) span;
               (* The abstractions introduced so far should be endable *)
-              sanity_check __FILE__ __LINE__ (abs.can_end = true) meta;
+              sanity_check __FILE__ __LINE__ (abs.can_end = true) span;
               add_aid abs.abs_id;
               abs
           | _ -> abs
@@ -672,12 +672,12 @@ let compute_loop_entry_fixed_point (config : config) (meta : Meta.meta)
       | Continue _ | Panic -> ()
       | Break _ ->
           (* We enforce that we can't get there: see {!PrePasses.remove_loop_breaks} *)
-          craise __FILE__ __LINE__ meta "Unreachable"
+          craise __FILE__ __LINE__ span "Unreachable"
       | Unit | LoopReturn _ | EndEnterLoop _ | EndContinue _ ->
           (* For why we can't get [Unit], see the comments inside {!eval_loop_concrete}.
              For [EndEnterLoop] and [EndContinue]: we don't support nested loops for now.
           *)
-          craise __FILE__ __LINE__ meta "Unreachable"
+          craise __FILE__ __LINE__ span "Unreachable"
       | Return ->
           log#ldebug (lazy "compute_loop_entry_fixed_point: cf_loop: Return");
           (* Should we consume the return value and pop the frame?
@@ -692,14 +692,14 @@ let compute_loop_entry_fixed_point (config : config) (meta : Meta.meta)
                  order (and we check that it is indeed the case) *)
               let abs_id = AbstractionId.of_int (RegionGroupId.to_int rg_id) in
               (* By default, the [SynthInput] abs can't end *)
-              let ctx = ctx_set_abs_can_end meta ctx abs_id true in
+              let ctx = ctx_set_abs_can_end span ctx abs_id true in
               sanity_check __FILE__ __LINE__
                 (let abs = ctx_lookup_abs ctx abs_id in
                  abs.kind = SynthInput rg_id)
-                meta;
+                span;
               (* End this abstraction *)
               let ctx =
-                InterpreterBorrows.end_abstraction_no_synth config meta abs_id
+                InterpreterBorrows.end_abstraction_no_synth config span abs_id
                   ctx
               in
               (* Explore the context, and check which abstractions are not there anymore *)
@@ -718,7 +718,7 @@ let compute_loop_entry_fixed_point (config : config) (meta : Meta.meta)
         (fun _ ids ->
           cassert __FILE__ __LINE__
             (AbstractionId.Set.disjoint !aids_union ids)
-            meta
+            span
             "The sets of abstractions we need to end per region group are not \
              pairwise disjoint";
           aids_union := AbstractionId.Set.union ids !aids_union)
@@ -729,7 +729,7 @@ let compute_loop_entry_fixed_point (config : config) (meta : Meta.meta)
        se, but if it doesn't happen it is bizarre and worth investigating... *)
     sanity_check __FILE__ __LINE__
       (AbstractionId.Set.equal !aids_union !fp_aids)
-      meta;
+      span;
 
     (* Merge the abstractions which need to be merged, and compute the map from
        region id to abstraction id *)
@@ -768,7 +768,7 @@ let compute_loop_entry_fixed_point (config : config) (meta : Meta.meta)
               in
               let abs = ctx_lookup_abs !fp !id0 in
               let abs = { abs with kind = abs_kind } in
-              let fp', _ = ctx_subst_abs meta !fp !id0 abs in
+              let fp', _ = ctx_subst_abs span !fp !id0 abs in
               fp := fp';
               (* Merge all the abstractions into this one *)
               List.iter
@@ -781,14 +781,14 @@ let compute_loop_entry_fixed_point (config : config) (meta : Meta.meta)
                         ^ AbstractionId.to_string !id0));
                     (* Note that we merge *into* [id0] *)
                     let fp', id0' =
-                      merge_into_abstraction meta loop_id abs_kind false !fp id
+                      merge_into_abstraction span loop_id abs_kind false !fp id
                         !id0
                     in
                     fp := fp';
                     id0 := id0';
                     ()
                   with ValueMatchFailure _ ->
-                    craise __FILE__ __LINE__ meta "Unexpected")
+                    craise __FILE__ __LINE__ span "Unexpected")
                 ids;
               (* Register the mapping *)
               let abs = ctx_lookup_abs !fp !id0 in
@@ -799,7 +799,7 @@ let compute_loop_entry_fixed_point (config : config) (meta : Meta.meta)
 
     (* Reorder the loans and borrows in the fresh abstractions in the fixed-point *)
     let fp =
-      reorder_loans_borrows_in_fresh_abs meta (Option.get !fixed_ids).aids !fp
+      reorder_loans_borrows_in_fresh_abs span (Option.get !fixed_ids).aids !fp
     in
 
     (* Update the abstraction's [can_end] field and their kinds.
@@ -821,8 +821,8 @@ let compute_loop_entry_fixed_point (config : config) (meta : Meta.meta)
         method! visit_abs _ abs =
           match abs.kind with
           | Loop (loop_id', _, kind) ->
-              sanity_check __FILE__ __LINE__ (loop_id' = loop_id) meta;
-              sanity_check __FILE__ __LINE__ (kind = LoopSynthInput) meta;
+              sanity_check __FILE__ __LINE__ (loop_id' = loop_id) span;
+              sanity_check __FILE__ __LINE__ (kind = LoopSynthInput) span;
               let kind : abs_kind =
                 if remove_rg_id then Loop (loop_id, None, LoopSynthInput)
                 else abs.kind
@@ -844,7 +844,7 @@ let compute_loop_entry_fixed_point (config : config) (meta : Meta.meta)
         (lazy
           ("compute_fixed_point: fixed point after matching with the function \
             region groups:\n"
-          ^ eval_ctx_to_string_no_filter ~meta:(Some meta) fp_test));
+          ^ eval_ctx_to_string_no_filter ~span:(Some span) fp_test));
       compute_fixed_point fp_test 1 1
     in
 
@@ -856,30 +856,30 @@ let compute_loop_entry_fixed_point (config : config) (meta : Meta.meta)
   (* Return *)
   (fp, fixed_ids, rg_to_abs)
 
-let compute_fixed_point_id_correspondance (meta : Meta.meta)
+let compute_fixed_point_id_correspondance (span : Meta.span)
     (fixed_ids : ids_sets) (src_ctx : eval_ctx) (tgt_ctx : eval_ctx) :
     borrow_loan_corresp =
   log#ldebug
     (lazy
       ("compute_fixed_point_id_correspondance:\n\n- fixed_ids:\n"
      ^ show_ids_sets fixed_ids ^ "\n\n- src_ctx:\n"
-      ^ eval_ctx_to_string ~meta:(Some meta) src_ctx
+      ^ eval_ctx_to_string ~span:(Some span) src_ctx
       ^ "\n\n- tgt_ctx:\n"
-      ^ eval_ctx_to_string ~meta:(Some meta) tgt_ctx
+      ^ eval_ctx_to_string ~span:(Some span) tgt_ctx
       ^ "\n\n"));
 
-  let filt_src_env, _, _ = ctx_split_fixed_new meta fixed_ids src_ctx in
+  let filt_src_env, _, _ = ctx_split_fixed_new span fixed_ids src_ctx in
   let filt_src_ctx = { src_ctx with env = filt_src_env } in
-  let filt_tgt_env, new_absl, _ = ctx_split_fixed_new meta fixed_ids tgt_ctx in
+  let filt_tgt_env, new_absl, _ = ctx_split_fixed_new span fixed_ids tgt_ctx in
   let filt_tgt_ctx = { tgt_ctx with env = filt_tgt_env } in
 
   log#ldebug
     (lazy
       ("compute_fixed_point_id_correspondance:\n\n- fixed_ids:\n"
      ^ show_ids_sets fixed_ids ^ "\n\n- filt_src_ctx:\n"
-      ^ eval_ctx_to_string ~meta:(Some meta) filt_src_ctx
+      ^ eval_ctx_to_string ~span:(Some span) filt_src_ctx
       ^ "\n\n- filt_tgt_ctx:\n"
-      ^ eval_ctx_to_string ~meta:(Some meta) filt_tgt_ctx
+      ^ eval_ctx_to_string ~span:(Some span) filt_tgt_ctx
       ^ "\n\n"));
 
   (* Match the source context and the filtered target context *)
@@ -888,15 +888,15 @@ let compute_fixed_point_id_correspondance (meta : Meta.meta)
     let fixed_ids = ids_sets_empty_borrows_loans fixed_ids in
     let open InterpreterBorrowsCore in
     let lookup_shared_loan lid ctx : typed_value =
-      match snd (lookup_loan meta ek_all lid ctx) with
+      match snd (lookup_loan span ek_all lid ctx) with
       | Concrete (VSharedLoan (_, v)) -> v
       | Abstract (ASharedLoan (_, v, _)) -> v
-      | _ -> craise __FILE__ __LINE__ meta "Unreachable"
+      | _ -> craise __FILE__ __LINE__ span "Unreachable"
     in
     let lookup_in_tgt id = lookup_shared_loan id tgt_ctx in
     let lookup_in_src id = lookup_shared_loan id src_ctx in
     Option.get
-      (match_ctxs meta check_equiv fixed_ids lookup_in_tgt lookup_in_src
+      (match_ctxs span check_equiv fixed_ids lookup_in_tgt lookup_in_src
          filt_tgt_ctx filt_src_ctx)
   in
 
@@ -953,7 +953,7 @@ let compute_fixed_point_id_correspondance (meta : Meta.meta)
       (* Check that the loan and borrows are related *)
       sanity_check __FILE__ __LINE__
         (BorrowId.Set.equal ids.borrow_ids loan_ids)
-        meta)
+        span)
     new_absl;
 
   (* For every target abstraction (going back to the [list_nth_mut] example,
@@ -996,7 +996,7 @@ let compute_fixed_point_id_correspondance (meta : Meta.meta)
     loan_to_borrow_id_map = tgt_loan_to_borrow;
   }
 
-let compute_fp_ctx_symbolic_values (meta : Meta.meta) (ctx : eval_ctx)
+let compute_fp_ctx_symbolic_values (span : Meta.span) (ctx : eval_ctx)
     (fp_ctx : eval_ctx) : SymbolicValueId.Set.t * symbolic_value list =
   let old_ids, _ = compute_ctx_ids ctx in
   let fp_ids, fp_ids_maps = compute_ctx_ids fp_ctx in
@@ -1077,10 +1077,10 @@ let compute_fp_ctx_symbolic_values (meta : Meta.meta) (ctx : eval_ctx)
         method! visit_VSharedBorrow env bid =
           let open InterpreterBorrowsCore in
           let v =
-            match snd (lookup_loan meta ek_all bid fp_ctx) with
+            match snd (lookup_loan span ek_all bid fp_ctx) with
             | Concrete (VSharedLoan (_, v)) -> v
             | Abstract (ASharedLoan (_, v, _)) -> v
-            | _ -> craise __FILE__ __LINE__ meta "Unreachable"
+            | _ -> craise __FILE__ __LINE__ span "Unreachable"
           in
           self#visit_typed_value env v
 
@@ -1101,9 +1101,9 @@ let compute_fp_ctx_symbolic_values (meta : Meta.meta) (ctx : eval_ctx)
   log#ldebug
     (lazy
       ("compute_fp_ctx_symbolic_values:" ^ "\n- src context:\n"
-      ^ eval_ctx_to_string_no_filter ~meta:(Some meta) ctx
+      ^ eval_ctx_to_string_no_filter ~span:(Some span) ctx
       ^ "\n- fixed point:\n"
-      ^ eval_ctx_to_string_no_filter ~meta:(Some meta) fp_ctx
+      ^ eval_ctx_to_string_no_filter ~span:(Some span) fp_ctx
       ^ "\n- fresh_sids: "
       ^ SymbolicValueId.Set.show fresh_sids
       ^ "\n- input_svalues: "
diff --git a/compiler/InterpreterLoopsFixedPoint.mli b/compiler/InterpreterLoopsFixedPoint.mli
index d367c94c..59d42812 100644
--- a/compiler/InterpreterLoopsFixedPoint.mli
+++ b/compiler/InterpreterLoopsFixedPoint.mli
@@ -13,7 +13,7 @@ open InterpreterLoopsCore
    - config
    - fixed ids (the fixeds ids are the ids we consider as non-fresh)
  *)
-val cleanup_fresh_values_and_abs : config -> Meta.meta -> ids_sets -> Cps.cm_fun
+val cleanup_fresh_values_and_abs : config -> Meta.span -> ids_sets -> Cps.cm_fun
 
 (** Prepare the shared loans in the abstractions by moving them to fresh
     abstractions.
@@ -60,7 +60,7 @@ val cleanup_fresh_values_and_abs : config -> Meta.meta -> ids_sets -> Cps.cm_fun
 
     we only introduce a fresh abstraction for [l1].
   *)
-val prepare_ashared_loans : Meta.meta -> loop_id option -> Cps.cm_fun
+val prepare_ashared_loans : Meta.span -> loop_id option -> Cps.cm_fun
 
 (** Compute a fixed-point for the context at the entry of the loop.
     We also return:
@@ -78,7 +78,7 @@ val prepare_ashared_loans : Meta.meta -> loop_id option -> Cps.cm_fun
  *)
 val compute_loop_entry_fixed_point :
   config ->
-  Meta.meta ->
+  Meta.span ->
   loop_id ->
   (* This function is the function to evaluate the loop body (eval_statement applied
      to the proper arguments) *)
@@ -163,7 +163,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 :
-  Meta.meta -> ids_sets -> eval_ctx -> eval_ctx -> borrow_loan_corresp
+  Meta.span -> ids_sets -> eval_ctx -> eval_ctx -> borrow_loan_corresp
 
 (** Compute the set of "quantified" symbolic value ids in a fixed-point context.
 
@@ -172,7 +172,7 @@ val compute_fixed_point_id_correspondance :
     - the list of input symbolic values
  *)
 val compute_fp_ctx_symbolic_values :
-  Meta.meta ->
+  Meta.span ->
   eval_ctx ->
   eval_ctx ->
   symbolic_value_id_set * symbolic_value list