Nested scopes may cause issues with the validity of created pointers
ID0002245: This issue was created automatically from Mantis Issue 2245. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0002245 | Frama-C | Plug-in > wp | public | 2016-08-17 | 2016-08-17 |
| 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 :
Upon 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.
Additional Information :
This bug occurs on both Sodium in Cygwin and Aluminum on Linux.
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.