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] Pbs avec WP appelant Why3 sous Cygwin

Bonjour Dillon,
Merci pour le retour !

Concernant les diff?rents points : 
1) Je laisse cette question aux d?veloppeurs de Why3 ;-)
2) Effectivement, il y a un soucis.
Tout d'abord, sous Windows, on ne sais pas facilement tuer l'arborescence des processus.
Peut-?tre qu'il faut tout simplement ne pas mettre de timeout sur le processus Why-3 et se contenter de lui passer le timeout voulu.
Je vais tenter de corriger ?a...

	L.

Le 14 mai 2013 ? 13:35, Pariente Dillon a ?crit :

> Bonjour,
>  
> 2 soucis ? signaler sur Fluorine.
>  
> 1?) Cygpath
> Il semble bien que WP appelant des prouveurs via Why3 ne fonctionne pas dans l?environnement Cygwin.
> A 1?re vue, ce n?est pas WP qui est en cause, sauf erreur (de configuration) de ma part, mais plut?t Why3 qui ne traite pas bien les noms de fichiers ? ? la Windows ?.
> Pour que ?a fonctionne, il faut que tout chemin+nom de fichier soit au format ? cygpath ?m ?.
> Voici pour info les endroits dans Why3 o? ?a ? coin?ait ? :
> ./src/driver/driver.ml let load_file file = ? (* => cygpath -m file *)
> ./src/driver/driver.ml let input_lexer filename = ? (* => cygpath -m filename *)
> ./src/driver/driver.ml    | s   -> raise (UnknownSpec s) in let file = ? (* => cygpath -m file *)
> ./src/ide/gconfig.ml let init () = ? load_icon_names (); ? (* pb lors du chargement des ic?nes : cette partie du code a ?t? mise en commentaire *)
> ./src/ide/gmain.ml let load_path = Filename.concat (datadir main) "lang" in (* => cygpath ?m load_path *)
> ./src/util/rc.mll let from_file f = ? (* => cygpath -m f *)
>  
> Ce n?est pas la bonne liste, mais je sais que pas mal ? d?oreilles de Why3 ? sont ? l??coute de cette liste (priv?e) !
> Et puis comme ?a les mainteneurs de Frama-C seront au courant ? ;-)
> (Au passage, quand on essaie de lancer WP/Why3/Vampire, on obtient une erreur comme quoi tptp-fof n?a pas ?t? trouv? ? une id?e ?)
>  
> 2?) Timeout
> Autre souci, probablement plus propre ? WP :
> Quand on fixe un timeout, mettons de 60s dans WP, apr?s le lancement de WP via la GUI sur une annotation donn?e, ce timeout prend en compte le temps pass? par Why3 ? faire ses calculs avant de faire appel ? un prouveur.
> Par exemple, si Why3 a pass? 40s ? calculer, au bout de 20s seulement de prouveur, Frama-C-gui/WP reprend la main (normal !), avec le r?sultat qui est celui obtenu au bout de 20s de traitement du prouveur (donc Unknown) !
> Mais le probl?me c?est que ce m?me prouveur continue de s?ex?cuter pendant 40s sur la m?me PO (ce qui sous-entend que le passage du timeout de 60s de Frama-C/WP vers Why3 se fait bien).
>  
> Peut-on envisager que WP tue toute l?arborescence de processus cr??s par Why3 ? la fin du time-out ?
> Ou alors ? peut-?tre plus simple ! ? que Why3 s?en charge lorsqu?il re?oit le signal Kill qui va bien ?
>  
> Bien cordialement,
> D.
>  
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr
> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20130521/6aaa8cb4/attachment.html>