View Issue Details [ Jump to Notes ] | [ 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 | ||||||
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 |
|
![]() |
||||||
|
![]() |
|||
Date Modified | Username | Field | Change |
---|---|---|---|
2009-09-08 11:07 | pascal | New Issue | |
2009-09-08 11:08 | pascal | Relationship added | child of 0000068 |
2009-09-10 14:02 | svn | ||
2009-09-10 14:02 | svn | Status | new => resolved |
2009-09-10 14:02 | svn | Resolution | open => fixed |
2009-09-12 09:07 | signoles | Status | resolved => assigned |
2009-09-12 09:07 | signoles | Assigned To | => pascal |
2009-09-12 09:08 | signoles | Status | assigned => resolved |
2009-09-12 09:08 | signoles | Fixed in Version | => Frama-C Bore |
2009-09-23 15:26 | signoles | Fixed in Version | Frama-C Bore => Frama-C Beryllium 2 |
2009-09-23 20:22 | signoles | Status | resolved => closed |
2013-12-19 01:13 | pascal | Source_changeset_attached | => framac master 0986deca |
2014-02-12 16:56 | pascal | Source_changeset_attached | => framac stable/neon 0986deca |