Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0002245Frama-CPlug-in > wppublic2016-08-17 15:352016-08-17 15:35
Assigned Tocorrenson 
PlatformOSOS Version
Product VersionFrama-C Aluminium 
Target VersionFixed in Version 
Summary0002245: Nested scopes may cause issues with the validity of created pointers
DescriptionUpon 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.
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.
Additional InformationThis bug occurs on both Sodium in Cygwin and Aluminum on Linux.
TagsNo tags attached.
Attached Filesc file icon bug.c [^] (180 bytes) 2016-08-17 15:35 [Show Content]

- Relationships

-  Notes
There are no notes attached to this issue.

- Issue History
Date Modified Username Field Change
2016-08-17 15:35 jrobbins New Issue
2016-08-17 15:35 jrobbins Status new => assigned
2016-08-17 15:35 jrobbins Assigned To => correnson
2016-08-17 15:35 jrobbins File Added: bug.c

Copyright © 2000 - 2020 MantisBT Team
Powered by Mantis Bugtracker