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

[Frama-c-discuss] Question regarding the default out path on windows



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>