diff options
Diffstat (limited to 'gcc/ada/libgnat/s-aridou.ads')
-rw-r--r-- | gcc/ada/libgnat/s-aridou.ads | 12 |
1 files changed, 9 insertions, 3 deletions
diff --git a/gcc/ada/libgnat/s-aridou.ads b/gcc/ada/libgnat/s-aridou.ads index 58aa775..b22f0db 100644 --- a/gcc/ada/libgnat/s-aridou.ads +++ b/gcc/ada/libgnat/s-aridou.ads @@ -77,18 +77,24 @@ is function Big (Arg : Double_Int) return Big_Integer is (Signed_Conversion.To_Big_Integer (Arg)) - with Ghost; + with + Ghost, + Annotate => (GNATprove, Inline_For_Proof); package Unsigned_Conversion is new BI_Ghost.Unsigned_Conversions (Int => Double_Uns); function Big (Arg : Double_Uns) return Big_Integer is (Unsigned_Conversion.To_Big_Integer (Arg)) - with Ghost; + with + Ghost, + Annotate => (GNATprove, Inline_For_Proof); function In_Double_Int_Range (Arg : Big_Integer) return Boolean is (BI_Ghost.In_Range (Arg, Big (Double_Int'First), Big (Double_Int'Last))) - with Ghost; + with + Ghost, + Annotate => (GNATprove, Inline_For_Proof); function Add_With_Ovflo_Check (X, Y : Double_Int) return Double_Int with |