src/HOL/SPARK/Examples/RIPEMD-160/wordops.ads

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/SPARK/Examples/RIPEMD-160/wordops.ads	Sat Jan 15 12:35:29 2011 +0100
@@ -0,0 +1,19 @@
+
+with Interfaces;
+--# inherit Interfaces;
+
+package WordOps is
+
+   subtype Word is Interfaces.Unsigned_32;
+
+   subtype Rotate_Amount is Integer range 0..15;
+
+   --# function rotate_left(I : Rotate_Amount; W : Word) return Word;
+
+   function Rotate(I : Rotate_Amount; W : Word) return Word;
+   --# return rotate_left(I, W);
+   --# accept W, 3, "Expecting this warning";
+   pragma Inline (Rotate);
+   --# end accept;
+
+end Wordops;