2021-02-24 19:03 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0000230Frama-CKernelpublic2014-02-12 16:56
Assigned Topascal 
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

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

There are no notes attached to this issue.

-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