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