Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision Next revision | Previous revision Next revision Both sides next revision | ||
sav08:forward_symbolic_execution [2009/03/11 10:47] vkuncak |
sav08:forward_symbolic_execution [2009/03/11 12:44] philippe.suter |
||
---|---|---|---|
Line 17: | Line 17: | ||
=== Exploiting Analogy with Execution === | === Exploiting Analogy with Execution === | ||
- | Maintain symbolic state formula $R(x_0,x)$ in the following normal form: | + | Maintain symbolic state formula $R(x_0,y_0,x,y)$ in the following normal form: |
\[ | \[ | ||
x = e_x \land y = e_y \land P | x = e_x \land y = e_y \land P | ||
Line 42: | Line 42: | ||
Special case: if initial condition specifies values of variables, then we know which branch to enter. | Special case: if initial condition specifies values of variables, then we know which branch to enter. | ||
+ | |||
===== Symbolic Execution Rules ===== | ===== Symbolic Execution Rules ===== | ||
Line 74: | Line 75: | ||
assume(F) | assume(F) | ||
change state: | change state: | ||
- | P := P & F | + | P := P & F[x<-e_x, y<-e_y] |
=== Havoc === | === Havoc === |