function To_Neg_Int (A : Double_Uns) return Double_Int
with
- Annotate => (GNATprove, Terminating),
+ Annotate => (GNATprove, Always_Return),
Pre => In_Double_Int_Range (-Big (A)),
Post => Big (To_Neg_Int'Result) = -Big (A);
-- Convert to negative integer equivalent. If the input is in the range
function To_Pos_Int (A : Double_Uns) return Double_Int
with
- Annotate => (GNATprove, Terminating),
+ Annotate => (GNATprove, Always_Return),
Pre => In_Double_Int_Range (Big (A)),
Post => Big (To_Pos_Int'Result) = Big (A);
-- Convert to positive integer equivalent. If the input is in the range
function To_Neg_Int (A : Uns32) return Int32
with
- Annotate => (GNATprove, Terminating),
+ Annotate => (GNATprove, Always_Return),
Pre => In_Int32_Range (-Big (A)),
Post => Big (To_Neg_Int'Result) = -Big (A);
-- Convert to negative integer equivalent. If the input is in the range
function To_Pos_Int (A : Uns32) return Int32
with
- Annotate => (GNATprove, Terminating),
+ Annotate => (GNATprove, Always_Return),
Pre => In_Int32_Range (Big (A)),
Post => Big (To_Pos_Int'Result) = Big (A);
-- Convert to positive integer equivalent. If the input is in the range
package System.SPARK.Cut_Operations with
SPARK_Mode,
Pure,
- Annotate => (GNATprove, Terminating)
+ Annotate => (GNATprove, Always_Return)
is
function By (Consequence, Premise : Boolean) return Boolean with