5

I installed frama-c Magnesium version using instruction provided here. I didn't get any error during installation and executing command frama-c -versionin Cygwin printed Frama-c version as: Magnesium-20151002. But when I executed -wp plugin on a very small example, for the goals which used alt-ergo, I get following errors:

1 [main] frama-c 8168 child_info_fork::abort: unable to map C:\cygwin\usr\local\lib\frama-c\plugins\Users.cmxs, Win32 error 998 1 [main] frama-c 7956 child_info_fork::abort: unable to map C:\cygwin\usr\local\lib\frama-c\plugins\Value.cmxs, Win32 error 998

0 [main] frama-c 300 child_info_fork::abort: unable to map C:\cygwin\usr\local\lib\frama-c\plugins\Value.cmxs, Win32 error 998 [wp] [Alt-Ergo] Goal typed_changeCase_assert_rte_signed_overflow_2 : Failed Error: Resource temporarily unavailable

Value plugin executes successfully. I searched the error and found this post. So I also executed rebaseall -v command, but that too didn't help. To confirm that my Cygwin is not corrupted I installed Frama-c Sodium version again and was able to execute WP plugin successfully.

Can anyone help me fix this issue, we want to be able to use Frama-c Magnesium version on Windows?

Edit: Machine details: I tried it on my computer and also on a VM. On VM, I executed commands ./configure && make and make install to install frama-c Magnesium.

I have 32 bit Cygwin on both machine. Both Windows are 64-bit.

  1. Ocaml version on my machine: 4.02.3, Ocaml version on VM: 4.01.0
  2. Cygwin version on my machine and on VM: CYGWIN_NT-6.1-WOW64 1.7.27(0.271/5/3) 2013-12-09 11:57 i686 Cygwin
Community
  • 1
  • 1
Gunjan Aggarwal
  • 710
  • 5
  • 19
  • Which version of alt-ergo did you try? I suppose you installed it using fdopen's OPAM MinGW repository? – anol Apr 26 '16 at 17:06
  • alt-ergo version is 1.01 and I used it with both Frama-c Sodium and Magnesium version. I followed instruction given here: https://bts.frama-c.com/dokuwiki/doku.php?id=mantis:frama-c:compiling_from_source , which I think is using fdopen's OPAM MinGW repository – Gunjan Aggarwal Apr 26 '16 at 17:13
  • I got a different error message using alt-ergo 1.01 (`Signal unavailable`), but using 0.99.1 I've been able to prove a few simple assertions. The [WP manual](http://frama-c.com/download/wp-manual-Magnesium-20151002.pdf) does mention that alt-ergo `0.99.1+` is compatible, but I'm not sure the "+" there means "any major version", or just "0.99.1", or "0.99.2", etc. I'm going to check it, but I'd recommend trying `opam install alt-ergo.0.99.1` and seeing if that helps. – anol Apr 26 '16 at 17:18
  • Your log is not visible in the comment, consider editing the question to add the version of alt-ergo (which seems relevant to your question) and then adding the log when you tried to downgrade it to 0.99.1. – anol Apr 26 '16 at 17:35
  • Sorry about that. I installed alt-ergo 0.99.1. But it doesn't help. I get the same error with alt-ergo version 0.99.1. I don't think that alt-ergo is even executing in my case as I used flag `-wp-alt-ergo-opt="dfkdkskl"` while executing `-wp` plugin, which is of-course not a valid option. I was hoping to get error message from alt-ergo, but I didn't. – Gunjan Aggarwal Apr 26 '16 at 17:46
  • Indeed, the error message does seem more related to dynamic linking than alt-ergo itself. I guess more details about your exact configuration would be necessary, since I cannot reproduce it otherwise: Windows version (also, if 32 or 64-bit), OCaml version, Cygwin version; also, are you using a virtual machine? Just wondering if memory/disk limitations could be an issue... – anol Apr 26 '16 at 18:33
  • I updated my question and added information about my configuration. I have enough memory on both environments. Can you provide me details of your configuration and I can try creating the same setup? – Gunjan Aggarwal Apr 26 '16 at 19:34
  • Let us [continue this discussion in chat](http://chat.stackoverflow.com/rooms/110337/discussion-between-anol-and-user2888308). – anol Apr 27 '16 at 06:30

1 Answers1

1

At the time Frama-C Magnesium was released, alt-ergo 1.01 did not exist yet. So when the WP manual for Magnesium mentioned compatibility with alt-ergo 0.99.1+, it could not foresee that there would be an incompatibility with the then future release of alt-ergo.

Fortunately, the next release (Aluminium) will be compatible with alt-ergo 1.01, so this should not be a problem in the future.

Meanwhile, you should be able to use alt-ergo 0.99.1.

Edit: Based on the error message and further details, it could be related to your Cygwin version, which seems relatively old, from 2013; yours is 1.7.27, while I'm using 2.4.1.

anol
  • 8,264
  • 3
  • 34
  • 78
  • I am able to use alt-ergo version 1.01 with Frama-c Magnesium on Linux environment. I do have to use option `-wp-alt-ergo-opt="-backward-compat"` to make it work properly, – Gunjan Aggarwal Apr 26 '16 at 17:51
  • I installed alt-ergo 0.99.1. But it doesn't help. I get the same error with alt-ergo version 0.99.1. I don't think that alt-ergo is even executing in my case as I used flag -wp-alt-ergo-opt="dfkdkskl" while executing -wp plugin, which is of-course not a valid option. I was hoping to get error message from alt-ergo, but I didn't. – Gunjan Aggarwal Apr 26 '16 at 17:57