2021-03-03 03:46 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0001478Frama-CPlug-in > E-ACSLpublic2014-03-25 14:17
Reporterdmentre 
Assigned Tosignoles 
PrioritynormalSeveritymajorReproducibilityalways
StatusclosedResolutionfixed 
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 Files
  • c file icon q7_invalid_under_eacsl.c (481 bytes) 2013-09-04 14:53 -
    #include "stdlib.h"
    
    int global_i = 0;
    int* global_i_ptr = &global_i;
    
    /*@ requires global_i == 0;
        requires \valid(global_i_ptr);
        requires global_i_ptr == &global_i;
        assigns global_i;
     */
    void loop(void)
    {
      int i;
    
      if (global_i != 0)
        abort();
    
      /*@ loop invariant 0 <= i <= 99;
          loop invariant global_i_ptr == &global_i;
          loop assigns i, global_i;
       */
      for (i=0; i<99; i++) {
        *global_i_ptr = i;
      }
    }
    
    int main(void)
    {
      loop();
    
      return 0;
    }
    
    c file icon q7_invalid_under_eacsl.c (481 bytes) 2013-09-04 14:53 +

-Relationships
+Relationships

-Notes

~0004057

signoles (manager)

should take global initializers into account in the pre-dataflow analysis.

~0004059

signoles (manager)

Last edited: 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)

Fixed in E-ACSL 0.3.

~0004990

signoles (manager)

Fix committed to stable/neon branch.
+Notes

-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
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 Source_changeset_attached => e-acsl stable/neon 2047e8fb
2014-03-25 14:17 signoles Note Added: 0004990
+Issue History