Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0001179Frama-CPlug-in > wppublic2012-05-10 18:072016-06-21 14:08
ReporterJochen 
Assigned Tocorrenson 
PrioritynormalSeveritytweakReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
Product VersionFrama-C Nitrogen-20111001 
Target VersionFixed in VersionFrama-C Aluminium 
Summary0001179: Suggest to supply values of global consts to provers
DescriptionWp/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.
TagsNo tags attached.
Attached Filesc file icon ftest.c [^] (166 bytes) 2012-05-10 18:07 [Show Content]
c file icon ftest2.c [^] (202 bytes) 2012-05-12 14:51 [Show Content]

- Relationships

-  Notes
(0003006)
virgile (developer)
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).
(0003007)
monate (reporter)
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.
(0003008)
monate (reporter)
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.
(0003009)
virgile (developer)
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.
(0003011)
monate (reporter)
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.
(0003012)
Jochen (reporter)
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.
(0003013)
pascal (reporter)
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).

http://stackoverflow.com/questions/1674032/static-const-vs-define-in-c [^]

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.
(0003014)
yakobowski (manager)
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.
(0003027)
Jochen (reporter)
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)first.fhg.de, I'll contact you then again without bothering other users of this BTS with detailled questions about implementation issues.
Best Regards,
Jochen Burghardt
(0006122)
signoles (manager)
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
(0006137)
correnson (manager)
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.
(0006192)
Jochen (reporter)
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.)
(0006193)
correnson (manager)
2016-06-13 16:43

Solved by -lib-entry, -main and -wp-init-const

- Issue History
Date Modified Username Field Change
2012-05-10 18:07 Jochen New Issue
2012-05-10 18:07 Jochen Status new => assigned
2012-05-10 18:07 Jochen Assigned To => correnson
2012-05-10 18:07 Jochen File Added: ftest.c
2012-05-11 09:36 virgile Note Added: 0003006
2012-05-11 12:36 monate Note Added: 0003007
2012-05-11 12:41 monate Note Added: 0003008
2012-05-11 12:41 monate Status assigned => resolved
2012-05-11 12:41 monate Resolution open => no change required
2012-05-11 14:33 virgile Note Added: 0003009
2012-05-11 14:33 virgile Status resolved => feedback
2012-05-11 14:33 virgile Resolution no change required => reopened
2012-05-11 18:30 monate Note Added: 0003011
2012-05-12 14:51 Jochen File Added: ftest2.c
2012-05-12 14:59 Jochen Note Added: 0003012
2012-05-12 22:09 pascal Note Added: 0003013
2012-05-15 19:42 yakobowski Note Added: 0003014
2012-05-21 16:27 Jochen Note Added: 0003027
2016-01-26 09:09 signoles Note Added: 0006122
2016-01-26 17:02 correnson Note Added: 0006137
2016-06-13 16:35 Jochen Note Added: 0006192
2016-06-13 16:35 Jochen Status feedback => assigned
2016-06-13 16:43 correnson Note Added: 0006193
2016-06-13 16:43 correnson Status assigned => resolved
2016-06-13 16:43 correnson Resolution reopened => fixed
2016-06-21 14:08 signoles Fixed in Version => Frama-C Aluminium
2016-06-21 14:08 signoles Status resolved => closed


Copyright © 2000 - 2018 MantisBT Team
Powered by Mantis Bugtracker