2021-02-27 10:19 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0001715Frama-CPlug-in > E-ACSLpublic2014-09-15 17:20
Reporterarvidj 
Assigned Tosignoles 
PrioritynormalSeverityminorReproducibilityalways
StatusclosedResolutionfixed 
Product Version 
Target VersionFixed in VersionFrama-C Neon-20140301 
Summary0001715: "[...]/e_acsl_bittree.c:341: __get_exact: Assertion `0' failed." using full memory model, asserting validty of local var
DescriptionThe attached program fails with the following message:

bug-full-mmodel.gen.c.out: /home/arvidj/dev/e-acsl/share/e-acsl/memory_model/e_acsl_bittree.c:341: __get_exact: Assertion `0' failed.
Aborted (core dumped)
Steps To ReproduceFrama-c run with the following parameters:
 -machdep x86_64 -e-acsl -e-acsl-full-mmodel bug-full-mmodel.c -then-on e-acsl -print -ocode bug-full-mmodel.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 $1.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 $1 -lgmp
TagsNo tags attached.
Attached Files
  • c file icon bug-full-mmodel.c (289 bytes) 2014-03-25 10:18 -
    // this program fails on an assertion in
    // testgen.c.out: /home/arvidj/dev/e-acsl/share/e-acsl/memory_model/e_acsl_bittree.c:341: __get_exact: Assertion `0' failed.
    // when compiled with -e-acsl-full-mmodel
    int main(void) {
    	int a = 10, *p;
    	p = &a;
    	/*@assert \valid(p); */
    	return 0;
    }
    
    c file icon bug-full-mmodel.c (289 bytes) 2014-03-25 10:18 +

-Relationships
+Relationships

-Notes

~0005461

signoles (manager)

Fixed in E-ACSL v0.4.1.
+Notes

-Issue History
Date Modified Username Field Change
2014-03-25 10:18 arvidj New Issue
2014-03-25 10:18 arvidj Status new => assigned
2014-03-25 10:18 arvidj Assigned To => signoles
2014-03-25 10:18 arvidj File Added: bug-full-mmodel.c
2014-03-25 11:23 signoles Status assigned => resolved
2014-03-25 11:23 signoles Resolution open => fixed
2014-03-25 14:17 signoles Source_changeset_attached => e-acsl master b493590c
2014-09-15 17:20 signoles Fixed in Version => Frama-C Neon-20140301
2014-09-15 17:20 signoles Note Added: 0005461
2014-09-15 17:20 signoles Status resolved => closed
+Issue History