GitLab

ID0002044: This issue was created automatically from Mantis Issue 2044. Further discussion may take place here.

---

Id	Project	Category	View	Due Date	Updated
ID0002044	Frama-C	Plug-in > wp	public	2015-01-06	2015-06-29

Reporter	ploc	Assigned To	correnson	Resolution	no change required
Priority	normal	Severity	minor	Reproducibility	always
Platform	-	OS	-	OS Version	-
Product Version	Frama-C GIT, precise the release id	Target Version	-	Fixed in Version	-

Description :

Bonjour, quelques problèmes avec le -save et le -load des sessions conjugés avec WP/Why3 et l'option no-let !!!!

1. Si on utilise pas -wp-out les fichiers temporaires de wp sont supprimés et lors du prochain appel de frama-c avec le -load, il se plaint de l'absence des fichiers

2. Si on specifie -wp-out, avec le -load, Frama-C retrouve les fichiers générés mais il ne semble pas retrouver tout ce dont il a besoin.

3. Enfin lors de l'utilisation de coq comme prover lors d'un run (avec -load et -save), au prochain appel avec toujours -load et -save, frama-c appelle systématiquement coq, y compris si on specifie -wp-prover altergo par exemple.

Steps To Reproduce :

Pour les points 1 et 2:

Par exemple, pour le fichier C suivant:

$ cat essai.c struct greycounter_mem {_Bool _first; };

/*@ requires \valid(self); @ ensures ((*self)._first ==1); @ assigns self;/ void greycounter_reset (struct greycounter_mem *self) { self->_first = 1;; return; }

Le script suivant active les différents problemes:

#!bin/bash src=essai.c

Error 1: temporary wp folder with no-let option and why3 solver (eg. altergo or CVC4)

frama-c -save session -wp-prop "@ensures" -wp-prover why3:altergo -wp-no-let $src frama-c -load session -save session -wp-prop "@assigns" $src

Error 2: no-let with why3:cvc4

frama-c -save session -wp-prop "@ensures" -wp-prover CVC4 $src -wp-no-let -wp-out wp frama-c -load session -save session -wp-prop "@assigns" $src

Here it works

frama-c -save session -wp-prop "@ensures" -wp-prover CVC4 $src -wp-out wp frama-c -load session -save session -wp-prop "@assigns" $src