--- layout: fc_discuss_archives title: Message 26 from Frama-C-discuss on September 2010 ---
[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