2021-03-05 02:40 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0002194Frama-CPlug-in > E-ACSLpublic2019-01-25 10:55
Assigned Tosignoles 
Product Version 
Target VersionFixed in Version 
Summary0002194: Failure to record global variable with initialiser
Description/* The following example wrongly fails the assertion */
#include <inttypes.h>
char *B = "foo";

unsigned long ref() {
   return (intptr_t)B;

int main(int argc, char **argv) {
    char *ptr = (char*)ref();
    //@ assert \valid_read(ptr);
    return 0;
Additional InformationThis seems to be the case where memory analysis incorrectly determines that global variable 'B' should not be modelled and therefore it is omitted from the instrumentation.
TagsNo tags attached.
Attached Files


There are no notes attached to this issue.

-Issue History
Date Modified Username Field Change
2015-12-04 12:01 kvorobyov New Issue
2015-12-04 12:01 kvorobyov Status new => assigned
2015-12-04 12:01 kvorobyov Assigned To => kvorobyov
2016-09-13 07:52 signoles Assigned To kvorobyov => signoles
2018-02-22 10:37 signoles Assigned To signoles => fmaurica
2019-01-25 10:55 signoles Assigned To fmaurica => signoles
+Issue History