Frama-C Bug Tracking System - Frama-C
View Issue Details
0001537Frama-CPlug-in > wppublic2013-10-28 16:102014-06-02 16:40
Assigned Tocorrenson 
PlatformOSOS Version
Product VersionFrama-C Fluorine-20130601 
Target VersionFixed in Version 
Summary0001537: Frama-C should warn about inconsistent specification of declared functions

The following code:

//@ assigns \result \from p; ensures sizeof(\result)==5;

void f()
char *p=g(p);
//@ assert sizeof(p)==5;
//@ assert \false;

analyzed by:
frama-c foo.c -no-unicode -wp

Qed proves the 2nd assert in f():
[wp] [Qed] Goal typed_f_assert_2 : Valid
TagsNo tags attached.
related to 0001678closed correnson Frama-C/WP does not warn about unsatisfied precondition 
Attached Files

2013-10-28 17:41   
I'll let Loïc confirm this, but to me this is not a bug. Frama-C always analyses a program over a given architecture, and none of the supported ones have 5 bytes pointer. Thus sizeof(\result) is always different from 5: the ensures of g is
reducible to \false, as well as the first assert in f, and the second assert gets proved.
2013-10-28 21:11   
In this case, it is not the sizeof for a basic C type, but for an array.
For instance :
#include <stdio.h>
int main() { char t1[5];
//@ assert sizeof(t1)==5;
The runtime of this program yields "5" as expected, and the assert is duly discharged by WP.
2013-10-28 22:24   
But this is a completely different program. On the following example:

int main() { char t1[5];
//@ assert sizeof(t1)==5;
//@ assert \false;
return sizeof(t1);

frama-c -wp foo.c fails to discharge the assert \false;
2013-10-29 12:53   
(Last edited: 2013-10-29 12:54)
Yes you're right Virgile!
With this code:

//@ assigns \result \from p; ensures sizeof(\result)==4;
void f()
{ char *p=g(p);
//@ assert sizeof(p)==4;
//@ assert \false;

the second assert is not validated.
So this might mean that there is the assumption you mentioned on the architecture "somewhere" when using sizeof.
If it is the case, this is not visible to the end-user: the local status of "sizeof(p)" should be false indeed when the actual size does not correspond to a possible arch: this could help when investigating what a (opensource and quite complex) program is really doing (!).


2013-10-29 14:26   
Technically, the consolidated status of the ensures is "Unverifiable but considered valid": it is up to the user to verify that the specification of a declared function makes sense.

That said, it is true that there could be a smoke-detector plug-in that would check that that said specification is not inconsistent with the global hypotheses made on the program.
2013-10-29 14:29   
re-classified as feature wish: there should be more warnings about 'suspicious' but unverifiable specifications.
2014-02-05 16:55   
Feature wish

Issue History
2013-10-28 16:10dparienteNew Issue
2013-10-28 16:10dparienteStatusnew => assigned
2013-10-28 16:10dparienteAssigned To => correnson
2013-10-28 17:41virgileNote Added: 0004171
2013-10-28 17:41virgileStatusassigned => feedback
2013-10-28 21:11dparienteNote Added: 0004177
2013-10-28 22:24virgileNote Added: 0004178
2013-10-29 12:53dparienteNote Added: 0004182
2013-10-29 12:54dparienteNote Edited: 0004182
2013-10-29 14:26virgileNote Added: 0004183
2013-10-29 14:29virgileNote Added: 0004184
2013-10-29 14:29virgileSeveritymajor => feature
2013-10-29 14:29virgileStatusfeedback => confirmed
2013-10-29 14:29virgileSummaryQed: sizeof ==> false => Frama-C should warn about inconsistent specification of declared functions
2014-02-05 16:55corrensonNote Added: 0004509
2014-02-05 16:55corrensonStatusconfirmed => acknowledged
2014-06-02 16:40corrensonRelationship addedrelated to 0001678