--- layout: fc_discuss_archives title: Message 26 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



This is a windows/cygwin question indeed. Did you check the /tmp directory actually exists from your terminal ?
	L.

Le 18 sept. 2014 ? 20:36, Ido Efrati <ido.p.efrati at gmail.com> a ?crit :

> 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
> 
> _______________________________________________
> 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 --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20140919/f1aaaaff/attachment.html>