Frama-C Bug Tracking System - Frama-C
View Issue Details
0001490Frama-CPlug-in > pathcrawlerpublic2013-10-01 09:012018-11-30 11:41
nicky 
muriel 
highmajoralways
closedfixed 
Frama-C GIT, precise the release id 
 
0001490: With -no-lib-entry, the dimension of global structs is not passed to the generator
Compare 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
ajout de unrollType dans save_const_dim_input
No tags attached.
c microwave.c (2,123) 2013-10-01 09:02
https://bts.frama-c.com/file_download.php?file_id=530&type=bug
Issue History
2013-10-01 09:01nickyNew Issue
2013-10-01 09:01nickyStatusnew => assigned
2013-10-01 09:01nickyAssigned To => muriel
2013-10-01 09:01nickyFile Added: fixed_domain.pl.no_lib_entry
2013-10-01 09:01nickyFile Deleted: fixed_domain.pl.no_lib_entry
2013-10-01 09:02nickyFile Added: microwave.c
2013-10-01 15:37murielStatusassigned => resolved
2013-10-01 15:37murielAdditional Information Updated
2014-03-13 16:41murielStatusresolved => closed
2018-11-30 10:50signolesCategoryPlug-in > PathCrawler => Plug-in > pathcrawler
2018-11-30 11:41signolesResolutionopen => fixed

There are no notes attached to this issue.