diff options
Diffstat (limited to 'content/zettel/3c3m1.md')
| -rw-r--r-- | content/zettel/3c3m1.md | 24 |
1 files changed, 24 insertions, 0 deletions
diff --git a/content/zettel/3c3m1.md b/content/zettel/3c3m1.md new file mode 100644 index 0000000..7d47f76 --- /dev/null +++ b/content/zettel/3c3m1.md @@ -0,0 +1,24 @@ ++++ +title = "Needing flexible evaluation for symbolic execution" +date = "2023-05-01" +author = "Yann Herklotz" +tags = [] +categories = [] +backlinks = ["3c3m"] +forwardlinks = ["3c3m2"] +zettelid = "3c3m1" ++++ + +When performing symbolic execution, we want flexible predicate +semantics, because we will encounter various situations in which +predicates are actually not evaluable by design. For example, we will +conditionally assign a predicate based on the value of another +predicate. In that case, we can only deduce what the evaluation is if +the original predicate was true. Otherwise, we do not even know whether +the expression assigned to the predicate is even evaluable, and it is +likely that that is not the case. + +Therefore, when we generate a predicate, we can use the flexible +evaluation semantics for a predicate to encode this information, and +still end up with a predicate that is evaluable, even though there are +parts of it that are not evaluable. |