Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0002285Frama-CPlug-in > wppublic2017-02-27 13:592017-10-09 17:30
ReporterJochen 
Assigned Tocorrenson 
PrioritylowSeverityfeatureReproducibilityalways
StatusassignedResolutionopen 
PlatformSilicon-20161101OSxubuntuOS Version
Product VersionFrama-C 14 Silicon 
Target VersionFixed in Version 
Summary0002285: suggest boolean expressions for "-wp-prop" arguments
DescriptionCurrently, 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.
Additional InformationComplex 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.
TagsNo tags attached.
Attached Filesc file icon proptest.c [^] (934 bytes) 2017-02-27 13:59 [Show Content]
c file icon bbb.c [^] (103 bytes) 2017-10-09 17:25 [Show Content]

- Relationships

-  Notes
(0006466)
Jochen (reporter)
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".

- Issue History
Date Modified Username Field Change
2017-02-27 13:59 Jochen New Issue
2017-02-27 13:59 Jochen Status new => assigned
2017-02-27 13:59 Jochen Assigned To => correnson
2017-02-27 13:59 Jochen File Added: proptest.c
2017-10-09 17:25 Jochen File Added: bbb.c
2017-10-09 17:30 Jochen Note Added: 0006466


Copyright © 2000 - 2017 MantisBT Team
Powered by Mantis Bugtracker