Frama-C Bug Tracking System - Frama-C
View Issue Details
0002285Frama-CPlug-in > wppublic2017-02-27 13:592019-10-17 18:03
closedwon't fix 
Frama-C 14-Silicon 
0002285: suggest boolean expressions for "-wp-prop" arguments
Currently, the semantics of "-wp-prop" arguments is unexplained and difficult to understand, when negation and more than one label is used. For example, using the attached file, "-wp=prop=A,B,-C" selects l4,l5,l6, whereas "-wp-prop=-C,B,A" selects all but l3, and so does "-wp-prop=A,B,c" (although the set of "C"-labelled lemmas is the complement of that of the "c"-labelled lemmas). I think, parsing arbitrary boolean expressions (built from "!", "&&", "||") isn't more difficult that the current mechanism, but is easier to describe in the manual and to understand. Alternatively, "-" could be kept as negation, "," could be used for cunjunction only, and the results of multiple args "-wp-prop=X -wp-prop=Y" could be or-ed together; this would at least allow to express arbitrary sets in disjunctive normal form.
Complex set expressions arise when labels are used during proof development to attach prover names (and even options) to properties. Using calls like "frama-c -wp -wp-prop=PROVE_WITH_CVC4 -wp-prover=cvc4 ..." can save a lot of proving time that is normally wasted by unsuccessful attempts by unsuitable provers. Other labels that can save time are "TODO", "NEEDS_LONG_TIMEOUT", etc. This way, boolean expressions arise in a natural way; and the user needs to be sure about their semantics, in order not to overlook proof obligations due to splitting by prover.
No tags attached.
c proptest.c (934) 2017-02-27 13:59
c bbb.c (103) 2017-10-09 17:25
Issue History
2017-02-27 13:59JochenNew Issue
2017-02-27 13:59JochenStatusnew => assigned
2017-02-27 13:59JochenAssigned To => correnson
2017-02-27 13:59JochenFile Added: proptest.c
2017-10-09 17:25JochenFile Added: bbb.c
2017-10-09 17:30JochenNote Added: 0006466
2019-10-17 17:34corrensonNote Added: 0006911
2019-10-17 17:35corrensonNote Added: 0006912
2019-10-17 17:35corrensonStatusassigned => resolved
2019-10-17 17:35corrensonResolutionopen => won't fix
2019-10-17 18:03signolesStatusresolved => closed

2017-10-09 17:30   
Similarly to the above, the effect of different command-line options "-wp-prop=..." depends on their order, too. For an easy-to-understand example, the new file "bbb.c" can be used. Running "frama-c -wp -wp-prop=-b -wp-prop=a bbb.c" schedules "c" and "a" for proof, while running "frama-c -wp -wp-prop=a -wp-prop=-b bbb.c" just schedules "a".
2019-10-17 17:34   
Actually, -wp-prop management was a nightmare. It has been recently improved.
2019-10-17 17:35   
We will not implement a boolean-based expression for wp-prop.