Sessions and WP do not interact properly
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 !!!!
-
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
-
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.
-
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