ada/SPARKlib
0
0
Fork 0
mirror of https://github.com/AdaCore/SPARKlib.git synced 2026-02-12 13:11:36 -08:00
Code Issues Packages Projects Releases Wiki Activity

Add SPARK_Mode Off to big integer conversions

Browse Source
This commit is contained in:
Claire Dross
2024-10-31 15:59:33 +01:00
parent 3c71f7e6c0
commit bd92fc3cf4
2 changed files with 11 additions and 2 deletions
Download Patch File Download Diff File Expand all files Collapse all files

8
src/spark-big_integers__light.adb
View File

@@ -12,7 +12,9 @@ is
-- Signed_Conversions --
------------------------
package body Signed_Conversions is
package body Signed_Conversions with
SPARK_Mode => Off
is
----------------------
-- From_Big_Integer --
@@ -40,7 +42,9 @@ is
-- Unsigned_Conversions --
--------------------------
package body Unsigned_Conversions is
package body Unsigned_Conversions with
SPARK_Mode => Off
is
----------------------
-- From_Big_Integer --

5
tests/V916-025__sparklib_light/test.out
View File

@@ -1,2 +1,7 @@
main.adb:28:13: info: implicit aspect Always_Terminates on "Hash" has been proved, subprogram will terminate
spark-big_integers__light.ads:31:32: warning: function Is_Valid is assumed to return True
spark-big_integers__light.ads:55:17: warning: function Is_Valid is assumed to return True
spark-big_integers__light.ads:61:17: warning: function Is_Valid is assumed to return True
spark-big_reals__light.ads:34:32: warning: function Is_Valid is assumed to return True
ok
ok