| View Issue Details [ Jump to Notes ] [ Related Changesets ] | [ Issue History ] [ Print ] |
| ID | Project | Category | View Status | Date Submitted | Last Update |
| 0000230 | Frama-C | Kernel | public | 2009-09-08 11:07 | 2014-02-12 16:56 |
|
| Reporter | pascal | |
| Assigned To | pascal | |
| Priority | normal | Severity | minor | Reproducibility | always |
| Status | closed | Resolution | fixed | |
| Platform | | OS | | OS Version | |
| Product Version | Frama-C Beryllium-20090901 | |
| Target Version | | Fixed in Version | Frama-C Beryllium-20090902 | |
|
| Summary | 0000230: Missing functions to convert logic terms directly to abstract values |
| Description | The logic allows to express imprecise memory locations (see bug 0000068).
The abstract domains allow to express imprecise memory locations.
Currently the conversion between the former and the latter goes through
C expressions, which do not allow to express the zones that can be
written in ACSL and could be represented meaningfully as abstract values.
Probably the missing function would take in argument an abstract state
and use it to resolve the value of C variables. Logic variables would not have
to be supported. |
| Tags | No tags attached. |
|
| Attached Files | |
|
Relationships 
Relationships