2020-12-05 00:12 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0002137Frama-CPlug-in > Evapublic2017-06-15 15:56
Reporterrcl 
Assigned Toyakobowski 
PrioritynormalSeverityminorReproducibilityalways
StatusclosedResolutionfixed 
Product VersionFrama-C Sodium 
Target VersionFrama-C 15-PhosphorusFixed in VersionFrama-C 15-Phosphorus 
Summary0002137: value analysis introduces weird pointer assert with variable length arrays
DescriptionThe value analysis plugin generates an assertion of the form

  /*@ assert
      Value: ptr_comparison:
        \pointer_comparable((void *)*(arr+0), (void *)val);
  */

when arr is a VLA. This assertion looks bogus; it doesn't make any sense and doesn't even type check.
Steps To ReproduceRun the value analysis plugin on the attached source code form.
TagsNo tags attached.
Attached Files
  • c file icon ptrcmp.c (384 bytes) 2015-06-26 13:09 -
    /* Frama-C erzeugt eine komische Assertion über Zeigervergleiche für
     * diesen Code wenn man den value analyzer laufen lässt. Ist das ein
     * Programmfehler in Frama-C? */
    
    #include <limits.h>
    #include "/home/rcl/.opam/system/share/frama-c/builtin.h"
    
    int main()
    {
    	const unsigned n = 10;
    	int arr[n], val = 0;
    
    	if (arr[0] == val)
    		Frama_C_abort();
    
    	return 0;
    }
    
    c file icon ptrcmp.c (384 bytes) 2015-06-26 13:09 +
  • c file icon ptrcmp.2.c (468 bytes) 2015-07-17 09:28 -
    /*
     * The Frama-C value analyzer generate a weird assertion about pointer
     * comparisons for this code. Is this a programming error in Frama-C?
     * Invoke Frama-C like this:
     *
     *     frama-c-gui -val ptrcmp.c
     *
     * The generated assertion is:
     *
     *     \pointer_comparable((void *)*(arr+0), (void *)val);
     */
    
    #include <limits.h>
    
    int main()
    {
    	const unsigned n = 10;
    	int arr[n], val = 0;
    
    	if (arr[0] == val)
    		Frama_C_abort();
    
    	return 0;
    }
    
    c file icon ptrcmp.2.c (468 bytes) 2015-07-17 09:28 +

-Relationships
+Relationships

-Notes

~0005943

jens (reporter)

- please add the exact command line with which you called Frama-C

- also your file contains an explicit (and probably unnecessary) reference to your local Frama-C installation.

- the remarks in your source are in German

~0005983

rcl (reporter)

Last edited: 2015-07-17 09:29

View 2 revisions

I'm sorry for not answering until now. Attached is an updated version of the source file that addresses your issues. Please invoke Frama-C like this on the source file:

    frama-c-gui -val ptrcmp.2.c

~0006191

yakobowski (manager)

Last edited: 2016-05-31 19:21

View 2 revisions

The modelization of alloca is/was broken (or, more to the point non-existent). This will be corrected in Frama-C Silicium.

~0006392

yakobowski (manager)

alloca will be properly handled in Phosphorus.

~0006414

maroneze (administrator)

Just for clarification, here's the current situation:

- alloca is not handled in Frama-C 15 Phosphorus;
- however, VLAs are, and their usage leads to a syntactic transformation that inserts calls to __fc_vla_alloc/__fc_vla_free.

Option -val-builtins-list shows that __fc_vla_alloc is mapped to the builtin Frama_C_vla_alloc_by_stack, and __fc_vla_free is mapped to Frama_C_vla_free. These builtins should ensure correct handling of VLAs.

In the example, with Frama-C 15 Phosphorus we have a definitive alarm about accessing the uninitialized array element, but no more \pointer_comparable. So the reported issue has been fixed.

Note that, unfortunately, using __fc_vla_alloc leads to a warning about "Neither code nor specification for function __fc_vla_alloc, generating default assigns from the prototype". This should be handled in the next Frama-C release.
+Notes

-Issue History
Date Modified Username Field Change
2015-06-26 13:09 rcl New Issue
2015-06-26 13:09 rcl Status new => assigned
2015-06-26 13:09 rcl Assigned To => yakobowski
2015-06-26 13:09 rcl File Added: ptrcmp.c
2015-06-26 20:21 jens Note Added: 0005943
2015-07-17 09:27 rcl Note Added: 0005983
2015-07-17 09:28 rcl File Added: ptrcmp.2.c
2015-07-17 09:29 rcl Note Edited: 0005983 View Revisions
2016-05-31 19:20 yakobowski Note Added: 0006191
2016-05-31 19:21 yakobowski Note Edited: 0006191 View Revisions
2017-03-06 11:35 yakobowski Target Version => Frama-C 15-Phosphorus
2017-03-31 20:21 yakobowski Note Added: 0006392
2017-03-31 20:21 yakobowski Status assigned => resolved
2017-03-31 20:21 yakobowski Resolution open => fixed
2017-05-31 19:04 signoles Fixed in Version => Frama-C 15-Phosphorus
2017-05-31 19:05 signoles Status resolved => closed
2017-06-15 15:55 maroneze Note Added: 0006414
2017-06-15 15:55 maroneze Status closed => resolved
2017-06-15 15:56 maroneze Status resolved => closed
2018-01-12 14:26 signoles Category Plug-in > value analysis => Plug-in > Eva
+Issue History