--- layout: fc_discuss_archives title: Message 4 from Frama-C-discuss on April 2020 ---
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