From 32a6fcb12814550633261960b540ffeb8a0fcab5 Mon Sep 17 00:00:00 2001
From: varobert <varobert@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Wed, 4 Apr 2012 11:59:40 +0000
Subject: Added safety to potentially overflowing arithmetics

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1872 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
---
 checklink/Safe.ml | 25 +++++++++++++++++++++++++
 1 file changed, 25 insertions(+)
 create mode 100644 checklink/Safe.ml

(limited to 'checklink/Safe.ml')

diff --git a/checklink/Safe.ml b/checklink/Safe.ml
new file mode 100644
index 0000000..efcd3bd
--- /dev/null
+++ b/checklink/Safe.ml
@@ -0,0 +1,25 @@
+(* "Hacker's Delight", section 2.12 *)
+
+let ( + ) x y =
+  let z = x + y in
+  (* Overflow occurs iff x and y have same sign and z's sign is different *)
+  if (z lxor x) land (z lxor y) < 0
+  then raise Exc.IntOverflow
+  else z
+
+let ( - ) x y =
+  let z = x - y in
+  (* Overflow occurs iff x and y have opposite signs and z and x have
+     opposite signs *)
+  if (x lxor y) land (z lxor x) < 0
+  then raise Exc.IntOverflow
+  else z
+
+let ( * ) x y =
+  let z = x * y in
+  if (x = min_int && y < 0) || (y <> 0 && z / y <> x)
+  then raise Exc.IntOverflow
+  else z
+
+let of_int32 = Safe32.to_int
+let to_int32 = Safe32.of_int
-- 
cgit v1.2.3