Skip to content

Commit

Permalink
remove unused preconditions
Browse files Browse the repository at this point in the history
  • Loading branch information
@kanigsson
kanigsson committed Jun 16, 2022
1 parent 3eeded7 commit f06fd42
Show file tree
Hide file tree
Showing 56 changed files with 117 additions and 1,335 deletions.
30 changes: 0 additions & 30 deletions rflx/generator/serializer.py
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1624,36 +1624,6 @@ def composite_setter_field_condition_precondition(
def composite_setter_preconditions(field: Field, size: Expr = None) -> List[Expr]:
return [
common.sufficient_space_for_field_condition(Variable(field.affixed_name), size),
Equal(
Mod(
Call(
"Field_First",
[Variable("Ctx"), Variable(field.affixed_name)],
),
Size(const.TYPES_BYTE),
),
Number(1),
),
Equal(
Mod(
Call(
"Field_Last",
[Variable("Ctx"), Variable(field.affixed_name)],
),
Size(const.TYPES_BYTE),
),
Number(0),
),
Equal(
Mod(
Call(
"Field_Size",
[Variable("Ctx"), Variable(field.affixed_name)],
),
Size(const.TYPES_BYTE),
),
Number(0),
),
]

def scalar_setter_and_getter_relation(
Expand Down
47 changes: 4 additions & 43 deletions tests/integration/messages/generated/rflx-universal-message.ads
View file
Original file line number Diff line number Diff line change
Expand Up @@ -562,9 +562,6 @@ is
and then Valid_Next (Ctx, F_Data)
and then Field_Condition (Ctx, F_Data, 0)
and then Available_Space (Ctx, F_Data) >= Field_Size (Ctx, F_Data)
and then Field_First (Ctx, F_Data) mod RFLX_Types.Byte'Size = 1
and then Field_Last (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0
and then Field_Size (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0
and then Field_Size (Ctx, F_Data) = 0,
Post =>
Has_Buffer (Ctx)
Expand All @@ -589,9 +586,6 @@ is
and then Valid_Next (Ctx, F_Option_Types)
and then Field_Condition (Ctx, F_Option_Types, 0)
and then Available_Space (Ctx, F_Option_Types) >= Field_Size (Ctx, F_Option_Types)
and then Field_First (Ctx, F_Option_Types) mod RFLX_Types.Byte'Size = 1
and then Field_Last (Ctx, F_Option_Types) mod RFLX_Types.Byte'Size = 0
and then Field_Size (Ctx, F_Option_Types) mod RFLX_Types.Byte'Size = 0
and then Field_Size (Ctx, F_Option_Types) = 0,
Post =>
Has_Buffer (Ctx)
Expand All @@ -616,9 +610,6 @@ is
and then Valid_Next (Ctx, F_Options)
and then Field_Condition (Ctx, F_Options, 0)
and then Available_Space (Ctx, F_Options) >= Field_Size (Ctx, F_Options)
and then Field_First (Ctx, F_Options) mod RFLX_Types.Byte'Size = 1
and then Field_Last (Ctx, F_Options) mod RFLX_Types.Byte'Size = 0
and then Field_Size (Ctx, F_Options) mod RFLX_Types.Byte'Size = 0
and then Field_Size (Ctx, F_Options) = 0,
Post =>
Has_Buffer (Ctx)
Expand All @@ -641,9 +632,6 @@ is
and then Valid_Next (Ctx, F_Values)
and then Field_Condition (Ctx, F_Values, 0)
and then Available_Space (Ctx, F_Values) >= Field_Size (Ctx, F_Values)
and then Field_First (Ctx, F_Values) mod RFLX_Types.Byte'Size = 1
and then Field_Last (Ctx, F_Values) mod RFLX_Types.Byte'Size = 0
and then Field_Size (Ctx, F_Values) mod RFLX_Types.Byte'Size = 0
and then Field_Size (Ctx, F_Values) = 0,
Post =>
Has_Buffer (Ctx)
Expand All @@ -665,9 +653,6 @@ is
and then Valid_Next (Ctx, F_Option_Types)
and then Field_Condition (Ctx, F_Option_Types, 0)
and then Available_Space (Ctx, F_Option_Types) >= Field_Size (Ctx, F_Option_Types)
and then Field_First (Ctx, F_Option_Types) mod RFLX_Types.Byte'Size = 1
and then Field_Last (Ctx, F_Option_Types) mod RFLX_Types.Byte'Size = 0
and then Field_Size (Ctx, F_Option_Types) mod RFLX_Types.Byte'Size = 0
and then Valid_Length (Ctx, F_Option_Types, Universal.Option_Types.Byte_Size (Seq_Ctx))
and then Universal.Option_Types.Has_Buffer (Seq_Ctx)
and then Universal.Option_Types.Valid (Seq_Ctx),
Expand Down Expand Up @@ -695,9 +680,6 @@ is
and then Valid_Next (Ctx, F_Options)
and then Field_Condition (Ctx, F_Options, 0)
and then Available_Space (Ctx, F_Options) >= Field_Size (Ctx, F_Options)
and then Field_First (Ctx, F_Options) mod RFLX_Types.Byte'Size = 1
and then Field_Last (Ctx, F_Options) mod RFLX_Types.Byte'Size = 0
and then Field_Size (Ctx, F_Options) mod RFLX_Types.Byte'Size = 0
and then Valid_Length (Ctx, F_Options, Universal.Options.Byte_Size (Seq_Ctx))
and then Universal.Options.Has_Buffer (Seq_Ctx)
and then Universal.Options.Valid (Seq_Ctx),
Expand All @@ -723,9 +705,6 @@ is
and then Valid_Next (Ctx, F_Values)
and then Field_Condition (Ctx, F_Values, 0)
and then Available_Space (Ctx, F_Values) >= Field_Size (Ctx, F_Values)
and then Field_First (Ctx, F_Values) mod RFLX_Types.Byte'Size = 1
and then Field_Last (Ctx, F_Values) mod RFLX_Types.Byte'Size = 0
and then Field_Size (Ctx, F_Values) mod RFLX_Types.Byte'Size = 0
and then Valid_Length (Ctx, F_Values, Universal.Values.Byte_Size (Seq_Ctx))
and then Universal.Values.Has_Buffer (Seq_Ctx)
and then Universal.Values.Valid (Seq_Ctx),
Expand All @@ -749,10 +728,7 @@ is
and then Has_Buffer (Ctx)
and then Valid_Next (Ctx, F_Data)
and then Valid_Length (Ctx, F_Data, Length)
and then Available_Space (Ctx, F_Data) >= RFLX_Types.To_Bit_Length (Length)
and then Field_First (Ctx, F_Data) mod RFLX_Types.Byte'Size = 1
and then Field_Last (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0
and then Field_Size (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0,
and then Available_Space (Ctx, F_Data) >= RFLX_Types.To_Bit_Length (Length),
Post =>
Has_Buffer (Ctx)
and Structural_Valid (Ctx, F_Data)
Expand All @@ -775,10 +751,7 @@ is
not Ctx'Constrained
and then Has_Buffer (Ctx)
and then Valid_Next (Ctx, F_Option_Types)
and then Available_Space (Ctx, F_Option_Types) >= Field_Size (Ctx, F_Option_Types)
and then Field_First (Ctx, F_Option_Types) mod RFLX_Types.Byte'Size = 1
and then Field_Last (Ctx, F_Option_Types) mod RFLX_Types.Byte'Size = 0
and then Field_Size (Ctx, F_Option_Types) mod RFLX_Types.Byte'Size = 0,
and then Available_Space (Ctx, F_Option_Types) >= Field_Size (Ctx, F_Option_Types),
Post =>
Has_Buffer (Ctx)
and Structural_Valid (Ctx, F_Option_Types)
Expand All @@ -801,10 +774,7 @@ is
and then Has_Buffer (Ctx)
and then Valid_Next (Ctx, F_Options)
and then Valid_Length (Ctx, F_Options, Length)
and then Available_Space (Ctx, F_Options) >= RFLX_Types.To_Bit_Length (Length)
and then Field_First (Ctx, F_Options) mod RFLX_Types.Byte'Size = 1
and then Field_Last (Ctx, F_Options) mod RFLX_Types.Byte'Size = 0
and then Field_Size (Ctx, F_Options) mod RFLX_Types.Byte'Size = 0,
and then Available_Space (Ctx, F_Options) >= RFLX_Types.To_Bit_Length (Length),
Post =>
Has_Buffer (Ctx)
and Structural_Valid (Ctx, F_Options)
Expand All @@ -825,10 +795,7 @@ is
not Ctx'Constrained
and then Has_Buffer (Ctx)
and then Valid_Next (Ctx, F_Values)
and then Available_Space (Ctx, F_Values) >= Field_Size (Ctx, F_Values)
and then Field_First (Ctx, F_Values) mod RFLX_Types.Byte'Size = 1
and then Field_Last (Ctx, F_Values) mod RFLX_Types.Byte'Size = 0
and then Field_Size (Ctx, F_Values) mod RFLX_Types.Byte'Size = 0,
and then Available_Space (Ctx, F_Values) >= Field_Size (Ctx, F_Values),
Post =>
Has_Buffer (Ctx)
and Structural_Valid (Ctx, F_Values)
Expand All @@ -848,9 +815,6 @@ is
and then Has_Buffer (Ctx)
and then Valid_Next (Ctx, F_Data)
and then Available_Space (Ctx, F_Data) >= Field_Size (Ctx, F_Data)
and then Field_First (Ctx, F_Data) mod RFLX_Types.Byte'Size = 1
and then Field_Last (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0
and then Field_Size (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0
and then Valid_Length (Ctx, F_Data, Data'Length)
and then Available_Space (Ctx, F_Data) >= Data'Length * RFLX_Types.Byte'Size
and then Field_Condition (Ctx, F_Data, 0),
Expand Down Expand Up @@ -880,9 +844,6 @@ is
and then Has_Buffer (Ctx)
and then Valid_Next (Ctx, F_Data)
and then Available_Space (Ctx, F_Data) >= Field_Size (Ctx, F_Data)
and then Field_First (Ctx, F_Data) mod RFLX_Types.Byte'Size = 1
and then Field_Last (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0
and then Field_Size (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0
and then Valid_Length (Ctx, F_Data, Length)
and then RFLX_Types.To_Length (Available_Space (Ctx, F_Data)) >= Length
and then Process_Data_Pre (Length),
Expand Down
14 changes: 1 addition & 13 deletions tests/integration/messages/generated/rflx-universal-option.ads
View file
Original file line number Diff line number Diff line change
Expand Up @@ -485,9 +485,6 @@ is
and then Valid_Next (Ctx, F_Data)
and then Field_Condition (Ctx, F_Data, 0)
and then Available_Space (Ctx, F_Data) >= Field_Size (Ctx, F_Data)
and then Field_First (Ctx, F_Data) mod RFLX_Types.Byte'Size = 1
and then Field_Last (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0
and then Field_Size (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0
and then Field_Size (Ctx, F_Data) = 0,
Post =>
Has_Buffer (Ctx)
Expand All @@ -507,10 +504,7 @@ is
not Ctx'Constrained
and then Has_Buffer (Ctx)
and then Valid_Next (Ctx, F_Data)
and then Available_Space (Ctx, F_Data) >= Field_Size (Ctx, F_Data)
and then Field_First (Ctx, F_Data) mod RFLX_Types.Byte'Size = 1
and then Field_Last (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0
and then Field_Size (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0,
and then Available_Space (Ctx, F_Data) >= Field_Size (Ctx, F_Data),
Post =>
Has_Buffer (Ctx)
and Structural_Valid (Ctx, F_Data)
Expand All @@ -530,9 +524,6 @@ is
and then Has_Buffer (Ctx)
and then Valid_Next (Ctx, F_Data)
and then Available_Space (Ctx, F_Data) >= Field_Size (Ctx, F_Data)
and then Field_First (Ctx, F_Data) mod RFLX_Types.Byte'Size = 1
and then Field_Last (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0
and then Field_Size (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0
and then Valid_Length (Ctx, F_Data, Data'Length)
and then Available_Space (Ctx, F_Data) >= Data'Length * RFLX_Types.Byte'Size
and then Field_Condition (Ctx, F_Data, 0),
Expand All @@ -559,9 +550,6 @@ is
and then Has_Buffer (Ctx)
and then Valid_Next (Ctx, F_Data)
and then Available_Space (Ctx, F_Data) >= Field_Size (Ctx, F_Data)
and then Field_First (Ctx, F_Data) mod RFLX_Types.Byte'Size = 1
and then Field_Last (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0
and then Field_Size (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0
and then Valid_Length (Ctx, F_Data, Length)
and then RFLX_Types.To_Length (Available_Space (Ctx, F_Data)) >= Length
and then Process_Data_Pre (Length),
Expand Down
47 changes: 4 additions & 43 deletions tests/integration/messages_with_implict_size/generated/rflx-universal-message.ads
View file
Original file line number Diff line number Diff line change
Expand Up @@ -562,9 +562,6 @@ is
and then Valid_Next (Ctx, F_Data)
and then Field_Condition (Ctx, F_Data, 0)
and then Available_Space (Ctx, F_Data) >= Field_Size (Ctx, F_Data)
and then Field_First (Ctx, F_Data) mod RFLX_Types.Byte'Size = 1
and then Field_Last (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0
and then Field_Size (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0
and then Field_Size (Ctx, F_Data) = 0,
Post =>
Has_Buffer (Ctx)
Expand All @@ -589,9 +586,6 @@ is
and then Valid_Next (Ctx, F_Option_Types)
and then Field_Condition (Ctx, F_Option_Types, 0)
and then Available_Space (Ctx, F_Option_Types) >= Field_Size (Ctx, F_Option_Types)
and then Field_First (Ctx, F_Option_Types) mod RFLX_Types.Byte'Size = 1
and then Field_Last (Ctx, F_Option_Types) mod RFLX_Types.Byte'Size = 0
and then Field_Size (Ctx, F_Option_Types) mod RFLX_Types.Byte'Size = 0
and then Field_Size (Ctx, F_Option_Types) = 0,
Post =>
Has_Buffer (Ctx)
Expand All @@ -616,9 +610,6 @@ is
and then Valid_Next (Ctx, F_Options)
and then Field_Condition (Ctx, F_Options, 0)
and then Available_Space (Ctx, F_Options) >= Field_Size (Ctx, F_Options)
and then Field_First (Ctx, F_Options) mod RFLX_Types.Byte'Size = 1
and then Field_Last (Ctx, F_Options) mod RFLX_Types.Byte'Size = 0
and then Field_Size (Ctx, F_Options) mod RFLX_Types.Byte'Size = 0
and then Field_Size (Ctx, F_Options) = 0,
Post =>
Has_Buffer (Ctx)
Expand All @@ -641,9 +632,6 @@ is
and then Valid_Next (Ctx, F_Values)
and then Field_Condition (Ctx, F_Values, 0)
and then Available_Space (Ctx, F_Values) >= Field_Size (Ctx, F_Values)
and then Field_First (Ctx, F_Values) mod RFLX_Types.Byte'Size = 1
and then Field_Last (Ctx, F_Values) mod RFLX_Types.Byte'Size = 0
and then Field_Size (Ctx, F_Values) mod RFLX_Types.Byte'Size = 0
and then Field_Size (Ctx, F_Values) = 0,
Post =>
Has_Buffer (Ctx)
Expand All @@ -665,9 +653,6 @@ is
and then Valid_Next (Ctx, F_Option_Types)
and then Field_Condition (Ctx, F_Option_Types, 0)
and then Available_Space (Ctx, F_Option_Types) >= Field_Size (Ctx, F_Option_Types)
and then Field_First (Ctx, F_Option_Types) mod RFLX_Types.Byte'Size = 1
and then Field_Last (Ctx, F_Option_Types) mod RFLX_Types.Byte'Size = 0
and then Field_Size (Ctx, F_Option_Types) mod RFLX_Types.Byte'Size = 0
and then Valid_Length (Ctx, F_Option_Types, Universal.Option_Types.Byte_Size (Seq_Ctx))
and then Universal.Option_Types.Has_Buffer (Seq_Ctx)
and then Universal.Option_Types.Valid (Seq_Ctx),
Expand Down Expand Up @@ -695,9 +680,6 @@ is
and then Valid_Next (Ctx, F_Options)
and then Field_Condition (Ctx, F_Options, 0)
and then Available_Space (Ctx, F_Options) >= Field_Size (Ctx, F_Options)
and then Field_First (Ctx, F_Options) mod RFLX_Types.Byte'Size = 1
and then Field_Last (Ctx, F_Options) mod RFLX_Types.Byte'Size = 0
and then Field_Size (Ctx, F_Options) mod RFLX_Types.Byte'Size = 0
and then Valid_Length (Ctx, F_Options, Universal.Options.Byte_Size (Seq_Ctx))
and then Universal.Options.Has_Buffer (Seq_Ctx)
and then Universal.Options.Valid (Seq_Ctx),
Expand All @@ -723,9 +705,6 @@ is
and then Valid_Next (Ctx, F_Values)
and then Field_Condition (Ctx, F_Values, 0)
and then Available_Space (Ctx, F_Values) >= Field_Size (Ctx, F_Values)
and then Field_First (Ctx, F_Values) mod RFLX_Types.Byte'Size = 1
and then Field_Last (Ctx, F_Values) mod RFLX_Types.Byte'Size = 0
and then Field_Size (Ctx, F_Values) mod RFLX_Types.Byte'Size = 0
and then Valid_Length (Ctx, F_Values, Universal.Values.Byte_Size (Seq_Ctx))
and then Universal.Values.Has_Buffer (Seq_Ctx)
and then Universal.Values.Valid (Seq_Ctx),
Expand All @@ -749,10 +728,7 @@ is
and then Has_Buffer (Ctx)
and then Valid_Next (Ctx, F_Data)
and then Valid_Length (Ctx, F_Data, Length)
and then Available_Space (Ctx, F_Data) >= RFLX_Types.To_Bit_Length (Length)
and then Field_First (Ctx, F_Data) mod RFLX_Types.Byte'Size = 1
and then Field_Last (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0
and then Field_Size (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0,
and then Available_Space (Ctx, F_Data) >= RFLX_Types.To_Bit_Length (Length),
Post =>
Has_Buffer (Ctx)
and Structural_Valid (Ctx, F_Data)
Expand All @@ -775,10 +751,7 @@ is
not Ctx'Constrained
and then Has_Buffer (Ctx)
and then Valid_Next (Ctx, F_Option_Types)
and then Available_Space (Ctx, F_Option_Types) >= Field_Size (Ctx, F_Option_Types)
and then Field_First (Ctx, F_Option_Types) mod RFLX_Types.Byte'Size = 1
and then Field_Last (Ctx, F_Option_Types) mod RFLX_Types.Byte'Size = 0
and then Field_Size (Ctx, F_Option_Types) mod RFLX_Types.Byte'Size = 0,
and then Available_Space (Ctx, F_Option_Types) >= Field_Size (Ctx, F_Option_Types),
Post =>
Has_Buffer (Ctx)
and Structural_Valid (Ctx, F_Option_Types)
Expand All @@ -801,10 +774,7 @@ is
and then Has_Buffer (Ctx)
and then Valid_Next (Ctx, F_Options)
and then Valid_Length (Ctx, F_Options, Length)
and then Available_Space (Ctx, F_Options) >= RFLX_Types.To_Bit_Length (Length)
and then Field_First (Ctx, F_Options) mod RFLX_Types.Byte'Size = 1
and then Field_Last (Ctx, F_Options) mod RFLX_Types.Byte'Size = 0
and then Field_Size (Ctx, F_Options) mod RFLX_Types.Byte'Size = 0,
and then Available_Space (Ctx, F_Options) >= RFLX_Types.To_Bit_Length (Length),
Post =>
Has_Buffer (Ctx)
and Structural_Valid (Ctx, F_Options)
Expand All @@ -825,10 +795,7 @@ is
not Ctx'Constrained
and then Has_Buffer (Ctx)
and then Valid_Next (Ctx, F_Values)
and then Available_Space (Ctx, F_Values) >= Field_Size (Ctx, F_Values)
and then Field_First (Ctx, F_Values) mod RFLX_Types.Byte'Size = 1
and then Field_Last (Ctx, F_Values) mod RFLX_Types.Byte'Size = 0
and then Field_Size (Ctx, F_Values) mod RFLX_Types.Byte'Size = 0,
and then Available_Space (Ctx, F_Values) >= Field_Size (Ctx, F_Values),
Post =>
Has_Buffer (Ctx)
and Structural_Valid (Ctx, F_Values)
Expand All @@ -848,9 +815,6 @@ is
and then Has_Buffer (Ctx)
and then Valid_Next (Ctx, F_Data)
and then Available_Space (Ctx, F_Data) >= Field_Size (Ctx, F_Data)
and then Field_First (Ctx, F_Data) mod RFLX_Types.Byte'Size = 1
and then Field_Last (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0
and then Field_Size (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0
and then Valid_Length (Ctx, F_Data, Data'Length)
and then Available_Space (Ctx, F_Data) >= Data'Length * RFLX_Types.Byte'Size
and then Field_Condition (Ctx, F_Data, 0),
Expand Down Expand Up @@ -880,9 +844,6 @@ is
and then Has_Buffer (Ctx)
and then Valid_Next (Ctx, F_Data)
and then Available_Space (Ctx, F_Data) >= Field_Size (Ctx, F_Data)
and then Field_First (Ctx, F_Data) mod RFLX_Types.Byte'Size = 1
and then Field_Last (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0
and then Field_Size (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0
and then Valid_Length (Ctx, F_Data, Length)
and then RFLX_Types.To_Length (Available_Space (Ctx, F_Data)) >= Length
and then Process_Data_Pre (Length),
Expand Down
Loading

0 comments on commit f06fd42

Please sign in to comment.