Frama-C Bug Tracking System - Frama-C
View Issue Details
0000506Frama-CKernelpublic2010-06-11 14:062014-02-12 16:55
sduprat 
virgile 
normalfeatureN/A
closedfixed 
Frama-C Boron-20100401 
Frama-C Carbon-20101201-beta1Frama-C Carbon-20101201-beta1 
0000506: line command option for doCollapseCallCast configuration
For specific syntactic verifications, we need to modify source-code with doCollapseCallCast set to true (cabs2cil.ml).
This is the case for example to check casts of called functions.
It would be nice to set this configuration throw a command-line option as it already exists for KeepComments (option -keep-comments).
We suggest a new kernel option -collapse-call-cast.
No tags attached.
Issue History
2010-06-11 14:06sdupratNew Issue
2010-06-11 15:02virgileNote Added: 0000927
2010-06-11 15:02virgileAssigned To => virgile
2010-06-11 15:02virgileStatusnew => acknowledged
2010-08-16 08:54virgileTarget Version => Frama-C Carbon
2010-08-17 11:34svnCheckin
2010-08-17 11:34svnStatusacknowledged => resolved
2010-08-17 11:34svnResolutionopen => fixed
2010-12-10 15:45signolesFixed in Version => Frama-C Carbon-20101201-beta1
2010-12-17 19:36signolesStatusresolved => closed

Notes
(0000927)
virgile   
2010-06-11 15:02   
A few other parameters of the normalization are not settable directly through command-line. They could be treated as well