Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0002194Frama-CPlug-in > E-ACSLpublic2015-12-04 12:012018-02-22 10:37
Assigned Tofmaurica 
PlatformOSOS Version
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

- Relationships

-  Notes
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

Copyright © 2000 - 2018 MantisBT Team
Powered by Mantis Bugtracker