2021-02-27 10:51 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0001716Frama-CPlug-in > E-ACSLpublic2014-09-15 17:20
Reporterarvidj 
Assigned Tosignoles 
PrioritynormalSeverityminorReproducibilityalways
StatusclosedResolutionfixed 
Product Version 
Target VersionFixed in VersionFrama-C Neon-20140301 
Summary0001716: Dynamically allocated variables in body of while without break are not instrumented
DescriptionThe assertion on line 14 of the attached program fails even though p is a valid pointer at this point. However if the break on line 12 is uncommented, the assertion passes.
Steps To ReproduceFrama-c run with the following parameters:
 -machdep x86_64 -e-acsl bug-while-without-break.c -then-on e-acsl -print -ocode bug-while-without-break.gen.c

Compiled with the following flags:
 export SHARE=`frama-c -print-share-path`
 gcc -g -O0 -std=c99 -pedantic -Wall -Wno-long-long -Wno-attributes -Wno-unused-but-set-variable -fno-builtin -o bug-while-without-break.c.out $SHARE/e-acsl/e_acsl.c $SHARE/e-acsl/memory_model/e_acsl_bittree.c $SHARE/e-acsl/memory_model/e_acsl_mmodel.c bug-while-without-break.gen.c -lgmp
TagsNo tags attached.
Attached Files
  • c file icon bug-while-without-break.c (459 bytes) 2014-03-25 10:30 -
    #include <stdlib.h>
    
    /** In this program, p will not be monitored (which should be an error since it
     *  has a valid annotation) and it will fail on the valid annotaiton. However,
     *  if one uncomments the line with the break, p will be monitored and the
     *  program will loop. */
    int main(void) {
    	int *p = NULL;
    
    	while (1) {
    		p = (int*)malloc(sizeof(int));
    		/* if (p == NULL) break; */
    		*p = 10;
    		/*@assert p != \null ==> \valid(p); */
    		free(p);
    	}
    }
    
    c file icon bug-while-without-break.c (459 bytes) 2014-03-25 10:30 +

-Relationships
+Relationships

-Notes

~0005460

signoles (manager)

Fixed in E-ACSL v0.4.1.
+Notes

-Issue History
Date Modified Username Field Change
2014-03-25 10:30 arvidj New Issue
2014-03-25 10:30 arvidj Status new => assigned
2014-03-25 10:30 arvidj Assigned To => signoles
2014-03-25 10:30 arvidj File Added: bug-while-without-break.c
2014-03-25 17:37 signoles Status assigned => resolved
2014-03-25 17:37 signoles Resolution open => fixed
2014-09-15 17:20 signoles Fixed in Version => Frama-C Neon-20140301
2014-09-15 17:20 signoles Note Added: 0005460
2014-09-15 17:20 signoles Status resolved => closed
+Issue History