From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: from mail3-relais-sop.national.inria.fr (mail3-relais-sop.national.inria.fr [192.134.164.104]) by sympa.inria.fr (Postfix) with ESMTPS id 825087FCCB for ; Sun, 19 Apr 2015 01:14:50 +0200 (CEST) Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of taostein@gmail.com) identity=pra; client-ip=209.85.223.180; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="taostein@gmail.com"; x-sender="taostein@gmail.com"; x-conformance=sidf_compatible Received-SPF: Pass (mail3-smtp-sop.national.inria.fr: domain of taostein@gmail.com designates 209.85.223.180 as permitted sender) identity=mailfrom; client-ip=209.85.223.180; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="taostein@gmail.com"; x-sender="taostein@gmail.com"; x-conformance=sidf_compatible; x-record-type="v=spf1" Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of postmaster@mail-ie0-f180.google.com) identity=helo; client-ip=209.85.223.180; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="taostein@gmail.com"; x-sender="postmaster@mail-ie0-f180.google.com"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: A0BLAgCV5DJVlLTfVdFcg15cBYMSwnKBeocwBzwQAQEBAQEBAREBAQEBBwsLCRIwhDkRHQEbHgMSAwYBBjcCJAERAQUBV4d0AQMRl0mNLYMuPjGLOYFrgnaJNAoZJw1UhQ0BBQ6QNIJSgUUFlSeGJZNYEiOBDAmBc4IkPDGCRAEBAQ X-IPAS-Result: A0BLAgCV5DJVlLTfVdFcg15cBYMSwnKBeocwBzwQAQEBAQEBAREBAQEBBwsLCRIwhDkRHQEbHgMSAwYBBjcCJAERAQUBV4d0AQMRl0mNLYMuPjGLOYFrgnaJNAoZJw1UhQ0BBQ6QNIJSgUUFlSeGJZNYEiOBDAmBc4IkPDGCRAEBAQ X-IronPort-AV: E=Sophos;i="5.11,601,1422918000"; d="scan'208";a="112007807" Received: from mail-ie0-f180.google.com ([209.85.223.180]) by mail3-smtp-sop.national.inria.fr with ESMTP/TLS/RC4-SHA; 19 Apr 2015 01:14:49 +0200 Received: by iedfl3 with SMTP id fl3so107094561ied.1 for ; Sat, 18 Apr 2015 16:14:48 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20120113; h=mime-version:date:message-id:subject:from:to:content-type; bh=eHBH0xFBWoo3lgCz/v2X7KJhwB2UxqzY/SvqeEFqmps=; b=AzdG3x9ps+1o+KEIVCadL8G/HQMeg3XQcI+xgkX79Kp73vdlwDApOm7OVitoUPblRj /X3RBZFHuRHlJnixf8ubXbeIHBnl06dezoPV1pYTcQKdBV3QZNj5bMzYosA2mh7O6cNf vpWJMZFO2IeaxtV6uFGI8EZfvys0Gnak1DhbKDtxkFv+USxXlkbOh68p3shiaVMH80md jITKALuyBfxYmMbOMerrT6Zc5T1ZUbLvOnkJWNaKQqLGlXJzwGP/vbdhCuUbdL4SzqLy vwtvfMGz77jMZebyBIr/8WgB3NfOWGzBtr64xU2R7yt1eQXEhotoDGzPvdPldWHHPSYn FztA== MIME-Version: 1.0 X-Received: by 10.50.132.33 with SMTP id or1mr7877401igb.31.1429398888288; Sat, 18 Apr 2015 16:14:48 -0700 (PDT) Received: by 10.107.38.17 with HTTP; Sat, 18 Apr 2015 16:14:48 -0700 (PDT) Date: Sun, 19 Apr 2015 01:14:48 +0200 Message-ID: From: Tao Stein To: caml-list@inria.fr Content-Type: multipart/alternative; boundary=047d7b1636e1fa9844051407dcec Subject: [Caml-list] strange integer division result in ocamlopt ... --047d7b1636e1fa9844051407dcec Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: quoted-printable I'm getting a strange result using ocamlopt that seems to violate the basic axioms of integer division. Some context first: taostein@~/b2/f2: which ocamlopt /Users/taostein/.opam/4.02.1/bin/ocamlopt taostein@~/b2/f2: ocamlopt -o foo.opt foo.ml taostein@~/b2/f2: which ocamlc /Users/taostein/.opam/4.02.1/bin/ocamlc taostein@~/artcode/b2/f2: ocamlc -o foo foo.ml Built with ocamlopt, the following code throws an exception. Built with ocamlc it does not. let k1 =3D 1;; let rec f i k =3D if (((i / k1) * k1 + (i mod k1)) <> i) then (raise (Failure "violation of integer division axiom")) else (if (i < 10) then (f (i + 1) k) else ()) in f 0 1;; Now, if I change the above only on line 3 changing k1 to k, then it works fine, no problem. let k1 =3D 1;; let rec f i k =3D if (((i / k) * k + (i mod k)) <> i) then (raise (Failure "violation of integer division axiom")) else (if (i < 10) then (f (i + 1) k) else ()) in f 0 1;; No exception in either ocamlc or ocamlopt. Using ocamlopt, it seems 1 mod 1 =3D 1. This is problematic. Tao Stein / =E7=9F=B3=E6=B6=9B --047d7b1636e1fa9844051407dcec Content-Type: text/html; charset=UTF-8 Content-Transfer-Encoding: quoted-printable

I'm getting a strange result using= ocamlopt that seems to violate the basic axioms of integer division.
=

Some context first:
taostein@~/b2/f2: which ocamlo= pt
/Users/taostein/.opam/4.02.1/bin/ocamlopt
taostein@~/b2/f2: o= camlopt -o foo.opt foo.ml
taostein@~/b2/f2= : which ocamlc
/Users/taostein/.opam/4.02.1/bin/ocamlc
taostein@~/a= rtcode/b2/f2: ocamlc -o foo foo.ml

Bui= lt with ocamlopt, the following code throws an exception. Built with ocamlc= it does not.

let k1 =3D 1;;
let rec f i k =3D
=C2= =A0 if (((i / k1) * k1 + (i mod k1)) <> i)
=C2=A0 then (raise (Fai= lure "violation of integer division axiom"))
=C2=A0 else (if (= i < 10) then (f (i + 1) k) else ()) in
f 0 1;;

Now= , if I change the above only on line 3 changing k1 to k, then it works fine= , no problem.

let k1 =3D 1;;
let rec f i k =3D
=C2= =A0 if (((i / k) * k + (i m= od k)) <> i)
=C2=A0 then (raise (Failure "violation of= integer division axiom"))
=C2=A0 else (if (i < 10) then (f (i += 1) k) else ()) in
f 0 1;;

No exception in eith= er ocamlc or ocamlopt.

Using ocamlopt, it seems 1 = mod 1 =3D 1. This is problematic.

Tao Stein / =E7= =9F=B3=E6=B6=9B

--047d7b1636e1fa9844051407dcec--