added assign_desc ghost block check

nyu-acsys · May 7, 2024 · ba8fe2a · ba8fe2a
1 parent c09ed90
commit ba8fe2a
Show file tree

Hide file tree

Showing 2 changed files with 3 additions and 3 deletions.
diff --git a/lib/backend/checker.ml b/lib/backend/checker.ml
@@ -1,7 +1,7 @@
 open Smt_solver
 open Ast
 open Base
-open Ast
+(* open Ast *)
 (* open Frontend *)
 open SmtLibAST
 open Util

diff --git a/lib/frontend/rewrites/rewrites.ml b/lib/frontend/rewrites/rewrites.ml
@@ -1472,8 +1472,8 @@ module AtomicityAnalysis = struct
 
         if is_assign_desc_lhs_ghost then
           Rewriter.return stmt
-        (* else if ghost_block then
-          Error.error stmt.stmt_loc "Cannot assign to non-ghost variables in a ghost block" *)
+        else if ghost_block then
+          Error.error stmt.stmt_loc "Cannot assign to non-ghost variables in a ghost block"
         else if List.length assign_desc.assign_lhs > 1 then
           let atomicity_state = take_non_atomic_step ~loc atomicity_state in
           let* _ = Rewriter.set_user_state atomicity_state in