diff options
Diffstat (limited to 'src/InterpreterPaths.ml')
| -rw-r--r-- | src/InterpreterPaths.ml | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/src/InterpreterPaths.ml b/src/InterpreterPaths.ml index 300e50c5..8b103eb8 100644 --- a/src/InterpreterPaths.ml +++ b/src/InterpreterPaths.ml @@ -11,6 +11,7 @@ open InterpreterUtils open InterpreterBorrowsCore open InterpreterBorrows open InterpreterExpansion +module Synth = SynthesizeSymbolic (** The local logger *) let log = L.paths_log @@ -473,6 +474,7 @@ let rec update_ctx_along_read_place (config : C.config) (access : access_kind) | FailSymbolic (_pe, sp) -> (* Expand the symbolic value *) expand_symbolic_value_no_branching config sp + (Some (Synth.mk_place p ctx)) | FailBottom (_, _, _) -> (* We can't expand [Bottom] values while reading them *) failwith "Found [Bottom] while reading a place" @@ -502,6 +504,7 @@ let rec update_ctx_along_write_place (config : C.config) (access : access_kind) | FailSymbolic (_pe, sp) -> (* Expand the symbolic value *) expand_symbolic_value_no_branching config sp + (Some (Synth.mk_place p ctx)) | FailBottom (remaining_pes, pe, ty) -> (* Expand the [Bottom] value *) fun cf ctx -> |