minor

nyu-acsys · Feb 25, 2025 · 461b5f1 · 461b5f1
1 parent 8cce7d6
commit 461b5f1
Show file tree

Hide file tree

Showing 2 changed files with 17 additions and 22 deletions.
diff --git a/lib/frontend/rewrites/heapsExplicitTrnsl.ml b/lib/frontend/rewrites/heapsExplicitTrnsl.ml
@@ -2224,18 +2224,8 @@ module TrnslInhale = struct
                [ field_heap_expr ])
         in
 
-        (* let* injectivity_assertion =
-          generate_injectivity_assertions ~loc universal_quants conds e1
-        in *)
-
-        let stmts_list =
-          match univ_quants_list with
-          | [] -> []
-          | _ -> [ (* injectivity_assertion *) ]
-        in
-
         let stmts_list =
-          stmts_list @ [ havoc_stmt; assume_stmt ] @ forward_trigger_assertions @ [ eq_stmt; assume_heap_valid ]
+          [ havoc_stmt; assume_stmt ] @ forward_trigger_assertions @ [ eq_stmt; assume_heap_valid ]
         in
 
         let stmt = Stmt.mk_block_stmt ~loc stmts_list in
@@ -4369,18 +4359,8 @@ module TrnslExhale = struct
                [ field_heap_expr ])
         in
 
-        (* let* injectivity_assertion =
-          generate_injectivity_assertions ~loc universal_quants conds e1
-        in *)
-
-        let stmts_list =
-          match univ_quants_list with
-          | [] -> []
-          | _ -> [ (* injectivity_assertion *) ]
-        in
-
         let stmts_list =
-          stmts_list @ [ havoc_stmt; assume_stmt ] @ forward_trigger_assertions @ [ eq_stmt; assert_heap_valid ]
+          [ havoc_stmt; assume_stmt ] @ forward_trigger_assertions @ [ eq_stmt; assert_heap_valid ]
         in
 
         let stmt = Stmt.mk_block_stmt ~loc stmts_list in

diff --git a/lib/frontend/rewrites/rewrites.ml b/lib/frontend/rewrites/rewrites.ml
@@ -2630,8 +2630,18 @@ let rec rewrites_phase_2 (m : Module.t) : Module.t Rewriter.t =
          ~f:HeapsExplicitTrnsl.TrnslInhale.rewriter_eliminate_binds_for_inhale m)
   in
 
+  Logs.debug (fun m1 ->
+    m1
+      "Rewrites.all_rewrites: Starting rewrite_fpu \
+       on module %a"
+      Ident.pr m.mod_decl.mod_decl_name);
   let* m = Rewriter.Module.rewrite_stmts ~f:HeapsExplicitTrnsl.rewrite_fpu m in
 
+  Logs.debug (fun m1 ->
+    m1
+      "Rewrites.all_rewrites: Starting rewrite_binds \
+       on module %a"
+      Ident.pr m.mod_decl.mod_decl_name);
   let* m =
     Rewriter.Module.rewrite_stmts ~f:HeapsExplicitTrnsl.rewrite_binds m
   in
@@ -2668,6 +2678,11 @@ let rec rewrites_phase_2 (m : Module.t) : Module.t Rewriter.t =
       ~f:HeapsExplicitTrnsl.rewrite_make_heaps_explicit m
   in
 
+  Logs.debug (fun m1 ->
+    m1
+      "Rewrites.all_rewrites: Starting rewrite_expand_types \
+       on module %a"
+      Ident.pr m.mod_decl.mod_decl_name);
   let* m = Rewriter.Module.rewrite_types ~f:rewrite_expand_types m in
 
   Logs.debug (fun m1 ->