--- layout: fc_discuss_archives title: Message 1 from Frama-C-discuss on December 2019 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] WP and unsigned int



> 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.