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

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>