This is the mail archive of the gcc-patches@gcc.gnu.org mailing list for the GCC project.
Index Nav: | [Date Index] [Subject Index] [Author Index] [Thread Index] | |
---|---|---|
Message Nav: | [Date Prev] [Date Next] | [Thread Prev] [Thread Next] |
Other format: | [Raw text] |
This patch implements apect/pragma Contract_Cases on enties. ------------ -- Source -- ------------ -- tracker.ads package Tracker is type Check_Kind is (Pre, Refined_Post, Post, Conseq_1, Conseq_2); type Tested_Array is array (Check_Kind) of Boolean; -- A value of "True" indicates that a check has been tested function Greater_Than (Kind : Check_Kind; Val : Natural; Exp : Natural) return Boolean; -- Determine whether value Val is greater than expected value Exp. The -- routine also updates the history for check of kind Kind. Duplicate -- attempts to modify the history are flagged as errors. procedure Reset; -- Reset the history procedure Verify (Exp : Tested_Array); -- Verify whether expected tests Exp were indeed checked. Emit an error if -- this is not the case. end Tracker; -- tacker.adb with Ada.Text_IO; use Ada.Text_IO; package body Tracker is History : array (Check_Kind) of Boolean := (others => False); -- The history of performed checked. A value of "True" indicates that a -- check was performed. ------------------ -- Greater_Than -- ------------------ function Greater_Than (Kind : Check_Kind; Val : Natural; Exp : Natural) return Boolean is begin if History (Kind) then Put_Line (" ERROR: " & Kind'Img & " tested multiple times"); else History (Kind) := True; end if; return Val > Exp; end Greater_Than; ----------- -- Reset -- ----------- procedure Reset is begin History := (others => False); end Reset; ------------ -- Verify -- ------------ procedure Verify (Exp : Tested_Array) is begin for Index in Check_Kind'Range loop if Exp (Index) and not History (Index) then Put_Line (" ERROR: " & Index'Img & " was not tested"); elsif not Exp (Index) and History (Index) then Put_Line (" ERROR: " & Index'Img & " was tested"); end if; end loop; end Verify; end Tracker; -- sync_contracts.ads with Tracker; use Tracker; package Sync_Contracts with SPARK_Mode, Abstract_State => State is protected type Prot_Typ is entry Prot_Entry (Input : Natural; Output : out Natural) with Global => (Input => State), Depends => ((Prot_Typ, Output) => (State, Prot_Typ, Input)), Pre => Greater_Than (Pre, Input, 1), Post => Greater_Than (Post, Output, 4), Contract_Cases => (Input < 5 => True, Input = 5 => Greater_Than (Conseq_1, Output, 6), Input = 6 => Greater_Than (Conseq_2, Output, 7), Input > 6 => False); procedure Prot_Proc (Input : Natural; Output : out Natural) with Pre => Greater_Than (Pre , Input, 1), Post => Greater_Than (Post, Output, 4), Contract_Cases => (Input < 5 => True, Input = 5 => Greater_Than (Conseq_1, Output, 6), Input = 6 => Greater_Than (Conseq_2, Output, 7), Input > 6 => False); function Prot_Func (Input : Natural) return Natural with Pre => Greater_Than (Pre , Input, 1), Post => Greater_Than (Post, Prot_Func'Result, 4), Contract_Cases => (Input < 5 => True, Input = 5 => Greater_Than (Conseq_1, Prot_Func'Result, 6), Input = 6 => Greater_Than (Conseq_2, Prot_Func'Result, 7), Input > 6 => False); end Prot_Typ; task type Tsk_Typ is entry Tsk_Entry (Input : Natural; Output : out Natural) with Pre => Greater_Than (Pre , Input, 1), Post => Greater_Than (Post, Output, 4), Contract_Cases => (Input < 5 => True, Input = 5 => Greater_Than (Conseq_1, Output, 6), Input = 6 => Greater_Than (Conseq_2, Output, 7), Input > 6 => False); end Tsk_Typ; end Sync_Contracts; -- sync_contracts.adb package body Sync_Contracts with SPARK_Mode, Refined_State => (State => Var) is Var : Integer := 1; protected body Prot_Typ is entry Prot_Entry (Input : Natural; Output : out Natural) with Refined_Global => (Input => Var), Refined_Depends => ((Prot_Typ, Output) => (Var, Prot_Typ, Input)), Refined_Post => Greater_Than (Refined_Post, Output, 3) when True is begin Output := Input + 1; end Prot_Entry; procedure Prot_Proc (Input : Natural; Output : out Natural) with Refined_Post => Greater_Than (Refined_Post, Output, 3) is begin Output := Input + 1; end Prot_Proc; function Prot_Func (Input : Natural) return Natural with Refined_Post => Greater_Than (Refined_Post, Prot_Func'Result, 3) is begin return Input + 1; end Prot_Func; end Prot_Typ; task body Tsk_Typ is begin select accept Tsk_Entry (Input : Natural; Output : out Natural) do Output := Input + 1; end Tsk_Entry; or terminate; end select; end Tsk_Typ; end Sync_Contracts; -- main.adb with Ada.Assertions; use Ada.Assertions; with Ada.Text_IO; use Ada.Text_IO; with Sync_Contracts; use Sync_Contracts; with Tracker; use Tracker; procedure Main is Result : Natural; begin -- NOTES: -- 1) Refined_Post does not work on entry bodies due to an implementation -- limitation. -- 2) The consequences of Contract_Cases are mutually exclusive, only one -- should fail at any one time. declare P : Prot_Typ; begin -- Protected preconditions Put_Line ("Test 1"); Reset; begin P.Prot_Entry (1, Result); Put_Line ("ERROR: Test 1: did not fail"); exception when Assertion_Error => Verify ((True, False, False, False, False)); when others => Put_Line ("ERROR: Test 1: unexpected error"); end; Put_Line ("Test 2"); Reset; begin P.Prot_Proc (1, Result); Put_Line ("ERROR: Test 2: did not fail"); exception when Assertion_Error => Verify ((True, False, False, False, False)); when others => Put_Line ("ERROR: Test 2: unexpected error"); end; Put_Line ("Test 3"); Reset; begin Result := P.Prot_Func (1); Put_Line ("ERROR: Test 3: did not fail"); exception when Assertion_Error => Verify ((True, False, False, False, False)); when others => Put_Line ("ERROR: Test 3: unexpected error"); end; -- Protected refined postconditions Put_Line ("Test 4"); Reset; begin P.Prot_Entry (2, Result); Put_Line ("ERROR: Test 4: did not fail"); exception when Assertion_Error => Verify ((True, False, True, False, False)); when others => Put_Line ("ERROR: Test 4: unexpected error"); end; Put_Line ("Test 5"); Reset; begin P.Prot_Proc (2, Result); Put_Line ("ERROR: Test 5: did not fail"); exception when Assertion_Error => Verify ((True, True, False, False, False)); when others => Put_Line ("ERROR: Test 5: unexpected error"); end; Put_Line ("Test 6"); Reset; begin Result := P.Prot_Func (2); Put_Line ("ERROR: Test 6: did not fail"); exception when Assertion_Error => Verify ((True, True, False, False, False)); when others => Put_Line ("ERROR: Test 6: unexpected error"); end; -- Protected postconditions Put_Line ("Test 7"); Reset; begin P.Prot_Entry (3, Result); Put_Line ("ERROR: Test 7: did not fail"); exception when Assertion_Error => Verify ((True, False, True, False, False)); when others => Put_Line ("ERROR: Test 7: unexpected error"); end; Put_Line ("Test 8"); Reset; begin P.Prot_Proc (3, Result); Put_Line ("ERROR: Test 8: did not fail"); exception when Assertion_Error => Verify ((True, True, True, False, False)); when others => Put_Line ("ERROR: Test 8: unexpected error"); end; Put_Line ("Test 9"); Reset; begin Result := P.Prot_Func (3); Put_Line ("ERROR: Test 9: did not fail"); exception when Assertion_Error => Verify ((True, True, True, False, False)); when others => Put_Line ("ERROR: Test 9: unexpected error"); end; -- Protected contract cases Put_Line ("Test 10"); Reset; begin P.Prot_Entry (5, Result); Put_Line ("ERROR: Test 10: did not fail"); exception when Assertion_Error => Verify ((True, False, True, True, False)); when others => Put_Line ("ERROR: Test 10: unexpected error"); end; Put_Line ("Test 11"); Reset; begin P.Prot_Entry (6, Result); Put_Line ("ERROR: Test 11: did not fail"); exception when Assertion_Error => Verify ((True, False, True, False, True)); when others => Put_Line ("ERROR: Test 11: unexpected error"); end; Put_Line ("Test 12"); Reset; begin P.Prot_Proc (5, Result); Put_Line ("ERROR: Test 12: did not fail"); exception when Assertion_Error => Verify ((True, True, True, True, False)); when others => Put_Line ("ERROR: Test 12: unexpected error"); end; -- NOTE: Put_Line ("Test 13"); Reset; begin P.Prot_Proc (6, Result); Put_Line ("ERROR: Test 13: did not fail"); exception when Assertion_Error => Verify ((True, True, True, False, True)); when others => Put_Line ("ERROR: Test 13: unexpected error"); end; Put_Line ("Test 14"); Reset; begin Result := P.Prot_Func (5); Put_Line ("ERROR: Test 14: did not fail"); exception when Assertion_Error => Verify ((True, True, True, True, False)); when others => Put_Line ("ERROR: Test 14: unexpected error"); end; Put_Line ("Test 15"); Reset; begin Result := P.Prot_Func (6); Put_Line ("ERROR: Test 15: did not fail"); exception when Assertion_Error => Verify ((True, True, True, False, True)); when others => Put_Line ("ERROR: Test 15: unexpected error"); end; end; -- Task entry precondition Put_Line ("Test 16"); Reset; declare T : Tsk_Typ; begin T.Tsk_Entry (1, Result); Put_Line ("ERROR: Test 16: did not fail"); exception when Assertion_Error => Verify ((True, False, False, False, False)); when others => Put_Line ("ERROR: Test 16: unexpected error"); end; -- Task entry postcondition Put_Line ("Test 17"); Reset; declare T : Tsk_Typ; begin T.Tsk_Entry (3, Result); Put_Line ("ERROR: Test 17: did not fail"); exception when Assertion_Error => Verify ((True, False, True, False, False)); when others => Put_Line ("ERROR: Test 17: unexpected error"); end; -- Task contract cases Put_Line ("Test 18"); Reset; declare T : Tsk_Typ; begin T.Tsk_Entry (5, Result); Put_Line ("ERROR: Test 18: did not fail"); exception when Assertion_Error => Verify ((True, False, True, True, False)); when others => Put_Line ("ERROR: Test 18: unexpected error"); end; Put_Line ("Test 19"); Reset; declare T : Tsk_Typ; begin T.Tsk_Entry (6, Result); Put_Line ("ERROR: Test 19: did not fail"); exception when Assertion_Error => Verify ((True, False, True, False, True)); when others => Put_Line ("ERROR: Test 19: unexpected error"); end; end Main; ---------------------------- -- Compilation and output -- ---------------------------- $ gnatmake -q -gnata main.adb $ ./main Test 1 Test 2 Test 3 Test 4 Test 5 Test 6 Test 7 Test 8 Test 9 Test 10 Test 11 Test 12 Test 13 Test 14 Test 15 Test 16 Test 17 Test 18 Test 19 Tested on x86_64-pc-linux-gnu, committed on trunk 2015-11-12 Hristian Kirtchev <kirtchev@adacore.com> * contracts.adb (Analyze_Entry_Or_Subprogram_Body_Contract): Remove the guard concerning entry bodies as it is spurious. (Analyze_Entry_Or_Subprogram_Contract): Skip the analysis of Contract_Cases when not annotating the tree. * einfo.adb Node25 is now used as Contract_Wrapper. (Contract_Wrapper): New routine. (PPC_Wrapper): Removed. (Set_Contract_Wrapper): New routine. (Set_PPC_Wrapper): Removed. (Write_Field25_Name): Add output for Contract_Wrapper. Remove output for PPC_Wrapper. * einfo.ads New attribute Contract_Wrapper along with usage in entities. Remove attribute PPC_Wrapper along with usage in nodes. (Contract_Wrapper): New routine along with pragma Inline. (PPC_Wrapper): Removed along with pragma Inline. (Set_Contract_Wrapper): New routine along with pragma Inline. (Set_PPC_Wrapper): Removed along with pragma Inline. * exp_ch9.adb (Build_Contract_Wrapper): New routine. (Build_PPC_Wrapper): Removed. (Build_Protected_Entry): Code cleanup. (Expand_Entry_Declaration): Create a contract wrapper which now verifies Contract_Cases along with pre/postconditions. (Expand_N_Task_Type_Declaration): There is no need to check whether an entry has pre/postconditions as this is now done in Build_Contract_Wrapper. * sem_ch13.adb (Analyze_Aspect_Specifications): Pragma Refined_Post is now properly inserted in entry bodies. (Insert_Pragma): Add circuitry to insert in an entry body. Redo the instance "header" circuitry. Remove the now obsolete special case of inserting pre- conditions. * sem_prag.adb (Analyze_Pragma): Pragma Contract_Cases now applies to entries. * sem_res.adb (Resolve_Entry_Call): Update the calls to PPC_Wrapper.
Attachment:
difs
Description: Text document
Index Nav: | [Date Index] [Subject Index] [Author Index] [Thread Index] | |
---|---|---|
Message Nav: | [Date Prev] [Date Next] | [Thread Prev] [Thread Next] |