diff options
author | Son Ho | 2022-01-06 15:31:05 +0100 |
---|---|---|
committer | Son Ho | 2022-01-06 15:31:05 +0100 |
commit | 973e14973ca857ed0b3fd69fa45901c8ae08820e (patch) | |
tree | 5a8bda663f788ec7df203c6b42f539df1421c48d /src/Synthesis.ml | |
parent | a263101a71d5be9d3f2a738527c2eedc850eb9ad (diff) |
Fix some issues when evaluating assertions
Diffstat (limited to 'src/Synthesis.ml')
-rw-r--r-- | src/Synthesis.ml | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/src/Synthesis.ml b/src/Synthesis.ml index 85834e7a..79fa4065 100644 --- a/src/Synthesis.ml +++ b/src/Synthesis.ml @@ -23,6 +23,8 @@ open InterpreterProjectors * `s := op1 + op2` * *) +(* TODO: error Panic *) + (** Synthesize code for a symbolic expansion which doesn't lead to branching (i.e., applied on a value which is not an enumeration with several variants). *) @@ -66,3 +68,7 @@ let synthesize_function_call (_fid : A.fun_id) (_args : V.typed_value list) (_dest : E.place) (_res : V.symbolic_value) : unit = () + +let synthesize_panic () : unit = () + +let synthesize_assert (v : V.typed_value) : unit = () |