Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0002245Frama-CPlug-in > wppublic2016-08-17 15:352016-08-17 15:35
Assigned Tocorrenson 
PlatformOSOS Version
Product VersionFrama-C Aluminium 
Target VersionFixed in Version 
Summary0002245: Nested scopes may cause issues with the validity of created pointers
DescriptionUpon entering a nested scope (caused by conditional blocks, or even just wrapping parts of code in {}), pointers once known as valid may become unknown in validity. This only seems to occur when more than 1 pointer is being reasoned about in the scope.
Steps To Reproduce== Program bug.c:
ensures \valid(\result);
int* foo();

void main() {
    int* x = foo();
        int y;
        //@ assert \valid(x);
        //@ assert \valid(&y);
== Command to run:
frama-c bug.c -wp
== Output:
[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing bug.c (with preprocessing)
bug.c:6:[kernel] warning: No code nor implicit assigns clause for function foo, generating default assigns from the prototype
[wp] warning: Missing RTE guards
[wp] 2 goals scheduled
[wp] [Alt-Ergo] Goal typed_main_assert : Unknown (51ms)
[wp] Proved goals: 1 / 2
     Qed: 1
     Alt-Ergo: 0 (unknown: 1)
== Expected output:
Both assertions to pass, since x is ensures to be valid, and the & operator always returns a valid pointer.
== Real output:
The pointer we ensure to be valid could not be proven to be valid.

Moving the definition of y to the outer scope fixes this issue, as well as moving the definition of x inside.
Additional InformationThis bug occurs on both Sodium in Cygwin and Aluminum on Linux.
TagsNo tags attached.
Attached Filesc file icon bug.c [^] (180 bytes) 2016-08-17 15:35 [Show Content]

- Relationships

-  Notes
There are no notes attached to this issue.

- Issue History
Date Modified Username Field Change
2016-08-17 15:35 jrobbins New Issue
2016-08-17 15:35 jrobbins Status new => assigned
2016-08-17 15:35 jrobbins Assigned To => correnson
2016-08-17 15:35 jrobbins File Added: bug.c

Copyright © 2000 - 2019 MantisBT Team
Powered by Mantis Bugtracker