Frama-C Bug Tracking System - Frama-C
View Issue Details
0001179Frama-CPlug-in > wppublic2012-05-10 18:072016-06-21 14:08
Frama-C Nitrogen-20111001 
Frama-C Aluminium 
0001179: Suggest to supply values of global consts to provers
Wp/Simplify couldn't prove behavior-disjointness in line 5 of the attached program. The reason is that no information about the fixed values of c1 and c2 appears in the proof obligation. If the declarations in line 1-2 are replaced by #define-s, the proof is trivially found. I suggest to replace in the proof obligation each const variable by its value, if it is known at compile time. The latter restriction is satisfied for all variables visible in contracts (as opposed e.g. to asserts). Preferring C constants to macros is considered good software engineering practice; it shouldn't be discouraged by Frama-C/Wp.
No tags attached.
c ftest.c (166) 2012-05-10 18:07
c ftest2.c (202) 2012-05-12 14:51
Issue History
2012-05-10 18:07JochenNew Issue
2012-05-10 18:07JochenStatusnew => assigned
2012-05-10 18:07JochenAssigned To => correnson
2012-05-10 18:07JochenFile Added: ftest.c
2012-05-11 09:36virgileNote Added: 0003006
2012-05-11 12:36monateNote Added: 0003007
2012-05-11 12:41monateNote Added: 0003008
2012-05-11 12:41monateStatusassigned => resolved
2012-05-11 12:41monateResolutionopen => no change required
2012-05-11 14:33virgileNote Added: 0003009
2012-05-11 14:33virgileStatusresolved => feedback
2012-05-11 14:33virgileResolutionno change required => reopened
2012-05-11 18:30monateNote Added: 0003011
2012-05-12 14:51JochenFile Added: ftest2.c
2012-05-12 14:59JochenNote Added: 0003012
2012-05-12 22:09pascalNote Added: 0003013
2012-05-15 19:42yakobowskiNote Added: 0003014
2012-05-21 16:27JochenNote Added: 0003027
2016-01-26 09:09signolesNote Added: 0006122
2016-01-26 17:02corrensonNote Added: 0006137
2016-06-13 16:35JochenNote Added: 0006192
2016-06-13 16:35JochenStatusfeedback => assigned
2016-06-13 16:43corrensonNote Added: 0006193
2016-06-13 16:43corrensonStatusassigned => resolved
2016-06-13 16:43corrensonResolutionreopened => fixed
2016-06-21 14:08signolesFixed in Version => Frama-C Aluminium
2016-06-21 14:08signolesStatusresolved => closed

2012-05-11 09:36   
Unfortunately, const is merely an indication than a strict requirement. For instance, gcc will let the following pass without a warning: void ftest(int a) { int * pc = (int *)&c1; *pc = 2; }. Thus, we cannot simply add new hypotheses, some validation must also be done. It might be worth considering a kernel option that would treat global const as really constant values, e.g. by generating a global invariant (provided that WP handles them, which it does not at this time).
2012-05-11 12:36   
If you add the option "-main ftest" to frama-c's command line, your property is proved by WP. This option tells the WP that ftest is the entry point of your program and thus that globals still contain their initial values.
2012-05-11 12:41   
Semantics of C is sadly very weak on this point. Option -main is probably enough. Feel free to reopen if you do not agree.
2012-05-11 14:33   
While using -main can be seen as a workaround, I don't think that it can be called a proper fix, because 1) you have to relaunch Frama-C with a new -main for every function you want to prove, and 2) this allows to have as an hypothesis that const have their initial values, but does not check that this assumption holds, even though it can easily be circumvented by some code that does not trigger the slightest warning with gcc. Point 1 can be mitigated by an appropriate script, but point 2 makes Frama-C unsafe.
2012-05-11 18:30   
About 1 : you can do this in the GUI. About 2 : using -main f does not make Frama-C unsound. It guarantees to Frama-C that function f is called in a state equivalent to the one of the entry point of the program. This assumption has to be checked externally as much as any assumption made by other global option of Frama-C.
2012-05-12 14:59   
I verified that disjointness is proven with "-main" for ftest.c (Note 3007). However, for the slightly extended version ftest2.c, it is not. Concerning the option suggested in Note 3006, if I may utter a wish, I'd like Frama-C to check strict handling of "const", that is, reporting an invalid initialization for the given example "void ftest(int a) { int * pc = (int *)&c1; *pc = 2; }". Gcc does this if the cast is omitted; so I believe analyzing proper use of "const" is no principal problem.
2012-05-12 22:09   
> Preferring C constants to macros is considered good software engineering practice; I believe that the choice between const variables and macros in C is a little more subtle than "one is good and the other is bad". A more nuanced comparison can be found below, if one reads all the answers, not just the accepted one (that answer is listed first by choice of a single person, the one who asked the question. The questions below are ordered by votes, and do benefit from the wisdom of the crowds). I would add to the points raised there that defining a non-static const variable FORCES the compiler to allocate a memory location containing that value, even if the compiler was able to inline the constant throughout the generated code. > if I may utter a wish, I'd like Frama-C to check strict handling of "const", > that is, reporting an invalid initialization for the given example > "void ftest(int a) { int * pc = (int *)&c1; *pc = 2; }". > Gcc does this if the cast is omitted; so I believe analyzing proper use of "const" > is no principal problem. If you are asking for a syntactic check of the same nature as GCC's neither-sound-nor-complete helpful warning, but that would warn *also* with the cast to (int*) present, it would be possible to do, and we could do this for you on the understanding that this is a custom development that we will never be able to amortize over other users. Such a check would flag all realistic C programs of moderate size. It would be enough for a program to at some point use memcpy() to copy pointers to be flagged as possibly misusing the const attribute. In fact, any casting between pointer-to-object and pointer-to-incomplete-type would probably have to be flagged. These happen more frequently than you might expect. The check would also in all likelihood flag the very program you are trying to verify as possibly misusing the const attribute. The proper way would be a semantic check that does not reduce the good usage of "const" to simple typing rules. But then it is very much a request for a entire new feature.
2012-05-15 19:42   
If you are willing to use a mixed Value/WP approach, it is possible to write some simple plugins that performs the following checks: (1) check that a (global or local) variable is never written (2) check that a const subpart of a variable, typically a const field is never written (Of course (2) implies (1)) Plugin (1) can be written in approximately 30 lines, using the results of the Out analysis of the Inout plugin. Plugin (2) would be slightly bigger, as it requires checking all the offsets of a variable separately. Still, I would say it can be written in less than 150 lines. If you are interested in this approach, I can offer some hints on which functions you should use. I would also review your code, provided you agree that we integrate it into Frama-C.
2012-05-21 16:27   
Dear Boris Yakobowski, I would like to try to write at least plugin (1) as sketched in your Note 3014, and I appreciate your offer of help very much. I'll have the necessary time when the University semester is over, i.e. about mid of July. If you send me your e-mail address to jochen(at), I'll contact you then again without bothering other users of this BTS with detailled questions about implementation issues. Best Regards, Jochen Burghardt
2016-01-26 09:09   
Dear Jochen, Is it possible to close this issue or do you need additional time to check some details? Best regards, Julien Signoles
2016-01-26 17:02   
Just to mention it, WP has a new option (-wp-init-const), making global const variables to be assigned their initialization value in the pre-state of each function. Unfortunately, this option is not (yet) taken into account when proving disjoint and complete behaviors clauses.
2016-06-13 16:35   
From my point of view, this issue can be closed. (Sorry for the delayed answer to Julien's note 6122, I didn't work with this BTS for a long time.)
2016-06-13 16:43   
Solved by -lib-entry, -main and -wp-init-const