2021-02-24 19:03 CET
  

View Issue Details [ Jump to Notes ] [ Issue History ] [ Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000230Frama-CKernelpublic2009-09-08 11:072014-02-12 16:56
Reporterpascal 
Assigned Topascal 
PrioritynormalSeverityminorReproducibilityalways
StatusclosedResolutionfixed 
Product VersionFrama-C Beryllium-20090901 
Target VersionFixed in VersionFrama-C Beryllium-20090902 
Summary0000230: Missing functions to convert logic terms directly to abstract values
DescriptionThe 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.
TagsNo tags attached.
Attached Files

-Relationships
child of 0000068closedpascal Plug-in inout fails to parse clause /*@ assigns s[..]; */ 
+Relationships

-Notes
There are no notes attached to this issue.
+Notes

-Issue History
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
+Issue History