diff options
Diffstat (limited to 'src/InterpreterStatements.ml')
-rw-r--r-- | src/InterpreterStatements.ml | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/src/InterpreterStatements.ml b/src/InterpreterStatements.ml index 8768461c..885d1bdc 100644 --- a/src/InterpreterStatements.ml +++ b/src/InterpreterStatements.ml @@ -602,7 +602,7 @@ let rec eval_statement (config : C.config) (ctx : C.eval_ctx) (st : A.statement) * checking the invariants *) let ctx = greedy_expand_symbolic_values config ctx in (* Sanity check *) - if config.C.check_invariants then Inv.check_invariants ctx; + if config.C.check_invariants then Inv.check_invariants config ctx; (* Evaluate *) match st with | A.Assign (p, rvalue) -> ( @@ -617,7 +617,8 @@ let rec eval_statement (config : C.config) (ctx : C.eval_ctx) (st : A.statement) in List.map assign res) | A.FakeRead p -> - let ctx, _ = prepare_rplace config Read p ctx in + let expand_prim_copy = false in + let ctx, _ = prepare_rplace config expand_prim_copy Read p ctx in [ Ok (ctx, Unit) ] | A.SetDiscriminant (p, variant_id) -> [ Ok (set_discriminant config ctx p variant_id) ] @@ -1028,7 +1029,7 @@ and eval_function_body (config : C.config) (ctx : C.eval_ctx) * checking the invariants *) let ctx = greedy_expand_symbolic_values config ctx in (* Sanity check *) - if config.C.check_invariants then Inv.check_invariants ctx; + if config.C.check_invariants then Inv.check_invariants config ctx; match res with | Unit | Break _ | Continue _ -> failwith "Inconsistent state" | Return -> Ok ctx) |