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
- Subject: [Frama-c-discuss] Problems with Window Installation of Frama-C
- From: virgile.prevosto at cea.fr (Virgile Prevosto)
- Date: Fri, 17 Sep 2010 11:49:46 +0200
- In-reply-to: <1735D919BCD0FC42B73E548E65AB8CC02333AC@SERVER.ITPower.local>
- References: <20100916080145.210250@gmx.net> <5EFD4D7AC6265F4D9D3A849CEA9219190F5030@LAXA.intra.cea.fr> <1735D919BCD0FC42B73E548E65AB8CC0233399@SERVER.ITPower.local> <EFF6534C8F2FC940A9D7929433E12D4E216EFE@TITAN.first.fraunhofer.de> <1735D919BCD0FC42B73E548E65AB8CC02333AC@SERVER.ITPower.local>
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
- Follow-Ups:
- [Frama-c-discuss] Problems with Window Installation of Frama-C
- From: jens.gerlach at first.fraunhofer.de (Jens Gerlach)
- [Frama-c-discuss] Problems with Window Installation of Frama-C
- References:
- [Frama-c-discuss] RE : RE : problems with plugin-integration
- From: virgile.prevosto at cea.fr (PREVOSTO Virgile)
- [Frama-c-discuss] Problems with Window Installation of Frama-C
- From: Hans-Werner.Wiesbrock at itpower.de (Hans-Werner Wiesbrock)
- [Frama-c-discuss] Problems with Window Installation of Frama-C
- From: jens.gerlach at first.fraunhofer.de (Jens Gerlach)
- [Frama-c-discuss] Problems with Window Installation of Frama-C
- From: Hans-Werner.Wiesbrock at itpower.de (Hans-Werner Wiesbrock)
- [Frama-c-discuss] RE : RE : problems with plugin-integration
- Prev by Date: [Frama-c-discuss] Message-passing (concurrent) code verification
- Next by Date: [Frama-c-discuss] casting from float to ulong and vice versa
- Previous by thread: [Frama-c-discuss] Problems with Window Installation of Frama-C
- Next by thread: [Frama-c-discuss] Problems with Window Installation of Frama-C
- Index(es):