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: Hans-Werner.Wiesbrock at itpower.de (Hans-Werner Wiesbrock)
- Date: Thu, 16 Sep 2010 12:36:30 +0200
- References: <20100916080145.210250@gmx.net><5EFD4D7AC6265F4D9D3A849CEA9219190F5030@LAXA.intra.cea.fr> <1735D919BCD0FC42B73E548E65AB8CC0233399@SERVER.ITPower.local> <EFF6534C8F2FC940A9D7929433E12D4E216EFE@TITAN.first.fraunhofer.de>
Thanks for the pointers, I tried them but got: Why -config -> Cannot find prelude file 'C:\Programme\Theorem\Prover\Frama-C\lib\why' \why\prelude.why (WHYLIB is set to 'C:\Programme\Theorem\Prover\Frama-C\lib\why') When executing afterwards: frama-c -jessie -jessie-atp simplify swap1.c the former error still is thrown. I changed the environment variable WHYLIB = 'C:\Programme\Theorem\Prover\Frama-C\lib\why' and dropped the "'". But then I get for why -config: Fatal error:exception Sys_error("config: No such fileor directory") 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. Best regards HWW -----Urspr?ngliche Nachricht----- Von: frama-c-discuss-bounces at lists.gforge.inria.fr [mailto:frama-c-discuss-bounces at lists.gforge.inria.fr] Im Auftrag von Jens Gerlach Gesendet: Donnerstag, 16. September 2010 11:38 An: Frama-C public discussion Betreff: AW: [Frama-c-discuss] Problems with Window Installation of Frama-C Hi, I am not sure whether this solves your issue under Windows, but under Mac OS X it is recommended that one calls "why-config" before frama-c is called the first time. Regards Jens Gerlach -----Urspr?ngliche Nachricht----- Von: frama-c-discuss-bounces at lists.gforge.inria.fr im Auftrag von Hans-Werner Wiesbrock Gesendet: Do 9/16/2010 11:16 An: Frama-C public discussion Betreff: [Frama-c-discuss] Problems with Window Installation of Frama-C Hi, I'm a freshman in Frama-C and tried to install Frama-C (Boron-20100401) under Windows XP. I further installed cygwin and MinGW 5.1.6 for gcc et.al. But when I want to execute: frama-c -jessie -jessie-atp simplify swap1.c where swap1.c is a simple example: /*@ requires \valid(p); requires \valid(q); assigns *p; assigns *q; ensures *p == \old(*q); ensures *q == \old(*p); */ void swap(int* p, int* q) { int const save = *p; *p = *q; *q = save; } I get: (under cygwin) [kernel] preprocessing with "gcc -C -E -I. -dD swap1.c" [jessie] Starting Jessie translation [jessie] Producing Jessie files in subdir swap1.jessie [jessie] File swap1.jessie/swap1.jc written. [jessie] File swap1.jessie/swap1.cloc written. [jessie] Calling Jessie tool in subdir swap1.jessie Generating Why function swap [jessie] Calling VCs generator. why -simplify [...] why/swap1.why Anomaly: Sys_error<"C:\\Programme\\TheoremProver\\Frama-C\\lib\\whywhyjessie.why: No such file... (under dos) ... why -simplify [...] why/swap1.why Der Befehl "WHYLIB" ist entweder falsch geschrieben oder konnte nicht gefunden werden. What did I make wrong and should do instead? Thank you in advance HWW _______________________________________________ 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
- Follow-Ups:
- [Frama-c-discuss] Problems with Window Installation of Frama-C
- From: virgile.prevosto at cea.fr (Virgile Prevosto)
- [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] RE : RE : problems with plugin-integration
- Prev by Date: [Frama-c-discuss] RE : Problems with Window Installation of Frama-C
- Next by Date: [Frama-c-discuss] GUI - Opening a file (Windows XP)
- 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):