Missing functions to convert logic terms directly to abstract values
ID0000230: This issue was created automatically from Mantis Issue 230. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0000230 | Frama-C | Kernel | public | 2009-09-08 | 2014-02-12 |
| Reporter | pascal | Assigned To | pascal | Resolution | fixed |
| Priority | normal | Severity | minor | Reproducibility | always |
| Platform | - | OS | - | OS Version | - |
| Product Version | Frama-C Beryllium-20090901 | Target Version | - | Fixed in Version | Frama-C Beryllium-20090902 |
Description :
The logic allows to express imprecise memory locations (see bug #68 (closed)).
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.