From mboxrd@z Thu Jan  1 00:00:00 1970
X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me
X-Spam-Level: 
X-Spam-Status: No, score=-0.9 required=5.0 tests=BAYES_00,FORGED_GMAIL_RCVD,
	FREEMAIL_FROM autolearn=no autolearn_force=no version=3.4.4
X-Google-Thread: 103376,834610f4f567e94b
X-Google-NewGroupId: yes
X-Google-Attributes: gida07f3367d7,domainid0,public,usenet
X-Google-Language: ENGLISH,ASCII-7-bit
Received: by 10.66.74.6 with SMTP id p6mr3903738pav.5.1346784310238;
        Tue, 04 Sep 2012 11:45:10 -0700 (PDT)
Received: by 10.68.218.226 with SMTP id pj2mr3561820pbc.19.1346784310220; Tue,
 04 Sep 2012 11:45:10 -0700 (PDT)
Path: 
 t10ni19137469pbh.0!nntp.google.com!4no6710164pbn.1!postnews.google.com!glegroupsg2000goo.googlegroups.com!not-for-mail
Newsgroups: comp.lang.ada
Date: Tue, 4 Sep 2012 11:45:09 -0700 (PDT)
In-Reply-To: <5045bc39$0$6569$9b4e6d93@newsspool3.arcor-online.net>
Complaints-To: groups-abuse@google.com
Injection-Info: glegroupsg2000goo.googlegroups.com;
 posting-host=69.20.190.126;
 posting-account=lJ3JNwoAAAAQfH3VV9vttJLkThaxtTfC
NNTP-Posting-Host: 69.20.190.126
References: <5045278b$0$6576$9b4e6d93@newsspool3.arcor-online.net>
 <269901b0-6570-4d7a-bcd4-19d590383515@googlegroups.com>
 <f9c3420e-7959-4ddf-b61c-d0eabbfdd197@googlegroups.com>
 <5045bc39$0$6569$9b4e6d93@newsspool3.arcor-online.net>
User-Agent: G2/1.0
MIME-Version: 1.0
Message-ID: <0a08a5e2-1696-4ea1-b47e-1e68a28f0cdd@googlegroups.com>
Subject: Re: Hi-Lite high integrity showcase and overflow errors
From: Shark8 <onewingedshark@gmail.com>
Injection-Date: Tue, 04 Sep 2012 18:45:10 +0000
Content-Type: text/plain; charset=ISO-8859-1
Content-Transfer-Encoding: quoted-printable
Date: 2012-09-04T11:45:09-07:00
List-Id: <comp.lang.ada>

On Tuesday, September 4, 2012 2:30:50 AM UTC-6, Georg Bauhaus wrote:
> On 04.09.12 05:05, Shark8 wrote:

Ah, I see; I'm not currently interested in SPARK but saw the problem in gen=
eral Ada terms.  Here's the SPARK-safe version:

	function Mult (X , Y : My_Int) return My_Int is
	    Type Mod_X is mod 2**My_Int'Size; -- must be power-of-2 for mod
	    Tmp_X : Mod_X :=3D Mod_X( X );
	    Tmp_Y : Mod_X :=3D Mod_X( Y );
	    Tmp_R : Mod_X :=3D Tmp_X * Tmp_Y;
	    Last  : Constant :=3D Integer(My_Int'Last);
	begin
	    Return Result : My_Int do
		-- We need to check that the result of the modular operation
		-- isn'tin excess of the given constraint; then check if the
		-- result is less than one of the inputs, in either case we
		-- need to return the maximum number... this might be avoided
  		-- by making the mod-type's modular number the same as
		-- My_Int'Last, however as SPARK is mentioned here that may
		-- not be an option as only powers-of-2 are permitted.
		if (integer(tmp_r) > Last) or else (tmp_R < Tmp_X) then
		    Result:=3D My_Int'Last;
		else
		    Result:=3D My_Int( tmp_R );
		end if;
	    End Return;
	end Mult;

You have to use modular-types to bypass overflowing-errors, but then there'=
s also the problem of non power-of-2 Last, which I address in the algorithm=
 presented. Another problem is if the My_Int range has non-zero lower-bound=
s, in which case the "2**My_Int'Size" should be replaced with the proper st=
atic expression something like Log(My_Int'Last-My_Int'First), or some other=
 appropriate bounds.

In general Ada I believe you can forgo the range-check by having the type b=
e Mod (My_Int'Last-My_Int'First), with the offset of My_Int'First added/sub=
tracted as necessary for the conversions.