From 92704a264150fc3d2946b0414072c4d9292125cb Mon Sep 17 00:00:00 2001 From: Johannes Kanig Date: Thu, 17 Feb 2022 10:08:12 +0900 Subject: [PATCH] disable inlining via trivial postconditions To improve gnatprove performance --- rflx/generator/generator.py | 105 ++++++++++++++---- rflx/generator/parser.py | 13 ++- rflx/generator/serializer.py | 15 ++- .../generated/rflx-universal-message.ads | 73 ++++++++++-- .../generated/rflx-universal-option.ads | 73 ++++++++++-- .../generated/rflx-universal-message.ads | 73 ++++++++++-- .../generated/rflx-universal-option.ads | 73 ++++++++++-- .../generated/rflx-test-message.ads | 73 ++++++++++-- .../generated/rflx-universal-message.ads | 73 ++++++++++-- .../generated/rflx-universal-option.ads | 73 ++++++++++-- .../generated/rflx-universal-message.ads | 73 ++++++++++-- .../generated/rflx-universal-option.ads | 73 ++++++++++-- .../generated/rflx-universal-message.ads | 73 ++++++++++-- .../generated/rflx-universal-option.ads | 73 ++++++++++-- .../generated/rflx-universal-message.ads | 73 ++++++++++-- .../generated/rflx-universal-option.ads | 73 ++++++++++-- .../generated/rflx-universal-message.ads | 73 ++++++++++-- .../generated/rflx-universal-option.ads | 73 ++++++++++-- .../generated/rflx-universal-message.ads | 73 ++++++++++-- .../generated/rflx-universal-option.ads | 73 ++++++++++-- .../generated/rflx-universal-message.ads | 73 ++++++++++-- .../generated/rflx-universal-option.ads | 73 ++++++++++-- .../generated/rflx-messages-msg.ads | 73 ++++++++++-- .../generated/rflx-messages-msg_le.ads | 73 ++++++++++-- .../generated/rflx-messages-msg_le_nested.ads | 73 ++++++++++-- .../rflx-fixed_size-simple_message.ads | 73 ++++++++++-- .../generated/rflx-universal-message.ads | 73 ++++++++++-- .../generated/rflx-universal-option.ads | 73 ++++++++++-- .../generated/rflx-universal-message.ads | 73 ++++++++++-- .../generated/rflx-universal-option.ads | 73 ++++++++++-- .../generated/rflx-universal-message.ads | 73 ++++++++++-- .../generated/rflx-universal-option.ads | 73 ++++++++++-- .../generated/rflx-universal-message.ads | 73 ++++++++++-- .../generated/rflx-universal-option.ads | 73 ++++++++++-- .../generated/rflx-universal-message.ads | 73 ++++++++++-- .../generated/rflx-universal-option.ads | 73 ++++++++++-- .../generated/rflx-tlv-message.ads | 73 ++++++++++-- .../generated/rflx-universal-message.ads | 73 ++++++++++-- .../generated/rflx-universal-option.ads | 73 ++++++++++-- .../generated/rflx-universal-message.ads | 73 ++++++++++-- .../generated/rflx-universal-option.ads | 73 ++++++++++-- .../generated/rflx-derivation-message.ads | 73 ++++++++++-- .../generated/rflx-enumeration-message.ads | 73 ++++++++++-- tests/spark/generated/rflx-ethernet-frame.ads | 73 ++++++++++-- .../generated/rflx-expression-message.ads | 73 ++++++++++-- .../rflx-fixed_size-simple_message.ads | 73 ++++++++++-- tests/spark/generated/rflx-icmp-message.ads | 73 ++++++++++-- tests/spark/generated/rflx-ipv4-option.ads | 73 ++++++++++-- tests/spark/generated/rflx-ipv4-packet.ads | 73 ++++++++++-- .../generated/rflx-sequence-inner_message.ads | 73 ++++++++++-- .../spark/generated/rflx-sequence-message.ads | 73 ++++++++++-- .../rflx-sequence-messages_message.ads | 73 ++++++++++-- ...-sequence_size_defined_by_message_size.ads | 73 ++++++++++-- tests/spark/generated/rflx-tlv-message.ads | 73 ++++++++++-- tests/spark/generated/rflx-udp-datagram.ads | 73 ++++++++++-- 55 files changed, 3438 insertions(+), 491 deletions(-) diff --git a/rflx/generator/generator.py b/rflx/generator/generator.py index 03a99709a..a09ed37a6 100644 --- a/rflx/generator/generator.py +++ b/rflx/generator/generator.py @@ -525,6 +525,11 @@ def __create_cursor_type(message: Message) -> UnitPart: PrivateType("Field_Cursors", aspects=[DefaultInitialCondition(FALSE)]), ], private=[ + # WORKAROUND: Componolit/Workarounds#47 + Pragma( + "Warnings", + [Variable("Off"), String("postcondition does not mention function result")], + ), ExpressionFunctionDeclaration( FunctionSpecification( "Valid_Value", "Boolean", [Parameter(["Val"], "Field_Dependent_Value")] @@ -545,6 +550,11 @@ def __create_cursor_type(message: Message) -> UnitPart: (Variable(FINAL.affixed_name), FALSE), ], ), + [Postcondition(TRUE)], + ), + Pragma( + "Warnings", + [Variable("On"), String("postcondition does not mention function result")], ), RecordType( "Field_Cursor", @@ -1039,7 +1049,18 @@ def __create_initialized_function(message: Message) -> UnitPart: first_field = message.fields[0] return UnitPart( - [SubprogramDeclaration(specification, [Ghost()])], + [ + # WORKAROUND: Componolit/Workarounds#47 + Pragma( + "Warnings", + [Variable("Off"), String("postcondition does not mention function result")], + ), + SubprogramDeclaration(specification, [Ghost(), Postcondition(TRUE)]), + Pragma( + "Warnings", + [Variable("On"), String("postcondition does not mention function result")], + ), + ], private=[ ExpressionFunctionDeclaration( specification, @@ -1673,6 +1694,11 @@ def condition(field: Field, message: Message) -> Expr: return UnitPart( [ + # WORKAROUND Compolonit/Workarounds#47 + Pragma( + "Warnings", + [Variable("Off"), String("postcondition does not mention function result")], + ), SubprogramDeclaration( specification, [ @@ -1680,9 +1706,14 @@ def condition(field: Field, message: Message) -> Expr: And( Call("Valid_Predecessor", [Variable("Ctx"), Variable("Fld")]), ) - ) + ), + Postcondition(TRUE), ], - ) + ), + Pragma( + "Warnings", + [Variable("On"), String("postcondition does not mention function result")], + ), ], private=[ ExpressionFunctionDeclaration( @@ -1875,6 +1906,11 @@ def substituted( return UnitPart( [ + # WORKAROUND Compolonit/Workarounds#47 + Pragma( + "Warnings", + [Variable("Off"), String("postcondition does not mention function result")], + ), SubprogramDeclaration( specification, [ @@ -1882,9 +1918,14 @@ def substituted( And( Call("Valid_Next", [Variable("Ctx"), Variable("Fld")]), ) - ) + ), + Postcondition(TRUE), ], - ) + ), + Pragma( + "Warnings", + [Variable("On"), String("postcondition does not mention function result")], + ), ], private=[ ExpressionFunctionDeclaration( @@ -2021,6 +2062,11 @@ def condition(field: Field, message: Message) -> Expr: return UnitPart( [ + # WORKAROUND Compolonit/Workarounds#47 + Pragma( + "Warnings", + [Variable("Off"), String("postcondition does not mention function result")], + ), SubprogramDeclaration( specification, [ @@ -2030,9 +2076,14 @@ def condition(field: Field, message: Message) -> Expr: In(Variable("Val.Fld"), Range("Field")), Call("Valid_Predecessor", [Variable("Ctx"), Variable("Val.Fld")]), ) - ) + ), + Postcondition(TRUE), ], - ) + ), + Pragma( + "Warnings", + [Variable("On"), String("postcondition does not mention function result")], + ), ], private=[ ExpressionFunctionDeclaration( @@ -2057,7 +2108,18 @@ def __create_predecessor_function() -> UnitPart: ) return UnitPart( - [SubprogramDeclaration(specification)], + [ + # WORKAROUND Compolonit/Workarounds#47 + Pragma( + "Warnings", + [Variable("Off"), String("postcondition does not mention function result")], + ), + SubprogramDeclaration(specification, [Postcondition(TRUE)]), + Pragma( + "Warnings", + [Variable("On"), String("postcondition does not mention function result")], + ), + ], private=[ ExpressionFunctionDeclaration( specification, @@ -2399,7 +2461,18 @@ def __create_valid_predecessor_function( ) return UnitPart( - [SubprogramDeclaration(specification)], + [ + # WORKAROUND Compolonit/Workarounds#47 + Pragma( + "Warnings", + [Variable("Off"), String("postcondition does not mention function result")], + ), + SubprogramDeclaration(specification, [Postcondition(TRUE)]), + Pragma( + "Warnings", + [Variable("On"), String("postcondition does not mention function result")], + ), + ], private=[ ExpressionFunctionDeclaration( specification, @@ -3254,15 +3327,10 @@ def __create_valid_context_function( String('"Buffer" is not modified, could be of access constant type'), ], ), - # We want to avoid inlining of the context predicate for proof. The way to do - # that in SPARK Pro 23.x is to add a dummy postcondition ("True"). We silence - # the warning that this dummy postcondition doesn't mention the function result. + # WORKAROUND: Componolit/Workarounds#47 Pragma( "Warnings", - [ - Variable("Off"), - String("postcondition does not mention function result"), - ], + [Variable("Off"), String("postcondition does not mention function result")], ), ExpressionFunctionDeclaration( specification, @@ -3278,10 +3346,7 @@ def __create_valid_context_function( ), Pragma( "Warnings", - [ - Variable("On"), - String("postcondition does not mention function result"), - ], + [Variable("On"), String("postcondition does not mention function result")], ), ], ) diff --git a/rflx/generator/parser.py b/rflx/generator/parser.py index 7cc20a3ea..1828205ed 100644 --- a/rflx/generator/parser.py +++ b/rflx/generator/parser.py @@ -678,7 +678,18 @@ def create_incomplete_message_function(message: Message) -> UnitPart: ) return UnitPart( - [SubprogramDeclaration(specification)], + [ + # WORKAROUND Compolonit/Workarounds#47 + Pragma( + "Warnings", + [Variable("Off"), String("postcondition does not mention function result")], + ), + SubprogramDeclaration(specification, [Postcondition(TRUE)]), + Pragma( + "Warnings", + [Variable("On"), String("postcondition does not mention function result")], + ), + ], private=[ ExpressionFunctionDeclaration( specification, diff --git a/rflx/generator/serializer.py b/rflx/generator/serializer.py index 8a50ce133..2dc82e117 100644 --- a/rflx/generator/serializer.py +++ b/rflx/generator/serializer.py @@ -45,6 +45,7 @@ OutParameter, Parameter, Postcondition, + Pragma, PragmaStatement, Precondition, ProcedureSpecification, @@ -326,6 +327,11 @@ def substituted(expression: expr.Expr) -> Expr: return UnitPart( [ + # WORKAROUND Compolonit/Workarounds#47 + Pragma( + "Warnings", + [Variable("Off"), String("postcondition does not mention function result")], + ), SubprogramDeclaration( specification, [ @@ -333,9 +339,14 @@ def substituted(expression: expr.Expr) -> Expr: And( Call("Valid_Next", [Variable("Ctx"), Variable("Fld")]), ) - ) + ), + Postcondition(TRUE), ], - ) + ), + Pragma( + "Warnings", + [Variable("On"), String("postcondition does not mention function result")], + ), ], private=[ ExpressionFunctionDeclaration( diff --git a/tests/integration/messages/generated/rflx-universal-message.ads b/tests/integration/messages/generated/rflx-universal-message.ads index 489b50a8f..b70fa9f65 100644 --- a/tests/integration/messages/generated/rflx-universal-message.ads +++ b/tests/integration/messages/generated/rflx-universal-message.ads @@ -115,8 +115,14 @@ is Depends => (Ctx => (Buffer, First, Last, Written_Last), Buffer => null); + pragma Warnings (Off, "postcondition does not mention function result"); + function Initialized (Ctx : Context) return Boolean with - Ghost; + Ghost, + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); procedure Reset (Ctx : in out Context) with Pre => @@ -246,15 +252,27 @@ is and then Structural_Valid_Message (Ctx) and then Data'Length = Byte_Size (Ctx); + pragma Warnings (Off, "postcondition does not mention function result"); + function Path_Condition (Ctx : Context; Fld : Field) return Boolean with Pre => - Valid_Predecessor (Ctx, Fld); + Valid_Predecessor (Ctx, Fld), + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); + + pragma Warnings (Off, "postcondition does not mention function result"); function Field_Condition (Ctx : Context; Val : Field_Dependent_Value) return Boolean with Pre => Has_Buffer (Ctx) and Val.Fld in Field'Range - and Valid_Predecessor (Ctx, Val.Fld); + and Valid_Predecessor (Ctx, Val.Fld), + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); function Field_Size (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Length with Pre => @@ -266,9 +284,15 @@ is when others => True); + pragma Warnings (Off, "postcondition does not mention function result"); + function Field_First (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Index with Pre => - Valid_Next (Ctx, Fld); + Valid_Next (Ctx, Fld), + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); function Field_Last (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Index with Pre => @@ -281,9 +305,21 @@ is when others => True); - function Predecessor (Ctx : Context; Fld : Virtual_Field) return Virtual_Field; + pragma Warnings (Off, "postcondition does not mention function result"); + + function Predecessor (Ctx : Context; Fld : Virtual_Field) return Virtual_Field with + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); + + pragma Warnings (Off, "postcondition does not mention function result"); + + function Valid_Predecessor (Ctx : Context; Fld : Virtual_Field) return Boolean with + Post => + True; - function Valid_Predecessor (Ctx : Context; Fld : Virtual_Field) return Boolean; + pragma Warnings (On, "postcondition does not mention function result"); function Valid_Next (Ctx : Context; Fld : Field) return Boolean; @@ -332,7 +368,13 @@ is Pre => Has_Buffer (Ctx); - function Incomplete_Message (Ctx : Context) return Boolean; + pragma Warnings (Off, "postcondition does not mention function result"); + + function Incomplete_Message (Ctx : Context) return Boolean with + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); pragma Warnings (Off, "precondition is always False"); @@ -373,9 +415,15 @@ is Has_Buffer (Ctx) and Present (Ctx, F_Data); + pragma Warnings (Off, "postcondition does not mention function result"); + function Valid_Length (Ctx : Context; Fld : Field; Length : RFLX_Types.Length) return Boolean with Pre => - Valid_Next (Ctx, Fld); + Valid_Next (Ctx, Fld), + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); procedure Set_Message_Type (Ctx : in out Context; Val : RFLX.Universal.Message_Type) with Pre => @@ -1082,6 +1130,8 @@ private type Cursor_State is (S_Valid, S_Structural_Valid, S_Invalid, S_Incomplete); + pragma Warnings (Off, "postcondition does not mention function result"); + function Valid_Value (Val : Field_Dependent_Value) return Boolean is ((case Val.Fld is when F_Message_Type => @@ -1095,7 +1145,12 @@ private when F_Values => True, when F_Initial | F_Final => - False)); + False)) + with + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); type Field_Cursor (State : Cursor_State := S_Invalid) is record diff --git a/tests/integration/messages/generated/rflx-universal-option.ads b/tests/integration/messages/generated/rflx-universal-option.ads index 0e2088b5b..553cfe1ed 100644 --- a/tests/integration/messages/generated/rflx-universal-option.ads +++ b/tests/integration/messages/generated/rflx-universal-option.ads @@ -110,8 +110,14 @@ is Depends => (Ctx => (Buffer, First, Last, Written_Last), Buffer => null); + pragma Warnings (Off, "postcondition does not mention function result"); + function Initialized (Ctx : Context) return Boolean with - Ghost; + Ghost, + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); procedure Reset (Ctx : in out Context) with Pre => @@ -241,15 +247,27 @@ is and then Structural_Valid_Message (Ctx) and then Data'Length = Byte_Size (Ctx); + pragma Warnings (Off, "postcondition does not mention function result"); + function Path_Condition (Ctx : Context; Fld : Field) return Boolean with Pre => - Valid_Predecessor (Ctx, Fld); + Valid_Predecessor (Ctx, Fld), + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); + + pragma Warnings (Off, "postcondition does not mention function result"); function Field_Condition (Ctx : Context; Val : Field_Dependent_Value) return Boolean with Pre => Has_Buffer (Ctx) and Val.Fld in Field'Range - and Valid_Predecessor (Ctx, Val.Fld); + and Valid_Predecessor (Ctx, Val.Fld), + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); function Field_Size (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Length with Pre => @@ -261,9 +279,15 @@ is when others => True); + pragma Warnings (Off, "postcondition does not mention function result"); + function Field_First (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Index with Pre => - Valid_Next (Ctx, Fld); + Valid_Next (Ctx, Fld), + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); function Field_Last (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Index with Pre => @@ -276,9 +300,21 @@ is when others => True); - function Predecessor (Ctx : Context; Fld : Virtual_Field) return Virtual_Field; + pragma Warnings (Off, "postcondition does not mention function result"); + + function Predecessor (Ctx : Context; Fld : Virtual_Field) return Virtual_Field with + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); + + pragma Warnings (Off, "postcondition does not mention function result"); + + function Valid_Predecessor (Ctx : Context; Fld : Virtual_Field) return Boolean with + Post => + True; - function Valid_Predecessor (Ctx : Context; Fld : Virtual_Field) return Boolean; + pragma Warnings (On, "postcondition does not mention function result"); function Valid_Next (Ctx : Context; Fld : Field) return Boolean; @@ -327,7 +363,13 @@ is Pre => Has_Buffer (Ctx); - function Incomplete_Message (Ctx : Context) return Boolean; + pragma Warnings (Off, "postcondition does not mention function result"); + + function Incomplete_Message (Ctx : Context) return Boolean with + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); pragma Warnings (Off, "precondition is always False"); @@ -364,9 +406,15 @@ is Has_Buffer (Ctx) and Present (Ctx, F_Data); + pragma Warnings (Off, "postcondition does not mention function result"); + function Valid_Length (Ctx : Context; Fld : Field; Length : RFLX_Types.Length) return Boolean with Pre => - Valid_Next (Ctx, Fld); + Valid_Next (Ctx, Fld), + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); procedure Set_Option_Type (Ctx : in out Context; Val : RFLX.Universal.Option_Type_Enum) with Pre => @@ -531,6 +579,8 @@ private type Cursor_State is (S_Valid, S_Structural_Valid, S_Invalid, S_Incomplete); + pragma Warnings (Off, "postcondition does not mention function result"); + function Valid_Value (Val : Field_Dependent_Value) return Boolean is ((case Val.Fld is when F_Option_Type => @@ -540,7 +590,12 @@ private when F_Data => True, when F_Initial | F_Final => - False)); + False)) + with + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); type Field_Cursor (State : Cursor_State := S_Invalid) is record diff --git a/tests/integration/messages_with_implict_size/generated/rflx-universal-message.ads b/tests/integration/messages_with_implict_size/generated/rflx-universal-message.ads index 489b50a8f..b70fa9f65 100644 --- a/tests/integration/messages_with_implict_size/generated/rflx-universal-message.ads +++ b/tests/integration/messages_with_implict_size/generated/rflx-universal-message.ads @@ -115,8 +115,14 @@ is Depends => (Ctx => (Buffer, First, Last, Written_Last), Buffer => null); + pragma Warnings (Off, "postcondition does not mention function result"); + function Initialized (Ctx : Context) return Boolean with - Ghost; + Ghost, + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); procedure Reset (Ctx : in out Context) with Pre => @@ -246,15 +252,27 @@ is and then Structural_Valid_Message (Ctx) and then Data'Length = Byte_Size (Ctx); + pragma Warnings (Off, "postcondition does not mention function result"); + function Path_Condition (Ctx : Context; Fld : Field) return Boolean with Pre => - Valid_Predecessor (Ctx, Fld); + Valid_Predecessor (Ctx, Fld), + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); + + pragma Warnings (Off, "postcondition does not mention function result"); function Field_Condition (Ctx : Context; Val : Field_Dependent_Value) return Boolean with Pre => Has_Buffer (Ctx) and Val.Fld in Field'Range - and Valid_Predecessor (Ctx, Val.Fld); + and Valid_Predecessor (Ctx, Val.Fld), + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); function Field_Size (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Length with Pre => @@ -266,9 +284,15 @@ is when others => True); + pragma Warnings (Off, "postcondition does not mention function result"); + function Field_First (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Index with Pre => - Valid_Next (Ctx, Fld); + Valid_Next (Ctx, Fld), + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); function Field_Last (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Index with Pre => @@ -281,9 +305,21 @@ is when others => True); - function Predecessor (Ctx : Context; Fld : Virtual_Field) return Virtual_Field; + pragma Warnings (Off, "postcondition does not mention function result"); + + function Predecessor (Ctx : Context; Fld : Virtual_Field) return Virtual_Field with + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); + + pragma Warnings (Off, "postcondition does not mention function result"); + + function Valid_Predecessor (Ctx : Context; Fld : Virtual_Field) return Boolean with + Post => + True; - function Valid_Predecessor (Ctx : Context; Fld : Virtual_Field) return Boolean; + pragma Warnings (On, "postcondition does not mention function result"); function Valid_Next (Ctx : Context; Fld : Field) return Boolean; @@ -332,7 +368,13 @@ is Pre => Has_Buffer (Ctx); - function Incomplete_Message (Ctx : Context) return Boolean; + pragma Warnings (Off, "postcondition does not mention function result"); + + function Incomplete_Message (Ctx : Context) return Boolean with + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); pragma Warnings (Off, "precondition is always False"); @@ -373,9 +415,15 @@ is Has_Buffer (Ctx) and Present (Ctx, F_Data); + pragma Warnings (Off, "postcondition does not mention function result"); + function Valid_Length (Ctx : Context; Fld : Field; Length : RFLX_Types.Length) return Boolean with Pre => - Valid_Next (Ctx, Fld); + Valid_Next (Ctx, Fld), + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); procedure Set_Message_Type (Ctx : in out Context; Val : RFLX.Universal.Message_Type) with Pre => @@ -1082,6 +1130,8 @@ private type Cursor_State is (S_Valid, S_Structural_Valid, S_Invalid, S_Incomplete); + pragma Warnings (Off, "postcondition does not mention function result"); + function Valid_Value (Val : Field_Dependent_Value) return Boolean is ((case Val.Fld is when F_Message_Type => @@ -1095,7 +1145,12 @@ private when F_Values => True, when F_Initial | F_Final => - False)); + False)) + with + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); type Field_Cursor (State : Cursor_State := S_Invalid) is record diff --git a/tests/integration/messages_with_implict_size/generated/rflx-universal-option.ads b/tests/integration/messages_with_implict_size/generated/rflx-universal-option.ads index 0e2088b5b..553cfe1ed 100644 --- a/tests/integration/messages_with_implict_size/generated/rflx-universal-option.ads +++ b/tests/integration/messages_with_implict_size/generated/rflx-universal-option.ads @@ -110,8 +110,14 @@ is Depends => (Ctx => (Buffer, First, Last, Written_Last), Buffer => null); + pragma Warnings (Off, "postcondition does not mention function result"); + function Initialized (Ctx : Context) return Boolean with - Ghost; + Ghost, + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); procedure Reset (Ctx : in out Context) with Pre => @@ -241,15 +247,27 @@ is and then Structural_Valid_Message (Ctx) and then Data'Length = Byte_Size (Ctx); + pragma Warnings (Off, "postcondition does not mention function result"); + function Path_Condition (Ctx : Context; Fld : Field) return Boolean with Pre => - Valid_Predecessor (Ctx, Fld); + Valid_Predecessor (Ctx, Fld), + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); + + pragma Warnings (Off, "postcondition does not mention function result"); function Field_Condition (Ctx : Context; Val : Field_Dependent_Value) return Boolean with Pre => Has_Buffer (Ctx) and Val.Fld in Field'Range - and Valid_Predecessor (Ctx, Val.Fld); + and Valid_Predecessor (Ctx, Val.Fld), + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); function Field_Size (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Length with Pre => @@ -261,9 +279,15 @@ is when others => True); + pragma Warnings (Off, "postcondition does not mention function result"); + function Field_First (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Index with Pre => - Valid_Next (Ctx, Fld); + Valid_Next (Ctx, Fld), + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); function Field_Last (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Index with Pre => @@ -276,9 +300,21 @@ is when others => True); - function Predecessor (Ctx : Context; Fld : Virtual_Field) return Virtual_Field; + pragma Warnings (Off, "postcondition does not mention function result"); + + function Predecessor (Ctx : Context; Fld : Virtual_Field) return Virtual_Field with + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); + + pragma Warnings (Off, "postcondition does not mention function result"); + + function Valid_Predecessor (Ctx : Context; Fld : Virtual_Field) return Boolean with + Post => + True; - function Valid_Predecessor (Ctx : Context; Fld : Virtual_Field) return Boolean; + pragma Warnings (On, "postcondition does not mention function result"); function Valid_Next (Ctx : Context; Fld : Field) return Boolean; @@ -327,7 +363,13 @@ is Pre => Has_Buffer (Ctx); - function Incomplete_Message (Ctx : Context) return Boolean; + pragma Warnings (Off, "postcondition does not mention function result"); + + function Incomplete_Message (Ctx : Context) return Boolean with + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); pragma Warnings (Off, "precondition is always False"); @@ -364,9 +406,15 @@ is Has_Buffer (Ctx) and Present (Ctx, F_Data); + pragma Warnings (Off, "postcondition does not mention function result"); + function Valid_Length (Ctx : Context; Fld : Field; Length : RFLX_Types.Length) return Boolean with Pre => - Valid_Next (Ctx, Fld); + Valid_Next (Ctx, Fld), + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); procedure Set_Option_Type (Ctx : in out Context; Val : RFLX.Universal.Option_Type_Enum) with Pre => @@ -531,6 +579,8 @@ private type Cursor_State is (S_Valid, S_Structural_Valid, S_Invalid, S_Incomplete); + pragma Warnings (Off, "postcondition does not mention function result"); + function Valid_Value (Val : Field_Dependent_Value) return Boolean is ((case Val.Fld is when F_Option_Type => @@ -540,7 +590,12 @@ private when F_Data => True, when F_Initial | F_Final => - False)); + False)) + with + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); type Field_Cursor (State : Cursor_State := S_Invalid) is record diff --git a/tests/integration/parameterized_messages/generated/rflx-test-message.ads b/tests/integration/parameterized_messages/generated/rflx-test-message.ads index d92e7e873..6e6f05691 100644 --- a/tests/integration/parameterized_messages/generated/rflx-test-message.ads +++ b/tests/integration/parameterized_messages/generated/rflx-test-message.ads @@ -113,8 +113,14 @@ is Depends => (Ctx => (Buffer, First, Last, Length, Extended, Written_Last), Buffer => null); + pragma Warnings (Off, "postcondition does not mention function result"); + function Initialized (Ctx : Context) return Boolean with - Ghost; + Ghost, + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); procedure Reset (Ctx : in out Context; Length : Test.Length; Extended : Boolean) with Pre => @@ -250,15 +256,27 @@ is and then Structural_Valid_Message (Ctx) and then Data'Length = Byte_Size (Ctx); + pragma Warnings (Off, "postcondition does not mention function result"); + function Path_Condition (Ctx : Context; Fld : Field) return Boolean with Pre => - Valid_Predecessor (Ctx, Fld); + Valid_Predecessor (Ctx, Fld), + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); + + pragma Warnings (Off, "postcondition does not mention function result"); function Field_Condition (Ctx : Context; Val : Field_Dependent_Value) return Boolean with Pre => Has_Buffer (Ctx) and Val.Fld in Field'Range - and Valid_Predecessor (Ctx, Val.Fld); + and Valid_Predecessor (Ctx, Val.Fld), + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); function Field_Size (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Length with Pre => @@ -268,9 +286,15 @@ is when F_Data | F_Extension => Field_Size'Result rem RFLX_Types.Byte'Size = 0); + pragma Warnings (Off, "postcondition does not mention function result"); + function Field_First (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Index with Pre => - Valid_Next (Ctx, Fld); + Valid_Next (Ctx, Fld), + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); function Field_Last (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Index with Pre => @@ -281,9 +305,21 @@ is when F_Data | F_Extension => Field_Last'Result rem RFLX_Types.Byte'Size = 0); - function Predecessor (Ctx : Context; Fld : Virtual_Field) return Virtual_Field; + pragma Warnings (Off, "postcondition does not mention function result"); + + function Predecessor (Ctx : Context; Fld : Virtual_Field) return Virtual_Field with + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); + + pragma Warnings (Off, "postcondition does not mention function result"); + + function Valid_Predecessor (Ctx : Context; Fld : Virtual_Field) return Boolean with + Post => + True; - function Valid_Predecessor (Ctx : Context; Fld : Virtual_Field) return Boolean; + pragma Warnings (On, "postcondition does not mention function result"); function Valid_Next (Ctx : Context; Fld : Field) return Boolean; @@ -336,7 +372,13 @@ is Pre => Has_Buffer (Ctx); - function Incomplete_Message (Ctx : Context) return Boolean; + pragma Warnings (Off, "postcondition does not mention function result"); + + function Incomplete_Message (Ctx : Context) return Boolean with + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); pragma Warnings (Off, "precondition is always False"); @@ -388,9 +430,15 @@ is Has_Buffer (Ctx) and Present (Ctx, F_Extension); + pragma Warnings (Off, "postcondition does not mention function result"); + function Valid_Length (Ctx : Context; Fld : Field; Length : RFLX_Types.Length) return Boolean with Pre => - Valid_Next (Ctx, Fld); + Valid_Next (Ctx, Fld), + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); procedure Initialize_Data (Ctx : in out Context) with Pre => @@ -572,12 +620,19 @@ private type Cursor_State is (S_Valid, S_Structural_Valid, S_Invalid, S_Incomplete); + pragma Warnings (Off, "postcondition does not mention function result"); + function Valid_Value (Val : Field_Dependent_Value) return Boolean is ((case Val.Fld is when F_Data | F_Extension => True, when F_Initial | F_Final => - False)); + False)) + with + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); type Field_Cursor (State : Cursor_State := S_Invalid) is record diff --git a/tests/integration/session_append_unconstrained/generated/rflx-universal-message.ads b/tests/integration/session_append_unconstrained/generated/rflx-universal-message.ads index 489b50a8f..b70fa9f65 100644 --- a/tests/integration/session_append_unconstrained/generated/rflx-universal-message.ads +++ b/tests/integration/session_append_unconstrained/generated/rflx-universal-message.ads @@ -115,8 +115,14 @@ is Depends => (Ctx => (Buffer, First, Last, Written_Last), Buffer => null); + pragma Warnings (Off, "postcondition does not mention function result"); + function Initialized (Ctx : Context) return Boolean with - Ghost; + Ghost, + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); procedure Reset (Ctx : in out Context) with Pre => @@ -246,15 +252,27 @@ is and then Structural_Valid_Message (Ctx) and then Data'Length = Byte_Size (Ctx); + pragma Warnings (Off, "postcondition does not mention function result"); + function Path_Condition (Ctx : Context; Fld : Field) return Boolean with Pre => - Valid_Predecessor (Ctx, Fld); + Valid_Predecessor (Ctx, Fld), + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); + + pragma Warnings (Off, "postcondition does not mention function result"); function Field_Condition (Ctx : Context; Val : Field_Dependent_Value) return Boolean with Pre => Has_Buffer (Ctx) and Val.Fld in Field'Range - and Valid_Predecessor (Ctx, Val.Fld); + and Valid_Predecessor (Ctx, Val.Fld), + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); function Field_Size (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Length with Pre => @@ -266,9 +284,15 @@ is when others => True); + pragma Warnings (Off, "postcondition does not mention function result"); + function Field_First (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Index with Pre => - Valid_Next (Ctx, Fld); + Valid_Next (Ctx, Fld), + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); function Field_Last (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Index with Pre => @@ -281,9 +305,21 @@ is when others => True); - function Predecessor (Ctx : Context; Fld : Virtual_Field) return Virtual_Field; + pragma Warnings (Off, "postcondition does not mention function result"); + + function Predecessor (Ctx : Context; Fld : Virtual_Field) return Virtual_Field with + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); + + pragma Warnings (Off, "postcondition does not mention function result"); + + function Valid_Predecessor (Ctx : Context; Fld : Virtual_Field) return Boolean with + Post => + True; - function Valid_Predecessor (Ctx : Context; Fld : Virtual_Field) return Boolean; + pragma Warnings (On, "postcondition does not mention function result"); function Valid_Next (Ctx : Context; Fld : Field) return Boolean; @@ -332,7 +368,13 @@ is Pre => Has_Buffer (Ctx); - function Incomplete_Message (Ctx : Context) return Boolean; + pragma Warnings (Off, "postcondition does not mention function result"); + + function Incomplete_Message (Ctx : Context) return Boolean with + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); pragma Warnings (Off, "precondition is always False"); @@ -373,9 +415,15 @@ is Has_Buffer (Ctx) and Present (Ctx, F_Data); + pragma Warnings (Off, "postcondition does not mention function result"); + function Valid_Length (Ctx : Context; Fld : Field; Length : RFLX_Types.Length) return Boolean with Pre => - Valid_Next (Ctx, Fld); + Valid_Next (Ctx, Fld), + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); procedure Set_Message_Type (Ctx : in out Context; Val : RFLX.Universal.Message_Type) with Pre => @@ -1082,6 +1130,8 @@ private type Cursor_State is (S_Valid, S_Structural_Valid, S_Invalid, S_Incomplete); + pragma Warnings (Off, "postcondition does not mention function result"); + function Valid_Value (Val : Field_Dependent_Value) return Boolean is ((case Val.Fld is when F_Message_Type => @@ -1095,7 +1145,12 @@ private when F_Values => True, when F_Initial | F_Final => - False)); + False)) + with + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); type Field_Cursor (State : Cursor_State := S_Invalid) is record diff --git a/tests/integration/session_append_unconstrained/generated/rflx-universal-option.ads b/tests/integration/session_append_unconstrained/generated/rflx-universal-option.ads index 0e2088b5b..553cfe1ed 100644 --- a/tests/integration/session_append_unconstrained/generated/rflx-universal-option.ads +++ b/tests/integration/session_append_unconstrained/generated/rflx-universal-option.ads @@ -110,8 +110,14 @@ is Depends => (Ctx => (Buffer, First, Last, Written_Last), Buffer => null); + pragma Warnings (Off, "postcondition does not mention function result"); + function Initialized (Ctx : Context) return Boolean with - Ghost; + Ghost, + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); procedure Reset (Ctx : in out Context) with Pre => @@ -241,15 +247,27 @@ is and then Structural_Valid_Message (Ctx) and then Data'Length = Byte_Size (Ctx); + pragma Warnings (Off, "postcondition does not mention function result"); + function Path_Condition (Ctx : Context; Fld : Field) return Boolean with Pre => - Valid_Predecessor (Ctx, Fld); + Valid_Predecessor (Ctx, Fld), + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); + + pragma Warnings (Off, "postcondition does not mention function result"); function Field_Condition (Ctx : Context; Val : Field_Dependent_Value) return Boolean with Pre => Has_Buffer (Ctx) and Val.Fld in Field'Range - and Valid_Predecessor (Ctx, Val.Fld); + and Valid_Predecessor (Ctx, Val.Fld), + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); function Field_Size (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Length with Pre => @@ -261,9 +279,15 @@ is when others => True); + pragma Warnings (Off, "postcondition does not mention function result"); + function Field_First (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Index with Pre => - Valid_Next (Ctx, Fld); + Valid_Next (Ctx, Fld), + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); function Field_Last (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Index with Pre => @@ -276,9 +300,21 @@ is when others => True); - function Predecessor (Ctx : Context; Fld : Virtual_Field) return Virtual_Field; + pragma Warnings (Off, "postcondition does not mention function result"); + + function Predecessor (Ctx : Context; Fld : Virtual_Field) return Virtual_Field with + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); + + pragma Warnings (Off, "postcondition does not mention function result"); + + function Valid_Predecessor (Ctx : Context; Fld : Virtual_Field) return Boolean with + Post => + True; - function Valid_Predecessor (Ctx : Context; Fld : Virtual_Field) return Boolean; + pragma Warnings (On, "postcondition does not mention function result"); function Valid_Next (Ctx : Context; Fld : Field) return Boolean; @@ -327,7 +363,13 @@ is Pre => Has_Buffer (Ctx); - function Incomplete_Message (Ctx : Context) return Boolean; + pragma Warnings (Off, "postcondition does not mention function result"); + + function Incomplete_Message (Ctx : Context) return Boolean with + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); pragma Warnings (Off, "precondition is always False"); @@ -364,9 +406,15 @@ is Has_Buffer (Ctx) and Present (Ctx, F_Data); + pragma Warnings (Off, "postcondition does not mention function result"); + function Valid_Length (Ctx : Context; Fld : Field; Length : RFLX_Types.Length) return Boolean with Pre => - Valid_Next (Ctx, Fld); + Valid_Next (Ctx, Fld), + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); procedure Set_Option_Type (Ctx : in out Context; Val : RFLX.Universal.Option_Type_Enum) with Pre => @@ -531,6 +579,8 @@ private type Cursor_State is (S_Valid, S_Structural_Valid, S_Invalid, S_Incomplete); + pragma Warnings (Off, "postcondition does not mention function result"); + function Valid_Value (Val : Field_Dependent_Value) return Boolean is ((case Val.Fld is when F_Option_Type => @@ -540,7 +590,12 @@ private when F_Data => True, when F_Initial | F_Final => - False)); + False)) + with + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); type Field_Cursor (State : Cursor_State := S_Invalid) is record diff --git a/tests/integration/session_binding/generated/rflx-universal-message.ads b/tests/integration/session_binding/generated/rflx-universal-message.ads index 489b50a8f..b70fa9f65 100644 --- a/tests/integration/session_binding/generated/rflx-universal-message.ads +++ b/tests/integration/session_binding/generated/rflx-universal-message.ads @@ -115,8 +115,14 @@ is Depends => (Ctx => (Buffer, First, Last, Written_Last), Buffer => null); + pragma Warnings (Off, "postcondition does not mention function result"); + function Initialized (Ctx : Context) return Boolean with - Ghost; + Ghost, + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); procedure Reset (Ctx : in out Context) with Pre => @@ -246,15 +252,27 @@ is and then Structural_Valid_Message (Ctx) and then Data'Length = Byte_Size (Ctx); + pragma Warnings (Off, "postcondition does not mention function result"); + function Path_Condition (Ctx : Context; Fld : Field) return Boolean with Pre => - Valid_Predecessor (Ctx, Fld); + Valid_Predecessor (Ctx, Fld), + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); + + pragma Warnings (Off, "postcondition does not mention function result"); function Field_Condition (Ctx : Context; Val : Field_Dependent_Value) return Boolean with Pre => Has_Buffer (Ctx) and Val.Fld in Field'Range - and Valid_Predecessor (Ctx, Val.Fld); + and Valid_Predecessor (Ctx, Val.Fld), + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); function Field_Size (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Length with Pre => @@ -266,9 +284,15 @@ is when others => True); + pragma Warnings (Off, "postcondition does not mention function result"); + function Field_First (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Index with Pre => - Valid_Next (Ctx, Fld); + Valid_Next (Ctx, Fld), + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); function Field_Last (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Index with Pre => @@ -281,9 +305,21 @@ is when others => True); - function Predecessor (Ctx : Context; Fld : Virtual_Field) return Virtual_Field; + pragma Warnings (Off, "postcondition does not mention function result"); + + function Predecessor (Ctx : Context; Fld : Virtual_Field) return Virtual_Field with + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); + + pragma Warnings (Off, "postcondition does not mention function result"); + + function Valid_Predecessor (Ctx : Context; Fld : Virtual_Field) return Boolean with + Post => + True; - function Valid_Predecessor (Ctx : Context; Fld : Virtual_Field) return Boolean; + pragma Warnings (On, "postcondition does not mention function result"); function Valid_Next (Ctx : Context; Fld : Field) return Boolean; @@ -332,7 +368,13 @@ is Pre => Has_Buffer (Ctx); - function Incomplete_Message (Ctx : Context) return Boolean; + pragma Warnings (Off, "postcondition does not mention function result"); + + function Incomplete_Message (Ctx : Context) return Boolean with + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); pragma Warnings (Off, "precondition is always False"); @@ -373,9 +415,15 @@ is Has_Buffer (Ctx) and Present (Ctx, F_Data); + pragma Warnings (Off, "postcondition does not mention function result"); + function Valid_Length (Ctx : Context; Fld : Field; Length : RFLX_Types.Length) return Boolean with Pre => - Valid_Next (Ctx, Fld); + Valid_Next (Ctx, Fld), + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); procedure Set_Message_Type (Ctx : in out Context; Val : RFLX.Universal.Message_Type) with Pre => @@ -1082,6 +1130,8 @@ private type Cursor_State is (S_Valid, S_Structural_Valid, S_Invalid, S_Incomplete); + pragma Warnings (Off, "postcondition does not mention function result"); + function Valid_Value (Val : Field_Dependent_Value) return Boolean is ((case Val.Fld is when F_Message_Type => @@ -1095,7 +1145,12 @@ private when F_Values => True, when F_Initial | F_Final => - False)); + False)) + with + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); type Field_Cursor (State : Cursor_State := S_Invalid) is record diff --git a/tests/integration/session_binding/generated/rflx-universal-option.ads b/tests/integration/session_binding/generated/rflx-universal-option.ads index 0e2088b5b..553cfe1ed 100644 --- a/tests/integration/session_binding/generated/rflx-universal-option.ads +++ b/tests/integration/session_binding/generated/rflx-universal-option.ads @@ -110,8 +110,14 @@ is Depends => (Ctx => (Buffer, First, Last, Written_Last), Buffer => null); + pragma Warnings (Off, "postcondition does not mention function result"); + function Initialized (Ctx : Context) return Boolean with - Ghost; + Ghost, + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); procedure Reset (Ctx : in out Context) with Pre => @@ -241,15 +247,27 @@ is and then Structural_Valid_Message (Ctx) and then Data'Length = Byte_Size (Ctx); + pragma Warnings (Off, "postcondition does not mention function result"); + function Path_Condition (Ctx : Context; Fld : Field) return Boolean with Pre => - Valid_Predecessor (Ctx, Fld); + Valid_Predecessor (Ctx, Fld), + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); + + pragma Warnings (Off, "postcondition does not mention function result"); function Field_Condition (Ctx : Context; Val : Field_Dependent_Value) return Boolean with Pre => Has_Buffer (Ctx) and Val.Fld in Field'Range - and Valid_Predecessor (Ctx, Val.Fld); + and Valid_Predecessor (Ctx, Val.Fld), + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); function Field_Size (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Length with Pre => @@ -261,9 +279,15 @@ is when others => True); + pragma Warnings (Off, "postcondition does not mention function result"); + function Field_First (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Index with Pre => - Valid_Next (Ctx, Fld); + Valid_Next (Ctx, Fld), + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); function Field_Last (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Index with Pre => @@ -276,9 +300,21 @@ is when others => True); - function Predecessor (Ctx : Context; Fld : Virtual_Field) return Virtual_Field; + pragma Warnings (Off, "postcondition does not mention function result"); + + function Predecessor (Ctx : Context; Fld : Virtual_Field) return Virtual_Field with + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); + + pragma Warnings (Off, "postcondition does not mention function result"); + + function Valid_Predecessor (Ctx : Context; Fld : Virtual_Field) return Boolean with + Post => + True; - function Valid_Predecessor (Ctx : Context; Fld : Virtual_Field) return Boolean; + pragma Warnings (On, "postcondition does not mention function result"); function Valid_Next (Ctx : Context; Fld : Field) return Boolean; @@ -327,7 +363,13 @@ is Pre => Has_Buffer (Ctx); - function Incomplete_Message (Ctx : Context) return Boolean; + pragma Warnings (Off, "postcondition does not mention function result"); + + function Incomplete_Message (Ctx : Context) return Boolean with + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); pragma Warnings (Off, "precondition is always False"); @@ -364,9 +406,15 @@ is Has_Buffer (Ctx) and Present (Ctx, F_Data); + pragma Warnings (Off, "postcondition does not mention function result"); + function Valid_Length (Ctx : Context; Fld : Field; Length : RFLX_Types.Length) return Boolean with Pre => - Valid_Next (Ctx, Fld); + Valid_Next (Ctx, Fld), + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); procedure Set_Option_Type (Ctx : in out Context; Val : RFLX.Universal.Option_Type_Enum) with Pre => @@ -531,6 +579,8 @@ private type Cursor_State is (S_Valid, S_Structural_Valid, S_Invalid, S_Incomplete); + pragma Warnings (Off, "postcondition does not mention function result"); + function Valid_Value (Val : Field_Dependent_Value) return Boolean is ((case Val.Fld is when F_Option_Type => @@ -540,7 +590,12 @@ private when F_Data => True, when F_Initial | F_Final => - False)); + False)) + with + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); type Field_Cursor (State : Cursor_State := S_Invalid) is record diff --git a/tests/integration/session_channel_multiplexing/generated/rflx-universal-message.ads b/tests/integration/session_channel_multiplexing/generated/rflx-universal-message.ads index 489b50a8f..b70fa9f65 100644 --- a/tests/integration/session_channel_multiplexing/generated/rflx-universal-message.ads +++ b/tests/integration/session_channel_multiplexing/generated/rflx-universal-message.ads @@ -115,8 +115,14 @@ is Depends => (Ctx => (Buffer, First, Last, Written_Last), Buffer => null); + pragma Warnings (Off, "postcondition does not mention function result"); + function Initialized (Ctx : Context) return Boolean with - Ghost; + Ghost, + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); procedure Reset (Ctx : in out Context) with Pre => @@ -246,15 +252,27 @@ is and then Structural_Valid_Message (Ctx) and then Data'Length = Byte_Size (Ctx); + pragma Warnings (Off, "postcondition does not mention function result"); + function Path_Condition (Ctx : Context; Fld : Field) return Boolean with Pre => - Valid_Predecessor (Ctx, Fld); + Valid_Predecessor (Ctx, Fld), + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); + + pragma Warnings (Off, "postcondition does not mention function result"); function Field_Condition (Ctx : Context; Val : Field_Dependent_Value) return Boolean with Pre => Has_Buffer (Ctx) and Val.Fld in Field'Range - and Valid_Predecessor (Ctx, Val.Fld); + and Valid_Predecessor (Ctx, Val.Fld), + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); function Field_Size (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Length with Pre => @@ -266,9 +284,15 @@ is when others => True); + pragma Warnings (Off, "postcondition does not mention function result"); + function Field_First (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Index with Pre => - Valid_Next (Ctx, Fld); + Valid_Next (Ctx, Fld), + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); function Field_Last (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Index with Pre => @@ -281,9 +305,21 @@ is when others => True); - function Predecessor (Ctx : Context; Fld : Virtual_Field) return Virtual_Field; + pragma Warnings (Off, "postcondition does not mention function result"); + + function Predecessor (Ctx : Context; Fld : Virtual_Field) return Virtual_Field with + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); + + pragma Warnings (Off, "postcondition does not mention function result"); + + function Valid_Predecessor (Ctx : Context; Fld : Virtual_Field) return Boolean with + Post => + True; - function Valid_Predecessor (Ctx : Context; Fld : Virtual_Field) return Boolean; + pragma Warnings (On, "postcondition does not mention function result"); function Valid_Next (Ctx : Context; Fld : Field) return Boolean; @@ -332,7 +368,13 @@ is Pre => Has_Buffer (Ctx); - function Incomplete_Message (Ctx : Context) return Boolean; + pragma Warnings (Off, "postcondition does not mention function result"); + + function Incomplete_Message (Ctx : Context) return Boolean with + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); pragma Warnings (Off, "precondition is always False"); @@ -373,9 +415,15 @@ is Has_Buffer (Ctx) and Present (Ctx, F_Data); + pragma Warnings (Off, "postcondition does not mention function result"); + function Valid_Length (Ctx : Context; Fld : Field; Length : RFLX_Types.Length) return Boolean with Pre => - Valid_Next (Ctx, Fld); + Valid_Next (Ctx, Fld), + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); procedure Set_Message_Type (Ctx : in out Context; Val : RFLX.Universal.Message_Type) with Pre => @@ -1082,6 +1130,8 @@ private type Cursor_State is (S_Valid, S_Structural_Valid, S_Invalid, S_Incomplete); + pragma Warnings (Off, "postcondition does not mention function result"); + function Valid_Value (Val : Field_Dependent_Value) return Boolean is ((case Val.Fld is when F_Message_Type => @@ -1095,7 +1145,12 @@ private when F_Values => True, when F_Initial | F_Final => - False)); + False)) + with + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); type Field_Cursor (State : Cursor_State := S_Invalid) is record diff --git a/tests/integration/session_channel_multiplexing/generated/rflx-universal-option.ads b/tests/integration/session_channel_multiplexing/generated/rflx-universal-option.ads index 0e2088b5b..553cfe1ed 100644 --- a/tests/integration/session_channel_multiplexing/generated/rflx-universal-option.ads +++ b/tests/integration/session_channel_multiplexing/generated/rflx-universal-option.ads @@ -110,8 +110,14 @@ is Depends => (Ctx => (Buffer, First, Last, Written_Last), Buffer => null); + pragma Warnings (Off, "postcondition does not mention function result"); + function Initialized (Ctx : Context) return Boolean with - Ghost; + Ghost, + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); procedure Reset (Ctx : in out Context) with Pre => @@ -241,15 +247,27 @@ is and then Structural_Valid_Message (Ctx) and then Data'Length = Byte_Size (Ctx); + pragma Warnings (Off, "postcondition does not mention function result"); + function Path_Condition (Ctx : Context; Fld : Field) return Boolean with Pre => - Valid_Predecessor (Ctx, Fld); + Valid_Predecessor (Ctx, Fld), + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); + + pragma Warnings (Off, "postcondition does not mention function result"); function Field_Condition (Ctx : Context; Val : Field_Dependent_Value) return Boolean with Pre => Has_Buffer (Ctx) and Val.Fld in Field'Range - and Valid_Predecessor (Ctx, Val.Fld); + and Valid_Predecessor (Ctx, Val.Fld), + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); function Field_Size (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Length with Pre => @@ -261,9 +279,15 @@ is when others => True); + pragma Warnings (Off, "postcondition does not mention function result"); + function Field_First (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Index with Pre => - Valid_Next (Ctx, Fld); + Valid_Next (Ctx, Fld), + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); function Field_Last (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Index with Pre => @@ -276,9 +300,21 @@ is when others => True); - function Predecessor (Ctx : Context; Fld : Virtual_Field) return Virtual_Field; + pragma Warnings (Off, "postcondition does not mention function result"); + + function Predecessor (Ctx : Context; Fld : Virtual_Field) return Virtual_Field with + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); + + pragma Warnings (Off, "postcondition does not mention function result"); + + function Valid_Predecessor (Ctx : Context; Fld : Virtual_Field) return Boolean with + Post => + True; - function Valid_Predecessor (Ctx : Context; Fld : Virtual_Field) return Boolean; + pragma Warnings (On, "postcondition does not mention function result"); function Valid_Next (Ctx : Context; Fld : Field) return Boolean; @@ -327,7 +363,13 @@ is Pre => Has_Buffer (Ctx); - function Incomplete_Message (Ctx : Context) return Boolean; + pragma Warnings (Off, "postcondition does not mention function result"); + + function Incomplete_Message (Ctx : Context) return Boolean with + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); pragma Warnings (Off, "precondition is always False"); @@ -364,9 +406,15 @@ is Has_Buffer (Ctx) and Present (Ctx, F_Data); + pragma Warnings (Off, "postcondition does not mention function result"); + function Valid_Length (Ctx : Context; Fld : Field; Length : RFLX_Types.Length) return Boolean with Pre => - Valid_Next (Ctx, Fld); + Valid_Next (Ctx, Fld), + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); procedure Set_Option_Type (Ctx : in out Context; Val : RFLX.Universal.Option_Type_Enum) with Pre => @@ -531,6 +579,8 @@ private type Cursor_State is (S_Valid, S_Structural_Valid, S_Invalid, S_Incomplete); + pragma Warnings (Off, "postcondition does not mention function result"); + function Valid_Value (Val : Field_Dependent_Value) return Boolean is ((case Val.Fld is when F_Option_Type => @@ -540,7 +590,12 @@ private when F_Data => True, when F_Initial | F_Final => - False)); + False)) + with + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); type Field_Cursor (State : Cursor_State := S_Invalid) is record diff --git a/tests/integration/session_channels/generated/rflx-universal-message.ads b/tests/integration/session_channels/generated/rflx-universal-message.ads index 489b50a8f..b70fa9f65 100644 --- a/tests/integration/session_channels/generated/rflx-universal-message.ads +++ b/tests/integration/session_channels/generated/rflx-universal-message.ads @@ -115,8 +115,14 @@ is Depends => (Ctx => (Buffer, First, Last, Written_Last), Buffer => null); + pragma Warnings (Off, "postcondition does not mention function result"); + function Initialized (Ctx : Context) return Boolean with - Ghost; + Ghost, + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); procedure Reset (Ctx : in out Context) with Pre => @@ -246,15 +252,27 @@ is and then Structural_Valid_Message (Ctx) and then Data'Length = Byte_Size (Ctx); + pragma Warnings (Off, "postcondition does not mention function result"); + function Path_Condition (Ctx : Context; Fld : Field) return Boolean with Pre => - Valid_Predecessor (Ctx, Fld); + Valid_Predecessor (Ctx, Fld), + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); + + pragma Warnings (Off, "postcondition does not mention function result"); function Field_Condition (Ctx : Context; Val : Field_Dependent_Value) return Boolean with Pre => Has_Buffer (Ctx) and Val.Fld in Field'Range - and Valid_Predecessor (Ctx, Val.Fld); + and Valid_Predecessor (Ctx, Val.Fld), + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); function Field_Size (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Length with Pre => @@ -266,9 +284,15 @@ is when others => True); + pragma Warnings (Off, "postcondition does not mention function result"); + function Field_First (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Index with Pre => - Valid_Next (Ctx, Fld); + Valid_Next (Ctx, Fld), + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); function Field_Last (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Index with Pre => @@ -281,9 +305,21 @@ is when others => True); - function Predecessor (Ctx : Context; Fld : Virtual_Field) return Virtual_Field; + pragma Warnings (Off, "postcondition does not mention function result"); + + function Predecessor (Ctx : Context; Fld : Virtual_Field) return Virtual_Field with + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); + + pragma Warnings (Off, "postcondition does not mention function result"); + + function Valid_Predecessor (Ctx : Context; Fld : Virtual_Field) return Boolean with + Post => + True; - function Valid_Predecessor (Ctx : Context; Fld : Virtual_Field) return Boolean; + pragma Warnings (On, "postcondition does not mention function result"); function Valid_Next (Ctx : Context; Fld : Field) return Boolean; @@ -332,7 +368,13 @@ is Pre => Has_Buffer (Ctx); - function Incomplete_Message (Ctx : Context) return Boolean; + pragma Warnings (Off, "postcondition does not mention function result"); + + function Incomplete_Message (Ctx : Context) return Boolean with + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); pragma Warnings (Off, "precondition is always False"); @@ -373,9 +415,15 @@ is Has_Buffer (Ctx) and Present (Ctx, F_Data); + pragma Warnings (Off, "postcondition does not mention function result"); + function Valid_Length (Ctx : Context; Fld : Field; Length : RFLX_Types.Length) return Boolean with Pre => - Valid_Next (Ctx, Fld); + Valid_Next (Ctx, Fld), + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); procedure Set_Message_Type (Ctx : in out Context; Val : RFLX.Universal.Message_Type) with Pre => @@ -1082,6 +1130,8 @@ private type Cursor_State is (S_Valid, S_Structural_Valid, S_Invalid, S_Incomplete); + pragma Warnings (Off, "postcondition does not mention function result"); + function Valid_Value (Val : Field_Dependent_Value) return Boolean is ((case Val.Fld is when F_Message_Type => @@ -1095,7 +1145,12 @@ private when F_Values => True, when F_Initial | F_Final => - False)); + False)) + with + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); type Field_Cursor (State : Cursor_State := S_Invalid) is record diff --git a/tests/integration/session_channels/generated/rflx-universal-option.ads b/tests/integration/session_channels/generated/rflx-universal-option.ads index 0e2088b5b..553cfe1ed 100644 --- a/tests/integration/session_channels/generated/rflx-universal-option.ads +++ b/tests/integration/session_channels/generated/rflx-universal-option.ads @@ -110,8 +110,14 @@ is Depends => (Ctx => (Buffer, First, Last, Written_Last), Buffer => null); + pragma Warnings (Off, "postcondition does not mention function result"); + function Initialized (Ctx : Context) return Boolean with - Ghost; + Ghost, + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); procedure Reset (Ctx : in out Context) with Pre => @@ -241,15 +247,27 @@ is and then Structural_Valid_Message (Ctx) and then Data'Length = Byte_Size (Ctx); + pragma Warnings (Off, "postcondition does not mention function result"); + function Path_Condition (Ctx : Context; Fld : Field) return Boolean with Pre => - Valid_Predecessor (Ctx, Fld); + Valid_Predecessor (Ctx, Fld), + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); + + pragma Warnings (Off, "postcondition does not mention function result"); function Field_Condition (Ctx : Context; Val : Field_Dependent_Value) return Boolean with Pre => Has_Buffer (Ctx) and Val.Fld in Field'Range - and Valid_Predecessor (Ctx, Val.Fld); + and Valid_Predecessor (Ctx, Val.Fld), + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); function Field_Size (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Length with Pre => @@ -261,9 +279,15 @@ is when others => True); + pragma Warnings (Off, "postcondition does not mention function result"); + function Field_First (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Index with Pre => - Valid_Next (Ctx, Fld); + Valid_Next (Ctx, Fld), + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); function Field_Last (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Index with Pre => @@ -276,9 +300,21 @@ is when others => True); - function Predecessor (Ctx : Context; Fld : Virtual_Field) return Virtual_Field; + pragma Warnings (Off, "postcondition does not mention function result"); + + function Predecessor (Ctx : Context; Fld : Virtual_Field) return Virtual_Field with + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); + + pragma Warnings (Off, "postcondition does not mention function result"); + + function Valid_Predecessor (Ctx : Context; Fld : Virtual_Field) return Boolean with + Post => + True; - function Valid_Predecessor (Ctx : Context; Fld : Virtual_Field) return Boolean; + pragma Warnings (On, "postcondition does not mention function result"); function Valid_Next (Ctx : Context; Fld : Field) return Boolean; @@ -327,7 +363,13 @@ is Pre => Has_Buffer (Ctx); - function Incomplete_Message (Ctx : Context) return Boolean; + pragma Warnings (Off, "postcondition does not mention function result"); + + function Incomplete_Message (Ctx : Context) return Boolean with + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); pragma Warnings (Off, "precondition is always False"); @@ -364,9 +406,15 @@ is Has_Buffer (Ctx) and Present (Ctx, F_Data); + pragma Warnings (Off, "postcondition does not mention function result"); + function Valid_Length (Ctx : Context; Fld : Field; Length : RFLX_Types.Length) return Boolean with Pre => - Valid_Next (Ctx, Fld); + Valid_Next (Ctx, Fld), + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); procedure Set_Option_Type (Ctx : in out Context; Val : RFLX.Universal.Option_Type_Enum) with Pre => @@ -531,6 +579,8 @@ private type Cursor_State is (S_Valid, S_Structural_Valid, S_Invalid, S_Incomplete); + pragma Warnings (Off, "postcondition does not mention function result"); + function Valid_Value (Val : Field_Dependent_Value) return Boolean is ((case Val.Fld is when F_Option_Type => @@ -540,7 +590,12 @@ private when F_Data => True, when F_Initial | F_Final => - False)); + False)) + with + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); type Field_Cursor (State : Cursor_State := S_Invalid) is record diff --git a/tests/integration/session_comprehension_on_message_field/generated/rflx-universal-message.ads b/tests/integration/session_comprehension_on_message_field/generated/rflx-universal-message.ads index 489b50a8f..b70fa9f65 100644 --- a/tests/integration/session_comprehension_on_message_field/generated/rflx-universal-message.ads +++ b/tests/integration/session_comprehension_on_message_field/generated/rflx-universal-message.ads @@ -115,8 +115,14 @@ is Depends => (Ctx => (Buffer, First, Last, Written_Last), Buffer => null); + pragma Warnings (Off, "postcondition does not mention function result"); + function Initialized (Ctx : Context) return Boolean with - Ghost; + Ghost, + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); procedure Reset (Ctx : in out Context) with Pre => @@ -246,15 +252,27 @@ is and then Structural_Valid_Message (Ctx) and then Data'Length = Byte_Size (Ctx); + pragma Warnings (Off, "postcondition does not mention function result"); + function Path_Condition (Ctx : Context; Fld : Field) return Boolean with Pre => - Valid_Predecessor (Ctx, Fld); + Valid_Predecessor (Ctx, Fld), + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); + + pragma Warnings (Off, "postcondition does not mention function result"); function Field_Condition (Ctx : Context; Val : Field_Dependent_Value) return Boolean with Pre => Has_Buffer (Ctx) and Val.Fld in Field'Range - and Valid_Predecessor (Ctx, Val.Fld); + and Valid_Predecessor (Ctx, Val.Fld), + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); function Field_Size (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Length with Pre => @@ -266,9 +284,15 @@ is when others => True); + pragma Warnings (Off, "postcondition does not mention function result"); + function Field_First (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Index with Pre => - Valid_Next (Ctx, Fld); + Valid_Next (Ctx, Fld), + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); function Field_Last (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Index with Pre => @@ -281,9 +305,21 @@ is when others => True); - function Predecessor (Ctx : Context; Fld : Virtual_Field) return Virtual_Field; + pragma Warnings (Off, "postcondition does not mention function result"); + + function Predecessor (Ctx : Context; Fld : Virtual_Field) return Virtual_Field with + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); + + pragma Warnings (Off, "postcondition does not mention function result"); + + function Valid_Predecessor (Ctx : Context; Fld : Virtual_Field) return Boolean with + Post => + True; - function Valid_Predecessor (Ctx : Context; Fld : Virtual_Field) return Boolean; + pragma Warnings (On, "postcondition does not mention function result"); function Valid_Next (Ctx : Context; Fld : Field) return Boolean; @@ -332,7 +368,13 @@ is Pre => Has_Buffer (Ctx); - function Incomplete_Message (Ctx : Context) return Boolean; + pragma Warnings (Off, "postcondition does not mention function result"); + + function Incomplete_Message (Ctx : Context) return Boolean with + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); pragma Warnings (Off, "precondition is always False"); @@ -373,9 +415,15 @@ is Has_Buffer (Ctx) and Present (Ctx, F_Data); + pragma Warnings (Off, "postcondition does not mention function result"); + function Valid_Length (Ctx : Context; Fld : Field; Length : RFLX_Types.Length) return Boolean with Pre => - Valid_Next (Ctx, Fld); + Valid_Next (Ctx, Fld), + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); procedure Set_Message_Type (Ctx : in out Context; Val : RFLX.Universal.Message_Type) with Pre => @@ -1082,6 +1130,8 @@ private type Cursor_State is (S_Valid, S_Structural_Valid, S_Invalid, S_Incomplete); + pragma Warnings (Off, "postcondition does not mention function result"); + function Valid_Value (Val : Field_Dependent_Value) return Boolean is ((case Val.Fld is when F_Message_Type => @@ -1095,7 +1145,12 @@ private when F_Values => True, when F_Initial | F_Final => - False)); + False)) + with + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); type Field_Cursor (State : Cursor_State := S_Invalid) is record diff --git a/tests/integration/session_comprehension_on_message_field/generated/rflx-universal-option.ads b/tests/integration/session_comprehension_on_message_field/generated/rflx-universal-option.ads index 0e2088b5b..553cfe1ed 100644 --- a/tests/integration/session_comprehension_on_message_field/generated/rflx-universal-option.ads +++ b/tests/integration/session_comprehension_on_message_field/generated/rflx-universal-option.ads @@ -110,8 +110,14 @@ is Depends => (Ctx => (Buffer, First, Last, Written_Last), Buffer => null); + pragma Warnings (Off, "postcondition does not mention function result"); + function Initialized (Ctx : Context) return Boolean with - Ghost; + Ghost, + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); procedure Reset (Ctx : in out Context) with Pre => @@ -241,15 +247,27 @@ is and then Structural_Valid_Message (Ctx) and then Data'Length = Byte_Size (Ctx); + pragma Warnings (Off, "postcondition does not mention function result"); + function Path_Condition (Ctx : Context; Fld : Field) return Boolean with Pre => - Valid_Predecessor (Ctx, Fld); + Valid_Predecessor (Ctx, Fld), + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); + + pragma Warnings (Off, "postcondition does not mention function result"); function Field_Condition (Ctx : Context; Val : Field_Dependent_Value) return Boolean with Pre => Has_Buffer (Ctx) and Val.Fld in Field'Range - and Valid_Predecessor (Ctx, Val.Fld); + and Valid_Predecessor (Ctx, Val.Fld), + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); function Field_Size (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Length with Pre => @@ -261,9 +279,15 @@ is when others => True); + pragma Warnings (Off, "postcondition does not mention function result"); + function Field_First (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Index with Pre => - Valid_Next (Ctx, Fld); + Valid_Next (Ctx, Fld), + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); function Field_Last (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Index with Pre => @@ -276,9 +300,21 @@ is when others => True); - function Predecessor (Ctx : Context; Fld : Virtual_Field) return Virtual_Field; + pragma Warnings (Off, "postcondition does not mention function result"); + + function Predecessor (Ctx : Context; Fld : Virtual_Field) return Virtual_Field with + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); + + pragma Warnings (Off, "postcondition does not mention function result"); + + function Valid_Predecessor (Ctx : Context; Fld : Virtual_Field) return Boolean with + Post => + True; - function Valid_Predecessor (Ctx : Context; Fld : Virtual_Field) return Boolean; + pragma Warnings (On, "postcondition does not mention function result"); function Valid_Next (Ctx : Context; Fld : Field) return Boolean; @@ -327,7 +363,13 @@ is Pre => Has_Buffer (Ctx); - function Incomplete_Message (Ctx : Context) return Boolean; + pragma Warnings (Off, "postcondition does not mention function result"); + + function Incomplete_Message (Ctx : Context) return Boolean with + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); pragma Warnings (Off, "precondition is always False"); @@ -364,9 +406,15 @@ is Has_Buffer (Ctx) and Present (Ctx, F_Data); + pragma Warnings (Off, "postcondition does not mention function result"); + function Valid_Length (Ctx : Context; Fld : Field; Length : RFLX_Types.Length) return Boolean with Pre => - Valid_Next (Ctx, Fld); + Valid_Next (Ctx, Fld), + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); procedure Set_Option_Type (Ctx : in out Context; Val : RFLX.Universal.Option_Type_Enum) with Pre => @@ -531,6 +579,8 @@ private type Cursor_State is (S_Valid, S_Structural_Valid, S_Invalid, S_Incomplete); + pragma Warnings (Off, "postcondition does not mention function result"); + function Valid_Value (Val : Field_Dependent_Value) return Boolean is ((case Val.Fld is when F_Option_Type => @@ -540,7 +590,12 @@ private when F_Data => True, when F_Initial | F_Final => - False)); + False)) + with + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); type Field_Cursor (State : Cursor_State := S_Invalid) is record diff --git a/tests/integration/session_comprehension_on_sequence/generated/rflx-universal-message.ads b/tests/integration/session_comprehension_on_sequence/generated/rflx-universal-message.ads index 489b50a8f..b70fa9f65 100644 --- a/tests/integration/session_comprehension_on_sequence/generated/rflx-universal-message.ads +++ b/tests/integration/session_comprehension_on_sequence/generated/rflx-universal-message.ads @@ -115,8 +115,14 @@ is Depends => (Ctx => (Buffer, First, Last, Written_Last), Buffer => null); + pragma Warnings (Off, "postcondition does not mention function result"); + function Initialized (Ctx : Context) return Boolean with - Ghost; + Ghost, + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); procedure Reset (Ctx : in out Context) with Pre => @@ -246,15 +252,27 @@ is and then Structural_Valid_Message (Ctx) and then Data'Length = Byte_Size (Ctx); + pragma Warnings (Off, "postcondition does not mention function result"); + function Path_Condition (Ctx : Context; Fld : Field) return Boolean with Pre => - Valid_Predecessor (Ctx, Fld); + Valid_Predecessor (Ctx, Fld), + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); + + pragma Warnings (Off, "postcondition does not mention function result"); function Field_Condition (Ctx : Context; Val : Field_Dependent_Value) return Boolean with Pre => Has_Buffer (Ctx) and Val.Fld in Field'Range - and Valid_Predecessor (Ctx, Val.Fld); + and Valid_Predecessor (Ctx, Val.Fld), + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); function Field_Size (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Length with Pre => @@ -266,9 +284,15 @@ is when others => True); + pragma Warnings (Off, "postcondition does not mention function result"); + function Field_First (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Index with Pre => - Valid_Next (Ctx, Fld); + Valid_Next (Ctx, Fld), + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); function Field_Last (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Index with Pre => @@ -281,9 +305,21 @@ is when others => True); - function Predecessor (Ctx : Context; Fld : Virtual_Field) return Virtual_Field; + pragma Warnings (Off, "postcondition does not mention function result"); + + function Predecessor (Ctx : Context; Fld : Virtual_Field) return Virtual_Field with + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); + + pragma Warnings (Off, "postcondition does not mention function result"); + + function Valid_Predecessor (Ctx : Context; Fld : Virtual_Field) return Boolean with + Post => + True; - function Valid_Predecessor (Ctx : Context; Fld : Virtual_Field) return Boolean; + pragma Warnings (On, "postcondition does not mention function result"); function Valid_Next (Ctx : Context; Fld : Field) return Boolean; @@ -332,7 +368,13 @@ is Pre => Has_Buffer (Ctx); - function Incomplete_Message (Ctx : Context) return Boolean; + pragma Warnings (Off, "postcondition does not mention function result"); + + function Incomplete_Message (Ctx : Context) return Boolean with + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); pragma Warnings (Off, "precondition is always False"); @@ -373,9 +415,15 @@ is Has_Buffer (Ctx) and Present (Ctx, F_Data); + pragma Warnings (Off, "postcondition does not mention function result"); + function Valid_Length (Ctx : Context; Fld : Field; Length : RFLX_Types.Length) return Boolean with Pre => - Valid_Next (Ctx, Fld); + Valid_Next (Ctx, Fld), + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); procedure Set_Message_Type (Ctx : in out Context; Val : RFLX.Universal.Message_Type) with Pre => @@ -1082,6 +1130,8 @@ private type Cursor_State is (S_Valid, S_Structural_Valid, S_Invalid, S_Incomplete); + pragma Warnings (Off, "postcondition does not mention function result"); + function Valid_Value (Val : Field_Dependent_Value) return Boolean is ((case Val.Fld is when F_Message_Type => @@ -1095,7 +1145,12 @@ private when F_Values => True, when F_Initial | F_Final => - False)); + False)) + with + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); type Field_Cursor (State : Cursor_State := S_Invalid) is record diff --git a/tests/integration/session_comprehension_on_sequence/generated/rflx-universal-option.ads b/tests/integration/session_comprehension_on_sequence/generated/rflx-universal-option.ads index 0e2088b5b..553cfe1ed 100644 --- a/tests/integration/session_comprehension_on_sequence/generated/rflx-universal-option.ads +++ b/tests/integration/session_comprehension_on_sequence/generated/rflx-universal-option.ads @@ -110,8 +110,14 @@ is Depends => (Ctx => (Buffer, First, Last, Written_Last), Buffer => null); + pragma Warnings (Off, "postcondition does not mention function result"); + function Initialized (Ctx : Context) return Boolean with - Ghost; + Ghost, + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); procedure Reset (Ctx : in out Context) with Pre => @@ -241,15 +247,27 @@ is and then Structural_Valid_Message (Ctx) and then Data'Length = Byte_Size (Ctx); + pragma Warnings (Off, "postcondition does not mention function result"); + function Path_Condition (Ctx : Context; Fld : Field) return Boolean with Pre => - Valid_Predecessor (Ctx, Fld); + Valid_Predecessor (Ctx, Fld), + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); + + pragma Warnings (Off, "postcondition does not mention function result"); function Field_Condition (Ctx : Context; Val : Field_Dependent_Value) return Boolean with Pre => Has_Buffer (Ctx) and Val.Fld in Field'Range - and Valid_Predecessor (Ctx, Val.Fld); + and Valid_Predecessor (Ctx, Val.Fld), + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); function Field_Size (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Length with Pre => @@ -261,9 +279,15 @@ is when others => True); + pragma Warnings (Off, "postcondition does not mention function result"); + function Field_First (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Index with Pre => - Valid_Next (Ctx, Fld); + Valid_Next (Ctx, Fld), + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); function Field_Last (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Index with Pre => @@ -276,9 +300,21 @@ is when others => True); - function Predecessor (Ctx : Context; Fld : Virtual_Field) return Virtual_Field; + pragma Warnings (Off, "postcondition does not mention function result"); + + function Predecessor (Ctx : Context; Fld : Virtual_Field) return Virtual_Field with + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); + + pragma Warnings (Off, "postcondition does not mention function result"); + + function Valid_Predecessor (Ctx : Context; Fld : Virtual_Field) return Boolean with + Post => + True; - function Valid_Predecessor (Ctx : Context; Fld : Virtual_Field) return Boolean; + pragma Warnings (On, "postcondition does not mention function result"); function Valid_Next (Ctx : Context; Fld : Field) return Boolean; @@ -327,7 +363,13 @@ is Pre => Has_Buffer (Ctx); - function Incomplete_Message (Ctx : Context) return Boolean; + pragma Warnings (Off, "postcondition does not mention function result"); + + function Incomplete_Message (Ctx : Context) return Boolean with + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); pragma Warnings (Off, "precondition is always False"); @@ -364,9 +406,15 @@ is Has_Buffer (Ctx) and Present (Ctx, F_Data); + pragma Warnings (Off, "postcondition does not mention function result"); + function Valid_Length (Ctx : Context; Fld : Field; Length : RFLX_Types.Length) return Boolean with Pre => - Valid_Next (Ctx, Fld); + Valid_Next (Ctx, Fld), + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); procedure Set_Option_Type (Ctx : in out Context; Val : RFLX.Universal.Option_Type_Enum) with Pre => @@ -531,6 +579,8 @@ private type Cursor_State is (S_Valid, S_Structural_Valid, S_Invalid, S_Incomplete); + pragma Warnings (Off, "postcondition does not mention function result"); + function Valid_Value (Val : Field_Dependent_Value) return Boolean is ((case Val.Fld is when F_Option_Type => @@ -540,7 +590,12 @@ private when F_Data => True, when F_Initial | F_Final => - False)); + False)) + with + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); type Field_Cursor (State : Cursor_State := S_Invalid) is record diff --git a/tests/integration/session_conversion/generated/rflx-universal-message.ads b/tests/integration/session_conversion/generated/rflx-universal-message.ads index 489b50a8f..b70fa9f65 100644 --- a/tests/integration/session_conversion/generated/rflx-universal-message.ads +++ b/tests/integration/session_conversion/generated/rflx-universal-message.ads @@ -115,8 +115,14 @@ is Depends => (Ctx => (Buffer, First, Last, Written_Last), Buffer => null); + pragma Warnings (Off, "postcondition does not mention function result"); + function Initialized (Ctx : Context) return Boolean with - Ghost; + Ghost, + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); procedure Reset (Ctx : in out Context) with Pre => @@ -246,15 +252,27 @@ is and then Structural_Valid_Message (Ctx) and then Data'Length = Byte_Size (Ctx); + pragma Warnings (Off, "postcondition does not mention function result"); + function Path_Condition (Ctx : Context; Fld : Field) return Boolean with Pre => - Valid_Predecessor (Ctx, Fld); + Valid_Predecessor (Ctx, Fld), + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); + + pragma Warnings (Off, "postcondition does not mention function result"); function Field_Condition (Ctx : Context; Val : Field_Dependent_Value) return Boolean with Pre => Has_Buffer (Ctx) and Val.Fld in Field'Range - and Valid_Predecessor (Ctx, Val.Fld); + and Valid_Predecessor (Ctx, Val.Fld), + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); function Field_Size (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Length with Pre => @@ -266,9 +284,15 @@ is when others => True); + pragma Warnings (Off, "postcondition does not mention function result"); + function Field_First (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Index with Pre => - Valid_Next (Ctx, Fld); + Valid_Next (Ctx, Fld), + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); function Field_Last (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Index with Pre => @@ -281,9 +305,21 @@ is when others => True); - function Predecessor (Ctx : Context; Fld : Virtual_Field) return Virtual_Field; + pragma Warnings (Off, "postcondition does not mention function result"); + + function Predecessor (Ctx : Context; Fld : Virtual_Field) return Virtual_Field with + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); + + pragma Warnings (Off, "postcondition does not mention function result"); + + function Valid_Predecessor (Ctx : Context; Fld : Virtual_Field) return Boolean with + Post => + True; - function Valid_Predecessor (Ctx : Context; Fld : Virtual_Field) return Boolean; + pragma Warnings (On, "postcondition does not mention function result"); function Valid_Next (Ctx : Context; Fld : Field) return Boolean; @@ -332,7 +368,13 @@ is Pre => Has_Buffer (Ctx); - function Incomplete_Message (Ctx : Context) return Boolean; + pragma Warnings (Off, "postcondition does not mention function result"); + + function Incomplete_Message (Ctx : Context) return Boolean with + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); pragma Warnings (Off, "precondition is always False"); @@ -373,9 +415,15 @@ is Has_Buffer (Ctx) and Present (Ctx, F_Data); + pragma Warnings (Off, "postcondition does not mention function result"); + function Valid_Length (Ctx : Context; Fld : Field; Length : RFLX_Types.Length) return Boolean with Pre => - Valid_Next (Ctx, Fld); + Valid_Next (Ctx, Fld), + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); procedure Set_Message_Type (Ctx : in out Context; Val : RFLX.Universal.Message_Type) with Pre => @@ -1082,6 +1130,8 @@ private type Cursor_State is (S_Valid, S_Structural_Valid, S_Invalid, S_Incomplete); + pragma Warnings (Off, "postcondition does not mention function result"); + function Valid_Value (Val : Field_Dependent_Value) return Boolean is ((case Val.Fld is when F_Message_Type => @@ -1095,7 +1145,12 @@ private when F_Values => True, when F_Initial | F_Final => - False)); + False)) + with + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); type Field_Cursor (State : Cursor_State := S_Invalid) is record diff --git a/tests/integration/session_conversion/generated/rflx-universal-option.ads b/tests/integration/session_conversion/generated/rflx-universal-option.ads index 0e2088b5b..553cfe1ed 100644 --- a/tests/integration/session_conversion/generated/rflx-universal-option.ads +++ b/tests/integration/session_conversion/generated/rflx-universal-option.ads @@ -110,8 +110,14 @@ is Depends => (Ctx => (Buffer, First, Last, Written_Last), Buffer => null); + pragma Warnings (Off, "postcondition does not mention function result"); + function Initialized (Ctx : Context) return Boolean with - Ghost; + Ghost, + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); procedure Reset (Ctx : in out Context) with Pre => @@ -241,15 +247,27 @@ is and then Structural_Valid_Message (Ctx) and then Data'Length = Byte_Size (Ctx); + pragma Warnings (Off, "postcondition does not mention function result"); + function Path_Condition (Ctx : Context; Fld : Field) return Boolean with Pre => - Valid_Predecessor (Ctx, Fld); + Valid_Predecessor (Ctx, Fld), + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); + + pragma Warnings (Off, "postcondition does not mention function result"); function Field_Condition (Ctx : Context; Val : Field_Dependent_Value) return Boolean with Pre => Has_Buffer (Ctx) and Val.Fld in Field'Range - and Valid_Predecessor (Ctx, Val.Fld); + and Valid_Predecessor (Ctx, Val.Fld), + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); function Field_Size (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Length with Pre => @@ -261,9 +279,15 @@ is when others => True); + pragma Warnings (Off, "postcondition does not mention function result"); + function Field_First (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Index with Pre => - Valid_Next (Ctx, Fld); + Valid_Next (Ctx, Fld), + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); function Field_Last (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Index with Pre => @@ -276,9 +300,21 @@ is when others => True); - function Predecessor (Ctx : Context; Fld : Virtual_Field) return Virtual_Field; + pragma Warnings (Off, "postcondition does not mention function result"); + + function Predecessor (Ctx : Context; Fld : Virtual_Field) return Virtual_Field with + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); + + pragma Warnings (Off, "postcondition does not mention function result"); + + function Valid_Predecessor (Ctx : Context; Fld : Virtual_Field) return Boolean with + Post => + True; - function Valid_Predecessor (Ctx : Context; Fld : Virtual_Field) return Boolean; + pragma Warnings (On, "postcondition does not mention function result"); function Valid_Next (Ctx : Context; Fld : Field) return Boolean; @@ -327,7 +363,13 @@ is Pre => Has_Buffer (Ctx); - function Incomplete_Message (Ctx : Context) return Boolean; + pragma Warnings (Off, "postcondition does not mention function result"); + + function Incomplete_Message (Ctx : Context) return Boolean with + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); pragma Warnings (Off, "precondition is always False"); @@ -364,9 +406,15 @@ is Has_Buffer (Ctx) and Present (Ctx, F_Data); + pragma Warnings (Off, "postcondition does not mention function result"); + function Valid_Length (Ctx : Context; Fld : Field; Length : RFLX_Types.Length) return Boolean with Pre => - Valid_Next (Ctx, Fld); + Valid_Next (Ctx, Fld), + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); procedure Set_Option_Type (Ctx : in out Context; Val : RFLX.Universal.Option_Type_Enum) with Pre => @@ -531,6 +579,8 @@ private type Cursor_State is (S_Valid, S_Structural_Valid, S_Invalid, S_Incomplete); + pragma Warnings (Off, "postcondition does not mention function result"); + function Valid_Value (Val : Field_Dependent_Value) return Boolean is ((case Val.Fld is when F_Option_Type => @@ -540,7 +590,12 @@ private when F_Data => True, when F_Initial | F_Final => - False)); + False)) + with + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); type Field_Cursor (State : Cursor_State := S_Invalid) is record diff --git a/tests/integration/session_endianness/generated/rflx-messages-msg.ads b/tests/integration/session_endianness/generated/rflx-messages-msg.ads index 2b3e8d4f4..34a9a94b7 100644 --- a/tests/integration/session_endianness/generated/rflx-messages-msg.ads +++ b/tests/integration/session_endianness/generated/rflx-messages-msg.ads @@ -108,8 +108,14 @@ is Depends => (Ctx => (Buffer, First, Last, Written_Last), Buffer => null); + pragma Warnings (Off, "postcondition does not mention function result"); + function Initialized (Ctx : Context) return Boolean with - Ghost; + Ghost, + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); procedure Reset (Ctx : in out Context) with Pre => @@ -239,32 +245,62 @@ is and then Structural_Valid_Message (Ctx) and then Data'Length = Byte_Size (Ctx); + pragma Warnings (Off, "postcondition does not mention function result"); + function Path_Condition (Ctx : Context; Fld : Field) return Boolean with Pre => - Valid_Predecessor (Ctx, Fld); + Valid_Predecessor (Ctx, Fld), + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); + + pragma Warnings (Off, "postcondition does not mention function result"); function Field_Condition (Ctx : Context; Val : Field_Dependent_Value) return Boolean with Pre => Has_Buffer (Ctx) and Val.Fld in Field'Range - and Valid_Predecessor (Ctx, Val.Fld); + and Valid_Predecessor (Ctx, Val.Fld), + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); function Field_Size (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Length with Pre => Valid_Next (Ctx, Fld); + pragma Warnings (Off, "postcondition does not mention function result"); + function Field_First (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Index with Pre => - Valid_Next (Ctx, Fld); + Valid_Next (Ctx, Fld), + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); function Field_Last (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Index with Pre => Valid_Next (Ctx, Fld) and then Available_Space (Ctx, Fld) >= Field_Size (Ctx, Fld); - function Predecessor (Ctx : Context; Fld : Virtual_Field) return Virtual_Field; + pragma Warnings (Off, "postcondition does not mention function result"); + + function Predecessor (Ctx : Context; Fld : Virtual_Field) return Virtual_Field with + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); + + pragma Warnings (Off, "postcondition does not mention function result"); - function Valid_Predecessor (Ctx : Context; Fld : Virtual_Field) return Boolean; + function Valid_Predecessor (Ctx : Context; Fld : Virtual_Field) return Boolean with + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); function Valid_Next (Ctx : Context; Fld : Field) return Boolean; @@ -308,7 +344,13 @@ is Pre => Has_Buffer (Ctx); - function Incomplete_Message (Ctx : Context) return Boolean; + pragma Warnings (Off, "postcondition does not mention function result"); + + function Incomplete_Message (Ctx : Context) return Boolean with + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); pragma Warnings (Off, "precondition is always False"); @@ -322,9 +364,15 @@ is pragma Warnings (On, "precondition is always False"); + pragma Warnings (Off, "postcondition does not mention function result"); + function Valid_Length (Ctx : Context; Fld : Field; Length : RFLX_Types.Length) return Boolean with Pre => - Valid_Next (Ctx, Fld); + Valid_Next (Ctx, Fld), + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); procedure Set_A (Ctx : in out Context; Val : RFLX.Messages.Integer) with Pre => @@ -405,6 +453,8 @@ private type Cursor_State is (S_Valid, S_Structural_Valid, S_Invalid, S_Incomplete); + pragma Warnings (Off, "postcondition does not mention function result"); + function Valid_Value (Val : Field_Dependent_Value) return Boolean is ((case Val.Fld is when F_A => @@ -412,7 +462,12 @@ private when F_B => Valid (Val.B_Value), when F_Initial | F_Final => - False)); + False)) + with + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); type Field_Cursor (State : Cursor_State := S_Invalid) is record diff --git a/tests/integration/session_endianness/generated/rflx-messages-msg_le.ads b/tests/integration/session_endianness/generated/rflx-messages-msg_le.ads index 592b322ef..ae0ec5b11 100644 --- a/tests/integration/session_endianness/generated/rflx-messages-msg_le.ads +++ b/tests/integration/session_endianness/generated/rflx-messages-msg_le.ads @@ -108,8 +108,14 @@ is Depends => (Ctx => (Buffer, First, Last, Written_Last), Buffer => null); + pragma Warnings (Off, "postcondition does not mention function result"); + function Initialized (Ctx : Context) return Boolean with - Ghost; + Ghost, + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); procedure Reset (Ctx : in out Context) with Pre => @@ -239,32 +245,62 @@ is and then Structural_Valid_Message (Ctx) and then Data'Length = Byte_Size (Ctx); + pragma Warnings (Off, "postcondition does not mention function result"); + function Path_Condition (Ctx : Context; Fld : Field) return Boolean with Pre => - Valid_Predecessor (Ctx, Fld); + Valid_Predecessor (Ctx, Fld), + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); + + pragma Warnings (Off, "postcondition does not mention function result"); function Field_Condition (Ctx : Context; Val : Field_Dependent_Value) return Boolean with Pre => Has_Buffer (Ctx) and Val.Fld in Field'Range - and Valid_Predecessor (Ctx, Val.Fld); + and Valid_Predecessor (Ctx, Val.Fld), + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); function Field_Size (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Length with Pre => Valid_Next (Ctx, Fld); + pragma Warnings (Off, "postcondition does not mention function result"); + function Field_First (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Index with Pre => - Valid_Next (Ctx, Fld); + Valid_Next (Ctx, Fld), + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); function Field_Last (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Index with Pre => Valid_Next (Ctx, Fld) and then Available_Space (Ctx, Fld) >= Field_Size (Ctx, Fld); - function Predecessor (Ctx : Context; Fld : Virtual_Field) return Virtual_Field; + pragma Warnings (Off, "postcondition does not mention function result"); + + function Predecessor (Ctx : Context; Fld : Virtual_Field) return Virtual_Field with + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); + + pragma Warnings (Off, "postcondition does not mention function result"); - function Valid_Predecessor (Ctx : Context; Fld : Virtual_Field) return Boolean; + function Valid_Predecessor (Ctx : Context; Fld : Virtual_Field) return Boolean with + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); function Valid_Next (Ctx : Context; Fld : Field) return Boolean; @@ -308,7 +344,13 @@ is Pre => Has_Buffer (Ctx); - function Incomplete_Message (Ctx : Context) return Boolean; + pragma Warnings (Off, "postcondition does not mention function result"); + + function Incomplete_Message (Ctx : Context) return Boolean with + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); pragma Warnings (Off, "precondition is always False"); @@ -322,9 +364,15 @@ is pragma Warnings (On, "precondition is always False"); + pragma Warnings (Off, "postcondition does not mention function result"); + function Valid_Length (Ctx : Context; Fld : Field; Length : RFLX_Types.Length) return Boolean with Pre => - Valid_Next (Ctx, Fld); + Valid_Next (Ctx, Fld), + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); procedure Set_C (Ctx : in out Context; Val : RFLX.Messages.Integer) with Pre => @@ -405,6 +453,8 @@ private type Cursor_State is (S_Valid, S_Structural_Valid, S_Invalid, S_Incomplete); + pragma Warnings (Off, "postcondition does not mention function result"); + function Valid_Value (Val : Field_Dependent_Value) return Boolean is ((case Val.Fld is when F_C => @@ -412,7 +462,12 @@ private when F_D => Valid (Val.D_Value), when F_Initial | F_Final => - False)); + False)) + with + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); type Field_Cursor (State : Cursor_State := S_Invalid) is record diff --git a/tests/integration/session_endianness/generated/rflx-messages-msg_le_nested.ads b/tests/integration/session_endianness/generated/rflx-messages-msg_le_nested.ads index 939cfd222..431c56c69 100644 --- a/tests/integration/session_endianness/generated/rflx-messages-msg_le_nested.ads +++ b/tests/integration/session_endianness/generated/rflx-messages-msg_le_nested.ads @@ -110,8 +110,14 @@ is Depends => (Ctx => (Buffer, First, Last, Written_Last), Buffer => null); + pragma Warnings (Off, "postcondition does not mention function result"); + function Initialized (Ctx : Context) return Boolean with - Ghost; + Ghost, + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); procedure Reset (Ctx : in out Context) with Pre => @@ -241,32 +247,62 @@ is and then Structural_Valid_Message (Ctx) and then Data'Length = Byte_Size (Ctx); + pragma Warnings (Off, "postcondition does not mention function result"); + function Path_Condition (Ctx : Context; Fld : Field) return Boolean with Pre => - Valid_Predecessor (Ctx, Fld); + Valid_Predecessor (Ctx, Fld), + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); + + pragma Warnings (Off, "postcondition does not mention function result"); function Field_Condition (Ctx : Context; Val : Field_Dependent_Value) return Boolean with Pre => Has_Buffer (Ctx) and Val.Fld in Field'Range - and Valid_Predecessor (Ctx, Val.Fld); + and Valid_Predecessor (Ctx, Val.Fld), + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); function Field_Size (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Length with Pre => Valid_Next (Ctx, Fld); + pragma Warnings (Off, "postcondition does not mention function result"); + function Field_First (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Index with Pre => - Valid_Next (Ctx, Fld); + Valid_Next (Ctx, Fld), + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); function Field_Last (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Index with Pre => Valid_Next (Ctx, Fld) and then Available_Space (Ctx, Fld) >= Field_Size (Ctx, Fld); - function Predecessor (Ctx : Context; Fld : Virtual_Field) return Virtual_Field; + pragma Warnings (Off, "postcondition does not mention function result"); + + function Predecessor (Ctx : Context; Fld : Virtual_Field) return Virtual_Field with + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); + + pragma Warnings (Off, "postcondition does not mention function result"); - function Valid_Predecessor (Ctx : Context; Fld : Virtual_Field) return Boolean; + function Valid_Predecessor (Ctx : Context; Fld : Virtual_Field) return Boolean with + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); function Valid_Next (Ctx : Context; Fld : Field) return Boolean; @@ -310,7 +346,13 @@ is Pre => Has_Buffer (Ctx); - function Incomplete_Message (Ctx : Context) return Boolean; + pragma Warnings (Off, "postcondition does not mention function result"); + + function Incomplete_Message (Ctx : Context) return Boolean with + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); pragma Warnings (Off, "precondition is always False"); @@ -328,9 +370,15 @@ is pragma Warnings (On, "precondition is always False"); + pragma Warnings (Off, "postcondition does not mention function result"); + function Valid_Length (Ctx : Context; Fld : Field; Length : RFLX_Types.Length) return Boolean with Pre => - Valid_Next (Ctx, Fld); + Valid_Next (Ctx, Fld), + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); procedure Set_X_A (Ctx : in out Context; Val : RFLX.Messages.Integer) with Pre => @@ -439,6 +487,8 @@ private type Cursor_State is (S_Valid, S_Structural_Valid, S_Invalid, S_Incomplete); + pragma Warnings (Off, "postcondition does not mention function result"); + function Valid_Value (Val : Field_Dependent_Value) return Boolean is ((case Val.Fld is when F_X_A => @@ -448,7 +498,12 @@ private when F_Y => Valid (Val.Y_Value), when F_Initial | F_Final => - False)); + False)) + with + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); type Field_Cursor (State : Cursor_State := S_Invalid) is record diff --git a/tests/integration/session_functions/generated/rflx-fixed_size-simple_message.ads b/tests/integration/session_functions/generated/rflx-fixed_size-simple_message.ads index 233784ea2..c7be1983d 100644 --- a/tests/integration/session_functions/generated/rflx-fixed_size-simple_message.ads +++ b/tests/integration/session_functions/generated/rflx-fixed_size-simple_message.ads @@ -110,8 +110,14 @@ is Depends => (Ctx => (Buffer, First, Last, Written_Last), Buffer => null); + pragma Warnings (Off, "postcondition does not mention function result"); + function Initialized (Ctx : Context) return Boolean with - Ghost; + Ghost, + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); procedure Reset (Ctx : in out Context) with Pre => @@ -241,15 +247,27 @@ is and then Structural_Valid_Message (Ctx) and then Data'Length = Byte_Size (Ctx); + pragma Warnings (Off, "postcondition does not mention function result"); + function Path_Condition (Ctx : Context; Fld : Field) return Boolean with Pre => - Valid_Predecessor (Ctx, Fld); + Valid_Predecessor (Ctx, Fld), + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); + + pragma Warnings (Off, "postcondition does not mention function result"); function Field_Condition (Ctx : Context; Val : Field_Dependent_Value) return Boolean with Pre => Has_Buffer (Ctx) and Val.Fld in Field'Range - and Valid_Predecessor (Ctx, Val.Fld); + and Valid_Predecessor (Ctx, Val.Fld), + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); function Field_Size (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Length with Pre => @@ -261,9 +279,15 @@ is when others => True); + pragma Warnings (Off, "postcondition does not mention function result"); + function Field_First (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Index with Pre => - Valid_Next (Ctx, Fld); + Valid_Next (Ctx, Fld), + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); function Field_Last (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Index with Pre => @@ -276,9 +300,21 @@ is when others => True); - function Predecessor (Ctx : Context; Fld : Virtual_Field) return Virtual_Field; + pragma Warnings (Off, "postcondition does not mention function result"); + + function Predecessor (Ctx : Context; Fld : Virtual_Field) return Virtual_Field with + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); + + pragma Warnings (Off, "postcondition does not mention function result"); + + function Valid_Predecessor (Ctx : Context; Fld : Virtual_Field) return Boolean with + Post => + True; - function Valid_Predecessor (Ctx : Context; Fld : Virtual_Field) return Boolean; + pragma Warnings (On, "postcondition does not mention function result"); function Valid_Next (Ctx : Context; Fld : Field) return Boolean; @@ -327,7 +363,13 @@ is Pre => Has_Buffer (Ctx); - function Incomplete_Message (Ctx : Context) return Boolean; + pragma Warnings (Off, "postcondition does not mention function result"); + + function Incomplete_Message (Ctx : Context) return Boolean with + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); pragma Warnings (Off, "precondition is always False"); @@ -360,9 +402,15 @@ is Has_Buffer (Ctx) and Present (Ctx, F_Data); + pragma Warnings (Off, "postcondition does not mention function result"); + function Valid_Length (Ctx : Context; Fld : Field; Length : RFLX_Types.Length) return Boolean with Pre => - Valid_Next (Ctx, Fld); + Valid_Next (Ctx, Fld), + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); procedure Set_Message_Type (Ctx : in out Context; Val : RFLX.Universal.Option_Type_Enum) with Pre => @@ -492,6 +540,8 @@ private type Cursor_State is (S_Valid, S_Structural_Valid, S_Invalid, S_Incomplete); + pragma Warnings (Off, "postcondition does not mention function result"); + function Valid_Value (Val : Field_Dependent_Value) return Boolean is ((case Val.Fld is when F_Message_Type => @@ -499,7 +549,12 @@ private when F_Data => True, when F_Initial | F_Final => - False)); + False)) + with + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); type Field_Cursor (State : Cursor_State := S_Invalid) is record diff --git a/tests/integration/session_functions/generated/rflx-universal-message.ads b/tests/integration/session_functions/generated/rflx-universal-message.ads index 489b50a8f..b70fa9f65 100644 --- a/tests/integration/session_functions/generated/rflx-universal-message.ads +++ b/tests/integration/session_functions/generated/rflx-universal-message.ads @@ -115,8 +115,14 @@ is Depends => (Ctx => (Buffer, First, Last, Written_Last), Buffer => null); + pragma Warnings (Off, "postcondition does not mention function result"); + function Initialized (Ctx : Context) return Boolean with - Ghost; + Ghost, + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); procedure Reset (Ctx : in out Context) with Pre => @@ -246,15 +252,27 @@ is and then Structural_Valid_Message (Ctx) and then Data'Length = Byte_Size (Ctx); + pragma Warnings (Off, "postcondition does not mention function result"); + function Path_Condition (Ctx : Context; Fld : Field) return Boolean with Pre => - Valid_Predecessor (Ctx, Fld); + Valid_Predecessor (Ctx, Fld), + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); + + pragma Warnings (Off, "postcondition does not mention function result"); function Field_Condition (Ctx : Context; Val : Field_Dependent_Value) return Boolean with Pre => Has_Buffer (Ctx) and Val.Fld in Field'Range - and Valid_Predecessor (Ctx, Val.Fld); + and Valid_Predecessor (Ctx, Val.Fld), + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); function Field_Size (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Length with Pre => @@ -266,9 +284,15 @@ is when others => True); + pragma Warnings (Off, "postcondition does not mention function result"); + function Field_First (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Index with Pre => - Valid_Next (Ctx, Fld); + Valid_Next (Ctx, Fld), + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); function Field_Last (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Index with Pre => @@ -281,9 +305,21 @@ is when others => True); - function Predecessor (Ctx : Context; Fld : Virtual_Field) return Virtual_Field; + pragma Warnings (Off, "postcondition does not mention function result"); + + function Predecessor (Ctx : Context; Fld : Virtual_Field) return Virtual_Field with + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); + + pragma Warnings (Off, "postcondition does not mention function result"); + + function Valid_Predecessor (Ctx : Context; Fld : Virtual_Field) return Boolean with + Post => + True; - function Valid_Predecessor (Ctx : Context; Fld : Virtual_Field) return Boolean; + pragma Warnings (On, "postcondition does not mention function result"); function Valid_Next (Ctx : Context; Fld : Field) return Boolean; @@ -332,7 +368,13 @@ is Pre => Has_Buffer (Ctx); - function Incomplete_Message (Ctx : Context) return Boolean; + pragma Warnings (Off, "postcondition does not mention function result"); + + function Incomplete_Message (Ctx : Context) return Boolean with + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); pragma Warnings (Off, "precondition is always False"); @@ -373,9 +415,15 @@ is Has_Buffer (Ctx) and Present (Ctx, F_Data); + pragma Warnings (Off, "postcondition does not mention function result"); + function Valid_Length (Ctx : Context; Fld : Field; Length : RFLX_Types.Length) return Boolean with Pre => - Valid_Next (Ctx, Fld); + Valid_Next (Ctx, Fld), + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); procedure Set_Message_Type (Ctx : in out Context; Val : RFLX.Universal.Message_Type) with Pre => @@ -1082,6 +1130,8 @@ private type Cursor_State is (S_Valid, S_Structural_Valid, S_Invalid, S_Incomplete); + pragma Warnings (Off, "postcondition does not mention function result"); + function Valid_Value (Val : Field_Dependent_Value) return Boolean is ((case Val.Fld is when F_Message_Type => @@ -1095,7 +1145,12 @@ private when F_Values => True, when F_Initial | F_Final => - False)); + False)) + with + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); type Field_Cursor (State : Cursor_State := S_Invalid) is record diff --git a/tests/integration/session_functions/generated/rflx-universal-option.ads b/tests/integration/session_functions/generated/rflx-universal-option.ads index 0e2088b5b..553cfe1ed 100644 --- a/tests/integration/session_functions/generated/rflx-universal-option.ads +++ b/tests/integration/session_functions/generated/rflx-universal-option.ads @@ -110,8 +110,14 @@ is Depends => (Ctx => (Buffer, First, Last, Written_Last), Buffer => null); + pragma Warnings (Off, "postcondition does not mention function result"); + function Initialized (Ctx : Context) return Boolean with - Ghost; + Ghost, + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); procedure Reset (Ctx : in out Context) with Pre => @@ -241,15 +247,27 @@ is and then Structural_Valid_Message (Ctx) and then Data'Length = Byte_Size (Ctx); + pragma Warnings (Off, "postcondition does not mention function result"); + function Path_Condition (Ctx : Context; Fld : Field) return Boolean with Pre => - Valid_Predecessor (Ctx, Fld); + Valid_Predecessor (Ctx, Fld), + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); + + pragma Warnings (Off, "postcondition does not mention function result"); function Field_Condition (Ctx : Context; Val : Field_Dependent_Value) return Boolean with Pre => Has_Buffer (Ctx) and Val.Fld in Field'Range - and Valid_Predecessor (Ctx, Val.Fld); + and Valid_Predecessor (Ctx, Val.Fld), + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); function Field_Size (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Length with Pre => @@ -261,9 +279,15 @@ is when others => True); + pragma Warnings (Off, "postcondition does not mention function result"); + function Field_First (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Index with Pre => - Valid_Next (Ctx, Fld); + Valid_Next (Ctx, Fld), + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); function Field_Last (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Index with Pre => @@ -276,9 +300,21 @@ is when others => True); - function Predecessor (Ctx : Context; Fld : Virtual_Field) return Virtual_Field; + pragma Warnings (Off, "postcondition does not mention function result"); + + function Predecessor (Ctx : Context; Fld : Virtual_Field) return Virtual_Field with + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); + + pragma Warnings (Off, "postcondition does not mention function result"); + + function Valid_Predecessor (Ctx : Context; Fld : Virtual_Field) return Boolean with + Post => + True; - function Valid_Predecessor (Ctx : Context; Fld : Virtual_Field) return Boolean; + pragma Warnings (On, "postcondition does not mention function result"); function Valid_Next (Ctx : Context; Fld : Field) return Boolean; @@ -327,7 +363,13 @@ is Pre => Has_Buffer (Ctx); - function Incomplete_Message (Ctx : Context) return Boolean; + pragma Warnings (Off, "postcondition does not mention function result"); + + function Incomplete_Message (Ctx : Context) return Boolean with + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); pragma Warnings (Off, "precondition is always False"); @@ -364,9 +406,15 @@ is Has_Buffer (Ctx) and Present (Ctx, F_Data); + pragma Warnings (Off, "postcondition does not mention function result"); + function Valid_Length (Ctx : Context; Fld : Field; Length : RFLX_Types.Length) return Boolean with Pre => - Valid_Next (Ctx, Fld); + Valid_Next (Ctx, Fld), + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); procedure Set_Option_Type (Ctx : in out Context; Val : RFLX.Universal.Option_Type_Enum) with Pre => @@ -531,6 +579,8 @@ private type Cursor_State is (S_Valid, S_Structural_Valid, S_Invalid, S_Incomplete); + pragma Warnings (Off, "postcondition does not mention function result"); + function Valid_Value (Val : Field_Dependent_Value) return Boolean is ((case Val.Fld is when F_Option_Type => @@ -540,7 +590,12 @@ private when F_Data => True, when F_Initial | F_Final => - False)); + False)) + with + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); type Field_Cursor (State : Cursor_State := S_Invalid) is record diff --git a/tests/integration/session_integration/generated/rflx-universal-message.ads b/tests/integration/session_integration/generated/rflx-universal-message.ads index 489b50a8f..b70fa9f65 100644 --- a/tests/integration/session_integration/generated/rflx-universal-message.ads +++ b/tests/integration/session_integration/generated/rflx-universal-message.ads @@ -115,8 +115,14 @@ is Depends => (Ctx => (Buffer, First, Last, Written_Last), Buffer => null); + pragma Warnings (Off, "postcondition does not mention function result"); + function Initialized (Ctx : Context) return Boolean with - Ghost; + Ghost, + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); procedure Reset (Ctx : in out Context) with Pre => @@ -246,15 +252,27 @@ is and then Structural_Valid_Message (Ctx) and then Data'Length = Byte_Size (Ctx); + pragma Warnings (Off, "postcondition does not mention function result"); + function Path_Condition (Ctx : Context; Fld : Field) return Boolean with Pre => - Valid_Predecessor (Ctx, Fld); + Valid_Predecessor (Ctx, Fld), + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); + + pragma Warnings (Off, "postcondition does not mention function result"); function Field_Condition (Ctx : Context; Val : Field_Dependent_Value) return Boolean with Pre => Has_Buffer (Ctx) and Val.Fld in Field'Range - and Valid_Predecessor (Ctx, Val.Fld); + and Valid_Predecessor (Ctx, Val.Fld), + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); function Field_Size (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Length with Pre => @@ -266,9 +284,15 @@ is when others => True); + pragma Warnings (Off, "postcondition does not mention function result"); + function Field_First (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Index with Pre => - Valid_Next (Ctx, Fld); + Valid_Next (Ctx, Fld), + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); function Field_Last (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Index with Pre => @@ -281,9 +305,21 @@ is when others => True); - function Predecessor (Ctx : Context; Fld : Virtual_Field) return Virtual_Field; + pragma Warnings (Off, "postcondition does not mention function result"); + + function Predecessor (Ctx : Context; Fld : Virtual_Field) return Virtual_Field with + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); + + pragma Warnings (Off, "postcondition does not mention function result"); + + function Valid_Predecessor (Ctx : Context; Fld : Virtual_Field) return Boolean with + Post => + True; - function Valid_Predecessor (Ctx : Context; Fld : Virtual_Field) return Boolean; + pragma Warnings (On, "postcondition does not mention function result"); function Valid_Next (Ctx : Context; Fld : Field) return Boolean; @@ -332,7 +368,13 @@ is Pre => Has_Buffer (Ctx); - function Incomplete_Message (Ctx : Context) return Boolean; + pragma Warnings (Off, "postcondition does not mention function result"); + + function Incomplete_Message (Ctx : Context) return Boolean with + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); pragma Warnings (Off, "precondition is always False"); @@ -373,9 +415,15 @@ is Has_Buffer (Ctx) and Present (Ctx, F_Data); + pragma Warnings (Off, "postcondition does not mention function result"); + function Valid_Length (Ctx : Context; Fld : Field; Length : RFLX_Types.Length) return Boolean with Pre => - Valid_Next (Ctx, Fld); + Valid_Next (Ctx, Fld), + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); procedure Set_Message_Type (Ctx : in out Context; Val : RFLX.Universal.Message_Type) with Pre => @@ -1082,6 +1130,8 @@ private type Cursor_State is (S_Valid, S_Structural_Valid, S_Invalid, S_Incomplete); + pragma Warnings (Off, "postcondition does not mention function result"); + function Valid_Value (Val : Field_Dependent_Value) return Boolean is ((case Val.Fld is when F_Message_Type => @@ -1095,7 +1145,12 @@ private when F_Values => True, when F_Initial | F_Final => - False)); + False)) + with + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); type Field_Cursor (State : Cursor_State := S_Invalid) is record diff --git a/tests/integration/session_integration/generated/rflx-universal-option.ads b/tests/integration/session_integration/generated/rflx-universal-option.ads index 0e2088b5b..553cfe1ed 100644 --- a/tests/integration/session_integration/generated/rflx-universal-option.ads +++ b/tests/integration/session_integration/generated/rflx-universal-option.ads @@ -110,8 +110,14 @@ is Depends => (Ctx => (Buffer, First, Last, Written_Last), Buffer => null); + pragma Warnings (Off, "postcondition does not mention function result"); + function Initialized (Ctx : Context) return Boolean with - Ghost; + Ghost, + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); procedure Reset (Ctx : in out Context) with Pre => @@ -241,15 +247,27 @@ is and then Structural_Valid_Message (Ctx) and then Data'Length = Byte_Size (Ctx); + pragma Warnings (Off, "postcondition does not mention function result"); + function Path_Condition (Ctx : Context; Fld : Field) return Boolean with Pre => - Valid_Predecessor (Ctx, Fld); + Valid_Predecessor (Ctx, Fld), + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); + + pragma Warnings (Off, "postcondition does not mention function result"); function Field_Condition (Ctx : Context; Val : Field_Dependent_Value) return Boolean with Pre => Has_Buffer (Ctx) and Val.Fld in Field'Range - and Valid_Predecessor (Ctx, Val.Fld); + and Valid_Predecessor (Ctx, Val.Fld), + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); function Field_Size (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Length with Pre => @@ -261,9 +279,15 @@ is when others => True); + pragma Warnings (Off, "postcondition does not mention function result"); + function Field_First (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Index with Pre => - Valid_Next (Ctx, Fld); + Valid_Next (Ctx, Fld), + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); function Field_Last (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Index with Pre => @@ -276,9 +300,21 @@ is when others => True); - function Predecessor (Ctx : Context; Fld : Virtual_Field) return Virtual_Field; + pragma Warnings (Off, "postcondition does not mention function result"); + + function Predecessor (Ctx : Context; Fld : Virtual_Field) return Virtual_Field with + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); + + pragma Warnings (Off, "postcondition does not mention function result"); + + function Valid_Predecessor (Ctx : Context; Fld : Virtual_Field) return Boolean with + Post => + True; - function Valid_Predecessor (Ctx : Context; Fld : Virtual_Field) return Boolean; + pragma Warnings (On, "postcondition does not mention function result"); function Valid_Next (Ctx : Context; Fld : Field) return Boolean; @@ -327,7 +363,13 @@ is Pre => Has_Buffer (Ctx); - function Incomplete_Message (Ctx : Context) return Boolean; + pragma Warnings (Off, "postcondition does not mention function result"); + + function Incomplete_Message (Ctx : Context) return Boolean with + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); pragma Warnings (Off, "precondition is always False"); @@ -364,9 +406,15 @@ is Has_Buffer (Ctx) and Present (Ctx, F_Data); + pragma Warnings (Off, "postcondition does not mention function result"); + function Valid_Length (Ctx : Context; Fld : Field; Length : RFLX_Types.Length) return Boolean with Pre => - Valid_Next (Ctx, Fld); + Valid_Next (Ctx, Fld), + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); procedure Set_Option_Type (Ctx : in out Context; Val : RFLX.Universal.Option_Type_Enum) with Pre => @@ -531,6 +579,8 @@ private type Cursor_State is (S_Valid, S_Structural_Valid, S_Invalid, S_Incomplete); + pragma Warnings (Off, "postcondition does not mention function result"); + function Valid_Value (Val : Field_Dependent_Value) return Boolean is ((case Val.Fld is when F_Option_Type => @@ -540,7 +590,12 @@ private when F_Data => True, when F_Initial | F_Final => - False)); + False)) + with + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); type Field_Cursor (State : Cursor_State := S_Invalid) is record diff --git a/tests/integration/session_integration_multiple/generated/rflx-universal-message.ads b/tests/integration/session_integration_multiple/generated/rflx-universal-message.ads index 489b50a8f..b70fa9f65 100644 --- a/tests/integration/session_integration_multiple/generated/rflx-universal-message.ads +++ b/tests/integration/session_integration_multiple/generated/rflx-universal-message.ads @@ -115,8 +115,14 @@ is Depends => (Ctx => (Buffer, First, Last, Written_Last), Buffer => null); + pragma Warnings (Off, "postcondition does not mention function result"); + function Initialized (Ctx : Context) return Boolean with - Ghost; + Ghost, + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); procedure Reset (Ctx : in out Context) with Pre => @@ -246,15 +252,27 @@ is and then Structural_Valid_Message (Ctx) and then Data'Length = Byte_Size (Ctx); + pragma Warnings (Off, "postcondition does not mention function result"); + function Path_Condition (Ctx : Context; Fld : Field) return Boolean with Pre => - Valid_Predecessor (Ctx, Fld); + Valid_Predecessor (Ctx, Fld), + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); + + pragma Warnings (Off, "postcondition does not mention function result"); function Field_Condition (Ctx : Context; Val : Field_Dependent_Value) return Boolean with Pre => Has_Buffer (Ctx) and Val.Fld in Field'Range - and Valid_Predecessor (Ctx, Val.Fld); + and Valid_Predecessor (Ctx, Val.Fld), + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); function Field_Size (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Length with Pre => @@ -266,9 +284,15 @@ is when others => True); + pragma Warnings (Off, "postcondition does not mention function result"); + function Field_First (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Index with Pre => - Valid_Next (Ctx, Fld); + Valid_Next (Ctx, Fld), + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); function Field_Last (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Index with Pre => @@ -281,9 +305,21 @@ is when others => True); - function Predecessor (Ctx : Context; Fld : Virtual_Field) return Virtual_Field; + pragma Warnings (Off, "postcondition does not mention function result"); + + function Predecessor (Ctx : Context; Fld : Virtual_Field) return Virtual_Field with + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); + + pragma Warnings (Off, "postcondition does not mention function result"); + + function Valid_Predecessor (Ctx : Context; Fld : Virtual_Field) return Boolean with + Post => + True; - function Valid_Predecessor (Ctx : Context; Fld : Virtual_Field) return Boolean; + pragma Warnings (On, "postcondition does not mention function result"); function Valid_Next (Ctx : Context; Fld : Field) return Boolean; @@ -332,7 +368,13 @@ is Pre => Has_Buffer (Ctx); - function Incomplete_Message (Ctx : Context) return Boolean; + pragma Warnings (Off, "postcondition does not mention function result"); + + function Incomplete_Message (Ctx : Context) return Boolean with + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); pragma Warnings (Off, "precondition is always False"); @@ -373,9 +415,15 @@ is Has_Buffer (Ctx) and Present (Ctx, F_Data); + pragma Warnings (Off, "postcondition does not mention function result"); + function Valid_Length (Ctx : Context; Fld : Field; Length : RFLX_Types.Length) return Boolean with Pre => - Valid_Next (Ctx, Fld); + Valid_Next (Ctx, Fld), + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); procedure Set_Message_Type (Ctx : in out Context; Val : RFLX.Universal.Message_Type) with Pre => @@ -1082,6 +1130,8 @@ private type Cursor_State is (S_Valid, S_Structural_Valid, S_Invalid, S_Incomplete); + pragma Warnings (Off, "postcondition does not mention function result"); + function Valid_Value (Val : Field_Dependent_Value) return Boolean is ((case Val.Fld is when F_Message_Type => @@ -1095,7 +1145,12 @@ private when F_Values => True, when F_Initial | F_Final => - False)); + False)) + with + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); type Field_Cursor (State : Cursor_State := S_Invalid) is record diff --git a/tests/integration/session_integration_multiple/generated/rflx-universal-option.ads b/tests/integration/session_integration_multiple/generated/rflx-universal-option.ads index 0e2088b5b..553cfe1ed 100644 --- a/tests/integration/session_integration_multiple/generated/rflx-universal-option.ads +++ b/tests/integration/session_integration_multiple/generated/rflx-universal-option.ads @@ -110,8 +110,14 @@ is Depends => (Ctx => (Buffer, First, Last, Written_Last), Buffer => null); + pragma Warnings (Off, "postcondition does not mention function result"); + function Initialized (Ctx : Context) return Boolean with - Ghost; + Ghost, + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); procedure Reset (Ctx : in out Context) with Pre => @@ -241,15 +247,27 @@ is and then Structural_Valid_Message (Ctx) and then Data'Length = Byte_Size (Ctx); + pragma Warnings (Off, "postcondition does not mention function result"); + function Path_Condition (Ctx : Context; Fld : Field) return Boolean with Pre => - Valid_Predecessor (Ctx, Fld); + Valid_Predecessor (Ctx, Fld), + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); + + pragma Warnings (Off, "postcondition does not mention function result"); function Field_Condition (Ctx : Context; Val : Field_Dependent_Value) return Boolean with Pre => Has_Buffer (Ctx) and Val.Fld in Field'Range - and Valid_Predecessor (Ctx, Val.Fld); + and Valid_Predecessor (Ctx, Val.Fld), + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); function Field_Size (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Length with Pre => @@ -261,9 +279,15 @@ is when others => True); + pragma Warnings (Off, "postcondition does not mention function result"); + function Field_First (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Index with Pre => - Valid_Next (Ctx, Fld); + Valid_Next (Ctx, Fld), + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); function Field_Last (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Index with Pre => @@ -276,9 +300,21 @@ is when others => True); - function Predecessor (Ctx : Context; Fld : Virtual_Field) return Virtual_Field; + pragma Warnings (Off, "postcondition does not mention function result"); + + function Predecessor (Ctx : Context; Fld : Virtual_Field) return Virtual_Field with + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); + + pragma Warnings (Off, "postcondition does not mention function result"); + + function Valid_Predecessor (Ctx : Context; Fld : Virtual_Field) return Boolean with + Post => + True; - function Valid_Predecessor (Ctx : Context; Fld : Virtual_Field) return Boolean; + pragma Warnings (On, "postcondition does not mention function result"); function Valid_Next (Ctx : Context; Fld : Field) return Boolean; @@ -327,7 +363,13 @@ is Pre => Has_Buffer (Ctx); - function Incomplete_Message (Ctx : Context) return Boolean; + pragma Warnings (Off, "postcondition does not mention function result"); + + function Incomplete_Message (Ctx : Context) return Boolean with + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); pragma Warnings (Off, "precondition is always False"); @@ -364,9 +406,15 @@ is Has_Buffer (Ctx) and Present (Ctx, F_Data); + pragma Warnings (Off, "postcondition does not mention function result"); + function Valid_Length (Ctx : Context; Fld : Field; Length : RFLX_Types.Length) return Boolean with Pre => - Valid_Next (Ctx, Fld); + Valid_Next (Ctx, Fld), + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); procedure Set_Option_Type (Ctx : in out Context; Val : RFLX.Universal.Option_Type_Enum) with Pre => @@ -531,6 +579,8 @@ private type Cursor_State is (S_Valid, S_Structural_Valid, S_Invalid, S_Incomplete); + pragma Warnings (Off, "postcondition does not mention function result"); + function Valid_Value (Val : Field_Dependent_Value) return Boolean is ((case Val.Fld is when F_Option_Type => @@ -540,7 +590,12 @@ private when F_Data => True, when F_Initial | F_Final => - False)); + False)) + with + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); type Field_Cursor (State : Cursor_State := S_Invalid) is record diff --git a/tests/integration/session_minimal/generated/rflx-universal-message.ads b/tests/integration/session_minimal/generated/rflx-universal-message.ads index 489b50a8f..b70fa9f65 100644 --- a/tests/integration/session_minimal/generated/rflx-universal-message.ads +++ b/tests/integration/session_minimal/generated/rflx-universal-message.ads @@ -115,8 +115,14 @@ is Depends => (Ctx => (Buffer, First, Last, Written_Last), Buffer => null); + pragma Warnings (Off, "postcondition does not mention function result"); + function Initialized (Ctx : Context) return Boolean with - Ghost; + Ghost, + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); procedure Reset (Ctx : in out Context) with Pre => @@ -246,15 +252,27 @@ is and then Structural_Valid_Message (Ctx) and then Data'Length = Byte_Size (Ctx); + pragma Warnings (Off, "postcondition does not mention function result"); + function Path_Condition (Ctx : Context; Fld : Field) return Boolean with Pre => - Valid_Predecessor (Ctx, Fld); + Valid_Predecessor (Ctx, Fld), + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); + + pragma Warnings (Off, "postcondition does not mention function result"); function Field_Condition (Ctx : Context; Val : Field_Dependent_Value) return Boolean with Pre => Has_Buffer (Ctx) and Val.Fld in Field'Range - and Valid_Predecessor (Ctx, Val.Fld); + and Valid_Predecessor (Ctx, Val.Fld), + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); function Field_Size (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Length with Pre => @@ -266,9 +284,15 @@ is when others => True); + pragma Warnings (Off, "postcondition does not mention function result"); + function Field_First (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Index with Pre => - Valid_Next (Ctx, Fld); + Valid_Next (Ctx, Fld), + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); function Field_Last (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Index with Pre => @@ -281,9 +305,21 @@ is when others => True); - function Predecessor (Ctx : Context; Fld : Virtual_Field) return Virtual_Field; + pragma Warnings (Off, "postcondition does not mention function result"); + + function Predecessor (Ctx : Context; Fld : Virtual_Field) return Virtual_Field with + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); + + pragma Warnings (Off, "postcondition does not mention function result"); + + function Valid_Predecessor (Ctx : Context; Fld : Virtual_Field) return Boolean with + Post => + True; - function Valid_Predecessor (Ctx : Context; Fld : Virtual_Field) return Boolean; + pragma Warnings (On, "postcondition does not mention function result"); function Valid_Next (Ctx : Context; Fld : Field) return Boolean; @@ -332,7 +368,13 @@ is Pre => Has_Buffer (Ctx); - function Incomplete_Message (Ctx : Context) return Boolean; + pragma Warnings (Off, "postcondition does not mention function result"); + + function Incomplete_Message (Ctx : Context) return Boolean with + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); pragma Warnings (Off, "precondition is always False"); @@ -373,9 +415,15 @@ is Has_Buffer (Ctx) and Present (Ctx, F_Data); + pragma Warnings (Off, "postcondition does not mention function result"); + function Valid_Length (Ctx : Context; Fld : Field; Length : RFLX_Types.Length) return Boolean with Pre => - Valid_Next (Ctx, Fld); + Valid_Next (Ctx, Fld), + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); procedure Set_Message_Type (Ctx : in out Context; Val : RFLX.Universal.Message_Type) with Pre => @@ -1082,6 +1130,8 @@ private type Cursor_State is (S_Valid, S_Structural_Valid, S_Invalid, S_Incomplete); + pragma Warnings (Off, "postcondition does not mention function result"); + function Valid_Value (Val : Field_Dependent_Value) return Boolean is ((case Val.Fld is when F_Message_Type => @@ -1095,7 +1145,12 @@ private when F_Values => True, when F_Initial | F_Final => - False)); + False)) + with + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); type Field_Cursor (State : Cursor_State := S_Invalid) is record diff --git a/tests/integration/session_minimal/generated/rflx-universal-option.ads b/tests/integration/session_minimal/generated/rflx-universal-option.ads index 0e2088b5b..553cfe1ed 100644 --- a/tests/integration/session_minimal/generated/rflx-universal-option.ads +++ b/tests/integration/session_minimal/generated/rflx-universal-option.ads @@ -110,8 +110,14 @@ is Depends => (Ctx => (Buffer, First, Last, Written_Last), Buffer => null); + pragma Warnings (Off, "postcondition does not mention function result"); + function Initialized (Ctx : Context) return Boolean with - Ghost; + Ghost, + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); procedure Reset (Ctx : in out Context) with Pre => @@ -241,15 +247,27 @@ is and then Structural_Valid_Message (Ctx) and then Data'Length = Byte_Size (Ctx); + pragma Warnings (Off, "postcondition does not mention function result"); + function Path_Condition (Ctx : Context; Fld : Field) return Boolean with Pre => - Valid_Predecessor (Ctx, Fld); + Valid_Predecessor (Ctx, Fld), + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); + + pragma Warnings (Off, "postcondition does not mention function result"); function Field_Condition (Ctx : Context; Val : Field_Dependent_Value) return Boolean with Pre => Has_Buffer (Ctx) and Val.Fld in Field'Range - and Valid_Predecessor (Ctx, Val.Fld); + and Valid_Predecessor (Ctx, Val.Fld), + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); function Field_Size (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Length with Pre => @@ -261,9 +279,15 @@ is when others => True); + pragma Warnings (Off, "postcondition does not mention function result"); + function Field_First (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Index with Pre => - Valid_Next (Ctx, Fld); + Valid_Next (Ctx, Fld), + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); function Field_Last (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Index with Pre => @@ -276,9 +300,21 @@ is when others => True); - function Predecessor (Ctx : Context; Fld : Virtual_Field) return Virtual_Field; + pragma Warnings (Off, "postcondition does not mention function result"); + + function Predecessor (Ctx : Context; Fld : Virtual_Field) return Virtual_Field with + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); + + pragma Warnings (Off, "postcondition does not mention function result"); + + function Valid_Predecessor (Ctx : Context; Fld : Virtual_Field) return Boolean with + Post => + True; - function Valid_Predecessor (Ctx : Context; Fld : Virtual_Field) return Boolean; + pragma Warnings (On, "postcondition does not mention function result"); function Valid_Next (Ctx : Context; Fld : Field) return Boolean; @@ -327,7 +363,13 @@ is Pre => Has_Buffer (Ctx); - function Incomplete_Message (Ctx : Context) return Boolean; + pragma Warnings (Off, "postcondition does not mention function result"); + + function Incomplete_Message (Ctx : Context) return Boolean with + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); pragma Warnings (Off, "precondition is always False"); @@ -364,9 +406,15 @@ is Has_Buffer (Ctx) and Present (Ctx, F_Data); + pragma Warnings (Off, "postcondition does not mention function result"); + function Valid_Length (Ctx : Context; Fld : Field; Length : RFLX_Types.Length) return Boolean with Pre => - Valid_Next (Ctx, Fld); + Valid_Next (Ctx, Fld), + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); procedure Set_Option_Type (Ctx : in out Context; Val : RFLX.Universal.Option_Type_Enum) with Pre => @@ -531,6 +579,8 @@ private type Cursor_State is (S_Valid, S_Structural_Valid, S_Invalid, S_Incomplete); + pragma Warnings (Off, "postcondition does not mention function result"); + function Valid_Value (Val : Field_Dependent_Value) return Boolean is ((case Val.Fld is when F_Option_Type => @@ -540,7 +590,12 @@ private when F_Data => True, when F_Initial | F_Final => - False)); + False)) + with + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); type Field_Cursor (State : Cursor_State := S_Invalid) is record diff --git a/tests/integration/session_reuse_of_message/generated/rflx-universal-message.ads b/tests/integration/session_reuse_of_message/generated/rflx-universal-message.ads index 489b50a8f..b70fa9f65 100644 --- a/tests/integration/session_reuse_of_message/generated/rflx-universal-message.ads +++ b/tests/integration/session_reuse_of_message/generated/rflx-universal-message.ads @@ -115,8 +115,14 @@ is Depends => (Ctx => (Buffer, First, Last, Written_Last), Buffer => null); + pragma Warnings (Off, "postcondition does not mention function result"); + function Initialized (Ctx : Context) return Boolean with - Ghost; + Ghost, + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); procedure Reset (Ctx : in out Context) with Pre => @@ -246,15 +252,27 @@ is and then Structural_Valid_Message (Ctx) and then Data'Length = Byte_Size (Ctx); + pragma Warnings (Off, "postcondition does not mention function result"); + function Path_Condition (Ctx : Context; Fld : Field) return Boolean with Pre => - Valid_Predecessor (Ctx, Fld); + Valid_Predecessor (Ctx, Fld), + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); + + pragma Warnings (Off, "postcondition does not mention function result"); function Field_Condition (Ctx : Context; Val : Field_Dependent_Value) return Boolean with Pre => Has_Buffer (Ctx) and Val.Fld in Field'Range - and Valid_Predecessor (Ctx, Val.Fld); + and Valid_Predecessor (Ctx, Val.Fld), + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); function Field_Size (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Length with Pre => @@ -266,9 +284,15 @@ is when others => True); + pragma Warnings (Off, "postcondition does not mention function result"); + function Field_First (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Index with Pre => - Valid_Next (Ctx, Fld); + Valid_Next (Ctx, Fld), + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); function Field_Last (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Index with Pre => @@ -281,9 +305,21 @@ is when others => True); - function Predecessor (Ctx : Context; Fld : Virtual_Field) return Virtual_Field; + pragma Warnings (Off, "postcondition does not mention function result"); + + function Predecessor (Ctx : Context; Fld : Virtual_Field) return Virtual_Field with + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); + + pragma Warnings (Off, "postcondition does not mention function result"); + + function Valid_Predecessor (Ctx : Context; Fld : Virtual_Field) return Boolean with + Post => + True; - function Valid_Predecessor (Ctx : Context; Fld : Virtual_Field) return Boolean; + pragma Warnings (On, "postcondition does not mention function result"); function Valid_Next (Ctx : Context; Fld : Field) return Boolean; @@ -332,7 +368,13 @@ is Pre => Has_Buffer (Ctx); - function Incomplete_Message (Ctx : Context) return Boolean; + pragma Warnings (Off, "postcondition does not mention function result"); + + function Incomplete_Message (Ctx : Context) return Boolean with + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); pragma Warnings (Off, "precondition is always False"); @@ -373,9 +415,15 @@ is Has_Buffer (Ctx) and Present (Ctx, F_Data); + pragma Warnings (Off, "postcondition does not mention function result"); + function Valid_Length (Ctx : Context; Fld : Field; Length : RFLX_Types.Length) return Boolean with Pre => - Valid_Next (Ctx, Fld); + Valid_Next (Ctx, Fld), + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); procedure Set_Message_Type (Ctx : in out Context; Val : RFLX.Universal.Message_Type) with Pre => @@ -1082,6 +1130,8 @@ private type Cursor_State is (S_Valid, S_Structural_Valid, S_Invalid, S_Incomplete); + pragma Warnings (Off, "postcondition does not mention function result"); + function Valid_Value (Val : Field_Dependent_Value) return Boolean is ((case Val.Fld is when F_Message_Type => @@ -1095,7 +1145,12 @@ private when F_Values => True, when F_Initial | F_Final => - False)); + False)) + with + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); type Field_Cursor (State : Cursor_State := S_Invalid) is record diff --git a/tests/integration/session_reuse_of_message/generated/rflx-universal-option.ads b/tests/integration/session_reuse_of_message/generated/rflx-universal-option.ads index 0e2088b5b..553cfe1ed 100644 --- a/tests/integration/session_reuse_of_message/generated/rflx-universal-option.ads +++ b/tests/integration/session_reuse_of_message/generated/rflx-universal-option.ads @@ -110,8 +110,14 @@ is Depends => (Ctx => (Buffer, First, Last, Written_Last), Buffer => null); + pragma Warnings (Off, "postcondition does not mention function result"); + function Initialized (Ctx : Context) return Boolean with - Ghost; + Ghost, + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); procedure Reset (Ctx : in out Context) with Pre => @@ -241,15 +247,27 @@ is and then Structural_Valid_Message (Ctx) and then Data'Length = Byte_Size (Ctx); + pragma Warnings (Off, "postcondition does not mention function result"); + function Path_Condition (Ctx : Context; Fld : Field) return Boolean with Pre => - Valid_Predecessor (Ctx, Fld); + Valid_Predecessor (Ctx, Fld), + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); + + pragma Warnings (Off, "postcondition does not mention function result"); function Field_Condition (Ctx : Context; Val : Field_Dependent_Value) return Boolean with Pre => Has_Buffer (Ctx) and Val.Fld in Field'Range - and Valid_Predecessor (Ctx, Val.Fld); + and Valid_Predecessor (Ctx, Val.Fld), + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); function Field_Size (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Length with Pre => @@ -261,9 +279,15 @@ is when others => True); + pragma Warnings (Off, "postcondition does not mention function result"); + function Field_First (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Index with Pre => - Valid_Next (Ctx, Fld); + Valid_Next (Ctx, Fld), + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); function Field_Last (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Index with Pre => @@ -276,9 +300,21 @@ is when others => True); - function Predecessor (Ctx : Context; Fld : Virtual_Field) return Virtual_Field; + pragma Warnings (Off, "postcondition does not mention function result"); + + function Predecessor (Ctx : Context; Fld : Virtual_Field) return Virtual_Field with + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); + + pragma Warnings (Off, "postcondition does not mention function result"); + + function Valid_Predecessor (Ctx : Context; Fld : Virtual_Field) return Boolean with + Post => + True; - function Valid_Predecessor (Ctx : Context; Fld : Virtual_Field) return Boolean; + pragma Warnings (On, "postcondition does not mention function result"); function Valid_Next (Ctx : Context; Fld : Field) return Boolean; @@ -327,7 +363,13 @@ is Pre => Has_Buffer (Ctx); - function Incomplete_Message (Ctx : Context) return Boolean; + pragma Warnings (Off, "postcondition does not mention function result"); + + function Incomplete_Message (Ctx : Context) return Boolean with + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); pragma Warnings (Off, "precondition is always False"); @@ -364,9 +406,15 @@ is Has_Buffer (Ctx) and Present (Ctx, F_Data); + pragma Warnings (Off, "postcondition does not mention function result"); + function Valid_Length (Ctx : Context; Fld : Field; Length : RFLX_Types.Length) return Boolean with Pre => - Valid_Next (Ctx, Fld); + Valid_Next (Ctx, Fld), + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); procedure Set_Option_Type (Ctx : in out Context; Val : RFLX.Universal.Option_Type_Enum) with Pre => @@ -531,6 +579,8 @@ private type Cursor_State is (S_Valid, S_Structural_Valid, S_Invalid, S_Incomplete); + pragma Warnings (Off, "postcondition does not mention function result"); + function Valid_Value (Val : Field_Dependent_Value) return Boolean is ((case Val.Fld is when F_Option_Type => @@ -540,7 +590,12 @@ private when F_Data => True, when F_Initial | F_Final => - False)); + False)) + with + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); type Field_Cursor (State : Cursor_State := S_Invalid) is record diff --git a/tests/integration/session_sequence_append_head/generated/rflx-tlv-message.ads b/tests/integration/session_sequence_append_head/generated/rflx-tlv-message.ads index e84e7567f..d22005eb5 100644 --- a/tests/integration/session_sequence_append_head/generated/rflx-tlv-message.ads +++ b/tests/integration/session_sequence_append_head/generated/rflx-tlv-message.ads @@ -110,8 +110,14 @@ is Depends => (Ctx => (Buffer, First, Last, Written_Last), Buffer => null); + pragma Warnings (Off, "postcondition does not mention function result"); + function Initialized (Ctx : Context) return Boolean with - Ghost; + Ghost, + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); procedure Reset (Ctx : in out Context) with Pre => @@ -241,15 +247,27 @@ is and then Structural_Valid_Message (Ctx) and then Data'Length = Byte_Size (Ctx); + pragma Warnings (Off, "postcondition does not mention function result"); + function Path_Condition (Ctx : Context; Fld : Field) return Boolean with Pre => - Valid_Predecessor (Ctx, Fld); + Valid_Predecessor (Ctx, Fld), + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); + + pragma Warnings (Off, "postcondition does not mention function result"); function Field_Condition (Ctx : Context; Val : Field_Dependent_Value) return Boolean with Pre => Has_Buffer (Ctx) and Val.Fld in Field'Range - and Valid_Predecessor (Ctx, Val.Fld); + and Valid_Predecessor (Ctx, Val.Fld), + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); function Field_Size (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Length with Pre => @@ -261,9 +279,15 @@ is when others => True); + pragma Warnings (Off, "postcondition does not mention function result"); + function Field_First (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Index with Pre => - Valid_Next (Ctx, Fld); + Valid_Next (Ctx, Fld), + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); function Field_Last (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Index with Pre => @@ -276,9 +300,21 @@ is when others => True); - function Predecessor (Ctx : Context; Fld : Virtual_Field) return Virtual_Field; + pragma Warnings (Off, "postcondition does not mention function result"); + + function Predecessor (Ctx : Context; Fld : Virtual_Field) return Virtual_Field with + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); + + pragma Warnings (Off, "postcondition does not mention function result"); + + function Valid_Predecessor (Ctx : Context; Fld : Virtual_Field) return Boolean with + Post => + True; - function Valid_Predecessor (Ctx : Context; Fld : Virtual_Field) return Boolean; + pragma Warnings (On, "postcondition does not mention function result"); function Valid_Next (Ctx : Context; Fld : Field) return Boolean; @@ -327,7 +363,13 @@ is Pre => Has_Buffer (Ctx); - function Incomplete_Message (Ctx : Context) return Boolean; + pragma Warnings (Off, "postcondition does not mention function result"); + + function Incomplete_Message (Ctx : Context) return Boolean with + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); pragma Warnings (Off, "precondition is always False"); @@ -364,9 +406,15 @@ is Has_Buffer (Ctx) and Present (Ctx, F_Value); + pragma Warnings (Off, "postcondition does not mention function result"); + function Valid_Length (Ctx : Context; Fld : Field; Length : RFLX_Types.Length) return Boolean with Pre => - Valid_Next (Ctx, Fld); + Valid_Next (Ctx, Fld), + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); procedure Set_Tag (Ctx : in out Context; Val : RFLX.TLV.Tag) with Pre => @@ -531,6 +579,8 @@ private type Cursor_State is (S_Valid, S_Structural_Valid, S_Invalid, S_Incomplete); + pragma Warnings (Off, "postcondition does not mention function result"); + function Valid_Value (Val : Field_Dependent_Value) return Boolean is ((case Val.Fld is when F_Tag => @@ -540,7 +590,12 @@ private when F_Value => True, when F_Initial | F_Final => - False)); + False)) + with + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); type Field_Cursor (State : Cursor_State := S_Invalid) is record diff --git a/tests/integration/session_simple/generated/rflx-universal-message.ads b/tests/integration/session_simple/generated/rflx-universal-message.ads index 489b50a8f..b70fa9f65 100644 --- a/tests/integration/session_simple/generated/rflx-universal-message.ads +++ b/tests/integration/session_simple/generated/rflx-universal-message.ads @@ -115,8 +115,14 @@ is Depends => (Ctx => (Buffer, First, Last, Written_Last), Buffer => null); + pragma Warnings (Off, "postcondition does not mention function result"); + function Initialized (Ctx : Context) return Boolean with - Ghost; + Ghost, + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); procedure Reset (Ctx : in out Context) with Pre => @@ -246,15 +252,27 @@ is and then Structural_Valid_Message (Ctx) and then Data'Length = Byte_Size (Ctx); + pragma Warnings (Off, "postcondition does not mention function result"); + function Path_Condition (Ctx : Context; Fld : Field) return Boolean with Pre => - Valid_Predecessor (Ctx, Fld); + Valid_Predecessor (Ctx, Fld), + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); + + pragma Warnings (Off, "postcondition does not mention function result"); function Field_Condition (Ctx : Context; Val : Field_Dependent_Value) return Boolean with Pre => Has_Buffer (Ctx) and Val.Fld in Field'Range - and Valid_Predecessor (Ctx, Val.Fld); + and Valid_Predecessor (Ctx, Val.Fld), + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); function Field_Size (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Length with Pre => @@ -266,9 +284,15 @@ is when others => True); + pragma Warnings (Off, "postcondition does not mention function result"); + function Field_First (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Index with Pre => - Valid_Next (Ctx, Fld); + Valid_Next (Ctx, Fld), + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); function Field_Last (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Index with Pre => @@ -281,9 +305,21 @@ is when others => True); - function Predecessor (Ctx : Context; Fld : Virtual_Field) return Virtual_Field; + pragma Warnings (Off, "postcondition does not mention function result"); + + function Predecessor (Ctx : Context; Fld : Virtual_Field) return Virtual_Field with + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); + + pragma Warnings (Off, "postcondition does not mention function result"); + + function Valid_Predecessor (Ctx : Context; Fld : Virtual_Field) return Boolean with + Post => + True; - function Valid_Predecessor (Ctx : Context; Fld : Virtual_Field) return Boolean; + pragma Warnings (On, "postcondition does not mention function result"); function Valid_Next (Ctx : Context; Fld : Field) return Boolean; @@ -332,7 +368,13 @@ is Pre => Has_Buffer (Ctx); - function Incomplete_Message (Ctx : Context) return Boolean; + pragma Warnings (Off, "postcondition does not mention function result"); + + function Incomplete_Message (Ctx : Context) return Boolean with + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); pragma Warnings (Off, "precondition is always False"); @@ -373,9 +415,15 @@ is Has_Buffer (Ctx) and Present (Ctx, F_Data); + pragma Warnings (Off, "postcondition does not mention function result"); + function Valid_Length (Ctx : Context; Fld : Field; Length : RFLX_Types.Length) return Boolean with Pre => - Valid_Next (Ctx, Fld); + Valid_Next (Ctx, Fld), + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); procedure Set_Message_Type (Ctx : in out Context; Val : RFLX.Universal.Message_Type) with Pre => @@ -1082,6 +1130,8 @@ private type Cursor_State is (S_Valid, S_Structural_Valid, S_Invalid, S_Incomplete); + pragma Warnings (Off, "postcondition does not mention function result"); + function Valid_Value (Val : Field_Dependent_Value) return Boolean is ((case Val.Fld is when F_Message_Type => @@ -1095,7 +1145,12 @@ private when F_Values => True, when F_Initial | F_Final => - False)); + False)) + with + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); type Field_Cursor (State : Cursor_State := S_Invalid) is record diff --git a/tests/integration/session_simple/generated/rflx-universal-option.ads b/tests/integration/session_simple/generated/rflx-universal-option.ads index 0e2088b5b..553cfe1ed 100644 --- a/tests/integration/session_simple/generated/rflx-universal-option.ads +++ b/tests/integration/session_simple/generated/rflx-universal-option.ads @@ -110,8 +110,14 @@ is Depends => (Ctx => (Buffer, First, Last, Written_Last), Buffer => null); + pragma Warnings (Off, "postcondition does not mention function result"); + function Initialized (Ctx : Context) return Boolean with - Ghost; + Ghost, + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); procedure Reset (Ctx : in out Context) with Pre => @@ -241,15 +247,27 @@ is and then Structural_Valid_Message (Ctx) and then Data'Length = Byte_Size (Ctx); + pragma Warnings (Off, "postcondition does not mention function result"); + function Path_Condition (Ctx : Context; Fld : Field) return Boolean with Pre => - Valid_Predecessor (Ctx, Fld); + Valid_Predecessor (Ctx, Fld), + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); + + pragma Warnings (Off, "postcondition does not mention function result"); function Field_Condition (Ctx : Context; Val : Field_Dependent_Value) return Boolean with Pre => Has_Buffer (Ctx) and Val.Fld in Field'Range - and Valid_Predecessor (Ctx, Val.Fld); + and Valid_Predecessor (Ctx, Val.Fld), + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); function Field_Size (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Length with Pre => @@ -261,9 +279,15 @@ is when others => True); + pragma Warnings (Off, "postcondition does not mention function result"); + function Field_First (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Index with Pre => - Valid_Next (Ctx, Fld); + Valid_Next (Ctx, Fld), + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); function Field_Last (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Index with Pre => @@ -276,9 +300,21 @@ is when others => True); - function Predecessor (Ctx : Context; Fld : Virtual_Field) return Virtual_Field; + pragma Warnings (Off, "postcondition does not mention function result"); + + function Predecessor (Ctx : Context; Fld : Virtual_Field) return Virtual_Field with + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); + + pragma Warnings (Off, "postcondition does not mention function result"); + + function Valid_Predecessor (Ctx : Context; Fld : Virtual_Field) return Boolean with + Post => + True; - function Valid_Predecessor (Ctx : Context; Fld : Virtual_Field) return Boolean; + pragma Warnings (On, "postcondition does not mention function result"); function Valid_Next (Ctx : Context; Fld : Field) return Boolean; @@ -327,7 +363,13 @@ is Pre => Has_Buffer (Ctx); - function Incomplete_Message (Ctx : Context) return Boolean; + pragma Warnings (Off, "postcondition does not mention function result"); + + function Incomplete_Message (Ctx : Context) return Boolean with + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); pragma Warnings (Off, "precondition is always False"); @@ -364,9 +406,15 @@ is Has_Buffer (Ctx) and Present (Ctx, F_Data); + pragma Warnings (Off, "postcondition does not mention function result"); + function Valid_Length (Ctx : Context; Fld : Field; Length : RFLX_Types.Length) return Boolean with Pre => - Valid_Next (Ctx, Fld); + Valid_Next (Ctx, Fld), + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); procedure Set_Option_Type (Ctx : in out Context; Val : RFLX.Universal.Option_Type_Enum) with Pre => @@ -531,6 +579,8 @@ private type Cursor_State is (S_Valid, S_Structural_Valid, S_Invalid, S_Incomplete); + pragma Warnings (Off, "postcondition does not mention function result"); + function Valid_Value (Val : Field_Dependent_Value) return Boolean is ((case Val.Fld is when F_Option_Type => @@ -540,7 +590,12 @@ private when F_Data => True, when F_Initial | F_Final => - False)); + False)) + with + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); type Field_Cursor (State : Cursor_State := S_Invalid) is record diff --git a/tests/integration/session_variable_initialization/generated/rflx-universal-message.ads b/tests/integration/session_variable_initialization/generated/rflx-universal-message.ads index 489b50a8f..b70fa9f65 100644 --- a/tests/integration/session_variable_initialization/generated/rflx-universal-message.ads +++ b/tests/integration/session_variable_initialization/generated/rflx-universal-message.ads @@ -115,8 +115,14 @@ is Depends => (Ctx => (Buffer, First, Last, Written_Last), Buffer => null); + pragma Warnings (Off, "postcondition does not mention function result"); + function Initialized (Ctx : Context) return Boolean with - Ghost; + Ghost, + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); procedure Reset (Ctx : in out Context) with Pre => @@ -246,15 +252,27 @@ is and then Structural_Valid_Message (Ctx) and then Data'Length = Byte_Size (Ctx); + pragma Warnings (Off, "postcondition does not mention function result"); + function Path_Condition (Ctx : Context; Fld : Field) return Boolean with Pre => - Valid_Predecessor (Ctx, Fld); + Valid_Predecessor (Ctx, Fld), + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); + + pragma Warnings (Off, "postcondition does not mention function result"); function Field_Condition (Ctx : Context; Val : Field_Dependent_Value) return Boolean with Pre => Has_Buffer (Ctx) and Val.Fld in Field'Range - and Valid_Predecessor (Ctx, Val.Fld); + and Valid_Predecessor (Ctx, Val.Fld), + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); function Field_Size (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Length with Pre => @@ -266,9 +284,15 @@ is when others => True); + pragma Warnings (Off, "postcondition does not mention function result"); + function Field_First (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Index with Pre => - Valid_Next (Ctx, Fld); + Valid_Next (Ctx, Fld), + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); function Field_Last (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Index with Pre => @@ -281,9 +305,21 @@ is when others => True); - function Predecessor (Ctx : Context; Fld : Virtual_Field) return Virtual_Field; + pragma Warnings (Off, "postcondition does not mention function result"); + + function Predecessor (Ctx : Context; Fld : Virtual_Field) return Virtual_Field with + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); + + pragma Warnings (Off, "postcondition does not mention function result"); + + function Valid_Predecessor (Ctx : Context; Fld : Virtual_Field) return Boolean with + Post => + True; - function Valid_Predecessor (Ctx : Context; Fld : Virtual_Field) return Boolean; + pragma Warnings (On, "postcondition does not mention function result"); function Valid_Next (Ctx : Context; Fld : Field) return Boolean; @@ -332,7 +368,13 @@ is Pre => Has_Buffer (Ctx); - function Incomplete_Message (Ctx : Context) return Boolean; + pragma Warnings (Off, "postcondition does not mention function result"); + + function Incomplete_Message (Ctx : Context) return Boolean with + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); pragma Warnings (Off, "precondition is always False"); @@ -373,9 +415,15 @@ is Has_Buffer (Ctx) and Present (Ctx, F_Data); + pragma Warnings (Off, "postcondition does not mention function result"); + function Valid_Length (Ctx : Context; Fld : Field; Length : RFLX_Types.Length) return Boolean with Pre => - Valid_Next (Ctx, Fld); + Valid_Next (Ctx, Fld), + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); procedure Set_Message_Type (Ctx : in out Context; Val : RFLX.Universal.Message_Type) with Pre => @@ -1082,6 +1130,8 @@ private type Cursor_State is (S_Valid, S_Structural_Valid, S_Invalid, S_Incomplete); + pragma Warnings (Off, "postcondition does not mention function result"); + function Valid_Value (Val : Field_Dependent_Value) return Boolean is ((case Val.Fld is when F_Message_Type => @@ -1095,7 +1145,12 @@ private when F_Values => True, when F_Initial | F_Final => - False)); + False)) + with + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); type Field_Cursor (State : Cursor_State := S_Invalid) is record diff --git a/tests/integration/session_variable_initialization/generated/rflx-universal-option.ads b/tests/integration/session_variable_initialization/generated/rflx-universal-option.ads index 0e2088b5b..553cfe1ed 100644 --- a/tests/integration/session_variable_initialization/generated/rflx-universal-option.ads +++ b/tests/integration/session_variable_initialization/generated/rflx-universal-option.ads @@ -110,8 +110,14 @@ is Depends => (Ctx => (Buffer, First, Last, Written_Last), Buffer => null); + pragma Warnings (Off, "postcondition does not mention function result"); + function Initialized (Ctx : Context) return Boolean with - Ghost; + Ghost, + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); procedure Reset (Ctx : in out Context) with Pre => @@ -241,15 +247,27 @@ is and then Structural_Valid_Message (Ctx) and then Data'Length = Byte_Size (Ctx); + pragma Warnings (Off, "postcondition does not mention function result"); + function Path_Condition (Ctx : Context; Fld : Field) return Boolean with Pre => - Valid_Predecessor (Ctx, Fld); + Valid_Predecessor (Ctx, Fld), + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); + + pragma Warnings (Off, "postcondition does not mention function result"); function Field_Condition (Ctx : Context; Val : Field_Dependent_Value) return Boolean with Pre => Has_Buffer (Ctx) and Val.Fld in Field'Range - and Valid_Predecessor (Ctx, Val.Fld); + and Valid_Predecessor (Ctx, Val.Fld), + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); function Field_Size (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Length with Pre => @@ -261,9 +279,15 @@ is when others => True); + pragma Warnings (Off, "postcondition does not mention function result"); + function Field_First (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Index with Pre => - Valid_Next (Ctx, Fld); + Valid_Next (Ctx, Fld), + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); function Field_Last (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Index with Pre => @@ -276,9 +300,21 @@ is when others => True); - function Predecessor (Ctx : Context; Fld : Virtual_Field) return Virtual_Field; + pragma Warnings (Off, "postcondition does not mention function result"); + + function Predecessor (Ctx : Context; Fld : Virtual_Field) return Virtual_Field with + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); + + pragma Warnings (Off, "postcondition does not mention function result"); + + function Valid_Predecessor (Ctx : Context; Fld : Virtual_Field) return Boolean with + Post => + True; - function Valid_Predecessor (Ctx : Context; Fld : Virtual_Field) return Boolean; + pragma Warnings (On, "postcondition does not mention function result"); function Valid_Next (Ctx : Context; Fld : Field) return Boolean; @@ -327,7 +363,13 @@ is Pre => Has_Buffer (Ctx); - function Incomplete_Message (Ctx : Context) return Boolean; + pragma Warnings (Off, "postcondition does not mention function result"); + + function Incomplete_Message (Ctx : Context) return Boolean with + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); pragma Warnings (Off, "precondition is always False"); @@ -364,9 +406,15 @@ is Has_Buffer (Ctx) and Present (Ctx, F_Data); + pragma Warnings (Off, "postcondition does not mention function result"); + function Valid_Length (Ctx : Context; Fld : Field; Length : RFLX_Types.Length) return Boolean with Pre => - Valid_Next (Ctx, Fld); + Valid_Next (Ctx, Fld), + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); procedure Set_Option_Type (Ctx : in out Context; Val : RFLX.Universal.Option_Type_Enum) with Pre => @@ -531,6 +579,8 @@ private type Cursor_State is (S_Valid, S_Structural_Valid, S_Invalid, S_Incomplete); + pragma Warnings (Off, "postcondition does not mention function result"); + function Valid_Value (Val : Field_Dependent_Value) return Boolean is ((case Val.Fld is when F_Option_Type => @@ -540,7 +590,12 @@ private when F_Data => True, when F_Initial | F_Final => - False)); + False)) + with + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); type Field_Cursor (State : Cursor_State := S_Invalid) is record diff --git a/tests/spark/generated/rflx-derivation-message.ads b/tests/spark/generated/rflx-derivation-message.ads index fcc525f3a..c52ea2775 100644 --- a/tests/spark/generated/rflx-derivation-message.ads +++ b/tests/spark/generated/rflx-derivation-message.ads @@ -112,8 +112,14 @@ is Depends => (Ctx => (Buffer, First, Last, Written_Last), Buffer => null); + pragma Warnings (Off, "postcondition does not mention function result"); + function Initialized (Ctx : Context) return Boolean with - Ghost; + Ghost, + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); procedure Reset (Ctx : in out Context) with Pre => @@ -243,15 +249,27 @@ is and then Structural_Valid_Message (Ctx) and then Data'Length = Byte_Size (Ctx); + pragma Warnings (Off, "postcondition does not mention function result"); + function Path_Condition (Ctx : Context; Fld : Field) return Boolean with Pre => - Valid_Predecessor (Ctx, Fld); + Valid_Predecessor (Ctx, Fld), + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); + + pragma Warnings (Off, "postcondition does not mention function result"); function Field_Condition (Ctx : Context; Val : Field_Dependent_Value) return Boolean with Pre => Has_Buffer (Ctx) and Val.Fld in Field'Range - and Valid_Predecessor (Ctx, Val.Fld); + and Valid_Predecessor (Ctx, Val.Fld), + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); function Field_Size (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Length with Pre => @@ -263,9 +281,15 @@ is when others => True); + pragma Warnings (Off, "postcondition does not mention function result"); + function Field_First (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Index with Pre => - Valid_Next (Ctx, Fld); + Valid_Next (Ctx, Fld), + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); function Field_Last (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Index with Pre => @@ -278,9 +302,21 @@ is when others => True); - function Predecessor (Ctx : Context; Fld : Virtual_Field) return Virtual_Field; + pragma Warnings (Off, "postcondition does not mention function result"); + + function Predecessor (Ctx : Context; Fld : Virtual_Field) return Virtual_Field with + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); + + pragma Warnings (Off, "postcondition does not mention function result"); + + function Valid_Predecessor (Ctx : Context; Fld : Virtual_Field) return Boolean with + Post => + True; - function Valid_Predecessor (Ctx : Context; Fld : Virtual_Field) return Boolean; + pragma Warnings (On, "postcondition does not mention function result"); function Valid_Next (Ctx : Context; Fld : Field) return Boolean; @@ -329,7 +365,13 @@ is Pre => Has_Buffer (Ctx); - function Incomplete_Message (Ctx : Context) return Boolean; + pragma Warnings (Off, "postcondition does not mention function result"); + + function Incomplete_Message (Ctx : Context) return Boolean with + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); pragma Warnings (Off, "precondition is always False"); @@ -366,9 +408,15 @@ is Has_Buffer (Ctx) and Present (Ctx, F_Value); + pragma Warnings (Off, "postcondition does not mention function result"); + function Valid_Length (Ctx : Context; Fld : Field; Length : RFLX_Types.Length) return Boolean with Pre => - Valid_Next (Ctx, Fld); + Valid_Next (Ctx, Fld), + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); procedure Set_Tag (Ctx : in out Context; Val : RFLX.TLV.Tag) with Pre => @@ -533,6 +581,8 @@ private type Cursor_State is (S_Valid, S_Structural_Valid, S_Invalid, S_Incomplete); + pragma Warnings (Off, "postcondition does not mention function result"); + function Valid_Value (Val : Field_Dependent_Value) return Boolean is ((case Val.Fld is when F_Tag => @@ -542,7 +592,12 @@ private when F_Value => True, when F_Initial | F_Final => - False)); + False)) + with + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); type Field_Cursor (State : Cursor_State := S_Invalid) is record diff --git a/tests/spark/generated/rflx-enumeration-message.ads b/tests/spark/generated/rflx-enumeration-message.ads index a0c65459e..6e7574dfe 100644 --- a/tests/spark/generated/rflx-enumeration-message.ads +++ b/tests/spark/generated/rflx-enumeration-message.ads @@ -106,8 +106,14 @@ is Depends => (Ctx => (Buffer, First, Last, Written_Last), Buffer => null); + pragma Warnings (Off, "postcondition does not mention function result"); + function Initialized (Ctx : Context) return Boolean with - Ghost; + Ghost, + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); procedure Reset (Ctx : in out Context) with Pre => @@ -237,32 +243,62 @@ is and then Structural_Valid_Message (Ctx) and then Data'Length = Byte_Size (Ctx); + pragma Warnings (Off, "postcondition does not mention function result"); + function Path_Condition (Ctx : Context; Fld : Field) return Boolean with Pre => - Valid_Predecessor (Ctx, Fld); + Valid_Predecessor (Ctx, Fld), + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); + + pragma Warnings (Off, "postcondition does not mention function result"); function Field_Condition (Ctx : Context; Val : Field_Dependent_Value) return Boolean with Pre => Has_Buffer (Ctx) and Val.Fld in Field'Range - and Valid_Predecessor (Ctx, Val.Fld); + and Valid_Predecessor (Ctx, Val.Fld), + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); function Field_Size (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Length with Pre => Valid_Next (Ctx, Fld); + pragma Warnings (Off, "postcondition does not mention function result"); + function Field_First (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Index with Pre => - Valid_Next (Ctx, Fld); + Valid_Next (Ctx, Fld), + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); function Field_Last (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Index with Pre => Valid_Next (Ctx, Fld) and then Available_Space (Ctx, Fld) >= Field_Size (Ctx, Fld); - function Predecessor (Ctx : Context; Fld : Virtual_Field) return Virtual_Field; + pragma Warnings (Off, "postcondition does not mention function result"); + + function Predecessor (Ctx : Context; Fld : Virtual_Field) return Virtual_Field with + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); + + pragma Warnings (Off, "postcondition does not mention function result"); - function Valid_Predecessor (Ctx : Context; Fld : Virtual_Field) return Boolean; + function Valid_Predecessor (Ctx : Context; Fld : Virtual_Field) return Boolean with + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); function Valid_Next (Ctx : Context; Fld : Field) return Boolean; @@ -306,7 +342,13 @@ is Pre => Has_Buffer (Ctx); - function Incomplete_Message (Ctx : Context) return Boolean; + pragma Warnings (Off, "postcondition does not mention function result"); + + function Incomplete_Message (Ctx : Context) return Boolean with + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); pragma Warnings (Off, "precondition is always False"); @@ -316,9 +358,15 @@ is pragma Warnings (On, "precondition is always False"); + pragma Warnings (Off, "postcondition does not mention function result"); + function Valid_Length (Ctx : Context; Fld : Field; Length : RFLX_Types.Length) return Boolean with Pre => - Valid_Next (Ctx, Fld); + Valid_Next (Ctx, Fld), + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); procedure Set_Priority (Ctx : in out Context; Val : RFLX.Enumeration.Priority_Enum) with Pre => @@ -374,12 +422,19 @@ private type Cursor_State is (S_Valid, S_Structural_Valid, S_Invalid, S_Incomplete); + pragma Warnings (Off, "postcondition does not mention function result"); + function Valid_Value (Val : Field_Dependent_Value) return Boolean is ((case Val.Fld is when F_Priority => Valid (Val.Priority_Value), when F_Initial | F_Final => - False)); + False)) + with + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); type Field_Cursor (State : Cursor_State := S_Invalid) is record diff --git a/tests/spark/generated/rflx-ethernet-frame.ads b/tests/spark/generated/rflx-ethernet-frame.ads index d1aa9f004..29846e416 100644 --- a/tests/spark/generated/rflx-ethernet-frame.ads +++ b/tests/spark/generated/rflx-ethernet-frame.ads @@ -118,8 +118,14 @@ is Depends => (Ctx => (Buffer, First, Last, Written_Last), Buffer => null); + pragma Warnings (Off, "postcondition does not mention function result"); + function Initialized (Ctx : Context) return Boolean with - Ghost; + Ghost, + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); procedure Reset (Ctx : in out Context) with Pre => @@ -249,15 +255,27 @@ is and then Structural_Valid_Message (Ctx) and then Data'Length = Byte_Size (Ctx); + pragma Warnings (Off, "postcondition does not mention function result"); + function Path_Condition (Ctx : Context; Fld : Field) return Boolean with Pre => - Valid_Predecessor (Ctx, Fld); + Valid_Predecessor (Ctx, Fld), + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); + + pragma Warnings (Off, "postcondition does not mention function result"); function Field_Condition (Ctx : Context; Val : Field_Dependent_Value; Size : RFLX_Types.Bit_Length := 0) return Boolean with Pre => Has_Buffer (Ctx) and Val.Fld in Field'Range - and Valid_Predecessor (Ctx, Val.Fld); + and Valid_Predecessor (Ctx, Val.Fld), + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); function Field_Size (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Length with Pre => @@ -269,9 +287,15 @@ is when others => True); + pragma Warnings (Off, "postcondition does not mention function result"); + function Field_First (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Index with Pre => - Valid_Next (Ctx, Fld); + Valid_Next (Ctx, Fld), + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); function Field_Last (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Index with Pre => @@ -284,9 +308,21 @@ is when others => True); - function Predecessor (Ctx : Context; Fld : Virtual_Field) return Virtual_Field; + pragma Warnings (Off, "postcondition does not mention function result"); + + function Predecessor (Ctx : Context; Fld : Virtual_Field) return Virtual_Field with + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); + + pragma Warnings (Off, "postcondition does not mention function result"); + + function Valid_Predecessor (Ctx : Context; Fld : Virtual_Field) return Boolean with + Post => + True; - function Valid_Predecessor (Ctx : Context; Fld : Virtual_Field) return Boolean; + pragma Warnings (On, "postcondition does not mention function result"); function Valid_Next (Ctx : Context; Fld : Field) return Boolean; @@ -335,7 +371,13 @@ is Pre => Has_Buffer (Ctx); - function Incomplete_Message (Ctx : Context) return Boolean; + pragma Warnings (Off, "postcondition does not mention function result"); + + function Incomplete_Message (Ctx : Context) return Boolean with + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); pragma Warnings (Off, "precondition is always False"); @@ -388,9 +430,15 @@ is Has_Buffer (Ctx) and Present (Ctx, F_Payload); + pragma Warnings (Off, "postcondition does not mention function result"); + function Valid_Length (Ctx : Context; Fld : Field; Length : RFLX_Types.Length) return Boolean with Pre => - Valid_Next (Ctx, Fld); + Valid_Next (Ctx, Fld), + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); procedure Set_Destination (Ctx : in out Context; Val : RFLX.Ethernet.Address) with Pre => @@ -677,6 +725,8 @@ private type Cursor_State is (S_Valid, S_Structural_Valid, S_Invalid, S_Incomplete); + pragma Warnings (Off, "postcondition does not mention function result"); + function Valid_Value (Val : Field_Dependent_Value) return Boolean is ((case Val.Fld is when F_Destination => @@ -694,7 +744,12 @@ private when F_Payload => True, when F_Initial | F_Final => - False)); + False)) + with + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); type Field_Cursor (State : Cursor_State := S_Invalid) is record diff --git a/tests/spark/generated/rflx-expression-message.ads b/tests/spark/generated/rflx-expression-message.ads index cad88d382..ecf84171b 100644 --- a/tests/spark/generated/rflx-expression-message.ads +++ b/tests/spark/generated/rflx-expression-message.ads @@ -114,8 +114,14 @@ is Depends => (Ctx => (Buffer, First, Last, Written_Last), Buffer => null); + pragma Warnings (Off, "postcondition does not mention function result"); + function Initialized (Ctx : Context) return Boolean with - Ghost; + Ghost, + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); procedure Reset (Ctx : in out Context) with Pre => @@ -245,15 +251,27 @@ is and then Structural_Valid_Message (Ctx) and then Data'Length = Byte_Size (Ctx); + pragma Warnings (Off, "postcondition does not mention function result"); + function Path_Condition (Ctx : Context; Fld : Field) return Boolean with Pre => - Valid_Predecessor (Ctx, Fld); + Valid_Predecessor (Ctx, Fld), + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); + + pragma Warnings (Off, "postcondition does not mention function result"); function Field_Condition (Ctx : Context; Val : Field_Dependent_Value) return Boolean with Pre => Has_Buffer (Ctx) and Val.Fld in Field'Range - and Valid_Predecessor (Ctx, Val.Fld); + and Valid_Predecessor (Ctx, Val.Fld), + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); function Field_Size (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Length with Pre => @@ -263,9 +281,15 @@ is when F_Payload => Field_Size'Result rem RFLX_Types.Byte'Size = 0); + pragma Warnings (Off, "postcondition does not mention function result"); + function Field_First (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Index with Pre => - Valid_Next (Ctx, Fld); + Valid_Next (Ctx, Fld), + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); function Field_Last (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Index with Pre => @@ -276,9 +300,21 @@ is when F_Payload => Field_Last'Result rem RFLX_Types.Byte'Size = 0); - function Predecessor (Ctx : Context; Fld : Virtual_Field) return Virtual_Field; + pragma Warnings (Off, "postcondition does not mention function result"); + + function Predecessor (Ctx : Context; Fld : Virtual_Field) return Virtual_Field with + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); + + pragma Warnings (Off, "postcondition does not mention function result"); + + function Valid_Predecessor (Ctx : Context; Fld : Virtual_Field) return Boolean with + Post => + True; - function Valid_Predecessor (Ctx : Context; Fld : Virtual_Field) return Boolean; + pragma Warnings (On, "postcondition does not mention function result"); function Valid_Next (Ctx : Context; Fld : Field) return Boolean; @@ -327,7 +363,13 @@ is Pre => Has_Buffer (Ctx); - function Incomplete_Message (Ctx : Context) return Boolean; + pragma Warnings (Off, "postcondition does not mention function result"); + + function Incomplete_Message (Ctx : Context) return Boolean with + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); pragma Warnings (Off, "precondition is always False"); @@ -356,9 +398,15 @@ is Has_Buffer (Ctx) and Present (Ctx, F_Payload); + pragma Warnings (Off, "postcondition does not mention function result"); + function Valid_Length (Ctx : Context; Fld : Field; Length : RFLX_Types.Length) return Boolean with Pre => - Valid_Next (Ctx, Fld); + Valid_Next (Ctx, Fld), + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); procedure Initialize_Payload (Ctx : in out Context) with Pre => @@ -462,12 +510,19 @@ private type Cursor_State is (S_Valid, S_Structural_Valid, S_Invalid, S_Incomplete); + pragma Warnings (Off, "postcondition does not mention function result"); + function Valid_Value (Val : Field_Dependent_Value) return Boolean is ((case Val.Fld is when F_Payload => True, when F_Initial | F_Final => - False)); + False)) + with + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); type Field_Cursor (State : Cursor_State := S_Invalid) is record diff --git a/tests/spark/generated/rflx-fixed_size-simple_message.ads b/tests/spark/generated/rflx-fixed_size-simple_message.ads index 233784ea2..c7be1983d 100644 --- a/tests/spark/generated/rflx-fixed_size-simple_message.ads +++ b/tests/spark/generated/rflx-fixed_size-simple_message.ads @@ -110,8 +110,14 @@ is Depends => (Ctx => (Buffer, First, Last, Written_Last), Buffer => null); + pragma Warnings (Off, "postcondition does not mention function result"); + function Initialized (Ctx : Context) return Boolean with - Ghost; + Ghost, + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); procedure Reset (Ctx : in out Context) with Pre => @@ -241,15 +247,27 @@ is and then Structural_Valid_Message (Ctx) and then Data'Length = Byte_Size (Ctx); + pragma Warnings (Off, "postcondition does not mention function result"); + function Path_Condition (Ctx : Context; Fld : Field) return Boolean with Pre => - Valid_Predecessor (Ctx, Fld); + Valid_Predecessor (Ctx, Fld), + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); + + pragma Warnings (Off, "postcondition does not mention function result"); function Field_Condition (Ctx : Context; Val : Field_Dependent_Value) return Boolean with Pre => Has_Buffer (Ctx) and Val.Fld in Field'Range - and Valid_Predecessor (Ctx, Val.Fld); + and Valid_Predecessor (Ctx, Val.Fld), + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); function Field_Size (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Length with Pre => @@ -261,9 +279,15 @@ is when others => True); + pragma Warnings (Off, "postcondition does not mention function result"); + function Field_First (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Index with Pre => - Valid_Next (Ctx, Fld); + Valid_Next (Ctx, Fld), + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); function Field_Last (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Index with Pre => @@ -276,9 +300,21 @@ is when others => True); - function Predecessor (Ctx : Context; Fld : Virtual_Field) return Virtual_Field; + pragma Warnings (Off, "postcondition does not mention function result"); + + function Predecessor (Ctx : Context; Fld : Virtual_Field) return Virtual_Field with + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); + + pragma Warnings (Off, "postcondition does not mention function result"); + + function Valid_Predecessor (Ctx : Context; Fld : Virtual_Field) return Boolean with + Post => + True; - function Valid_Predecessor (Ctx : Context; Fld : Virtual_Field) return Boolean; + pragma Warnings (On, "postcondition does not mention function result"); function Valid_Next (Ctx : Context; Fld : Field) return Boolean; @@ -327,7 +363,13 @@ is Pre => Has_Buffer (Ctx); - function Incomplete_Message (Ctx : Context) return Boolean; + pragma Warnings (Off, "postcondition does not mention function result"); + + function Incomplete_Message (Ctx : Context) return Boolean with + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); pragma Warnings (Off, "precondition is always False"); @@ -360,9 +402,15 @@ is Has_Buffer (Ctx) and Present (Ctx, F_Data); + pragma Warnings (Off, "postcondition does not mention function result"); + function Valid_Length (Ctx : Context; Fld : Field; Length : RFLX_Types.Length) return Boolean with Pre => - Valid_Next (Ctx, Fld); + Valid_Next (Ctx, Fld), + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); procedure Set_Message_Type (Ctx : in out Context; Val : RFLX.Universal.Option_Type_Enum) with Pre => @@ -492,6 +540,8 @@ private type Cursor_State is (S_Valid, S_Structural_Valid, S_Invalid, S_Incomplete); + pragma Warnings (Off, "postcondition does not mention function result"); + function Valid_Value (Val : Field_Dependent_Value) return Boolean is ((case Val.Fld is when F_Message_Type => @@ -499,7 +549,12 @@ private when F_Data => True, when F_Initial | F_Final => - False)); + False)) + with + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); type Field_Cursor (State : Cursor_State := S_Invalid) is record diff --git a/tests/spark/generated/rflx-icmp-message.ads b/tests/spark/generated/rflx-icmp-message.ads index 3e4bc7504..43ac634a3 100644 --- a/tests/spark/generated/rflx-icmp-message.ads +++ b/tests/spark/generated/rflx-icmp-message.ads @@ -136,8 +136,14 @@ is Depends => (Ctx => (Buffer, First, Last, Written_Last), Buffer => null); + pragma Warnings (Off, "postcondition does not mention function result"); + function Initialized (Ctx : Context) return Boolean with - Ghost; + Ghost, + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); procedure Reset (Ctx : in out Context) with Pre => @@ -267,15 +273,27 @@ is and then Structural_Valid_Message (Ctx) and then Data'Length = Byte_Size (Ctx); + pragma Warnings (Off, "postcondition does not mention function result"); + function Path_Condition (Ctx : Context; Fld : Field) return Boolean with Pre => - Valid_Predecessor (Ctx, Fld); + Valid_Predecessor (Ctx, Fld), + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); + + pragma Warnings (Off, "postcondition does not mention function result"); function Field_Condition (Ctx : Context; Val : Field_Dependent_Value) return Boolean with Pre => Has_Buffer (Ctx) and Val.Fld in Field'Range - and Valid_Predecessor (Ctx, Val.Fld); + and Valid_Predecessor (Ctx, Val.Fld), + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); function Field_Size (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Length with Pre => @@ -287,9 +305,15 @@ is when others => True); + pragma Warnings (Off, "postcondition does not mention function result"); + function Field_First (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Index with Pre => - Valid_Next (Ctx, Fld); + Valid_Next (Ctx, Fld), + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); function Field_Last (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Index with Pre => @@ -302,9 +326,21 @@ is when others => True); - function Predecessor (Ctx : Context; Fld : Virtual_Field) return Virtual_Field; + pragma Warnings (Off, "postcondition does not mention function result"); + + function Predecessor (Ctx : Context; Fld : Virtual_Field) return Virtual_Field with + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); + + pragma Warnings (Off, "postcondition does not mention function result"); + + function Valid_Predecessor (Ctx : Context; Fld : Virtual_Field) return Boolean with + Post => + True; - function Valid_Predecessor (Ctx : Context; Fld : Virtual_Field) return Boolean; + pragma Warnings (On, "postcondition does not mention function result"); function Valid_Next (Ctx : Context; Fld : Field) return Boolean; @@ -353,7 +389,13 @@ is Pre => Has_Buffer (Ctx); - function Incomplete_Message (Ctx : Context) return Boolean; + pragma Warnings (Off, "postcondition does not mention function result"); + + function Incomplete_Message (Ctx : Context) return Boolean with + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); pragma Warnings (Off, "precondition is always False"); @@ -442,9 +484,15 @@ is Has_Buffer (Ctx) and Present (Ctx, F_Data); + pragma Warnings (Off, "postcondition does not mention function result"); + function Valid_Length (Ctx : Context; Fld : Field; Length : RFLX_Types.Length) return Boolean with Pre => - Valid_Next (Ctx, Fld); + Valid_Next (Ctx, Fld), + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); procedure Set_Tag (Ctx : in out Context; Val : RFLX.ICMP.Tag) with Pre => @@ -1199,6 +1247,8 @@ private type Cursor_State is (S_Valid, S_Structural_Valid, S_Invalid, S_Incomplete); + pragma Warnings (Off, "postcondition does not mention function result"); + function Valid_Value (Val : Field_Dependent_Value) return Boolean is ((case Val.Fld is when F_Tag => @@ -1234,7 +1284,12 @@ private when F_Transmit_Timestamp => Valid (Val.Transmit_Timestamp_Value), when F_Initial | F_Final => - False)); + False)) + with + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); type Field_Cursor (State : Cursor_State := S_Invalid) is record diff --git a/tests/spark/generated/rflx-ipv4-option.ads b/tests/spark/generated/rflx-ipv4-option.ads index ceb37a157..01874ec23 100644 --- a/tests/spark/generated/rflx-ipv4-option.ads +++ b/tests/spark/generated/rflx-ipv4-option.ads @@ -117,8 +117,14 @@ is Depends => (Ctx => (Buffer, First, Last, Written_Last), Buffer => null); + pragma Warnings (Off, "postcondition does not mention function result"); + function Initialized (Ctx : Context) return Boolean with - Ghost; + Ghost, + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); procedure Reset (Ctx : in out Context) with Pre => @@ -248,15 +254,27 @@ is and then Structural_Valid_Message (Ctx) and then Data'Length = Byte_Size (Ctx); + pragma Warnings (Off, "postcondition does not mention function result"); + function Path_Condition (Ctx : Context; Fld : Field) return Boolean with Pre => - Valid_Predecessor (Ctx, Fld); + Valid_Predecessor (Ctx, Fld), + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); + + pragma Warnings (Off, "postcondition does not mention function result"); function Field_Condition (Ctx : Context; Val : Field_Dependent_Value) return Boolean with Pre => Has_Buffer (Ctx) and Val.Fld in Field'Range - and Valid_Predecessor (Ctx, Val.Fld); + and Valid_Predecessor (Ctx, Val.Fld), + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); function Field_Size (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Length with Pre => @@ -268,9 +286,15 @@ is when others => True); + pragma Warnings (Off, "postcondition does not mention function result"); + function Field_First (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Index with Pre => - Valid_Next (Ctx, Fld); + Valid_Next (Ctx, Fld), + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); function Field_Last (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Index with Pre => @@ -283,9 +307,21 @@ is when others => True); - function Predecessor (Ctx : Context; Fld : Virtual_Field) return Virtual_Field; + pragma Warnings (Off, "postcondition does not mention function result"); + + function Predecessor (Ctx : Context; Fld : Virtual_Field) return Virtual_Field with + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); + + pragma Warnings (Off, "postcondition does not mention function result"); + + function Valid_Predecessor (Ctx : Context; Fld : Virtual_Field) return Boolean with + Post => + True; - function Valid_Predecessor (Ctx : Context; Fld : Virtual_Field) return Boolean; + pragma Warnings (On, "postcondition does not mention function result"); function Valid_Next (Ctx : Context; Fld : Field) return Boolean; @@ -334,7 +370,13 @@ is Pre => Has_Buffer (Ctx); - function Incomplete_Message (Ctx : Context) return Boolean; + pragma Warnings (Off, "postcondition does not mention function result"); + + function Incomplete_Message (Ctx : Context) return Boolean with + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); pragma Warnings (Off, "precondition is always False"); @@ -379,9 +421,15 @@ is Has_Buffer (Ctx) and Present (Ctx, F_Option_Data); + pragma Warnings (Off, "postcondition does not mention function result"); + function Valid_Length (Ctx : Context; Fld : Field; Length : RFLX_Types.Length) return Boolean with Pre => - Valid_Next (Ctx, Fld); + Valid_Next (Ctx, Fld), + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); procedure Set_Copied (Ctx : in out Context; Val : Boolean) with Pre => @@ -627,6 +675,8 @@ private type Cursor_State is (S_Valid, S_Structural_Valid, S_Invalid, S_Incomplete); + pragma Warnings (Off, "postcondition does not mention function result"); + function Valid_Value (Val : Field_Dependent_Value) return Boolean is ((case Val.Fld is when F_Copied => @@ -640,7 +690,12 @@ private when F_Option_Data => True, when F_Initial | F_Final => - False)); + False)) + with + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); type Field_Cursor (State : Cursor_State := S_Invalid) is record diff --git a/tests/spark/generated/rflx-ipv4-packet.ads b/tests/spark/generated/rflx-ipv4-packet.ads index 3cad27a18..5ab370198 100644 --- a/tests/spark/generated/rflx-ipv4-packet.ads +++ b/tests/spark/generated/rflx-ipv4-packet.ads @@ -140,8 +140,14 @@ is Depends => (Ctx => (Buffer, First, Last, Written_Last), Buffer => null); + pragma Warnings (Off, "postcondition does not mention function result"); + function Initialized (Ctx : Context) return Boolean with - Ghost; + Ghost, + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); procedure Reset (Ctx : in out Context) with Pre => @@ -271,15 +277,27 @@ is and then Structural_Valid_Message (Ctx) and then Data'Length = Byte_Size (Ctx); + pragma Warnings (Off, "postcondition does not mention function result"); + function Path_Condition (Ctx : Context; Fld : Field) return Boolean with Pre => - Valid_Predecessor (Ctx, Fld); + Valid_Predecessor (Ctx, Fld), + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); + + pragma Warnings (Off, "postcondition does not mention function result"); function Field_Condition (Ctx : Context; Val : Field_Dependent_Value) return Boolean with Pre => Has_Buffer (Ctx) and Val.Fld in Field'Range - and Valid_Predecessor (Ctx, Val.Fld); + and Valid_Predecessor (Ctx, Val.Fld), + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); function Field_Size (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Length with Pre => @@ -291,9 +309,15 @@ is when others => True); + pragma Warnings (Off, "postcondition does not mention function result"); + function Field_First (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Index with Pre => - Valid_Next (Ctx, Fld); + Valid_Next (Ctx, Fld), + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); function Field_Last (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Index with Pre => @@ -306,9 +330,21 @@ is when others => True); - function Predecessor (Ctx : Context; Fld : Virtual_Field) return Virtual_Field; + pragma Warnings (Off, "postcondition does not mention function result"); + + function Predecessor (Ctx : Context; Fld : Virtual_Field) return Virtual_Field with + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); + + pragma Warnings (Off, "postcondition does not mention function result"); + + function Valid_Predecessor (Ctx : Context; Fld : Virtual_Field) return Boolean with + Post => + True; - function Valid_Predecessor (Ctx : Context; Fld : Virtual_Field) return Boolean; + pragma Warnings (On, "postcondition does not mention function result"); function Valid_Next (Ctx : Context; Fld : Field) return Boolean; @@ -357,7 +393,13 @@ is Pre => Has_Buffer (Ctx); - function Incomplete_Message (Ctx : Context) return Boolean; + pragma Warnings (Off, "postcondition does not mention function result"); + + function Incomplete_Message (Ctx : Context) return Boolean with + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); pragma Warnings (Off, "precondition is always False"); @@ -446,9 +488,15 @@ is Has_Buffer (Ctx) and Present (Ctx, F_Payload); + pragma Warnings (Off, "postcondition does not mention function result"); + function Valid_Length (Ctx : Context; Fld : Field; Length : RFLX_Types.Length) return Boolean with Pre => - Valid_Next (Ctx, Fld); + Valid_Next (Ctx, Fld), + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); procedure Set_Version (Ctx : in out Context; Val : RFLX.IPv4.Version) with Pre => @@ -1471,6 +1519,8 @@ private type Cursor_State is (S_Valid, S_Structural_Valid, S_Invalid, S_Incomplete); + pragma Warnings (Off, "postcondition does not mention function result"); + function Valid_Value (Val : Field_Dependent_Value) return Boolean is ((case Val.Fld is when F_Version => @@ -1506,7 +1556,12 @@ private when F_Options | F_Payload => True, when F_Initial | F_Final => - False)); + False)) + with + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); type Field_Cursor (State : Cursor_State := S_Invalid) is record diff --git a/tests/spark/generated/rflx-sequence-inner_message.ads b/tests/spark/generated/rflx-sequence-inner_message.ads index fb8b52b4e..7886ce774 100644 --- a/tests/spark/generated/rflx-sequence-inner_message.ads +++ b/tests/spark/generated/rflx-sequence-inner_message.ads @@ -108,8 +108,14 @@ is Depends => (Ctx => (Buffer, First, Last, Written_Last), Buffer => null); + pragma Warnings (Off, "postcondition does not mention function result"); + function Initialized (Ctx : Context) return Boolean with - Ghost; + Ghost, + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); procedure Reset (Ctx : in out Context) with Pre => @@ -239,15 +245,27 @@ is and then Structural_Valid_Message (Ctx) and then Data'Length = Byte_Size (Ctx); + pragma Warnings (Off, "postcondition does not mention function result"); + function Path_Condition (Ctx : Context; Fld : Field) return Boolean with Pre => - Valid_Predecessor (Ctx, Fld); + Valid_Predecessor (Ctx, Fld), + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); + + pragma Warnings (Off, "postcondition does not mention function result"); function Field_Condition (Ctx : Context; Val : Field_Dependent_Value) return Boolean with Pre => Has_Buffer (Ctx) and Val.Fld in Field'Range - and Valid_Predecessor (Ctx, Val.Fld); + and Valid_Predecessor (Ctx, Val.Fld), + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); function Field_Size (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Length with Pre => @@ -259,9 +277,15 @@ is when others => True); + pragma Warnings (Off, "postcondition does not mention function result"); + function Field_First (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Index with Pre => - Valid_Next (Ctx, Fld); + Valid_Next (Ctx, Fld), + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); function Field_Last (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Index with Pre => @@ -274,9 +298,21 @@ is when others => True); - function Predecessor (Ctx : Context; Fld : Virtual_Field) return Virtual_Field; + pragma Warnings (Off, "postcondition does not mention function result"); + + function Predecessor (Ctx : Context; Fld : Virtual_Field) return Virtual_Field with + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); + + pragma Warnings (Off, "postcondition does not mention function result"); + + function Valid_Predecessor (Ctx : Context; Fld : Virtual_Field) return Boolean with + Post => + True; - function Valid_Predecessor (Ctx : Context; Fld : Virtual_Field) return Boolean; + pragma Warnings (On, "postcondition does not mention function result"); function Valid_Next (Ctx : Context; Fld : Field) return Boolean; @@ -325,7 +361,13 @@ is Pre => Has_Buffer (Ctx); - function Incomplete_Message (Ctx : Context) return Boolean; + pragma Warnings (Off, "postcondition does not mention function result"); + + function Incomplete_Message (Ctx : Context) return Boolean with + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); pragma Warnings (Off, "precondition is always False"); @@ -358,9 +400,15 @@ is Has_Buffer (Ctx) and Present (Ctx, F_Payload); + pragma Warnings (Off, "postcondition does not mention function result"); + function Valid_Length (Ctx : Context; Fld : Field; Length : RFLX_Types.Length) return Boolean with Pre => - Valid_Next (Ctx, Fld); + Valid_Next (Ctx, Fld), + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); procedure Set_Length (Ctx : in out Context; Val : RFLX.Sequence.Length) with Pre => @@ -513,6 +561,8 @@ private type Cursor_State is (S_Valid, S_Structural_Valid, S_Invalid, S_Incomplete); + pragma Warnings (Off, "postcondition does not mention function result"); + function Valid_Value (Val : Field_Dependent_Value) return Boolean is ((case Val.Fld is when F_Length => @@ -520,7 +570,12 @@ private when F_Payload => True, when F_Initial | F_Final => - False)); + False)) + with + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); type Field_Cursor (State : Cursor_State := S_Invalid) is record diff --git a/tests/spark/generated/rflx-sequence-message.ads b/tests/spark/generated/rflx-sequence-message.ads index 4011c7881..9c9a778b7 100644 --- a/tests/spark/generated/rflx-sequence-message.ads +++ b/tests/spark/generated/rflx-sequence-message.ads @@ -112,8 +112,14 @@ is Depends => (Ctx => (Buffer, First, Last, Written_Last), Buffer => null); + pragma Warnings (Off, "postcondition does not mention function result"); + function Initialized (Ctx : Context) return Boolean with - Ghost; + Ghost, + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); procedure Reset (Ctx : in out Context) with Pre => @@ -243,15 +249,27 @@ is and then Structural_Valid_Message (Ctx) and then Data'Length = Byte_Size (Ctx); + pragma Warnings (Off, "postcondition does not mention function result"); + function Path_Condition (Ctx : Context; Fld : Field) return Boolean with Pre => - Valid_Predecessor (Ctx, Fld); + Valid_Predecessor (Ctx, Fld), + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); + + pragma Warnings (Off, "postcondition does not mention function result"); function Field_Condition (Ctx : Context; Val : Field_Dependent_Value) return Boolean with Pre => Has_Buffer (Ctx) and Val.Fld in Field'Range - and Valid_Predecessor (Ctx, Val.Fld); + and Valid_Predecessor (Ctx, Val.Fld), + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); function Field_Size (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Length with Pre => @@ -263,9 +281,15 @@ is when others => True); + pragma Warnings (Off, "postcondition does not mention function result"); + function Field_First (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Index with Pre => - Valid_Next (Ctx, Fld); + Valid_Next (Ctx, Fld), + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); function Field_Last (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Index with Pre => @@ -278,9 +302,21 @@ is when others => True); - function Predecessor (Ctx : Context; Fld : Virtual_Field) return Virtual_Field; + pragma Warnings (Off, "postcondition does not mention function result"); + + function Predecessor (Ctx : Context; Fld : Virtual_Field) return Virtual_Field with + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); + + pragma Warnings (Off, "postcondition does not mention function result"); + + function Valid_Predecessor (Ctx : Context; Fld : Virtual_Field) return Boolean with + Post => + True; - function Valid_Predecessor (Ctx : Context; Fld : Virtual_Field) return Boolean; + pragma Warnings (On, "postcondition does not mention function result"); function Valid_Next (Ctx : Context; Fld : Field) return Boolean; @@ -329,7 +365,13 @@ is Pre => Has_Buffer (Ctx); - function Incomplete_Message (Ctx : Context) return Boolean; + pragma Warnings (Off, "postcondition does not mention function result"); + + function Incomplete_Message (Ctx : Context) return Boolean with + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); pragma Warnings (Off, "precondition is always False"); @@ -339,9 +381,15 @@ is pragma Warnings (On, "precondition is always False"); + pragma Warnings (Off, "postcondition does not mention function result"); + function Valid_Length (Ctx : Context; Fld : Field; Length : RFLX_Types.Length) return Boolean with Pre => - Valid_Next (Ctx, Fld); + Valid_Next (Ctx, Fld), + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); procedure Set_Length (Ctx : in out Context; Val : RFLX.Sequence.Length) with Pre => @@ -907,6 +955,8 @@ private type Cursor_State is (S_Valid, S_Structural_Valid, S_Invalid, S_Incomplete); + pragma Warnings (Off, "postcondition does not mention function result"); + function Valid_Value (Val : Field_Dependent_Value) return Boolean is ((case Val.Fld is when F_Length => @@ -914,7 +964,12 @@ private when F_Modular_Vector | F_Range_Vector | F_Enumeration_Vector | F_AV_Enumeration_Vector => True, when F_Initial | F_Final => - False)); + False)) + with + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); type Field_Cursor (State : Cursor_State := S_Invalid) is record diff --git a/tests/spark/generated/rflx-sequence-messages_message.ads b/tests/spark/generated/rflx-sequence-messages_message.ads index 2351bca06..2d0b20217 100644 --- a/tests/spark/generated/rflx-sequence-messages_message.ads +++ b/tests/spark/generated/rflx-sequence-messages_message.ads @@ -109,8 +109,14 @@ is Depends => (Ctx => (Buffer, First, Last, Written_Last), Buffer => null); + pragma Warnings (Off, "postcondition does not mention function result"); + function Initialized (Ctx : Context) return Boolean with - Ghost; + Ghost, + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); procedure Reset (Ctx : in out Context) with Pre => @@ -240,15 +246,27 @@ is and then Structural_Valid_Message (Ctx) and then Data'Length = Byte_Size (Ctx); + pragma Warnings (Off, "postcondition does not mention function result"); + function Path_Condition (Ctx : Context; Fld : Field) return Boolean with Pre => - Valid_Predecessor (Ctx, Fld); + Valid_Predecessor (Ctx, Fld), + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); + + pragma Warnings (Off, "postcondition does not mention function result"); function Field_Condition (Ctx : Context; Val : Field_Dependent_Value) return Boolean with Pre => Has_Buffer (Ctx) and Val.Fld in Field'Range - and Valid_Predecessor (Ctx, Val.Fld); + and Valid_Predecessor (Ctx, Val.Fld), + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); function Field_Size (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Length with Pre => @@ -260,9 +278,15 @@ is when others => True); + pragma Warnings (Off, "postcondition does not mention function result"); + function Field_First (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Index with Pre => - Valid_Next (Ctx, Fld); + Valid_Next (Ctx, Fld), + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); function Field_Last (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Index with Pre => @@ -275,9 +299,21 @@ is when others => True); - function Predecessor (Ctx : Context; Fld : Virtual_Field) return Virtual_Field; + pragma Warnings (Off, "postcondition does not mention function result"); + + function Predecessor (Ctx : Context; Fld : Virtual_Field) return Virtual_Field with + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); + + pragma Warnings (Off, "postcondition does not mention function result"); + + function Valid_Predecessor (Ctx : Context; Fld : Virtual_Field) return Boolean with + Post => + True; - function Valid_Predecessor (Ctx : Context; Fld : Virtual_Field) return Boolean; + pragma Warnings (On, "postcondition does not mention function result"); function Valid_Next (Ctx : Context; Fld : Field) return Boolean; @@ -326,7 +362,13 @@ is Pre => Has_Buffer (Ctx); - function Incomplete_Message (Ctx : Context) return Boolean; + pragma Warnings (Off, "postcondition does not mention function result"); + + function Incomplete_Message (Ctx : Context) return Boolean with + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); pragma Warnings (Off, "precondition is always False"); @@ -336,9 +378,15 @@ is pragma Warnings (On, "precondition is always False"); + pragma Warnings (Off, "postcondition does not mention function result"); + function Valid_Length (Ctx : Context; Fld : Field; Length : RFLX_Types.Length) return Boolean with Pre => - Valid_Next (Ctx, Fld); + Valid_Next (Ctx, Fld), + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); procedure Set_Length (Ctx : in out Context; Val : RFLX.Sequence.Length) with Pre => @@ -510,6 +558,8 @@ private type Cursor_State is (S_Valid, S_Structural_Valid, S_Invalid, S_Incomplete); + pragma Warnings (Off, "postcondition does not mention function result"); + function Valid_Value (Val : Field_Dependent_Value) return Boolean is ((case Val.Fld is when F_Length => @@ -517,7 +567,12 @@ private when F_Messages => True, when F_Initial | F_Final => - False)); + False)) + with + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); type Field_Cursor (State : Cursor_State := S_Invalid) is record diff --git a/tests/spark/generated/rflx-sequence-sequence_size_defined_by_message_size.ads b/tests/spark/generated/rflx-sequence-sequence_size_defined_by_message_size.ads index 469508d12..7e9829245 100644 --- a/tests/spark/generated/rflx-sequence-sequence_size_defined_by_message_size.ads +++ b/tests/spark/generated/rflx-sequence-sequence_size_defined_by_message_size.ads @@ -109,8 +109,14 @@ is Depends => (Ctx => (Buffer, First, Last, Written_Last), Buffer => null); + pragma Warnings (Off, "postcondition does not mention function result"); + function Initialized (Ctx : Context) return Boolean with - Ghost; + Ghost, + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); procedure Reset (Ctx : in out Context) with Pre => @@ -240,15 +246,27 @@ is and then Structural_Valid_Message (Ctx) and then Data'Length = Byte_Size (Ctx); + pragma Warnings (Off, "postcondition does not mention function result"); + function Path_Condition (Ctx : Context; Fld : Field) return Boolean with Pre => - Valid_Predecessor (Ctx, Fld); + Valid_Predecessor (Ctx, Fld), + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); + + pragma Warnings (Off, "postcondition does not mention function result"); function Field_Condition (Ctx : Context; Val : Field_Dependent_Value) return Boolean with Pre => Has_Buffer (Ctx) and Val.Fld in Field'Range - and Valid_Predecessor (Ctx, Val.Fld); + and Valid_Predecessor (Ctx, Val.Fld), + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); function Field_Size (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Length with Pre => @@ -260,9 +278,15 @@ is when others => True); + pragma Warnings (Off, "postcondition does not mention function result"); + function Field_First (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Index with Pre => - Valid_Next (Ctx, Fld); + Valid_Next (Ctx, Fld), + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); function Field_Last (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Index with Pre => @@ -275,9 +299,21 @@ is when others => True); - function Predecessor (Ctx : Context; Fld : Virtual_Field) return Virtual_Field; + pragma Warnings (Off, "postcondition does not mention function result"); + + function Predecessor (Ctx : Context; Fld : Virtual_Field) return Virtual_Field with + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); + + pragma Warnings (Off, "postcondition does not mention function result"); + + function Valid_Predecessor (Ctx : Context; Fld : Virtual_Field) return Boolean with + Post => + True; - function Valid_Predecessor (Ctx : Context; Fld : Virtual_Field) return Boolean; + pragma Warnings (On, "postcondition does not mention function result"); function Valid_Next (Ctx : Context; Fld : Field) return Boolean; @@ -326,7 +362,13 @@ is Pre => Has_Buffer (Ctx); - function Incomplete_Message (Ctx : Context) return Boolean; + pragma Warnings (Off, "postcondition does not mention function result"); + + function Incomplete_Message (Ctx : Context) return Boolean with + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); pragma Warnings (Off, "precondition is always False"); @@ -336,9 +378,15 @@ is pragma Warnings (On, "precondition is always False"); + pragma Warnings (Off, "postcondition does not mention function result"); + function Valid_Length (Ctx : Context; Fld : Field; Length : RFLX_Types.Length) return Boolean with Pre => - Valid_Next (Ctx, Fld); + Valid_Next (Ctx, Fld), + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); procedure Set_Header (Ctx : in out Context; Val : RFLX.Sequence.Enumeration) with Pre => @@ -512,6 +560,8 @@ private type Cursor_State is (S_Valid, S_Structural_Valid, S_Invalid, S_Incomplete); + pragma Warnings (Off, "postcondition does not mention function result"); + function Valid_Value (Val : Field_Dependent_Value) return Boolean is ((case Val.Fld is when F_Header => @@ -519,7 +569,12 @@ private when F_Vector => True, when F_Initial | F_Final => - False)); + False)) + with + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); type Field_Cursor (State : Cursor_State := S_Invalid) is record diff --git a/tests/spark/generated/rflx-tlv-message.ads b/tests/spark/generated/rflx-tlv-message.ads index e84e7567f..d22005eb5 100644 --- a/tests/spark/generated/rflx-tlv-message.ads +++ b/tests/spark/generated/rflx-tlv-message.ads @@ -110,8 +110,14 @@ is Depends => (Ctx => (Buffer, First, Last, Written_Last), Buffer => null); + pragma Warnings (Off, "postcondition does not mention function result"); + function Initialized (Ctx : Context) return Boolean with - Ghost; + Ghost, + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); procedure Reset (Ctx : in out Context) with Pre => @@ -241,15 +247,27 @@ is and then Structural_Valid_Message (Ctx) and then Data'Length = Byte_Size (Ctx); + pragma Warnings (Off, "postcondition does not mention function result"); + function Path_Condition (Ctx : Context; Fld : Field) return Boolean with Pre => - Valid_Predecessor (Ctx, Fld); + Valid_Predecessor (Ctx, Fld), + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); + + pragma Warnings (Off, "postcondition does not mention function result"); function Field_Condition (Ctx : Context; Val : Field_Dependent_Value) return Boolean with Pre => Has_Buffer (Ctx) and Val.Fld in Field'Range - and Valid_Predecessor (Ctx, Val.Fld); + and Valid_Predecessor (Ctx, Val.Fld), + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); function Field_Size (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Length with Pre => @@ -261,9 +279,15 @@ is when others => True); + pragma Warnings (Off, "postcondition does not mention function result"); + function Field_First (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Index with Pre => - Valid_Next (Ctx, Fld); + Valid_Next (Ctx, Fld), + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); function Field_Last (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Index with Pre => @@ -276,9 +300,21 @@ is when others => True); - function Predecessor (Ctx : Context; Fld : Virtual_Field) return Virtual_Field; + pragma Warnings (Off, "postcondition does not mention function result"); + + function Predecessor (Ctx : Context; Fld : Virtual_Field) return Virtual_Field with + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); + + pragma Warnings (Off, "postcondition does not mention function result"); + + function Valid_Predecessor (Ctx : Context; Fld : Virtual_Field) return Boolean with + Post => + True; - function Valid_Predecessor (Ctx : Context; Fld : Virtual_Field) return Boolean; + pragma Warnings (On, "postcondition does not mention function result"); function Valid_Next (Ctx : Context; Fld : Field) return Boolean; @@ -327,7 +363,13 @@ is Pre => Has_Buffer (Ctx); - function Incomplete_Message (Ctx : Context) return Boolean; + pragma Warnings (Off, "postcondition does not mention function result"); + + function Incomplete_Message (Ctx : Context) return Boolean with + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); pragma Warnings (Off, "precondition is always False"); @@ -364,9 +406,15 @@ is Has_Buffer (Ctx) and Present (Ctx, F_Value); + pragma Warnings (Off, "postcondition does not mention function result"); + function Valid_Length (Ctx : Context; Fld : Field; Length : RFLX_Types.Length) return Boolean with Pre => - Valid_Next (Ctx, Fld); + Valid_Next (Ctx, Fld), + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); procedure Set_Tag (Ctx : in out Context; Val : RFLX.TLV.Tag) with Pre => @@ -531,6 +579,8 @@ private type Cursor_State is (S_Valid, S_Structural_Valid, S_Invalid, S_Incomplete); + pragma Warnings (Off, "postcondition does not mention function result"); + function Valid_Value (Val : Field_Dependent_Value) return Boolean is ((case Val.Fld is when F_Tag => @@ -540,7 +590,12 @@ private when F_Value => True, when F_Initial | F_Final => - False)); + False)) + with + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); type Field_Cursor (State : Cursor_State := S_Invalid) is record diff --git a/tests/spark/generated/rflx-udp-datagram.ads b/tests/spark/generated/rflx-udp-datagram.ads index 64069c52d..db9e1a619 100644 --- a/tests/spark/generated/rflx-udp-datagram.ads +++ b/tests/spark/generated/rflx-udp-datagram.ads @@ -114,8 +114,14 @@ is Depends => (Ctx => (Buffer, First, Last, Written_Last), Buffer => null); + pragma Warnings (Off, "postcondition does not mention function result"); + function Initialized (Ctx : Context) return Boolean with - Ghost; + Ghost, + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); procedure Reset (Ctx : in out Context) with Pre => @@ -245,15 +251,27 @@ is and then Structural_Valid_Message (Ctx) and then Data'Length = Byte_Size (Ctx); + pragma Warnings (Off, "postcondition does not mention function result"); + function Path_Condition (Ctx : Context; Fld : Field) return Boolean with Pre => - Valid_Predecessor (Ctx, Fld); + Valid_Predecessor (Ctx, Fld), + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); + + pragma Warnings (Off, "postcondition does not mention function result"); function Field_Condition (Ctx : Context; Val : Field_Dependent_Value) return Boolean with Pre => Has_Buffer (Ctx) and Val.Fld in Field'Range - and Valid_Predecessor (Ctx, Val.Fld); + and Valid_Predecessor (Ctx, Val.Fld), + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); function Field_Size (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Length with Pre => @@ -265,9 +283,15 @@ is when others => True); + pragma Warnings (Off, "postcondition does not mention function result"); + function Field_First (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Index with Pre => - Valid_Next (Ctx, Fld); + Valid_Next (Ctx, Fld), + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); function Field_Last (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Index with Pre => @@ -280,9 +304,21 @@ is when others => True); - function Predecessor (Ctx : Context; Fld : Virtual_Field) return Virtual_Field; + pragma Warnings (Off, "postcondition does not mention function result"); + + function Predecessor (Ctx : Context; Fld : Virtual_Field) return Virtual_Field with + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); + + pragma Warnings (Off, "postcondition does not mention function result"); + + function Valid_Predecessor (Ctx : Context; Fld : Virtual_Field) return Boolean with + Post => + True; - function Valid_Predecessor (Ctx : Context; Fld : Virtual_Field) return Boolean; + pragma Warnings (On, "postcondition does not mention function result"); function Valid_Next (Ctx : Context; Fld : Field) return Boolean; @@ -331,7 +367,13 @@ is Pre => Has_Buffer (Ctx); - function Incomplete_Message (Ctx : Context) return Boolean; + pragma Warnings (Off, "postcondition does not mention function result"); + + function Incomplete_Message (Ctx : Context) return Boolean with + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); pragma Warnings (Off, "precondition is always False"); @@ -376,9 +418,15 @@ is Has_Buffer (Ctx) and Present (Ctx, F_Payload); + pragma Warnings (Off, "postcondition does not mention function result"); + function Valid_Length (Ctx : Context; Fld : Field; Length : RFLX_Types.Length) return Boolean with Pre => - Valid_Next (Ctx, Fld); + Valid_Next (Ctx, Fld), + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); procedure Set_Source_Port (Ctx : in out Context; Val : RFLX.UDP.Port) with Pre => @@ -630,6 +678,8 @@ private type Cursor_State is (S_Valid, S_Structural_Valid, S_Invalid, S_Incomplete); + pragma Warnings (Off, "postcondition does not mention function result"); + function Valid_Value (Val : Field_Dependent_Value) return Boolean is ((case Val.Fld is when F_Source_Port => @@ -643,7 +693,12 @@ private when F_Payload => True, when F_Initial | F_Final => - False)); + False)) + with + Post => + True; + + pragma Warnings (On, "postcondition does not mention function result"); type Field_Cursor (State : Cursor_State := S_Invalid) is record