Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision Next revision | Previous revision Last revision Both sides next revision | ||
|
sav07_lecture_9_skeleton [2007/04/17 15:14] vkuncak |
sav07_lecture_9_skeleton [2007/04/17 19:58] vkuncak |
||
|---|---|---|---|
| Line 32: | Line 32: | ||
| \end{equation*} | \end{equation*} | ||
| where $a^1,\ldots,a^n$ are variables ranging over a lattice $A$ (one for each control-flow graph node), and $f_k$ are monotonic functions on $A$ (one for each edge in the control-flow graph). | where $a^1,\ldots,a^n$ are variables ranging over a lattice $A$ (one for each control-flow graph node), and $f_k$ are monotonic functions on $A$ (one for each edge in the control-flow graph). | ||
| + | |||
| + | |||
| ==== From a system of equations to one equation ==== | ==== From a system of equations to one equation ==== | ||
| Line 79: | Line 81: | ||
| * [[http://www.di.ens.fr/~cousot/COUSOTpapers/POPL79.shtml|Systematic Design of Program Analysis Frameworks]] | * [[http://www.di.ens.fr/~cousot/COUSOTpapers/POPL79.shtml|Systematic Design of Program Analysis Frameworks]] | ||
| + | === Widening === | ||
| + | |||
| + | === Narrowing === | ||
| + | === Reduced product === | ||
| ===== ASTREE Static Analyzer ===== | ===== ASTREE Static Analyzer ===== | ||
| Line 89: | Line 95: | ||
| Section 5.4: A remark on notation: | Section 5.4: A remark on notation: | ||
| * if $\rho$ denotes the state and $S$ is a deterministic statement, then $[\![S]\!]^s(\rho)$ represents the new state after executing the statement; the relation corresponding to statement semantics would be $\{(S,[\![S]\!]^s(\rho)) \mid \rho \mbox{ is a state, mapping variables to their values \}$. | * if $\rho$ denotes the state and $S$ is a deterministic statement, then $[\![S]\!]^s(\rho)$ represents the new state after executing the statement; the relation corresponding to statement semantics would be $\{(S,[\![S]\!]^s(\rho)) \mid \rho \mbox{ is a state, mapping variables to their values \}$. | ||
| - | * this function is extended to map sets of states to sets of states, which gives function ampping $E$ to $[\![S]\!]^c(E)$ and is what we called strongest postcondition $sp(S,E)$. | + | * this function is extended to map sets of states to sets of states, which gives function mapping $E$ to $[\![S]\!]^c(E)$ and is what we called strongest postcondition $sp(S,E)$. |
| + | * this is abstracted to abstract domain | ||
| === The Octagon Abstract Domain === | === The Octagon Abstract Domain === | ||