Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Related Changesets ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000506Frama-CKernelpublic2010-06-11 14:062014-02-12 16:55
Reportersduprat 
Assigned Tovirgile 
PrioritynormalSeverityfeatureReproducibilityN/A
StatusclosedResolutionfixed 
PlatformOSOS Version
Product VersionFrama-C Boron-20100401 
Target VersionFrama-C Carbon-20101201-beta1Fixed in VersionFrama-C Carbon-20101201-beta1 
Summary0000506: line command option for doCollapseCallCast configuration
DescriptionFor 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.
TagsNo tags attached.
Attached Files

- Relationships

-  Notes
(0000927)
virgile (developer)
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

- Issue History
Date Modified Username Field Change
2010-06-11 14:06 sduprat New Issue
2010-06-11 15:02 virgile Note Added: 0000927
2010-06-11 15:02 virgile Assigned To => virgile
2010-06-11 15:02 virgile Status new => acknowledged
2010-08-16 08:54 virgile Target Version => Frama-C Carbon
2010-08-17 11:34 svn Checkin
2010-08-17 11:34 svn Status acknowledged => resolved
2010-08-17 11:34 svn Resolution open => fixed
2010-12-10 15:45 signoles Fixed in Version => Frama-C Carbon-20101201-beta1
2010-12-17 19:36 signoles Status resolved => closed


Copyright © 2000 - 2017 MantisBT Team
Powered by Mantis Bugtracker