Frama-C Bug Tracking System - Frama-C
View Issue Details
0000835Frama-CKernel > ACSL implementationpublic2011-05-24 15:502014-02-12 16:59
proux 
virgile 
normalminorN/A
closedfixed 
Frama-C Carbon-20110201 
Frama-C Nitrogen-20111001 
0000835: Aggregate logic types containing only C types
According to section 2.2.7 of current ACSL implementation documentation http://frama-c.com/download/acsl-implementation-Carbon-20110201.pdf 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.
No tags attached.
Issue History
2011-05-24 15:50prouxNew Issue
2011-05-24 15:50prouxStatusnew => assigned
2011-05-24 15:50prouxAssigned To => virgile
2011-05-24 17:38virgileNote Added: 0001924
2011-08-30 18:25svnCheckin
2011-08-30 18:25svnStatusassigned => resolved
2011-08-30 18:25svnResolutionopen => fixed
2011-10-10 14:13signolesFixed in Version => Frama-C Nitrogen-20111001
2011-10-10 14:14signolesStatusresolved => closed
2014-02-12 16:59Note Added: 0004745
2014-02-12 16:59Statusclosed => resolved

Notes
(0001924)
virgile   
2011-05-24 17:38   
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.
(0004745)
   
2014-02-12 16:59   
Fix committed to stable/neon branch.