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] Question regarding the default out path on windows

  • Subject: [Frama-c-discuss] Question regarding the default out path on windows
  • From: ido.p.efrati at gmail.com (Ido Efrati)
  • Date: Thu, 18 Sep 2014 14:36:16 -0400
Dear frama-c discuss,

I am writing regarding a problem that I am having with frama-c on a windows
machine with cygwin terminal. I will try to give as many details as
possible, but the fundamental question is if it is possible to change the
default location frama-c stores file for provers like alt-ergo?

I am using a windows 7 machine and performed all of my installations
through cygwin through which I installed:
1) Frama-C Neon with the following command :
   ./configure & make & make-install.
$ which frama-c
/usr/bin/frama-c

2) why3 (Why3 platform, version 0.85 (build date: Wed Sep 17 14:09:48 EDT
2014)):
   ./configure
   make
   make install
$which why3
/usr/bin/why3

3) alt-ergo (0.95.2) as an exe file (Win32 (MinGW) binary:
alt-ergo-0.95.2-mingw.exe) from http://alt-ergo.ocamlpro.com/download.php
and just put it with execution permissions in /usr/bin
$ which alt-ergo
  /usr/bin/alt-ergo

I used the swap code from the frama-c tutorial http://frama-c.com/wp.html
and via cygwin I ran the following command:
frama-c -wp -wp-rte -wp-proof alt-ergo swap.c

the Qed part was proved, but the alt-ergo validation triggered the
following errors:

Fatal error: exception
Sys_error("/tmp/wp54f5c5.dir/typed/swap_assert_rte_mem_access_3_Alt-Ergo.mlw:
No such file or directory")
Fatal error: exception
Sys_error("/tmp/wp54f5c5.dir/typed/swap_assign_part2_Alt-Ergo.mlw: No such
file or directory")
Fatal error: exception
Sys_error("/tmp/wp54f5c5.dir/typed/swap_assign_part3_Alt-Ergo.mlw: No such
file or directory")
[wp] [Alt-Ergo] Goal typed_swap_assign_part2 : Failed
     Error: Alt-Ergo exits with status [2]
[wp] [Alt-Ergo] Goal typed_swap_assign_part3 : Failed
     Error: Alt-Ergo exits with status [2]
[wp] Proved goals:    4 / 9
     Qed:             4
     Alt-Ergo:        0  (failed: 5)

>From what I was able to infer frama-c was trying to write (did not actually
write) to tmp (which is a cygwin path), but alt-ergo was looking for a
windows path. Thus, when it could not find the directory it resulted in a
fatal error.

Therefore, I tried to specify the out path with -wp-out <dir>, that sets
working directory for generated file. I specified a windows path for my
wp-out
frama-c -wp -wp-rte -wp-proof alt-ergo -wp-out c:/Users/user/Desktop/tmp2
../../cygdrive/c/Users/user/Desktop/swap.c

This solved the problem, and all goals were proved
[wp] [Qed] Goal typed_swap_post_B : Valid
[wp] [Qed] Goal typed_swap_assert_rte_mem_access_2 : Valid
[wp] [Qed] Goal typed_swap_assert_rte_mem_access_4 : Valid
[wp] [Qed] Goal typed_swap_assign_part1 : Valid
[wp] [Alt-Ergo] Goal typed_swap_assert_rte_mem_access : Valid (17)
[wp] [Alt-Ergo] Goal typed_swap_post_A : Valid (15)
[wp] [Alt-Ergo] Goal typed_swap_assert_rte_mem_access_3 : Valid (16ms) (17)
[wp] [Alt-Ergo] Goal typed_swap_assign_part2 : Valid (31ms) (22)
[wp] [Alt-Ergo] Goal typed_swap_assign_part3 : Valid (16ms) (22)
[wp] Proved goals:    9 / 9
     Qed:             4
     Alt-Ergo:        5  (16ms-31ms) (22)

I am trying to figure out if:
a) Did I install something incorrectly, i.e., could I configured the
default tmp path during the installation?
b) If I installed everything correctly, is there a way to configure the
default tmp path? (my fundamental question above)

Sincerely,
Ido
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20140918/0bfdb0b5/attachment.html>