Re: Hi-Lite high integrity showcase and overflow errors

[Shark8 <onewingedshark@gmail.com>]

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 general 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 := Mod_X( X );
	    Tmp_Y : Mod_X := Mod_X( Y );
	    Tmp_R : Mod_X := Tmp_X * Tmp_Y;
	    Last  : Constant := 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:= My_Int'Last;
		else
		    Result:= 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-bounds, in which case the "2**My_Int'Size" should be replaced with the proper static 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 be Mod (My_Int'Last-My_Int'First), with the offset of My_Int'First added/subtracted as necessary for the conversions.