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

Unfortunately , it not possible to do exactly what you what but, you can 
combine the use of one of the property label (here "unchanged" - notices 
that a property may has several labels) and the property categories you 
do not want (you have to list them - see the help given for -wp-prop to 
get the allowed category names).

So, -wp-prop=unchanged,- at invariant,- at assert
allow you to prove all properties having the label "unchanged" except 
invariants (that includes loop invariants) and assertions.

That is almost that you wanted !

Kind regards,
Patrick

Le 21/04/2020 à 09:58, Gerlach, Jens 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  ?
>
> Regards
>
> Jens
>
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr
> https://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss


-- 
Patrick Baudin, DILS/LSL, Bât. 862,
Point Courrier n° 174
Institut CARNOT CEA LIST,
CEA Saclay Nano-INNOV,
91191 Gif-sur-Yvette cedex, France.
tel: +33 (0)1 6908 2072