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

[Frama-c-discuss] Caching/Session Behavior



Hi,
Actually, there is a difference when issuing a proof on a single property rather than on all properties of a given function.
However, there shall be _no_ difference when working with one or several functions, since each function is treated separately. Could you minimize the problem and share your test cases?
Thanks!
L.

________________________________________
De : Frama-c-discuss [frama-c-discuss-bounces at lists.gforge.inria.fr] de la part de Alexander Bakst [abakst at galois.com]
Envoyé : mardi 17 mars 2020 23:33
À : Frama-C public discussion
Objet : [Frama-c-discuss] Caching/Session Behavior

Hi all,

I hope this finds everyone in good health.

I’m not sure I understand the caching/session behavior of frama-c/wp. I have a file with many functions `f,g,h` and so on. I’ve produced a proof using TIP/provers that appears to play back successfully from the cache when I run `frama-c -wp … -wp-fct f`. However, one of the postconditions of the proof _fails_ when I use the invocation `frama-c -wp … -wp-fct f,g,h,…`.

Is this behavior expected, or is there something I can do so that the verification of `f` succeeds with the latter command without rebuilding the proof?

Thanks,
Alexander
_______________________________________________
Frama-c-discuss mailing list
Frama-c-discuss at lists.gforge.inria.fr
https://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss