Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Related Changesets ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0001478Frama-CPlug-in > E-ACSLpublic2013-09-04 14:532014-03-25 14:17
Reporterdmentre 
Assigned Tosignoles 
PrioritynormalSeveritymajorReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
Product VersionFrama-C Fluorine-20130601 
Target VersionFixed in VersionFrama-C Fluorine-20130601 
Summary0001478: E-ACSL reports use of invalid pointer while in fact the pointer is valid
DescriptionOn 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
"""
TagsNo tags attached.
Attached Filesc file icon q7_invalid_under_eacsl.c [^] (481 bytes) 2013-09-04 14:53 [Show Content]

- Relationships

-  Notes
(0004057)
signoles (manager)
2013-09-04 15:08

should take global initializers into account in the pre-dataflow analysis.
(0004059)
signoles (manager)
2013-09-04 20:08
edited on: 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 (manager)
2013-09-23 20:04

Fixed in E-ACSL 0.3.
(0004990)
signoles (manager)
2014-03-25 14:17

Fix committed to stable/neon branch.

- Issue History
Date Modified Username Field Change
2013-09-04 14:53 dmentre New Issue
2013-09-04 14:53 dmentre Status new => assigned
2013-09-04 14:53 dmentre Assigned To => signoles
2013-09-04 14:53 dmentre File Added: q7_invalid_under_eacsl.c
2013-09-04 15:08 signoles Note Added: 0004057
2013-09-04 15:08 signoles Status assigned => confirmed
2013-09-04 15:52 svn Checkin
2013-09-04 15:52 svn Status confirmed => resolved
2013-09-04 15:52 svn Resolution open => fixed
2013-09-04 20:08 signoles Note Added: 0004059
2013-09-04 20:08 signoles Note Edited: 0004059
2013-09-23 20:04 signoles Note Added: 0004085
2013-09-23 20:04 signoles Fixed in Version => Frama-C Fluorine-20130601
2013-09-23 20:04 signoles Status resolved => closed
2014-03-25 14:17 signoles Note Added: 0004990


Copyright © 2000 - 2018 MantisBT Team
Powered by Mantis Bugtracker