note
	description: "[
		Detect Integer Overflow
		debug
			ToDo: Pre/Post-conditions
		end
		ToDo: multiply and divide
	]"
	author: ""
	date: "$Date$"
	revision: "$Revision$"

class 
	INTEGER_OVERFLOW

create 
	default_create

feature 

	Max_int: INTEGER_64
		once
			Result := Result.Max_value
		end

	Min_int: INTEGER_64
		once
			Result := Result.Min_value
		end

	safe_plus (left, right: INTEGER_64): BOOLEAN
		do
			if right > 0 then
				Result := (left <= Max_int - right)
			else
				Result := (left >= Min_int - right)
			end
		ensure
				right >= 0 implies Result = (left <= Max_int - right)
				right <= 0 implies Result = (left >= Min_int - right)
		end

	safe_minus (left, right: INTEGER_64): BOOLEAN
		do
			if right > 0 then
				Result := (left >= Min_int + right)
			else
				Result := (left <= Max_int + right)
			end
		ensure
				right >= 0 implies Result = (left >= Min_int + right)
				right <= 0 implies Result = (left <= Max_int + right)
		end
	
end -- class INTEGER_OVERFLOW

Generated by ISE EiffelStudio