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] Problems with Window Installation of Frama-C

Hello,

Le jeu. 16 sept. 2010 12:36:30 CEST,
"Hans-Werner Wiesbrock" <Hans-Werner.Wiesbrock at itpower.de> a ?crit :

> Thanks for the pointers, I tried them but got:
> Why -config ->

It's not why -config, but why_config (this is a separate executable
from why itself).

> Then I changed the variable JESSIELIBFILES in swap1.jessie/swap1.makefile 
> $(WHYLIB)\\why\\jessie.why  -> $(WHYLIB)/why/jessie.why and tried why -simplify [...] why/swap1.why, I ran into the same error as before. 

I have been able to reproduce your issue by positioning explicitly
the variable JESSIELIBFILES on the command line of the cygwin shell:

JESSIELIBFILES=C:\\Frama-C\\lib\\why\\why\\jessie.why frama-c
-jessie -jessie-atp simplify file.c

When you use / instead, as in 
JESSIELIBFILES=C:/Frama-C/lib/why/why/jessie.why frama-c
-jessie -jessie-atp simplify file.c

then the proof obligations are generated (whether they are proved by
Simplify is another matter of course). Could you try that on your
setting? i.e.

JESSIELIBFILES=C:/Programme/TheoremProver/Frama-C/lib/why/why/jessie.why
frama-c -jessie -jessie-atp simplify swap1.c

Best regards,
-- 
Virgile Prevosto
Ing?nieur-Chercheur, CEA, LIST
Laboratoire de S?ret? des Logiciels
+33/0 1 69 08 82 98