Skip to content

Commit

Permalink
Add Always_Return annotations
Browse files Browse the repository at this point in the history 
Ref. #1131
  • Loading branch information
@treiher
treiher committed Aug 19, 2022
1 parent 4b542d8 commit 011624e
Show file tree
Hide file tree
Showing 18 changed files with 54 additions and 18 deletions.
4 changes: 3 additions & 1 deletion rflx/templates/rflx_arithmetic.ads
View file
Original file line number Diff line number Diff line change
@@ -1,7 +1,9 @@
pragma Style_Checks ("N3aAbcdefhiIklnOprStux");

package {prefix}RFLX_Arithmetic with
SPARK_Mode
SPARK_Mode,
Annotate =>
(GNATprove, Always_Return)
is

type U64 is mod 2**64 with
Expand Down
4 changes: 3 additions & 1 deletion rflx/templates/rflx_builtin_types-conversions.ads
View file
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,9 @@ pragma Style_Checks ("N3aAbcdefhiIklnOprStux");
with {prefix}RFLX_Arithmetic;

package {prefix}RFLX_Builtin_Types.Conversions with
SPARK_Mode
SPARK_Mode,
Annotate =>
(GNATprove, Always_Return)
is

pragma Annotate (GNATprove, Always_Return, Conversions);
Expand Down
4 changes: 3 additions & 1 deletion rflx/templates/rflx_builtin_types.ads
View file
Original file line number Diff line number Diff line change
@@ -1,7 +1,9 @@
pragma Style_Checks ("N3aAbcdefhiIklnOprStux");

package {prefix}RFLX_Builtin_Types with
SPARK_Mode
SPARK_Mode,
Annotate =>
(GNATprove, Always_Return)
is

type Length is new Natural;
Expand Down
4 changes: 3 additions & 1 deletion rflx/templates/rflx_generic_types.ads
View file
Original file line number Diff line number Diff line change
Expand Up @@ -11,7 +11,9 @@ generic
type Custom_Length is range <>;
type Custom_Bit_Length is range <>;
package {prefix}RFLX_Generic_Types with
SPARK_Mode
SPARK_Mode,
Annotate =>
(GNATprove, Always_Return)
is

subtype Index is Custom_Index;
Expand Down
4 changes: 3 additions & 1 deletion rflx/templates/rflx_message_sequence.ads
View file
Original file line number Diff line number Diff line change
Expand Up @@ -12,7 +12,9 @@ generic
with function Element_Initialized (Ctx : Element_Context) return Boolean;
with function Element_Valid_Message (Ctx : Element_Context) return Boolean;
package {prefix}RFLX_Message_Sequence with
SPARK_Mode
SPARK_Mode,
Annotate =>
(GNATprove, Always_Return)
is

pragma Annotate (GNATprove, Always_Return, RFLX_Message_Sequence);
Expand Down
4 changes: 3 additions & 1 deletion rflx/templates/rflx_scalar_sequence.ads
View file
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,9 @@ generic
with function To_Actual (Element : {prefix}RFLX_Types.Base_Integer) return Element_Type;
with function To_Base_Int (Element : Element_Type) return {prefix}RFLX_Types.Base_Integer;
package {prefix}RFLX_Scalar_Sequence with
SPARK_Mode
SPARK_Mode,
Annotate =>
(GNATprove, Always_Return)
is

pragma Annotate (GNATprove, Always_Return, RFLX_Scalar_Sequence);
Expand Down
4 changes: 3 additions & 1 deletion tests/integration/shared/generated/rflx-rflx_arithmetic.ads
View file
Original file line number Diff line number Diff line change
@@ -1,7 +1,9 @@
pragma Style_Checks ("N3aAbcdefhiIklnOprStux");

package RFLX.RFLX_Arithmetic with
SPARK_Mode
SPARK_Mode,
Annotate =>
(GNATprove, Always_Return)
is

type U64 is mod 2**64 with
Expand Down
4 changes: 3 additions & 1 deletion tests/integration/shared/generated/rflx-rflx_builtin_types-conversions.ads
View file
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,9 @@ pragma Style_Checks ("N3aAbcdefhiIklnOprStux");
with RFLX.RFLX_Arithmetic;

package RFLX.RFLX_Builtin_Types.Conversions with
SPARK_Mode
SPARK_Mode,
Annotate =>
(GNATprove, Always_Return)
is

pragma Annotate (GNATprove, Always_Return, Conversions);
Expand Down
4 changes: 3 additions & 1 deletion tests/integration/shared/generated/rflx-rflx_builtin_types.ads
View file
Original file line number Diff line number Diff line change
@@ -1,7 +1,9 @@
pragma Style_Checks ("N3aAbcdefhiIklnOprStux");

package RFLX.RFLX_Builtin_Types with
SPARK_Mode
SPARK_Mode,
Annotate =>
(GNATprove, Always_Return)
is

type Length is new Natural;
Expand Down
4 changes: 3 additions & 1 deletion tests/integration/shared/generated/rflx-rflx_generic_types.ads
View file
Original file line number Diff line number Diff line change
Expand Up @@ -11,7 +11,9 @@ generic
type Custom_Length is range <>;
type Custom_Bit_Length is range <>;
package RFLX.RFLX_Generic_Types with
SPARK_Mode
SPARK_Mode,
Annotate =>
(GNATprove, Always_Return)
is

subtype Index is Custom_Index;
Expand Down
4 changes: 3 additions & 1 deletion tests/integration/shared/generated/rflx-rflx_message_sequence.ads
View file
Original file line number Diff line number Diff line change
Expand Up @@ -12,7 +12,9 @@ generic
with function Element_Initialized (Ctx : Element_Context) return Boolean;
with function Element_Valid_Message (Ctx : Element_Context) return Boolean;
package RFLX.RFLX_Message_Sequence with
SPARK_Mode
SPARK_Mode,
Annotate =>
(GNATprove, Always_Return)
is

pragma Annotate (GNATprove, Always_Return, RFLX_Message_Sequence);
Expand Down
4 changes: 3 additions & 1 deletion tests/integration/shared/generated/rflx-rflx_scalar_sequence.ads
View file
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,9 @@ generic
with function To_Actual (Element : RFLX.RFLX_Types.Base_Integer) return Element_Type;
with function To_Base_Int (Element : Element_Type) return RFLX.RFLX_Types.Base_Integer;
package RFLX.RFLX_Scalar_Sequence with
SPARK_Mode
SPARK_Mode,
Annotate =>
(GNATprove, Always_Return)
is

pragma Annotate (GNATprove, Always_Return, RFLX_Scalar_Sequence);
Expand Down
4 changes: 3 additions & 1 deletion tests/spark/generated/rflx-rflx_arithmetic.ads
View file
Original file line number Diff line number Diff line change
@@ -1,7 +1,9 @@
pragma Style_Checks ("N3aAbcdefhiIklnOprStux");

package RFLX.RFLX_Arithmetic with
SPARK_Mode
SPARK_Mode,
Annotate =>
(GNATprove, Always_Return)
is

type U64 is mod 2**64 with
Expand Down
4 changes: 3 additions & 1 deletion tests/spark/generated/rflx-rflx_builtin_types-conversions.ads
View file
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,9 @@ pragma Style_Checks ("N3aAbcdefhiIklnOprStux");
with RFLX.RFLX_Arithmetic;

package RFLX.RFLX_Builtin_Types.Conversions with
SPARK_Mode
SPARK_Mode,
Annotate =>
(GNATprove, Always_Return)
is

pragma Annotate (GNATprove, Always_Return, Conversions);
Expand Down
4 changes: 3 additions & 1 deletion tests/spark/generated/rflx-rflx_builtin_types.ads
View file
Original file line number Diff line number Diff line change
@@ -1,7 +1,9 @@
pragma Style_Checks ("N3aAbcdefhiIklnOprStux");

package RFLX.RFLX_Builtin_Types with
SPARK_Mode
SPARK_Mode,
Annotate =>
(GNATprove, Always_Return)
is

type Length is new Natural;
Expand Down
4 changes: 3 additions & 1 deletion tests/spark/generated/rflx-rflx_generic_types.ads
View file
Original file line number Diff line number Diff line change
Expand Up @@ -11,7 +11,9 @@ generic
type Custom_Length is range <>;
type Custom_Bit_Length is range <>;
package RFLX.RFLX_Generic_Types with
SPARK_Mode
SPARK_Mode,
Annotate =>
(GNATprove, Always_Return)
is

subtype Index is Custom_Index;
Expand Down
4 changes: 3 additions & 1 deletion tests/spark/generated/rflx-rflx_message_sequence.ads
View file
Original file line number Diff line number Diff line change
Expand Up @@ -12,7 +12,9 @@ generic
with function Element_Initialized (Ctx : Element_Context) return Boolean;
with function Element_Valid_Message (Ctx : Element_Context) return Boolean;
package RFLX.RFLX_Message_Sequence with
SPARK_Mode
SPARK_Mode,
Annotate =>
(GNATprove, Always_Return)
is

pragma Annotate (GNATprove, Always_Return, RFLX_Message_Sequence);
Expand Down
4 changes: 3 additions & 1 deletion tests/spark/generated/rflx-rflx_scalar_sequence.ads
View file
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,9 @@ generic
with function To_Actual (Element : RFLX.RFLX_Types.Base_Integer) return Element_Type;
with function To_Base_Int (Element : Element_Type) return RFLX.RFLX_Types.Base_Integer;
package RFLX.RFLX_Scalar_Sequence with
SPARK_Mode
SPARK_Mode,
Annotate =>
(GNATprove, Always_Return)
is

pragma Annotate (GNATprove, Always_Return, RFLX_Scalar_Sequence);
Expand Down

0 comments on commit 011624e

Please sign in to comment.