Frama-C Bug Tracking System - Frama-C
View Issue Details
0001478Frama-CPlug-in > E-ACSLpublic2013-09-04 14:532014-03-25 14:17
dmentre 
signoles 
normalmajoralways
closedfixed 
Frama-C Fluorine-20130601 
Frama-C Fluorine-20130601 
0001478: E-ACSL reports use of invalid pointer while in fact the pointer is valid
On attached program, E-ACSL reports use of invalid pointer: """ Precondition failed at line 7 in function loop. The failing predicate is: \valid(global_i_ptr). """ But in fact the pointer is valid. This is checked by reading and executing the program, but also statically with WP and Value analysis. The attached program is compiled with following script, replacing $1 with q7_invalid_under_eacsl.c. """ PATH=/usr/local/stow/frama-c-Fluorine-20130601/bin:$PATH export PATH eacsl_path=`frama-c -print-share-path`/e-acsl frama-c \ -cpp-command 'gcc -C -E -I/usr/local/stow/frama-c-Fluorine-20130601/share/frama-c/libc -I SSI'\ -e-acsl \ $1 \ -then-on e-acsl -print -ocode a-e-acsl.c \ && \ gcc -I$eacsl_path $eacsl_path/memory_model/e_acsl_bittree.c $eacsl_path/memory_model/e_acsl_mmodel.c $eacsl_path/e_acsl.c a-e-acsl.c """
No tags attached.
c q7_invalid_under_eacsl.c (481) 2013-09-04 14:53
https://bts.frama-c.com/file_download.php?file_id=521&type=bug
Issue History
2013-09-04 14:53dmentreNew Issue
2013-09-04 14:53dmentreStatusnew => assigned
2013-09-04 14:53dmentreAssigned To => signoles
2013-09-04 14:53dmentreFile Added: q7_invalid_under_eacsl.c
2013-09-04 15:08signolesNote Added: 0004057
2013-09-04 15:08signolesStatusassigned => confirmed
2013-09-04 15:52svnCheckin
2013-09-04 15:52svnStatusconfirmed => resolved
2013-09-04 15:52svnResolutionopen => fixed
2013-09-04 20:08signolesNote Added: 0004059
2013-09-04 20:08signolesNote Edited: 0004059
2013-09-23 20:04signolesNote Added: 0004085
2013-09-23 20:04signolesFixed in Version => Frama-C Fluorine-20130601
2013-09-23 20:04signolesStatusresolved => closed
2014-03-25 14:17signolesNote Added: 0004990

Notes
(0004057)
signoles   
2013-09-04 15:08   
should take global initializers into account in the pre-dataflow analysis.
(0004059)
signoles   
2013-09-04 20:08   
Thanks for the bug report. It will be fixed in the next E-ACSL release. Workaround for this example: put the initializer of global_i_ptr in the main (as the first statement).
(0004085)
signoles   
2013-09-23 20:04   
Fixed in E-ACSL 0.3.
(0004990)
signoles   
2014-03-25 14:17   
Fix committed to stable/neon branch.