2021-03-05 07:28 CET
  

View Issue Details [ Jump to Notes ] [ Issue History ] [ Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0001537Frama-CPlug-in > wppublic2013-10-28 16:102014-06-02 16:40
Reporterdpariente 
Assigned Tocorrenson 
PrioritynormalSeverityfeatureReproducibilityalways
StatusacknowledgedResolutionopen 
Product VersionFrama-C Fluorine-20130601 
Target VersionFixed in Version 
Summary0001537: Frama-C should warn about inconsistent specification of declared functions
Description[STANCE]

The following code:

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

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.
Attached Files

-Relationships
related to 0001678closedcorrenson Frama-C/WP does not warn about unsatisfied precondition 
+Relationships

-Notes

~0004171

virgile (developer)

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.

~0004177

dpariente (reporter)

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;
printf("%d\",sizeof(t1));
}
The runtime of this program yields "5" as expected, and the assert is duly discharged by WP.

~0004178

virgile (developer)

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;

~0004182

dpariente (reporter)

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;
char*g(char*p);
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 (!).

Thanks.

~0004183

virgile (developer)

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.

~0004184

virgile (developer)

2013-10-29 14:29

 re-classified as feature wish: there should be more warnings about 'suspicious' but unverifiable specifications.

~0004509

correnson (manager)

2014-02-05 16:55

 Feature wish
+Notes

-Issue History
Date Modified Username Field Change
2013-10-28 16:10 dpariente New Issue
2013-10-28 16:10 dpariente Status new => assigned
2013-10-28 16:10 dpariente Assigned To => correnson
2013-10-28 17:41 virgile Note Added: 0004171
2013-10-28 17:41 virgile Status assigned => feedback
2013-10-28 21:11 dpariente Note Added: 0004177
2013-10-28 22:24 virgile Note Added: 0004178
2013-10-29 12:53 dpariente Note Added: 0004182
2013-10-29 12:54 dpariente Note Edited: 0004182
2013-10-29 14:26 virgile Note Added: 0004183
2013-10-29 14:29 virgile Note Added: 0004184
2013-10-29 14:29 virgile Severity major => feature
2013-10-29 14:29 virgile Status feedback => confirmed
2013-10-29 14:29 virgile Summary Qed: sizeof ==> false => Frama-C should warn about inconsistent specification of declared functions
2014-02-05 16:55 correnson Note Added: 0004509
2014-02-05 16:55 correnson Status confirmed => acknowledged
2014-06-02 16:40 correnson Relationship added related to 0001678
+Issue History