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