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] WP and unsigned int

  • Subject: [Frama-c-discuss] WP and unsigned int
  • From: loic.correnson at cea.fr (Loïc Correnson)
  • Date: Mon, 2 Dec 2019 09:14:18 +0100
  • In-reply-to: <CAED32A4-F5B6-4773-9ED0-B911CEA56442@galois.com>
  • References: <C754AA97-3290-4B27-A225-4F8529A5BDA6@galois.com> <CA+yPOVhe_QND0H6gsrOzcYi_EVTJr93JubMXgz8TmcDfUs+Fjw@mail.gmail.com> <BEFC6C6A-C272-4379-AD89-02EF7DDD85BE@galois.com> <D61E515D-5424-4777-9CE4-65AF9A795408@cea.fr> <40602C9E-A206-497E-998F-7586F6A8FF33@galois.com> <CAED32A4-F5B6-4773-9ED0-B911CEA56442@galois.com>
> I’m wondering what the recommended way is to maintain a session using version control. I don’t expect multiple developers to be working on the proof concurrently (and hence am not concerned about merges) — rather, there is one developer working on the proof and the rest may wish to replay it. Is it necessary or recommended to distribute the entire session directory with the program source in order to reproduce the proof? Or do I just need <session-dir>/script, for example?

The entire session dir shall be put under version control.
It contains :
 - portable cache for provers
 - script saved from TIP or -wp-auto strategies

Read carefully the documentation on cache modes ; all developers shall use « update » or « replay » modes on a day-to-day basis.
Sometimes, it is recommend to re-run proofs with cache mode « cleanup » to remove useless cache entries, but this might cause merge deletion/update conflicts.

For distribution, you may distribute session/cache or not.
If you distribute it but extern people are sceptical and don’t trust your results, they can re-run the proofs with env. variable « FRAMAC_WP_CACHE=rebuild »

	L.