--- layout: fc_discuss_archives title: Message 15 from Frama-C-discuss on September 2010 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Problems with Window Installation of Frama-C



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