src/HOL/SPARK/Examples/RIPEMD-160/wordops.ads
author wenzelm
Mon, 13 Apr 2020 22:08:14 +0200
changeset 71751 abf3e80bd815
parent 41561 d1318f3c86ba
permissions -rw-r--r--
tuned NEWS;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
41561
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
     1
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
     2
with Interfaces;
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
     3
--# inherit Interfaces;
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
     4
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
     5
package WordOps is
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
     6
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
     7
   subtype Word is Interfaces.Unsigned_32;
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
     8
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
     9
   subtype Rotate_Amount is Integer range 0..15;
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    10
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    11
   --# function rotate_left(I : Rotate_Amount; W : Word) return Word;
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    12
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    13
   function Rotate(I : Rotate_Amount; W : Word) return Word;
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    14
   --# return rotate_left(I, W);
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    15
   --# accept W, 3, "Expecting this warning";
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    16
   pragma Inline (Rotate);
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    17
   --# end accept;
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    18
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    19
end Wordops;