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

  • Subject: [Frama-c-discuss] Caching/Session Behavior
  • From: abakst at galois.com (Alexander Bakst)
  • Date: Tue, 17 Mar 2020 15:33:49 -0700
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