Creating a pointer to a local causes valid pointers above it to lose thier valid status
ID0002234: This issue was created automatically from Mantis Issue 2234. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0002234 | Frama-C | Plug-in > wp | public | 2016-06-21 | 2016-06-21 |
| Reporter | jrobbins | Assigned To | correnson | Resolution | open |
| Priority | normal | Severity | major | Reproducibility | always |
| Platform | - | OS | - | OS Version | - |
| Product Version | Frama-C Aluminium | Target Version | - | Fixed in Version | - |
Description :
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.
Additional Information :
Tested on Aluminum on a Linux machine.
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