Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision | Next revision Both sides next revision | ||
|
sav07_lecture_24 [2007/07/01 14:16] kremena.diatchka |
sav07_lecture_24 [2007/07/01 18:29] kremena.diatchka |
||
|---|---|---|---|
| Line 392: | Line 392: | ||
| - [[http://doi.acm.org/10.1145/989393.989429|Analysis of pointers and structures]] | - [[http://doi.acm.org/10.1145/989393.989429|Analysis of pointers and structures]] | ||
| - [[http://doi.acm.org/10.1145/53990.53993|Detecting conflicts between structure accesses]] | - [[http://doi.acm.org/10.1145/53990.53993|Detecting conflicts between structure accesses]] | ||
| + | |||
| Line 472: | Line 473: | ||
| * and pointer-valued fields of data structures are represented by binary predicates | * and pointer-valued fields of data structures are represented by binary predicates | ||
| - | (See table I in ref. 1) | + | {{predicates_small.png|}} |
| 3-valued logical structures are used to encode abstract stores (like the summary nodes of other algorithms). A 3-valued logical structure corresponds to a set of 2-valued logical structures. The way you abstract a 2-valued logical structure to a 3-valued one is the following: there is some predicates called abstraction predicates. Equivalence classes are formed by individuals in a 2-valued logical structure which have the same values for their abstraction predicates. All members of such equivalence classes are mapped to the same individual in the 3-valued structure. Then, for each nonabstraction predicate in the 2-valued structure, the following value is given to the corresponding predicate in the 3-valued strcture: | 3-valued logical structures are used to encode abstract stores (like the summary nodes of other algorithms). A 3-valued logical structure corresponds to a set of 2-valued logical structures. The way you abstract a 2-valued logical structure to a 3-valued one is the following: there is some predicates called abstraction predicates. Equivalence classes are formed by individuals in a 2-valued logical structure which have the same values for their abstraction predicates. All members of such equivalence classes are mapped to the same individual in the 3-valued structure. Then, for each nonabstraction predicate in the 2-valued structure, the following value is given to the corresponding predicate in the 3-valued strcture: | ||