summaryrefslogtreecommitdiff
path: root/src/Interpreter.ml
diff options
context:
space:
mode:
authorSon Ho2022-01-26 10:23:14 +0100
committerSon Ho2022-01-26 10:23:14 +0100
commitf10dff1e13c00eaa49d78f5d7ba79366fa028a73 (patch)
tree397462556137a4b7bae475d2b6a54a54582a0f19 /src/Interpreter.ml
parenta49f413c0e0de494c003c622f8483e8c37d2618a (diff)
Add some sanity checks and comments
Diffstat (limited to 'src/Interpreter.ml')
-rw-r--r--src/Interpreter.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/src/Interpreter.ml b/src/Interpreter.ml
index fbb7ef9b..d3e30519 100644
--- a/src/Interpreter.ml
+++ b/src/Interpreter.ml
@@ -47,8 +47,8 @@ module Test = struct
Introduces local variables initialized in the following manner:
- input arguments are initialized as symbolic values
- the remaining locals are initialized as ⊥
- "Dummy" abstractions are introduced for the regions present in the
- function signature.
+ Abstractions are introduced for the regions present in the function
+ signature.
*)
let initialize_symbolic_context_for_fun (m : M.cfim_module) (fdef : A.fun_def)
: C.eval_ctx =