2021-02-24 18:12 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0000835Frama-CKernel > ACSL implementationpublic2014-02-12 16:59
Assigned Tovirgile 
Product VersionFrama-C Carbon-20110201 
Target VersionFixed in VersionFrama-C Nitrogen-20111001 
Summary0000835: Aggregate logic types containing only C types
DescriptionAccording to section 2.2.7 of current ACSL implementation
it would be possible to use for example arrays of integers:
"Aggregate types can be declared in logic, and their contents may be any logic types themselves."
but when trying so, we got an error "not a C type".
Looking at type logic_type in cil/src/cil_types.mli
I understand that actually implementing what the documentation
says may require a non negligible amount of work
and I don't expect it anytime soon.
But putting a "not yet implemented" warning or something like that
in the implementation documentation would be nice.
TagsNo tags attached.
Attached Files




virgile (developer)

Actually this is flagged as unimplemented in section 2.6.8 (fig. 2.16) which deals specifically with concrete logic types. Admittedly, section 2.2.7 should refer to this.


Fix committed to stable/neon branch.

-Issue History
Date Modified Username Field Change
2011-05-24 15:50 proux New Issue
2011-05-24 15:50 proux Status new => assigned
2011-05-24 15:50 proux Assigned To => virgile
2011-05-24 17:38 virgile Note Added: 0001924
2011-08-30 18:25 svn
2011-08-30 18:25 svn Status assigned => resolved
2011-08-30 18:25 svn Resolution open => fixed
2011-10-10 14:13 signoles Fixed in Version => Frama-C Nitrogen-20111001
2011-10-10 14:14 signoles Status resolved => closed
2013-12-19 01:12 Source_changeset_attached => framac master 85986fba
2014-02-12 16:54 Source_changeset_attached => framac stable/neon 85986fba
2014-02-12 16:59 Note Added: 0004745
2014-02-12 16:59 Status closed => resolved
+Issue History