Add location to all assertion strings

src/lib/anf.ml

@@ -780,17 +780,14 @@ let rec anf (E_aux (e_aux, (l, tannot)) as exp) =
       let aexp = anf ret_exp in
       let aval, wrap = to_aval aexp in
       wrap (mk_aexp (AE_return (aval, typ_of exp)))
-  | E_assert (exp1, exp2) ->
+  | E_assert (exp1, exp2, exp3) ->
       let aexp1 = anf exp1 in
       let aexp2 = anf exp2 in
+      let aexp3 = anf exp3 in
       let aval1, wrap1 = to_aval aexp1 in
       let aval2, wrap2 = to_aval aexp2 in
-      (* Add the location of the assertion as a parameter. *)
-      let loc_string = Reporting.short_loc_to_string l in
-      let loc_aexp = mk_aexp (ae_lit (L_aux (L_string loc_string, l)) string_typ) in
-      let loc_aval, loc_wrap = to_aval loc_aexp in
-      (* TODO: What are these wrap functions? Do I need to use loc_wrap? *)
-      wrap1 (wrap2 (mk_aexp (AE_app (Extern (mk_id "sail_assert", None), [aval1; aval2; loc_aval], unit_typ))))
+      let aval3, wrap3 = to_aval aexp3 in
+      wrap1 (wrap2 ( wrap3(mk_aexp (AE_app (Extern (mk_id "sail_assert", None), [aval1; aval2; aval3], unit_typ)))))
   | E_cons (exp1, exp2) ->
       let aexp1 = anf exp1 in
       let aexp2 = anf exp2 in

src/lib/ast_util.ml

@@ -932,7 +932,7 @@ and map_exp_annot_aux f = function
   | E_exit exp -> E_exit (map_exp_annot f exp)
   | E_throw exp -> E_throw (map_exp_annot f exp)
   | E_return exp -> E_return (map_exp_annot f exp)
-  | E_assert (test, msg) -> E_assert (map_exp_annot f test, map_exp_annot f msg)
+  | E_assert (test, msg, loc) -> E_assert (map_exp_annot f test, map_exp_annot f msg, map_exp_annot f loc)
   | E_internal_value v -> E_internal_value v
   | E_var (lexp, exp1, exp2) -> E_var (map_lexp_annot f lexp, map_exp_annot f exp1, map_exp_annot f exp2)
   | E_internal_plet (pat, exp1, exp2) ->
@@ -1340,7 +1340,7 @@ let rec string_of_exp (E_aux (exp, _)) =
       "while " ^ string_of_measure measure ^ string_of_exp cond ^ " do " ^ string_of_exp body
   | E_loop (Until, measure, cond, body) ->
       "repeat " ^ string_of_measure measure ^ string_of_exp body ^ " until " ^ string_of_exp cond
-  | E_assert (test, msg) -> "assert(" ^ string_of_exp test ^ ", " ^ string_of_exp msg ^ ")"
+  | E_assert (test, msg, _loc) -> "assert(" ^ string_of_exp test ^ ", " ^ string_of_exp msg ^ ")"
   | E_exit exp -> "exit " ^ string_of_exp exp
   | E_throw exp -> "throw " ^ string_of_exp exp
   | E_cons (x, xs) -> string_of_exp x ^ " :: " ^ string_of_exp xs
@@ -1886,7 +1886,7 @@ let rec subst id value (E_aux (e_aux, annot) as exp) =
     | E_ref id' -> E_ref id'
     | E_throw exp -> E_throw (subst id value exp)
     | E_try (exp, pexps) -> E_try (subst id value exp, List.map (subst_pexp id value) pexps)
-    | E_assert (exp1, exp2) -> E_assert (subst id value exp1, subst id value exp2)
+    | E_assert (exp1, exp2, exp3) -> E_assert (subst id value exp1, subst id value exp2, subst id value exp3)
     | E_internal_value v -> E_internal_value v
     | E_var (lexp, exp1, exp2) -> E_var (subst_lexp id value lexp, subst id value exp1, subst id value exp2)
     | E_internal_assume (nc, exp) -> E_internal_assume (nc, subst id value exp)
@@ -2109,7 +2109,7 @@ let rec locate : 'a. (l -> l) -> 'a exp -> 'a exp =
     | E_ref id -> E_ref (locate_id f id)
     | E_throw exp -> E_throw (locate f exp)
     | E_try (exp, cases) -> E_try (locate f exp, List.map (locate_pexp f) cases)
-    | E_assert (exp, message) -> E_assert (locate f exp, locate f message)
+    | E_assert (exp, message, loc) -> E_assert (locate f exp, locate f message, locate f loc)
     | E_constraint constr -> E_constraint (locate_nc f constr)
     | E_var (lexp, exp1, exp2) -> E_var (locate_lexp f lexp, locate f exp1, locate f exp2)
     | E_internal_plet (pat, exp1, exp2) -> E_internal_plet (locate_pat f pat, locate f exp1, locate f exp2)

src/lib/constant_propagation.ml

@@ -568,9 +568,9 @@ let const_props target env ast =
       | E_return e ->
           let e', _ = const_prop_exp substs assigns e in
           re (E_return e') Bindings.empty
-      | E_assert (e1, e2) ->
-          let e1', e2', assigns = non_det_exp_2 e1 e2 in
-          re (E_assert (e1', e2')) assigns
+      | E_assert (e1, e2, e3) ->
+          let e1', e2', e3', assigns = non_det_exp_3 e1 e2 e3 in
+          re (E_assert (e1', e2', e3')) assigns
       | E_internal_assume (nc, e) ->
           let e', _ = const_prop_exp substs assigns e in
           re (E_internal_assume (nc, e')) assigns

src/lib/extraction/Ast.ml

@@ -20,7 +20,7 @@ module Coq_def_annot =
   type 'a record = { doc_comment : string option;
                      attrs : (Parse_ast.l * (string * attribute_data option))
                              list;
-                     visibility : visibility; loc : Parse_ast.l; env : 
+                     visibility : visibility; loc : Parse_ast.l; env :
                      'a }
  end
 
@@ -226,7 +226,7 @@ and 'a exp_aux =
 | E_ref of id
 | E_throw of 'a exp
 | E_try of 'a exp * 'a pexp list
-| E_assert of 'a exp * 'a exp
+| E_assert of 'a exp * 'a exp * 'a exp
 | E_var of 'a lexp * 'a exp * 'a exp
 | E_internal_plet of 'a pat * 'a exp * 'a exp
 | E_internal_return of 'a exp

src/lib/extraction/Ast.mli

@@ -20,7 +20,7 @@ module Coq_def_annot :
   type 'a record = { doc_comment : string option;
                      attrs : (Parse_ast.l * (string * attribute_data option))
                              list;
-                     visibility : visibility; loc : Parse_ast.l; env : 
+                     visibility : visibility; loc : Parse_ast.l; env :
                      'a }
  end
 
@@ -226,7 +226,7 @@ and 'a exp_aux =
 | E_ref of id
 | E_throw of 'a exp
 | E_try of 'a exp * 'a pexp list
-| E_assert of 'a exp * 'a exp
+| E_assert of 'a exp * 'a exp * 'a exp
 | E_var of 'a lexp * 'a exp * 'a exp
 | E_internal_plet of 'a pat * 'a exp * 'a exp
 | E_internal_return of 'a exp

src/lib/extraction/Semantics.ml

@@ -420,8 +420,8 @@ module Make =
      | E_try (head_exp, arms) ->
        E_aux ((E_try ((substitute n v head_exp),
          (map (substitute_arm n v) arms))), annot0)
-     | E_assert (x0, msg) ->
-       E_aux ((E_assert ((substitute n v x0), (substitute n v msg))), annot0)
+     | E_assert (x0, msg, loc) ->
+       E_aux ((E_assert ((substitute n v x0), (substitute n v msg), (substitute n v loc))), annot0)
      | E_var (l, x0, body) ->
        E_aux ((E_var ((substitute_lexp n v l), (substitute n v x0),
          (substitute n v body))), annot0)
@@ -1052,8 +1052,8 @@ module Make =
                then wrap (E_block xs0)
                else Monad.bind (step0 x0) (fun x' ->
                       wrap (E_block (x' :: xs0)))
-             | E_assert (e0, e1) ->
-               let x0 = E_aux ((E_assert (e0, e1)), annot1) in
+             | E_assert (e0, e1, e2) ->
+               let x0 = E_aux ((E_assert (e0, e1, e2)), annot1) in
                if is_value x0
                then wrap (E_block xs0)
                else Monad.bind (step0 x0) (fun x' ->
@@ -1441,7 +1441,7 @@ module Make =
               | Monad.Caught exn ->
                 wrap (E_match ((E_aux ((E_internal_value exn), annot0)),
                   (app arms (T.fallthrough :: []))))))
-       | E_assert (x, msg) ->
+       | E_assert (x, msg, loc) ->
          Monad.bind (get_bool x) (fun b ->
            match b with
            | Evaluated b0 ->
@@ -1453,9 +1453,9 @@ module Make =
                  else Monad.Assertion_failed s0
                | Unevaluated ->
                  Monad.bind (step0 msg) (fun msg' ->
-                   wrap (E_assert (x, msg'))))
+                   wrap (E_assert (x, msg', loc))))
            | Unevaluated ->
-             Monad.bind (step0 x) (fun x' -> wrap (E_assert (x', msg))))
+             Monad.bind (step0 x) (fun x' -> wrap (E_assert (x', msg, loc))))
        | E_var (l, x, body) ->
          wrap (E_block ((E_aux ((E_assign (l, x)), annot0)) :: (body :: [])))
        | E_internal_plet (_, _, _) -> Monad.Runtime_type_error (fst annot0)

src/lib/initial_check.ml

@@ -1365,7 +1365,9 @@ and to_ast_exp ctx exp =
         | P.E_throw exp -> E_throw (to_ast_exp ctx exp)
         | P.E_config key -> E_config [key]
         | P.E_return exp -> E_return (to_ast_exp ctx exp)
-        | P.E_assert (cond, msg) -> E_assert (to_ast_exp ctx cond, to_ast_exp ctx msg)
+        | P.E_assert (cond, msg) ->
+            let loc = E_lit (L_aux (L_string (Reporting.short_loc_to_string l), l)) in
+            E_assert (to_ast_exp ctx cond, to_ast_exp ctx msg, mk_exp loc)
         | P.E_internal_plet (pat, exp1, exp2) ->
             if !opt_magic_hash then E_internal_plet (to_ast_pat ctx pat, to_ast_exp ctx exp1, to_ast_exp ctx exp2)
             else raise (Reporting.err_general l "Internal plet construct found without -dmagic_hash")

src/lib/monomorphise.ml

@@ -595,7 +595,7 @@ let stop_at_false_assertions e =
               let e2, stop = exp e2 in
               (E_aux (E_let (LB_aux (LB_val (p, e1), lbann), e2), ann), stop)
         end
-    | E_assert (e1, _) when exp_false e1 -> (ea, Some (typ_of_annot ann))
+    | E_assert (e1, _, _) when exp_false e1 -> (ea, Some (typ_of_annot ann))
     | E_throw e -> (ea, Some (typ_of_annot ann))
     | _ -> (ea, None)
   in
@@ -631,7 +631,7 @@ let apply_pat_choices choices =
         | _ -> exp
       )
   in
-  let rewrite_assert (e1, e2) = E_assert (rewrite_assert_cond e1, e2) in
+  let rewrite_assert (e1, e2, e3) = E_assert (rewrite_assert_cond e1, e2, e3) in
   let rewrite_case (e, cases) =
     match List.assoc (exp_loc e) choices with
     | choice, max, subst -> (
@@ -1123,7 +1123,7 @@ let split_defs target all_errors (splits : split_req list) env ast =
         | E_throw e -> re (E_throw e)
         | E_try (e, cases) -> re (E_try (map_exp e, List.concat (List.map map_pexp cases)))
         | E_return e -> re (E_return (map_exp e))
-        | E_assert (e1, e2) -> re (E_assert (map_exp e1, map_exp e2))
+        | E_assert (e1, e2, e3) -> re (E_assert (map_exp e1, map_exp e2, map_exp e3))
         | E_var (le, e1, e2) -> re (E_var (map_lexp le, map_exp e1, map_exp e2))
         | E_internal_plet (p, e1, e2) -> re (E_internal_plet (check_single_pat p, map_exp e1, map_exp e2))
         | E_internal_return e -> re (E_internal_return (map_exp e))
@@ -2458,7 +2458,7 @@ module Analysis = struct
           in
           let ds, assigns, rs = split3 (List.map analyse_handler cases) in
           (merge_deps (deps :: ds), List.fold_left dep_bindings_merge Bindings.empty assigns, List.fold_left merge r rs)
-      | E_assert (e1, _) -> analyse_sub env assigns e1
+      | E_assert (e1, _, _) -> analyse_sub env assigns e1
       | E_internal_assume (nc, e1) -> analyse_sub env assigns e1
       | E_internal_plet _ | E_internal_return _ | E_internal_value _ ->
           raise
@@ -2788,7 +2788,7 @@ module Analysis = struct
         let kbound = kids_bound_by_pat p in
         let sets2 = KBindings.filter (fun kid _ -> not (KidSet.mem kid kbound)) sets2 in
         merge_set_asserts_by_kid sets1 sets2
-    | E_assert (exp1, _) -> sets_from_assert exp1
+    | E_assert (exp1, _, _) -> sets_from_assert exp1
     | _ -> KBindings.empty
 
   let print_set_assertions set_assertions =
@@ -4218,7 +4218,7 @@ module BitvectorSizeCasts = struct
             let result_typ = Env.base_typ_of env (typ_of_annot ann) in
             let rec aux = function
               | [] -> []
-              | (E_aux (E_assert (assert_exp, msg), _) as h) :: t ->
+              | (E_aux (E_assert (assert_exp, _msg, _loc), _) as h) :: t ->
                   (* Check the assertion for constraints that instantiate kids *)
                   let is_known_kid kid = KBindings.mem kid (Env.get_typ_vars env) in
                   begin

src/lib/nl_flow.ml

@@ -70,7 +70,8 @@ let rec pat_id (P_aux (aux, _)) =
 
 let add_assert cond (E_aux (aux, (l, uannot)) as exp) =
   let msg = mk_lit_exp (L_string "") in
-  let assertion = locate (fun _ -> gen_loc l) (mk_exp (E_assert (cond, msg))) in
+  let loc = E_lit (L_aux (L_string (Reporting.short_loc_to_string l), l)) in
+  let assertion = locate (fun _ -> gen_loc l) (mk_exp (E_assert (cond, msg, mk_exp loc))) in
   match aux with
   | E_block exps -> E_aux (E_block (assertion :: exps), (l, empty_uannot))
   | _ -> E_aux (E_block (assertion :: [exp]), (l, uannot))

src/lib/pretty_print_sail.ml

@@ -592,8 +592,8 @@ module Printer (Config : PRINT_CONFIG) = struct
     | E_app (id, exps) when not Config.resugar -> doc_id id ^^ parens (separate_map (comma ^^ space) doc_exp exps)
     | E_app (id, exps) when List.length exps != 2 -> doc_id id ^^ parens (separate_map (comma ^^ space) doc_exp exps)
     | E_constraint nc -> string "constraint" ^^ parens (doc_nc nc)
-    | E_assert (exp1, E_aux (E_lit (L_aux (L_string "", _)), _)) -> string "assert" ^^ parens (doc_exp exp1)
-    | E_assert (exp1, exp2) -> string "assert" ^^ parens (doc_exp exp1 ^^ comma ^^ space ^^ doc_exp exp2)
+    | E_assert (exp1, E_aux (E_lit (L_aux (L_string "", _)), _), _) -> string "assert" ^^ parens (doc_exp exp1)
+    | E_assert (exp1, exp2, _) -> string "assert" ^^ parens (doc_exp exp1 ^^ comma ^^ space ^^ doc_exp exp2)
     | E_exit exp -> string "exit" ^^ parens (doc_exp exp)
     | E_vector exps -> brackets (separate_map (comma ^^ space) doc_exp exps)
     | E_internal_value v ->

src/lib/rewriter.ml

@@ -236,7 +236,7 @@ let rewrite_exp rewriters (E_aux (exp, (l, annot))) =
   | E_exit e -> rewrap (E_exit (rewrite e))
   | E_throw e -> rewrap (E_throw (rewrite e))
   | E_return e -> rewrap (E_return (rewrite e))
-  | E_assert (e1, e2) -> rewrap (E_assert (rewrite e1, rewrite e2))
+  | E_assert (e1, e2, e3) -> rewrap (E_assert (rewrite e1, rewrite e2, rewrite e3))
   | E_var (lexp, e1, e2) ->
       rewrap
         (E_var
@@ -535,7 +535,7 @@ type ( 'a,
   e_throw : 'exp -> 'exp_aux;
   e_config : string list -> 'exp_aux;
   e_return : 'exp -> 'exp_aux;
-  e_assert : 'exp * 'exp -> 'exp_aux;
+  e_assert : 'exp * 'exp * 'exp -> 'exp_aux;
   e_var : 'lexp * 'exp * 'exp -> 'exp_aux;
   e_internal_plet : 'pat * 'exp * 'exp -> 'exp_aux;
   e_internal_return : 'exp -> 'exp_aux;
@@ -600,7 +600,7 @@ let rec fold_exp_aux alg = function
   | E_throw e -> alg.e_throw (fold_exp alg e)
   | E_config key -> alg.e_config key
   | E_return e -> alg.e_return (fold_exp alg e)
-  | E_assert (e1, e2) -> alg.e_assert (fold_exp alg e1, fold_exp alg e2)
+  | E_assert (e1, e2, e3) -> alg.e_assert (fold_exp alg e1, fold_exp alg e2, fold_exp alg e3)
   | E_var (lexp, e1, e2) -> alg.e_var (fold_lexp alg lexp, fold_exp alg e1, fold_exp alg e2)
   | E_internal_plet (pat, e1, e2) -> alg.e_internal_plet (fold_pat alg.pat_alg pat, fold_exp alg e1, fold_exp alg e2)
   | E_internal_return e -> alg.e_internal_return (fold_exp alg e)
@@ -674,7 +674,7 @@ let id_exp_alg =
     e_throw = (fun e1 -> E_throw e1);
     e_config = (fun key -> E_config key);
     e_return = (fun e1 -> E_return e1);
-    e_assert = (fun (e1, e2) -> E_assert (e1, e2));
+    e_assert = (fun (e1, e2, e3) -> E_assert (e1, e2, e3));
     e_var = (fun (lexp, e2, e3) -> E_var (lexp, e2, e3));
     e_internal_plet = (fun (pat, e1, e2) -> E_internal_plet (pat, e1, e2));
     e_internal_return = (fun e -> E_internal_return e);
@@ -798,7 +798,7 @@ let compute_exp_alg bot join =
     e_throw = (fun (v1, e1) -> (v1, E_throw e1));
     e_config = (fun key -> (bot, E_config key));
     e_return = (fun (v1, e1) -> (v1, E_return e1));
-    e_assert = (fun ((v1, e1), (v2, e2)) -> (join v1 v2, E_assert (e1, e2)));
+    e_assert = (fun ((v1, e1), (v2, e2), (v3, e3)) -> (join_list [v1; v2; v3], E_assert (e1, e2, e3)));
     e_var = (fun ((vl, lexp), (v2, e2), (v3, e3)) -> (join_list [vl; v2; v3], E_var (lexp, e2, e3)));
     e_internal_plet = (fun ((vp, pat), (v1, e1), (v2, e2)) -> (join_list [vp; v1; v2], E_internal_plet (pat, e1, e2)));
     e_internal_return = (fun (v, e) -> (v, E_internal_return e));
@@ -893,7 +893,7 @@ let pure_exp_alg bot join =
     e_throw = (fun v1 -> v1);
     e_config = (fun _ -> bot);
     e_return = (fun v1 -> v1);
-    e_assert = (fun (v1, v2) -> join v1 v2);
+    e_assert = (fun (v1, v2, v3) -> join_list [v1; v2; v3]);
     e_var = (fun (vl, v2, v3) -> join_list [vl; v2; v3]);
     e_internal_plet = (fun (vp, v1, v2) -> join_list [vp; v1; v2]);
     e_internal_return = (fun v -> v);
@@ -1145,10 +1145,11 @@ let default_fold_exp f x (E_aux (e, ann) as exp) =
   | E_return e ->
       let x, e = f x e in
       (x, re (E_return e))
-  | E_assert (e1, e2) ->
+  | E_assert (e1, e2, e3) ->
       let x, e1 = f x e1 in
       let x, e2 = f x e2 in
-      (x, re (E_assert (e1, e2)))
+      let x, e3 = f x e3 in
+      (x, re (E_assert (e1, e2, e3)))
   | E_var (lexp, e1, e2) ->
       let x, lexp = default_fold_lexp f x lexp in
       let x, e1 = f x e1 in

src/lib/rewriter.mli

@@ -159,7 +159,7 @@ type ( 'a,
   e_throw : 'exp -> 'exp_aux;
   e_config : string list -> 'exp_aux;
   e_return : 'exp -> 'exp_aux;
-  e_assert : 'exp * 'exp -> 'exp_aux;
+  e_assert : 'exp * 'exp * 'exp -> 'exp_aux;
   e_var : 'lexp * 'exp * 'exp -> 'exp_aux;
   e_internal_plet : 'pat * 'exp * 'exp -> 'exp_aux;
   e_internal_return : 'exp -> 'exp_aux;

src/lib/rewrites.ml

@@ -1030,8 +1030,9 @@ let rewrite_guarded_clauses fun_only mk_fallthrough l env pat_typ typ
 
 let mk_pattern_match_failure_pexp l env pat_typ typ =
   let p = P_aux (P_wild, (gen_loc l, mk_tannot env pat_typ)) in
-  let msg = "Pattern match failure at " ^ Reporting.short_loc_to_string l in
-  let a = mk_exp ~loc:(gen_loc l) (E_assert (mk_lit_exp L_false, mk_lit_exp (L_string msg))) in
+  let msg = "Pattern match failure"  in
+  let loc = Reporting.short_loc_to_string l in
+  let a = mk_exp ~loc:(gen_loc l) (E_assert (mk_lit_exp L_false, mk_lit_exp (L_string msg), mk_lit_exp (L_string loc))) in
   let b = mk_exp ~loc:(gen_loc l) (E_exit (mk_lit_exp L_unit)) in
   let (E_aux (_, (_, ann)) as e) = check_exp env (mk_exp ~loc:(gen_loc l) (E_block [a; b])) typ in
   construct_pexp (p, None, e, (gen_loc l, ann))
@@ -2421,8 +2422,8 @@ let rewrite_ast_letbind_effects effect_info env =
     | E_constraint nc -> k (rewrap (E_constraint nc))
     | E_assign (lexp, exp1) -> n_lexp lexp (fun lexp -> n_exp_name exp1 (fun exp1 -> k (rewrap (E_assign (lexp, exp1)))))
     | E_exit exp' -> k (E_aux (E_exit (n_exp_term (needs_monad exp') exp'), annot))
-    | E_assert (exp1, exp2) ->
-        n_exp_name exp1 (fun exp1 -> n_exp_name exp2 (fun exp2 -> k (rewrap (E_assert (exp1, exp2)))))
+    | E_assert (exp1, exp2, exp3) ->
+        n_exp_name exp1 (fun exp1 -> n_exp_name exp2 (fun exp2 -> n_exp_name exp3 (fun exp3 -> k (rewrap (E_assert (exp1, exp2, exp3))))))
     | E_var (lexp, exp1, exp2) ->
         n_lexp lexp (fun lexp -> n_exp exp1 (fun exp1 -> rewrap (E_var (lexp, exp1, n_exp exp2 k))))
     | E_internal_return exp1 ->
@@ -3088,7 +3089,7 @@ let rewrite_ast_remove_superfluous_letbinds env =
             let (E_aux (_, e1annot)) = exp1 in
             E_aux (E_internal_return exp1, e1annot)
         | _, (E_aux (E_throw e, a), _), _ -> E_aux (E_throw e, a)
-        | (pat, _), ((E_aux (E_assert (c, msg), a) as assert_exp), _), _ -> begin
+        | (pat, _), ((E_aux (E_assert (c, _msg, _loc), a) as assert_exp), _), _ -> begin
             match typ_of c with
             | Typ_aux (Typ_app (Id_aux (Id "atom_bool", _), [A_aux (A_bool nc, _)]), _)
               when prove __POS__ (env_of c) (nc_not nc) ->
@@ -4167,7 +4168,9 @@ let rewrite_explicit_measure effect_info env ast =
                     ),
                   (loc, empty_tannot)
                 ),
-              E_aux (E_lit (L_aux (L_string "recursion limit reached", loc)), (loc, empty_tannot))
+              E_aux (E_lit (L_aux (L_string "recursion limit reached", loc)), (loc, empty_tannot)),
+              (* TODO: Where is this? *)
+              E_aux (E_lit (L_aux (L_string "generated code", loc)), (loc, empty_tannot))
             ),
           (loc, empty_tannot)
         )
@@ -4283,7 +4286,8 @@ let rewrite_loops_with_escape_effect env defs =
     E_aux
       ( E_assert
           ( E_aux (E_lit (L_aux (L_true, Unknown)), dummy_ann),
-            E_aux (E_lit (L_aux (L_string "loop dummy assert", Unknown)), dummy_ann)
+            E_aux (E_lit (L_aux (L_string "loop dummy assert", Unknown)), dummy_ann),
+            E_aux (E_lit (L_aux (L_string "loop dummy location", Unknown)), dummy_ann)
           ),
         dummy_ann
       )