Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[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