--- layout: fc_discuss_archives title: Message 27 from Frama-C-discuss on September 2014 ---
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>