Skip to content

Commit

Permalink
Change code generation to support recent GNATprove versions
Browse files Browse the repository at this point in the history 
Ref. #494
  • Loading branch information
@treiher
treiher committed Mar 9, 2021
1 parent 39bc205 commit 7d15e9f
Show file tree
Hide file tree
Showing 38 changed files with 3,330 additions and 3,327 deletions.
26 changes: 14 additions & 12 deletions rflx/generator/generator.py
View file
Original file line number Diff line number Diff line change
Expand Up @@ -826,7 +826,7 @@ def __create_initialized_function(message: Message) -> UnitPart:

return UnitPart(
[SubprogramDeclaration(specification, [Ghost()])],
[
private=[
ExpressionFunctionDeclaration(
specification,
AndThen(
Expand Down Expand Up @@ -945,7 +945,7 @@ def condition(field: Field, message: Message) -> Expr:
],
)
],
[
private=[
ExpressionFunctionDeclaration(
specification,
Case(
Expand Down Expand Up @@ -1022,7 +1022,7 @@ def substituted(expression: expr.Expr) -> Expr:
],
)
],
[
private=[
ExpressionFunctionDeclaration(
specification,
Case(
Expand Down Expand Up @@ -1108,7 +1108,7 @@ def substituted(
],
)
],
[
private=[
ExpressionFunctionDeclaration(
specification,
Case(
Expand Down Expand Up @@ -1144,7 +1144,7 @@ def __create_field_last_function() -> UnitPart:
],
)
],
[
private=[
ExpressionFunctionDeclaration(
specification,
Add(
Expand Down Expand Up @@ -1211,7 +1211,7 @@ def condition(field: Field, message: Message) -> Expr:
],
)
],
[
private=[
ExpressionFunctionDeclaration(
specification,
Case(
Expand All @@ -1235,7 +1235,7 @@ def __create_predecessor_function() -> UnitPart:

return UnitPart(
[SubprogramDeclaration(specification)],
[
private=[
ExpressionFunctionDeclaration(
specification,
Case(
Expand Down Expand Up @@ -1533,7 +1533,9 @@ def __create_has_buffer_function() -> UnitPart:

return UnitPart(
[SubprogramDeclaration(specification)],
[ExpressionFunctionDeclaration(specification, NotEqual(Variable("Ctx.Buffer"), NULL))],
private=[
ExpressionFunctionDeclaration(specification, NotEqual(Variable("Ctx.Buffer"), NULL))
],
)

@staticmethod
Expand All @@ -1549,7 +1551,7 @@ def __create_valid_predecessor_function(

return UnitPart(
[SubprogramDeclaration(specification)],
[
private=[
ExpressionFunctionDeclaration(
specification,
Case(
Expand Down Expand Up @@ -1623,7 +1625,7 @@ def __create_available_space_function() -> UnitPart:
[Precondition(Call("Valid_Next", [Variable("Ctx"), Variable("Fld")]))],
)
],
[
private=[
ExpressionFunctionDeclaration(
specification,
Add(
Expand Down Expand Up @@ -2002,7 +2004,7 @@ def specification(field: Field) -> FunctionSpecification:
)
for f in sequence_fields
],
[
private=[
ExpressionFunctionDeclaration(
specification(f),
And(
Expand Down Expand Up @@ -2865,7 +2867,7 @@ def __create_valid_next_function() -> UnitPart:

return UnitPart(
[SubprogramDeclaration(specification)],
[
private=[
ExpressionFunctionDeclaration(
specification,
AndThen(
Expand Down
18 changes: 9 additions & 9 deletions rflx/generator/parser.py
View file
Original file line number Diff line number Diff line change
Expand Up @@ -421,7 +421,7 @@ def create_present_function() -> UnitPart:

return UnitPart(
[SubprogramDeclaration(specification)],
[
private=[
ExpressionFunctionDeclaration(
specification,
AndThen(
Expand Down Expand Up @@ -450,7 +450,7 @@ def create_structural_valid_function() -> UnitPart:

return UnitPart(
[SubprogramDeclaration(specification)],
[
private=[
ExpressionFunctionDeclaration(
specification,
And(
Expand Down Expand Up @@ -500,7 +500,7 @@ def create_valid_function() -> UnitPart:
],
)
],
[
private=[
ExpressionFunctionDeclaration(
specification,
AndThen(
Expand Down Expand Up @@ -528,7 +528,7 @@ def create_incomplete_function() -> UnitPart:

return UnitPart(
[SubprogramDeclaration(specification)],
[
private=[
ExpressionFunctionDeclaration(
specification,
Equal(
Expand All @@ -547,7 +547,7 @@ def create_invalid_function() -> UnitPart:

return UnitPart(
[SubprogramDeclaration(specification)],
[
private=[
ExpressionFunctionDeclaration(
specification,
Or(
Expand Down Expand Up @@ -577,7 +577,7 @@ def create_structural_valid_message_function(message: Message) -> UnitPart:
[Precondition(Call("Has_Buffer", [Variable("Ctx")]))],
)
],
[
private=[
ExpressionFunctionDeclaration(
specification,
valid_message_condition(message, structural=True),
Expand All @@ -598,7 +598,7 @@ def create_valid_message_function(message: Message) -> UnitPart:
[Precondition(Call("Has_Buffer", [Variable("Ctx")]))],
)
],
[
private=[
ExpressionFunctionDeclaration(
specification,
valid_message_condition(message),
Expand All @@ -614,7 +614,7 @@ def create_incomplete_message_function(message: Message) -> UnitPart:

return UnitPart(
[SubprogramDeclaration(specification)],
[
private=[
ExpressionFunctionDeclaration(
specification,
Or(
Expand Down Expand Up @@ -669,7 +669,7 @@ def result(field: Field) -> Expr:
],
Pragma("Warnings", [Variable("On"), String("precondition is always False")]),
],
[
private=[
ExpressionFunctionDeclaration(specification(f, t), result(f))
for f, t in scalar_fields.items()
],
Expand Down
5 changes: 2 additions & 3 deletions rflx/templates/rflx_generic_types.adb
View file
Original file line number Diff line number Diff line change
Expand Up @@ -142,9 +142,8 @@ is
LSE_Offset,
Byte'Size * Natural (I - LSE_Index));
pragma Loop_Invariant (I - LSE_Index <= 7);
pragma Loop_Invariant (if Byte'Size + Byte'Size * (I - LSE_Index) = U64'Size
then Result <= U64'Last
else Result < 2**(Byte'Size + Byte'Size * Natural (I - LSE_Index)));
pragma Loop_Invariant (if Byte'Size + Byte'Size * (I - LSE_Index) /= U64'Size
then Result < 2**(Byte'Size + Byte'Size * Natural (I - LSE_Index)));
end loop;

if MSE_Size > LSE_Offset then
Expand Down
9 changes: 0 additions & 9 deletions rflx/templates/rflx_message_sequence.adb
View file
Original file line number Diff line number Diff line change
Expand Up @@ -30,9 +30,6 @@ is
end if;
end Copy;

function Has_Element (Ctx : Context) return Boolean is
(Ctx.State = S_Valid and Ctx.Sequence_Last < Ctx.Last);

procedure Switch (Ctx : in out Context; Element_Ctx : out Element_Context) is
Buffer : Types.Bytes_Ptr := Ctx.Buffer;
begin
Expand All @@ -59,10 +56,4 @@ is
end if;
end Update;

function Valid (Ctx : Context) return Boolean is
(Ctx.State = S_Valid);

function Has_Buffer (Ctx : Context) return Boolean is
(Ctx.Buffer /= null);

end {prefix}RFLX_Message_Sequence;
9 changes: 9 additions & 0 deletions rflx/templates/rflx_message_sequence.ads
View file
Original file line number Diff line number Diff line change
Expand Up @@ -189,6 +189,15 @@ private
and Sequence_Last >= First - 1
and Sequence_Last <= Last);

function Has_Element (Ctx : Context) return Boolean is
(Ctx.State = S_Valid and Ctx.Sequence_Last < Ctx.Last);

function Valid (Ctx : Context) return Boolean is
(Ctx.State = S_Valid);

function Has_Buffer (Ctx : Context) return Boolean is
(Ctx.Buffer /= null);

function Sequence_Last (Ctx : Context) return Types.Bit_Length is
(Ctx.Sequence_Last);

Expand Down
12 changes: 0 additions & 12 deletions rflx/templates/rflx_scalar_sequence.adb
View file
Original file line number Diff line number Diff line change
Expand Up @@ -54,12 +54,6 @@ is
Ctx.Sequence_Last := Ctx.Sequence_Last + Element_Base_Type'Size;
end Next;

function Has_Element (Ctx : Context) return Boolean is
(Ctx.State = S_Valid and Ctx.Last - Ctx.Sequence_Last >= Element_Base_Type'Size);

function Valid_Element (Ctx : Context) return Boolean is
(Ctx.State = S_Valid and Valid (Ctx.Next_Element));

function Get_Element (Ctx : Context) return Element_Type is
(To_Actual (Ctx.Next_Element));

Expand All @@ -80,10 +74,4 @@ is
Ctx.Sequence_Last := Ctx.Sequence_Last + Element_Base_Type'Size;
end Append_Element;

function Valid (Ctx : Context) return Boolean is
(Ctx.State = S_Valid);

function Has_Buffer (Ctx : Context) return Boolean is
(Ctx.Buffer /= null);

end {prefix}RFLX_Scalar_Sequence;
16 changes: 14 additions & 2 deletions rflx/templates/rflx_scalar_sequence.ads
View file
Original file line number Diff line number Diff line change
Expand Up @@ -173,11 +173,23 @@ private
and Sequence_Last >= First - 1
and Sequence_Last <= Last);

function Has_Element (Ctx : Context) return Boolean is
(Ctx.State = S_Valid and Ctx.Last - Ctx.Sequence_Last >= Element_Base_Type'Size);

function Valid_Element (Ctx : Context) return Boolean is
(Ctx.State = S_Valid and Valid (Ctx.Next_Element));

function Valid (Ctx : Context) return Boolean is
(Ctx.State = S_Valid);

function Has_Buffer (Ctx : Context) return Boolean is
(Ctx.Buffer /= null);

function Sequence_Last (Ctx : Context) return Types.Bit_Length is
(Ctx.Sequence_Last);
(Ctx.Sequence_Last);

function Size (Ctx : Context) return Types.Bit_Length is
(Ctx.Sequence_Last - Ctx.First + 1);
(Ctx.Sequence_Last - Ctx.First + 1);

function Byte_Size (Ctx : Context) return Types.Length is
(if
Expand Down
Loading

0 comments on commit 7d15e9f

Please sign in to comment.