From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Original-To: caml-list@sympa.inria.fr Delivered-To: caml-list@sympa.inria.fr 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 363B07FCCB for ; Sun, 19 Apr 2015 01:20:49 +0200 (CEST) Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of hugo.heuzard@gmail.com) identity=pra; client-ip=209.85.212.176; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="hugo.heuzard@gmail.com"; x-sender="hugo.heuzard@gmail.com"; x-conformance=sidf_compatible Received-SPF: Pass (mail3-smtp-sop.national.inria.fr: domain of hugo.heuzard@gmail.com designates 209.85.212.176 as permitted sender) identity=mailfrom; client-ip=209.85.212.176; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="hugo.heuzard@gmail.com"; x-sender="hugo.heuzard@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-wi0-f176.google.com) identity=helo; client-ip=209.85.212.176; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="hugo.heuzard@gmail.com"; x-sender="postmaster@mail-wi0-f176.google.com"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: A0BMAgCL5TJVlLDUVdFCGoNeXAWDEsJyggKGAwKBIwc8EAEBAQEBAQERAQEBAQcLCwkSMIQhAQEDARIRHQEbHQEDDAYDAgQHNwICIQEBEQEFARwGEwgah3QBAwkIDTeXBZBbPjGLOYFrgnaJNAoZJw1UhGcBAQEBBgEBAQEBARYBBQ6LG4JHgjUHgmiBRQWBTJBlAYJ1hFeBToFZjQKEfRIjgQwJhDEiMQGCQwEBAQ X-IPAS-Result: A0BMAgCL5TJVlLDUVdFCGoNeXAWDEsJyggKGAwKBIwc8EAEBAQEBAQERAQEBAQcLCwkSMIQhAQEDARIRHQEbHQEDDAYDAgQHNwICIQEBEQEFARwGEwgah3QBAwkIDTeXBZBbPjGLOYFrgnaJNAoZJw1UhGcBAQEBBgEBAQEBARYBBQ6LG4JHgjUHgmiBRQWBTJBlAYJ1hFeBToFZjQKEfRIjgQwJhDEiMQGCQwEBAQ X-IronPort-AV: E=Sophos;i="5.11,601,1422918000"; d="scan'208";a="112008005" Received: from mail-wi0-f176.google.com ([209.85.212.176]) by mail3-smtp-sop.national.inria.fr with ESMTP/TLS/RC4-SHA; 19 Apr 2015 01:20:48 +0200 Received: by widdi4 with SMTP id di4so59372400wid.0 for ; Sat, 18 Apr 2015 16:20:48 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20120113; h=mime-version:in-reply-to:references:from:date:message-id:subject:to :cc:content-type; bh=ynolCDENuK7eDJIcgnFuarzYt10UA57wWOvhi3nRETQ=; b=wcZtYoufjMpQwTpv9pM/Bge0Z9s8QR1CMq1cCO+vdNDm99viuMYKchCop7f2+bzFbk XLNCURqUjTVho3M2rDB0ZXp1lkq7C/TANnbnUBwZQpvU6CvhTB7qyakNQpsKFr1Xpijl qPdykBXShxmH0EEdtEcsmqpaS7t7wwixsnOEyE7INjRk6QbRYTmhJZTDUR/YbjIaLbSk lB3HFy8h8+wdfdPWnAUYXivx90sR9rAo2eK6atIprq/AZfD+vr7hWRUs+xvHWO5DBfup DDy449VAoPJOJxJKVCDEihOGuKeG8VfD3XlhDU3PjvM4vceksGhx0rCvlKIiBquFcJkE vL2Q== X-Received: by 10.180.186.5 with SMTP id fg5mr13051784wic.60.1429399248083; Sat, 18 Apr 2015 16:20:48 -0700 (PDT) MIME-Version: 1.0 Received: by 10.27.17.214 with HTTP; Sat, 18 Apr 2015 16:20:27 -0700 (PDT) In-Reply-To: References: From: hugo Date: Sat, 18 Apr 2015 19:20:27 -0400 Message-ID: To: Tao Stein Cc: caml-list@inria.fr Content-Type: multipart/alternative; boundary=001a11c334e66ca273051407f22f Subject: Re: [Caml-list] strange integer division result in ocamlopt ... --001a11c334e66ca273051407f22f Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: quoted-printable see http://caml.inria.fr/mantis/view.php?id=3D6749 On Sat, Apr 18, 2015 at 7:14 PM, Tao Stein wrote: > > 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 > > --001a11c334e66ca273051407f22f Content-Type: text/html; charset=UTF-8 Content-Transfer-Encoding: quoted-printable

On Sat, Apr 18, 2015 at 7:1= 4 PM, Tao Stein <taostein@gmail.com> wrote:

I'm getting a s= trange result using ocamlopt that seems to violate the basic axioms of inte= ger 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/.o= pam/4.02.1/bin/ocamlc
taostein@~/artcode/b2/f2: ocamlc -o foo foo.ml

Built with ocamlopt, th= e 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) * k= 1 + (i mod k1)) <> 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;;

Now, if I change the abo= ve 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 mod k)) <> i)
=C2=A0 then (raise (Failure "violation of integer division axi= om"))
=C2=A0 else (if (i < 10) then (f (i + 1) k) else ()) inf 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


--001a11c334e66ca273051407f22f--