E-ACSL reports use of invalid pointer while in fact the pointer is valid
ID0001478: This issue was created automatically from Mantis Issue 1478. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0001478 | Frama-C | Plug-in > E-ACSL | public | 2013-09-04 | 2014-03-25 |
| Reporter | dmentre | Assigned To | signoles | Resolution | fixed |
| Priority | normal | Severity | major | Reproducibility | always |
| Platform | - | OS | - | OS Version | - |
| Product Version | Frama-C Fluorine-20130601 | Target Version | - | Fixed in Version | Frama-C Fluorine-20130601 |
Description :
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
"""