--- layout: fc_discuss_archives title: Message 3 from Frama-C-discuss on April 2020 ---
Hello Jens, Le mar. 21 avr. 2020 à 09:58, Gerlach, Jens < jens.gerlach at fokus.fraunhofer.de> a écrit : > Hello, > > The option -wp-prop allows to prove properties (annotations) with a > particular name, say â-wp-prop=unchangedâ . > However, I often have several post conditions, loop invariant and > assertion with the name âunchangedâ and > I am not always interested to verify all of them but only a specific > generated proof obligations. > > My question is if there is an option to verify a particular proof > obligation by supplying its âinternalâ names such as > typed_external_push_heap_ensures_unchanged ? > > As far as I know, this is not readily available. However, you might be able to combine several `-wp-prop`, `-wp-fct`, `-wp-bhv` and/or `-wp-skip-fct` to further restrict the selection of properties. Using the small program below: /*@ requires \valid(x); ensures unchanged: *x == 0; assigns *x; */ void reset(int* x) { *x = 0; //@ assert unchanged:skip: *x == 0; } void set(int* x) { *x = 1; //@ assert unchanged: *x == 1; } Each of the following command will select exactly one ACSL annotation: # all unchanged in set frama-c -wp-fct set -wp-prop unchanged test.c # all unchanged in reset that are not ensures frama-c -wp-fct reset -wp-prop unchanged -wp-prop=- at ensures test.c #all unchanged in f that are not skip frama-c -wp-fct reset -wp-prop unchanged,-skip test.c the @ensures in the second example is a wp-prop category. The full list can be found in the output of -wp-help. Hope this helps, -- E tutto per oggi, a la prossima volta Virgile -------------- section suivante -------------- Une pièce jointe HTML a été nettoyée... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20200421/cef3779f/attachment.html>