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 11:16:49 +0200
- References: <20100916080145.210250@gmx.net> <5EFD4D7AC6265F4D9D3A849CEA9219190F5030@LAXA.intra.cea.fr>
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
- Follow-Ups:
- [Frama-c-discuss] Problems with Window Installation of Frama-C
- From: jens.gerlach at first.fraunhofer.de (Jens Gerlach)
- [Frama-c-discuss] RE : Problems with Window Installation of Frama-C
- From: virgile.prevosto at cea.fr (PREVOSTO Virgile)
- [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] RE : RE : problems with plugin-integration
- Prev by Date: [Frama-c-discuss] RE : RE : problems with plugin-integration
- Next by Date: [Frama-c-discuss] Problems with Window Installation of Frama-C
- Previous by thread: [Frama-c-discuss] RE : RE : problems with plugin-integration
- Next by thread: [Frama-c-discuss] Problems with Window Installation of Frama-C
- Index(es):