Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0002272Frama-CKernelpublic2017-01-16 12:062017-01-16 15:29
ReporterJochen 
Assigned Tovirgile 
PrioritylowSeverityminorReproducibilityalways
StatusassignedResolutionopen 
PlatformSilicon-20161101OSxubuntuOS Version
Product VersionFrama-C 14-Silicon 
Target VersionFixed in Version 
Summary0002272: WP appears to assume left-to-right evaluation order for int addition
DescriptionThe following issue originated from our student Robert. Running "frama-c -wp -wp-rte robert.c" on the attached program reports 3 proof goals, all of which are proven by Qed. However, according to ISO/IEC 9899:2011 ยง6.5 (2), the behavior of this function is undefined, since "x" is modified more than once between two sequence points.

Replacing the "4" in the ensures clause in line 2 by "2" or "3", or replacing the whole formula in line 2 by "\false", all results in one unproven goal (and two proven goals). Therefore, it seems that Frama-C's justification for proving "\result==4" is not that the function won't return anyway, due to the undefined behavior, considered as throwing an exception.
TagsNo tags attached.
Attached Filesc file icon robert.c [^] (85 bytes) 2017-01-16 12:06 [Show Content]

- Relationships

-  Notes
(0006335)
jens (reporter)
2017-01-16 13:43

Shouldn't the Frama-C kernel reject the program even before WP starts its work?
(0006336)
virgile (developer)
2017-01-16 15:28

As a matter of fact, if you use option -unspecified-access, you'll get a (somewhat cryptic, I'll admit) warning about the side effects, and value will reject the program (more precisely tell you that foo is non terminating, with an assertion \separated(&x, &x) which is clearly invalid. However, WP does not take advantage of the additional information provided by -unspecified-access.

It's been a long time since we have done work in the area of badly sequenced accesses, and some re-architecture is probably in order (e.g. having rte plugin generate appropriate assertions so that verification is not restricted to Value) if you really need it.

Note in addition that -unspecified-access is restricted to intra-functional accesses. For instance, assuming that f is defined as

void f(int *x) { *x = 0; }

it will not warn about the expression f(y) + (y = 1)

there is an obsolete, never released, and very early-stage plug-in that uses Value to take care of such inter-procedural bad sequencing, that can be resurrected if needed.

- Issue History
Date Modified Username Field Change
2017-01-16 12:06 Jochen New Issue
2017-01-16 12:06 Jochen Status new => assigned
2017-01-16 12:06 Jochen Assigned To => correnson
2017-01-16 12:06 Jochen File Added: robert.c
2017-01-16 13:43 jens Note Added: 0006335
2017-01-16 15:28 virgile Note Added: 0006336
2017-01-16 15:29 virgile Assigned To correnson => virgile
2017-01-16 15:29 virgile Priority normal => low
2017-01-16 15:29 virgile Category Plug-in > wp => Kernel


Copyright © 2000 - 2019 MantisBT Team
Powered by Mantis Bugtracker