Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0001490Frama-CPlug-in > pathcrawlerpublic2013-10-01 09:012018-11-30 11:41
Reporternicky 
Assigned Tomuriel 
PriorityhighSeveritymajorReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
Product VersionFrama-C GIT, precise the release id 
Target VersionFixed in Version 
Summary0001490: With -no-lib-entry, the dimension of global structs is not passed to the generator
DescriptionCompare the fixed_domain.pl file produced by running
frama-c -pc-analyzer -main test_me microwave.c
and
frama-c -pc-analyzer -main test_me microwave.c -lib-entry

There is no const_dim_input clause for structs mw_state and mw_inputs with the -no-lib-entry option
Additional Informationajout de unrollType dans save_const_dim_input
TagsNo tags attached.
Attached Filesc file icon microwave.c [^] (2,123 bytes) 2013-10-01 09:02 [Show Content]

- Relationships

-  Notes
There are no notes attached to this issue.

- Issue History
Date Modified Username Field Change
2013-10-01 09:01 nicky New Issue
2013-10-01 09:01 nicky Status new => assigned
2013-10-01 09:01 nicky Assigned To => muriel
2013-10-01 09:01 nicky File Added: fixed_domain.pl.no_lib_entry
2013-10-01 09:01 nicky File Deleted: fixed_domain.pl.no_lib_entry
2013-10-01 09:02 nicky File Added: microwave.c
2013-10-01 15:37 muriel Status assigned => resolved
2013-10-01 15:37 muriel Additional Information Updated
2014-03-13 16:41 muriel Status resolved => closed
2018-11-30 10:50 signoles Category Plug-in > PathCrawler => Plug-in > pathcrawler
2018-11-30 11:41 signoles Resolution open => fixed


Copyright © 2000 - 2018 MantisBT Team
Powered by Mantis Bugtracker