--- layout: fc_discuss_archives title: Message 2 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,

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  ?

Regards

Jens