2 -- { dg-options "-gnata -gnateS" }
4 procedure SCOs1
with SPARK_Mode
=> On
is
6 LEN_IN_BITS
: constant := 20;
8 M_SIZE_BYTES
: constant := 2 ** LEN_IN_BITS
;
9 ET_BYTES
: constant := (M_SIZE_BYTES
- 4);
11 type T_BYTES
is new Integer range 0 .. ET_BYTES
with Size
=> 32;
12 subtype TYPE5_SCALAR
is T_BYTES
13 with Dynamic_Predicate
=> TYPE5_SCALAR
mod 4 = 0;
15 type E_16_BYTES
is new Integer;
16 subtype RD_BYTES
is E_16_BYTES
17 with Dynamic_Predicate
=> RD_BYTES
mod 4 = 0;
19 function "-" (left
: TYPE5_SCALAR
; right
: RD_BYTES
) return TYPE5_SCALAR
20 is ( left
- TYPE5_SCALAR
(right
) )
21 with Pre
=> TYPE5_SCALAR
(right
) <= left
and then
22 left
- TYPE5_SCALAR
(right
) <= T_BYTES
'Last, Inline_Always
;