--- layout: fc_discuss_archives title: Message 29 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



On mac os it reads "why-config" not "why_config".

Jens

-----Urspr?ngliche Nachricht-----


> 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

_______________________________________________
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 --------------
A non-text attachment was scrubbed...
Name: not available
Type: application/ms-tnef
Size: 3779 bytes
Desc: not available
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20100919/0f02503c/attachment.bin>