Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision | Next revision Both sides next revision | ||
|
sav08:forward_symbolic_execution [2009/03/11 10:48] vkuncak |
sav08:forward_symbolic_execution [2009/03/11 12:44] philippe.suter |
||
|---|---|---|---|
| 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 === | ||