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



Yes. It does with 777 permission
On Sep 19, 2014 5:38 AM, "Lo?c Correnson" <loic.correnson at cea.fr> wrote:

> 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
>
>
>
> _______________________________________________
> 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/ad207da7/attachment.html>