Frama-C Bug Tracking System - Frama-C
View Issue Details
0002234Frama-CPlug-in > wppublic2016-06-21 22:262016-06-21 22:26
jrobbins 
correnson 
normalmajoralways
assignedopen 
Frama-C Aluminium 
 
0002234: Creating a pointer to a local causes valid pointers above it to lose thier valid status
Pointers 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.
== 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
Tested on Aluminum on a Linux machine.
No tags attached.
Issue History
2016-06-21 22:26jrobbinsNew Issue
2016-06-21 22:26jrobbinsStatusnew => assigned
2016-06-21 22:26jrobbinsAssigned To => correnson

There are no notes attached to this issue.