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: jens.gerlach at first.fraunhofer.de (Jens Gerlach)
  • Date: Thu, 16 Sep 2010 11:38:02 +0200
  • References: <20100916080145.210250@gmx.net><5EFD4D7AC6265F4D9D3A849CEA9219190F5030@LAXA.intra.cea.fr> <1735D919BCD0FC42B73E548E65AB8CC0233399@SERVER.ITPower.local>
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

-------------- next part --------------
A non-text attachment was scrubbed...
Name: not available
Type: application/ms-tnef
Size: 3947 bytes
Desc: not available
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20100916/f2482da9/attachment.bin>