0002194: Failure to record global variable with initialiser

View Issue Details [ Jump to Notes ]

[ Issue History ] [ Print ]

Project

Category

View Status

Date Submitted

Last Update

0002194

Frama-C

Plug-in > E-ACSL

public

2015-12-04 12:01

2019-01-25 10:55

Reporter

kvorobyov

Assigned To

signoles

Priority

normal

Severity

minor

Reproducibility

always

Status

assigned

Resolution

open

Platform

OS Version

Product Version

Target Version

Fixed in Version

Summary

0002194: 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 Information

This 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.

Tags

No 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
2019-01-25 10:55	signoles	Assigned To	fmaurica => signoles