--- layout: fc_discuss_archives title: Message 52 from Frama-C-discuss on February 2011 ---
Le jeu. 17 f?vr. 2011 17:19:33 CET, Boris Hollas <hollas at informatik.htw-dresden.de> a ?crit : > > Yes, you're right, some manual intervention is necessary. Is this what > you mean with "to transform the spec into a statement > contract at the call point"? Well, this is not a manual intervention. The transformation I'm referring to is simply the substitution of formals by actual parameters and of \result by the lval were the returned value is stored. If you stick to a contract statement at the call point, this is all you need to do. > However, my code doesn't have loops, so most steps are quite easy. > Well, as soon as you have pointers, assignments themselves become an issue, as you have to take potential aliases into account. Things become messy very quickly. > I've done some experiments with the WP and RTE plugins, but so far I > can't verify code that verifies with Jessie. > > What are the differences between what the RTE plugin does for WP and > what the apron library does for Jessie? Both are completely orthogonal. Apron library is (was? I'm not sure of the current status of this part of Why) used to generate invariants (especially the "trivial" ones such as 0<=i<=n for the index, that are very boring to write but essential to complete proofs). RTE generates what appears in Jessie/Why as Safety proof obligations. But while this is handled internally by the jessie program (and thus completely opaque from a frama-c point of view), RTE just generates plain ACSL annotations, which means that WP is not the only plugin that can be used to verify these POs: they are registered in Frama-C's kernel like all annotations, and the user is free to use whatever combination of plugins s/he wants to ensure that they hold. -- E tutto per oggi, a la prossima volta. Virgile