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