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

Stop using Big_Integers_Ghost in the SPARKlib

Browse Source 
Make the SPARKlib were standalone to simplify the certification
process. It decorrelates the SPARKlib from the use of SPARK in the
certification of the light runtime.
This commit is contained in:
Claire Dross
2024-10-25 09:32:21 +02:00
parent 11713aaf3d
commit ba010efd6d
9 changed files with 399 additions and 353 deletions
Download Patch File Download Diff File Expand all files Collapse all files

11
sparklib_internal.gpr
View File

@@ -35,9 +35,8 @@ project SPARKlib_Internal is
package Prove renames SPARKlib_common.Prove;
Common_Excluded_Source_Files :=
("spark-big_integers__exec.adb",
"spark-big_integers__exec.ads",
"spark-big_integers__light.ads",
("spark-big_integers__light.ads",
"spark-big_integers__light.adb",
"spark-big_intervals__light.ads",
"spark-big_reals__light.adb",
"spark-big_reals__light.ads",
@@ -52,16 +51,16 @@ project SPARKlib_Internal is
case SPARK_Body_Mode is
when "On" =>
for Excluded_Source_Files use Common_Excluded_Source_Files
& ("spark-containers.ads");
& ("spark.ads");
when "Off" =>
for Excluded_Source_Files use Common_Excluded_Source_Files
& ("spark-containers__exec.ads");
& ("spark__exec.ads");
end case;
package Naming is
case SPARK_Body_Mode is
when "On" =>
for Spec ("SPARK.Containers") use "spark-containers__exec.ads";
for Spec ("SPARK") use "spark__exec.ads";
when "Off" =>
null;
end case;

16
sparklib_light_internal.gpr
View File

@@ -66,16 +66,15 @@ project SPARKlib_Light_Internal is
case SPARK_Body_Mode is
when "On" =>
for Excluded_Source_Files use Common_Excluded_Source_Files
& ("spark-containers.ads",
"spark-big_integers__light.ads");
& ("spark.ads");
when "Off" =>
for Excluded_Source_Files use Common_Excluded_Source_Files
& ("spark-containers__exec.ads",
"spark-big_integers__exec.ads",
"spark-big_integers__exec.adb");
& ("spark__exec.ads");
end case;
package Naming is
for Spec ("SPARK.Big_Integers") use "spark-big_integers__light.ads";
for Body ("SPARK.Big_Integers") use "spark-big_integers__light.adb";
for Spec ("SPARK.Big_Intervals") use "spark-big_intervals__light.ads";
for Spec ("SPARK.Big_Reals") use "spark-big_reals__light.ads";
for Body ("SPARK.Big_Reals") use "spark-big_reals__light.adb";
@@ -96,11 +95,8 @@ project SPARKlib_Light_Internal is
use "spark-containers-functional-vectors__light.ads";
case SPARK_Body_Mode is
when "On" =>
for Spec ("SPARK.Containers") use "spark-containers__exec.ads";
for Spec ("SPARK.Big_Integers") use "spark-big_integers__exec.ads";
for Body ("SPARK.Big_Integers") use "spark-big_integers__exec.adb";
when "Off" =>
for Spec ("SPARK.Big_Integers") use "spark-big_integers__light.ads";
for Spec ("SPARK") use "spark__exec.ads";
when "Off" => null;
end case;
end Naming;

176
src/spark-big_integers__exec.ads
View File

@@ -1,176 +0,0 @@
--
-- Copyright (C) 2016-2024, Free Software Foundation, Inc.
--
-- SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
--
-- This unit is meant to replace SPARK.Big_Integers for internal testing only
package SPARK.Big_Integers with
SPARK_Mode,
Ghost,
Pure,
Always_Terminates
is
type Big_Integer is private
with Integer_Literal => From_Universal_Image;
function Is_Valid (Arg : Big_Integer) return Boolean
with
Global => null;
subtype Valid_Big_Integer is Big_Integer
with Dynamic_Predicate => Is_Valid (Valid_Big_Integer),
Predicate_Failure => raise Program_Error;
function "=" (L, R : Valid_Big_Integer) return Boolean with
Global => null;
function "<" (L, R : Valid_Big_Integer) return Boolean with
Global => null;
function "<=" (L, R : Valid_Big_Integer) return Boolean with
Global => null;
function ">" (L, R : Valid_Big_Integer) return Boolean with
Global => null;
function ">=" (L, R : Valid_Big_Integer) return Boolean with
Global => null;
function To_Big_Integer (Arg : Integer) return Valid_Big_Integer
with
Global => null;
subtype Big_Positive is Big_Integer
with Dynamic_Predicate =>
(if Is_Valid (Big_Positive)
then Big_Positive > To_Big_Integer (0)),
Predicate_Failure => raise Constraint_Error;
subtype Big_Natural is Big_Integer
with Dynamic_Predicate =>
(if Is_Valid (Big_Natural)
then Big_Natural >= To_Big_Integer (0)),
Predicate_Failure => raise Constraint_Error;
function In_Range
(Arg : Valid_Big_Integer; Low, High : Big_Integer) return Boolean
is (Low <= Arg and Arg <= High)
with
Global => null;
function To_Integer (Arg : Valid_Big_Integer) return Integer
with
Pre => In_Range (Arg,
Low => To_Big_Integer (Integer'First),
High => To_Big_Integer (Integer'Last))
or else raise Constraint_Error,
Global => null;
generic
type Int is range <>;
package Signed_Conversions is
function To_Big_Integer (Arg : Int) return Valid_Big_Integer
with
Global => null;
function From_Big_Integer (Arg : Valid_Big_Integer) return Int
with
Pre => In_Range (Arg,
Low => To_Big_Integer (Int'First),
High => To_Big_Integer (Int'Last))
or else raise Constraint_Error,
Global => null;
end Signed_Conversions;
generic
type Int is mod <>;
package Unsigned_Conversions is
function To_Big_Integer (Arg : Int) return Valid_Big_Integer
with
Global => null;
function From_Big_Integer (Arg : Valid_Big_Integer) return Int
with
Pre => In_Range (Arg,
Low => To_Big_Integer (Int'First),
High => To_Big_Integer (Int'Last))
or else raise Constraint_Error,
Global => null;
end Unsigned_Conversions;
function From_String (Arg : String) return Valid_Big_Integer
with
Global => null;
function From_Universal_Image (Arg : String) return Valid_Big_Integer
renames From_String;
function "+" (L : Valid_Big_Integer) return Valid_Big_Integer
with
Global => null;
function "-" (L : Valid_Big_Integer) return Valid_Big_Integer
with
Global => null;
function "abs" (L : Valid_Big_Integer) return Valid_Big_Integer
with
Global => null;
function "+" (L, R : Valid_Big_Integer) return Valid_Big_Integer
with
Global => null;
function "-" (L, R : Valid_Big_Integer) return Valid_Big_Integer
with
Global => null;
function "*" (L, R : Valid_Big_Integer) return Valid_Big_Integer
with
Global => null;
function "/" (L, R : Valid_Big_Integer) return Valid_Big_Integer
with
Global => null;
function "mod" (L, R : Valid_Big_Integer) return Valid_Big_Integer
with
Global => null;
function "rem" (L, R : Valid_Big_Integer) return Valid_Big_Integer
with
Global => null;
function "**" (L : Valid_Big_Integer; R : Natural) return Valid_Big_Integer
with
Global => null;
function Min (L, R : Valid_Big_Integer) return Valid_Big_Integer
with
Global => null;
function Max (L, R : Valid_Big_Integer) return Valid_Big_Integer
with
Global => null;
function Greatest_Common_Divisor
(L, R : Valid_Big_Integer) return Big_Positive
with
Pre => (L /= To_Big_Integer (0) and R /= To_Big_Integer (0))
or else raise Constraint_Error,
Global => null;
private
pragma SPARK_Mode (Off);
type Big_Integer is record
V : Long_Long_Long_Integer;
end record;
end SPARK.Big_Integers;

348
src/spark-big_integers__exec.adb → src/spark-big_integers__light.adb
View File

@@ -8,81 +8,31 @@ package body SPARK.Big_Integers with
SPARK_Mode => Off
is
--------------
-- Is_Valid --
--------------
function Is_Valid (Arg : Big_Integer) return Boolean is
(True);
---------
-- "=" --
---------
function "=" (L, R : Valid_Big_Integer) return Boolean is
(L.V = R.V);
---------
-- "<" --
---------
function "<" (L, R : Valid_Big_Integer) return Boolean is
(L.V < R.V);
----------
-- "<=" --
----------
function "<=" (L, R : Valid_Big_Integer) return Boolean is
(L.V <= R.V);
---------
-- ">" --
---------
function ">" (L, R : Valid_Big_Integer) return Boolean is
(L.V > R.V);
----------
-- ">=" --
----------
function ">=" (L, R : Valid_Big_Integer) return Boolean is
(L.V >= R.V);
--------------------
-- To_Big_Integer --
--------------------
function To_Big_Integer (Arg : Integer) return Valid_Big_Integer is
((V => Long_Long_Long_Integer (Arg)));
----------------
-- To_Integer --
----------------
function To_Integer (Arg : Valid_Big_Integer) return Integer is
(Integer (Arg.V));
------------------------
-- Signed_Conversions --
------------------------
package body Signed_Conversions is
--------------------
-- To_Big_Integer --
--------------------
function To_Big_Integer (Arg : Int) return Valid_Big_Integer is
((V => Long_Long_Long_Integer (Arg)));
----------------------
-- From_Big_Integer --
----------------------
function From_Big_Integer (Arg : Valid_Big_Integer) return Int is
(Int (Arg.V));
begin
Check_Or_Fail;
return Int (Arg.V);
end From_Big_Integer;
--------------------
-- To_Big_Integer --
--------------------
function To_Big_Integer (Arg : Int) return Valid_Big_Integer is
begin
Check_Or_Fail;
return (V => Long_Long_Long_Integer (Arg));
end To_Big_Integer;
end Signed_Conversions;
@@ -92,91 +42,37 @@ is
package body Unsigned_Conversions is
--------------------
-- To_Big_Integer --
--------------------
function To_Big_Integer (Arg : Int) return Valid_Big_Integer is
((V => Long_Long_Long_Integer (Arg)));
----------------------
-- From_Big_Integer --
----------------------
function From_Big_Integer (Arg : Valid_Big_Integer) return Int is
(Int (Arg.V));
begin
Check_Or_Fail;
return Int (Arg.V);
end From_Big_Integer;
--------------------
-- To_Big_Integer --
--------------------
function To_Big_Integer (Arg : Int) return Valid_Big_Integer is
begin
Check_Or_Fail;
return (V => Long_Long_Long_Integer (Arg));
end To_Big_Integer;
end Unsigned_Conversions;
-----------------
-- From_String --
-----------------
function From_String (Arg : String) return Valid_Big_Integer is
((V => Long_Long_Long_Integer'Value (Arg)));
---------
-- "+" --
---------
function "+" (L : Valid_Big_Integer) return Valid_Big_Integer is
(L);
---------
-- "-" --
---------
function "-" (L : Valid_Big_Integer) return Valid_Big_Integer is
((V => -L.V));
-----------
-- "abs" --
-----------
function "abs" (L : Valid_Big_Integer) return Valid_Big_Integer is
((V => abs L.V));
---------
-- "+" --
---------
function "+" (L, R : Valid_Big_Integer) return Valid_Big_Integer is
((V => L.V + R.V));
---------
-- "-" --
---------
function "-" (L, R : Valid_Big_Integer) return Valid_Big_Integer is
((V => L.V - R.V));
---------
-- "*" --
---------
function "*" (L, R : Valid_Big_Integer) return Valid_Big_Integer is
((V => L.V * R.V));
---------
-- "/" --
---------
function "/" (L, R : Valid_Big_Integer) return Valid_Big_Integer is
((V => L.V / R.V));
-----------
-- "mod" --
-----------
function "mod" (L, R : Valid_Big_Integer) return Valid_Big_Integer is
((V => L.V mod R.V));
-----------
-- "rem" --
-----------
function "rem" (L, R : Valid_Big_Integer) return Valid_Big_Integer is
((V => L.V rem R.V));
begin
Check_Or_Fail;
return (V => L.V * R.V);
end "*";
----------
-- "**" --
@@ -184,7 +80,142 @@ is
function "**"
(L : Valid_Big_Integer; R : Natural) return Valid_Big_Integer is
((V => L.V ** R));
begin
Check_Or_Fail;
return (V => L.V ** R);
end "**";
---------
-- "+" --
---------
function "+" (L : Valid_Big_Integer) return Valid_Big_Integer is
begin
Check_Or_Fail;
return L;
end "+";
function "+" (L, R : Valid_Big_Integer) return Valid_Big_Integer is
begin
Check_Or_Fail;
return (V => L.V + R.V);
end "+";
---------
-- "-" --
---------
function "-" (L : Valid_Big_Integer) return Valid_Big_Integer is
begin
Check_Or_Fail;
return (V => -L.V);
end "-";
function "-" (L, R : Valid_Big_Integer) return Valid_Big_Integer is
begin
Check_Or_Fail;
return (V => L.V - R.V);
end "-";
---------
-- "/" --
---------
function "/" (L, R : Valid_Big_Integer) return Valid_Big_Integer is
begin
Check_Or_Fail;
return (V => L.V / R.V);
end "/";
---------
-- "<" --
---------
function "<" (L, R : Valid_Big_Integer) return Boolean is
begin
Check_Or_Fail;
return L.V < R.V;
end "<";
----------
-- "<=" --
----------
function "<=" (L, R : Valid_Big_Integer) return Boolean is
begin
Check_Or_Fail;
return L.V <= R.V;
end "<=";
---------
-- "=" --
---------
function "=" (L, R : Valid_Big_Integer) return Boolean is
begin
Check_Or_Fail;
return L.V = R.V;
end "=";
---------
-- ">" --
---------
function ">" (L, R : Valid_Big_Integer) return Boolean is
begin
Check_Or_Fail;
return L.V > R.V;
end ">";
----------
-- ">=" --
----------
function ">=" (L, R : Valid_Big_Integer) return Boolean is
begin
Check_Or_Fail;
return L.V >= R.V;
end ">=";
-----------
-- "abs" --
-----------
function "abs" (L : Valid_Big_Integer) return Valid_Big_Integer is
begin
Check_Or_Fail;
return (V => abs L.V);
end "abs";
-----------
-- "mod" --
-----------
function "mod" (L, R : Valid_Big_Integer) return Valid_Big_Integer is
begin
Check_Or_Fail;
return (V => L.V mod R.V);
end "mod";
-----------
-- "rem" --
-----------
function "rem" (L, R : Valid_Big_Integer) return Valid_Big_Integer is
begin
Check_Or_Fail;
return (V => L.V rem R.V);
end "rem";
-----------------
-- From_String --
-----------------
function From_String (Arg : String) return Valid_Big_Integer is
begin
Check_Or_Fail;
return (V => Long_Long_Long_Integer'Value (Arg));
end From_String;
-----------------------------
-- Greatest_Common_Divisor --
@@ -192,14 +223,18 @@ is
function Greatest_Common_Divisor
(L, R : Valid_Big_Integer) return Big_Positive
is (raise Program_Error);
is
begin
Check_Or_Fail;
return (raise Program_Error);
end Greatest_Common_Divisor;
---------
-- Min --
---------
--------------
-- Is_Valid --
--------------
function Min (L, R : Valid_Big_Integer) return Valid_Big_Integer is
(if L < R then L else R);
function Is_Valid (Arg : Big_Integer) return Boolean is
(True);
---------
-- Max --
@@ -208,4 +243,31 @@ is
function Max (L, R : Valid_Big_Integer) return Valid_Big_Integer is
(if L > R then L else R);
---------
-- Min --
---------
function Min (L, R : Valid_Big_Integer) return Valid_Big_Integer is
(if L < R then L else R);
--------------------
-- To_Big_Integer --
--------------------
function To_Big_Integer (Arg : Integer) return Valid_Big_Integer is
begin
Check_Or_Fail;
return (V => Long_Long_Long_Integer (Arg));
end To_Big_Integer;
----------------
-- To_Integer --
----------------
function To_Integer (Arg : Valid_Big_Integer) return Integer is
begin
Check_Or_Fail;
return Integer (Arg.V);
end To_Integer;
end SPARK.Big_Integers;

169
src/spark-big_integers__light.ads
View File

@@ -13,6 +13,171 @@
-- depend on System or Ada.Finalization, which makes it more convenient for
-- use in run-time units.
with Ada.Numerics.Big_Numbers.Big_Integers_Ghost;
package SPARK.Big_Integers with
SPARK_Mode,
Ghost,
Pure,
Always_Terminates
is
package SPARK.Big_Integers renames Ada.Numerics.Big_Numbers.Big_Integers_Ghost;
type Big_Integer is private
with Integer_Literal => From_Universal_Image;
function Is_Valid (Arg : Big_Integer) return Boolean
with
Global => null;
subtype Valid_Big_Integer is Big_Integer
with Dynamic_Predicate => Is_Valid (Valid_Big_Integer),
Predicate_Failure => raise Program_Error;
function "=" (L, R : Valid_Big_Integer) return Boolean with
Global => null;
function "<" (L, R : Valid_Big_Integer) return Boolean with
Global => null;
function "<=" (L, R : Valid_Big_Integer) return Boolean with
Global => null;
function ">" (L, R : Valid_Big_Integer) return Boolean with
Global => null;
function ">=" (L, R : Valid_Big_Integer) return Boolean with
Global => null;
function To_Big_Integer (Arg : Integer) return Valid_Big_Integer
with
Global => null;
subtype Big_Positive is Big_Integer
with Dynamic_Predicate =>
(if Is_Valid (Big_Positive)
then Big_Positive > To_Big_Integer (0)),
Predicate_Failure => raise Constraint_Error;
subtype Big_Natural is Big_Integer
with Dynamic_Predicate =>
(if Is_Valid (Big_Natural)
then Big_Natural >= To_Big_Integer (0)),
Predicate_Failure => raise Constraint_Error;
function In_Range
(Arg : Valid_Big_Integer; Low, High : Big_Integer) return Boolean
is (Low <= Arg and Arg <= High)
with
Global => null;
function To_Integer (Arg : Valid_Big_Integer) return Integer
with
Pre => In_Range (Arg,
Low => To_Big_Integer (Integer'First),
High => To_Big_Integer (Integer'Last))
or else raise Constraint_Error,
Global => null;
generic
type Int is range <>;
package Signed_Conversions is
function To_Big_Integer (Arg : Int) return Valid_Big_Integer
with
Global => null;
function From_Big_Integer (Arg : Valid_Big_Integer) return Int
with
Pre => In_Range (Arg,
Low => To_Big_Integer (Int'First),
High => To_Big_Integer (Int'Last))
or else raise Constraint_Error,
Global => null;
end Signed_Conversions;
generic
type Int is mod <>;
package Unsigned_Conversions is
function To_Big_Integer (Arg : Int) return Valid_Big_Integer
with
Global => null;
function From_Big_Integer (Arg : Valid_Big_Integer) return Int
with
Pre => In_Range (Arg,
Low => To_Big_Integer (Int'First),
High => To_Big_Integer (Int'Last))
or else raise Constraint_Error,
Global => null;
end Unsigned_Conversions;
function From_String (Arg : String) return Valid_Big_Integer
with
Global => null;
function From_Universal_Image (Arg : String) return Valid_Big_Integer
renames From_String;
function "+" (L : Valid_Big_Integer) return Valid_Big_Integer
with
Global => null;
function "-" (L : Valid_Big_Integer) return Valid_Big_Integer
with
Global => null;
function "abs" (L : Valid_Big_Integer) return Valid_Big_Integer
with
Global => null;
function "+" (L, R : Valid_Big_Integer) return Valid_Big_Integer
with
Global => null;
function "-" (L, R : Valid_Big_Integer) return Valid_Big_Integer
with
Global => null;
function "*" (L, R : Valid_Big_Integer) return Valid_Big_Integer
with
Global => null;
function "/" (L, R : Valid_Big_Integer) return Valid_Big_Integer
with
Global => null;
function "mod" (L, R : Valid_Big_Integer) return Valid_Big_Integer
with
Global => null;
function "rem" (L, R : Valid_Big_Integer) return Valid_Big_Integer
with
Global => null;
function "**" (L : Valid_Big_Integer; R : Natural) return Valid_Big_Integer
with
Global => null;
function Min (L, R : Valid_Big_Integer) return Valid_Big_Integer
with
Global => null;
function Max (L, R : Valid_Big_Integer) return Valid_Big_Integer
with
Global => null;
function Greatest_Common_Divisor
(L, R : Valid_Big_Integer) return Big_Positive
with
Pre => (L /= To_Big_Integer (0) and R /= To_Big_Integer (0))
or else raise Constraint_Error,
Global => null;
private
pragma SPARK_Mode (Off);
type Big_Integer is record
V : Long_Long_Long_Integer;
end record;
end SPARK.Big_Integers;

3
src/spark-containers.ads
View File

@@ -5,7 +5,4 @@
--
package SPARK.Containers with SPARK_Mode, Pure is
procedure Check_Or_Fail with Import;
end SPARK.Containers;

13
src/spark-containers__exec.ads
View File

@@ -1,13 +0,0 @@
--
-- Copyright (C) 2022-2024, AdaCore
--
-- SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
--
-- This unit is meant to replace SPARK.Containers for internal testing only
package SPARK.Containers with SPARK_Mode, Pure is
procedure Check_Or_Fail is null;
end SPARK.Containers;

3
src/spark.ads
View File

@@ -5,4 +5,7 @@
--
package SPARK with SPARK_Mode, Pure is
procedure Check_Or_Fail with Import;
end SPARK;

13
src/spark__exec.ads Normal file
View File

@@ -0,0 +1,13 @@
--
-- Copyright (C) 2022-2024, AdaCore
--
-- SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
--
-- This unit is meant to replace SPARK for internal testing only
package SPARK with SPARK_Mode, Pure is
procedure Check_Or_Fail is null;
end SPARK;