Changes between Version 14 and Version 15 of Language

Timestamp:

05/18/23 20:24:14 (3 years ago)

Author:

siegel

Comment:

--

Language

@@ -429 +429 @@
 The system function `$assert` has the signature
 {{{
-void $assert(_Bool expr, ...);
+$system void $assert(_Bool expr, ...);
 }}}
 It consumes a boolean expression and any number of optional expressions which are used to construct an error message.
@@ -447 +447 @@
 The system function `$assume` has signature
 {{{
-void $assume(_Bool expr);
+$system void $assume(_Bool expr);
 }}}
 During verification, the given expression is assumed to hold. If this leads to a contradiction on some execution, that execution is simply ignored. It never reports a violation, it only restricts the set of possible executions that will be explored by the verification algorithm.
@@ -457 +457 @@
 declares `N` and `B` to be integer inputs and restricts consideration to inputs satisfying 1 ≤ `N` ≤ `B`.
 
-=== `$assume_push`
-
-=== `$assume_pop`
+=== Temporary assumptions: `$assume_push` and `$assume_pop`
+
+These functions have signatures:
+{{{
+$system void $assume_push(_Bool pred);
+$system void $assume_pop();
+}}}
+In the concrete semantics, `$assume_push` has the same semantics as `$assume`, and `$assume_pop` is a no-op.
+
+In the symbolic semantics, they behave as follows: each process maintains a stack of boolean symbolic expressions known as the temporary assumption stack.
+At any state, the ''effective path condition'' is the conjunction of the permanent path condition , and the conjunction,
+over all processes ''p'',  of all entries in the temporary assumption stack of ''p''.
+A call to `$assume_push` pushes a new assumption onto the temporary assumption stack of the process making the call.
+A call to `$assume_pop` pops the stack of that process.
+This allows prior assumptions to be removed.
+This mechanism is consistent with the concrete semantics in that it yields an over-approximation of the set of reachable concrete states.
+Specifically, removing a clause from the effective path condition can only increase the set of concrete states represented by a symbolic state.
+This mechanism serves as a "widening operator" (in the sense of abstract interpretation), which enables symbolic execution to converge.
+
 
 === `$choose_int`