--- layout: fc_discuss_archives title: Message 3 from Frama-C-discuss on April 2020 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] WP: verifying a particular proof obligation



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>