--- layout: fc_discuss_archives title: Message 61 from Frama-C-discuss on October 2013 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] euklid.c



Here's an update on this issue.

I re-did everything with Ocaml 4.01.0.  No difference.

Then I tried with a 64-bit Lubuntu virtual machine, set up identically to the 32-bit version (with Ocaml 4.00.1).   Then it worked.

So there seems to be some defect with some module (Zarith?) in a 32-bit environment, that only comes up in very specific situations like this one.

By the way, in the 64-bit linux, there was some problem with opam install building the documentation for Coq.  I removed the tex packages to avoid the documentation building altogether, but there does seem to be a little bug there that someone might need to fix.

-Steve



On Oct 13, 2013, at 1:07 PM, Stephen Siegel <siegel at UDel.Edu> wrote:

> I started with a fresh Lubtutu 32-bit VM, installed opam and everything I could using opam, using 4.00.1, still getting the same error.  What I have installed:
> 
> user at 614v5:~/examples/basic$ ocaml -version
> The OCaml toplevel, version 4.00.1
> user at 614v5:~/examples/basic$ ocamlopt -version
> 4.00.1
> 
> user at 614v5:$ more ~/.opam/4.00.1/installed
> alt-ergo 0.95.2
> base-bigarray base
> base-threads base
> base-unix base
> camlp5 6.11
> conf-gnomecanvas 2
> conf-gtksourceview 2
> coq 8.4pl2
> frama-c 20130601
> lablgtk 2.16.0
> ocamlfind 1.4.0
> ocamlgraph 1.8.3
> why 2.33
> why3 0.81
> zarith 1.2
> 
> 
> Weirdly, the example works fine on Mac OS X, even though I installed everything almost exactly the same way:
> 
> basic$ ocaml -version
> The OCaml toplevel, version 4.00.1
> basic$ ocamlopt -version
> 4.00.1
> basic$
> 
> basic$ more ~/.opam/4.00.1/installed
> alt-ergo 0.95.2
> base-bigarray base
> base-threads base
> base-unix base
> camlp5 6.11
> conf-gnomecanvas 2
> conf-gtksourceview 2
> coq 8.4pl2
> frama-c 20130601
> lablgtk 2.16.0
> ocamlfind 1.4.0
> ocamlgraph 1.8.3
> why 2.33
> why3 0.81
> zarith 1.2
> 
> 
> The Mac is 64-bit, if that could make any difference.
> 
> -Steve
> 
> 
> On Oct 11, 2013, at 8:49 AM, Nanci Naomi <nnarai at gmail.com> wrote:
> 
>> Hi Stephen,
>> 
>> I have not run the example and I cannot help you, but I can say the ocaml version is old.
>> 
>> I have the version 4.01.0
>> 
>> Regards
>> 
>> Nanci Naomi
>> 
>> ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
>> Treat the Earth well.  It was not given to you by your parents,
>> it was loaned to you by your children. (Kenyan proverb) 
>> ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
>> 
>> 
>> 
>> On Thu, Oct 10, 2013 at 10:53 AM, Stephen Siegel <siegel at udel.edu> wrote:
>> I'm doing this in linux (Ubuntu), where I do have why 2.33, and every other example I have tried works fine.   But I guess I have an older ocaml?
>> 
>> user at cisc614:~/614/frama-c/examples/basic$ ocaml -version
>> The Objective Caml toplevel, version 3.12.1
>> user at cisc614:~/614/frama-c/examples/basic$ ocamlopt -version
>> 3.12.1
>> 
>> This is what got installed by apt-get ocaml ocaml-native-compilers.  apt-get thinks all these are up-to-date.
>> 
>> -s
>> 
>> 
>> 
>> 
>> 
>> On Oct 10, 2013, at 8:56 AM, Claude March? <Claude.Marche at inria.fr> wrote:
>> 
>> >
>> > I can't reproduce the problem. I've seen this error message in the past
>> > a long time ago. (e.g. http://bts.frama-c.com/view.php?id=1003)
>> >
>> >
>> > This may also depend on the version of OCaml.
>> > I hope it will disappear when you will install why 2.33
>> >
>> > - Claude
>> >
>> > Le 09/10/2013 22:53, Stephen Siegel a ?crit :
>> >> Uncaught exception: Invalid_argument("equal: abstract value")
>> >
>> > --
>> > Claude March?                          | tel: +33 1 72 92 59 69
>> > INRIA Saclay - ?le-de-France           |
>> > Universit? Paris-sud, Bat. 650         | http://www.lri.fr/~marche/
>> > F-91405 ORSAY Cedex                    |
>> 

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20131016/23aeb165/attachment-0001.html>