Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0002234Frama-CPlug-in > wppublic2016-06-21 22:262016-06-21 22:26
Reporterjrobbins 
Assigned Tocorrenson 
PrioritynormalSeveritymajorReproducibilityalways
StatusassignedResolutionopen 
PlatformOSOS Version
Product VersionFrama-C Aluminium 
Target VersionFixed in Version 
Summary0002234: Creating a pointer to a local causes valid pointers above it to lose thier valid status
DescriptionPointers that are \valid lose their status as \valid if there is code below it that assigns to a pointer. This only seems to happen when the pointer in question is wrapped in a struct.
Steps To Reproduce== file bug.c:

struct s {
    int* ptr;
};

/*@
requires \valid(t.ptr);
@*/
void foo(struct s t) {
    //@ assert \valid(t.ptr);
    int a;
    int* x = &a;
}

== Run command:

frama-c bug.c -wp

== Output:

[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing bug.c (with preprocessing)
[wp] warning: Missing RTE guards
[wp] 1 goal scheduled
[wp] [Alt-Ergo] Goal typed_foo_assert : Unknown (51ms)
[wp] Proved goals: 0 / 1
     Alt-Ergo: 0 (unknown: 1)

== File fixed.c:

struct s {
    int* ptr;
};

/*@
requires \valid(t.ptr);
@*/
void foo(struct s t) {
    //@ assert \valid(t.ptr);
    int a;
    int* x; // = &a;
}

== Run command:

frama-c bug.c -wp

== Output:

[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing bug.c (with preprocessing)
[wp] warning: Missing RTE guards
[wp] 1 goal scheduled
[wp] Proved goals: 1 / 1
     Qed: 1
Additional InformationTested on Aluminum on a Linux machine.
TagsNo tags attached.
Attached Files

- Relationships

-  Notes
There are no notes attached to this issue.

- Issue History
Date Modified Username Field Change
2016-06-21 22:26 jrobbins New Issue
2016-06-21 22:26 jrobbins Status new => assigned
2016-06-21 22:26 jrobbins Assigned To => correnson


Copyright © 2000 - 2019 MantisBT Team
Powered by Mantis Bugtracker