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

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