From 9843d9d84036ff8b055fe5b45a4917ac140d2718 Mon Sep 17 00:00:00 2001 From: jhugues Date: Tue, 25 Sep 2012 10:33:08 +0000 Subject: [PATCH] * When requirements are not met, the theorem should be flagged as wrong git-svn-id: https://tecsw.estec.esa.int/svn/taste/trunk/ocarina@5674 129961e7-ef38-4bb5-a8f7-c9a525a55882 --- examples/real/safety/model.aadl.out | 2 +- examples/real/security/all.aadl.out | 12 +++++----- src/backends/ocarina-backends-real.adb | 32 ++++++++++++++++++++------ tests/MANIFEST | 1 + tests/real_requires/test.aadl.out | 2 +- tests/real_requires_2/test.aadl.out | 8 +++---- 6 files changed, 38 insertions(+), 19 deletions(-) diff --git a/examples/real/safety/model.aadl.out b/examples/real/safety/model.aadl.out index a91d7969..b95e2e0a 100644 --- a/examples/real/safety/model.aadl.out +++ b/examples/real/safety/model.aadl.out @@ -5,7 +5,7 @@ model.aadl:92:04: Warning: The value of source_language has been converted into model.aadl:99:04: Warning: source_language is not a list while the corresponding property name at programming_properties.aadl:61:02 is a list. model.aadl:99:04: Warning: The value of source_language has been converted into a list. pok_safety execution -requirement : check_error_handling +Processing requirement : check_error_handling ------------------------------------- Evaluating theorem check_error_handling diff --git a/examples/real/security/all.aadl.out b/examples/real/security/all.aadl.out index ce77f28e..8d0259ec 100644 --- a/examples/real/security/all.aadl.out +++ b/examples/real/security/all.aadl.out @@ -6,7 +6,7 @@ all.aadl:196:07: warning: layer_secret references a component type all.aadl:197:07: warning: layer_unclassified references a component type ocarina: Total: 0 error and 6 warnings pok_security execution -requirement : one_security_level_by_memory +Processing requirement : one_security_level_by_memory ------------------------------------- Evaluating theorem one_security_level_by_memory @@ -92,7 +92,7 @@ lib.real:15:11 Backends: warning : use default boolean value of true for operato theorem one_security_level_by_memory is: TRUE -requirement : bell_lapadula +Processing requirement : bell_lapadula ------------------------------------- Evaluating theorem bell_lapadula @@ -167,7 +167,7 @@ Content of set b_dst (lib.real:35:16) is theorem bell_lapadula is: TRUE -requirement : biba +Processing requirement : biba ------------------------------------- Evaluating theorem biba @@ -242,7 +242,7 @@ Content of set b_dst (lib.real:59:16) is theorem biba is: TRUE -requirement : mils_1 +Processing requirement : mils_1 ------------------------------------- Evaluating theorem mils_1 @@ -317,7 +317,7 @@ Content of set b_dst (lib.real:81:16) is theorem mils_1 is: TRUE -requirement : mils_2 +Processing requirement : mils_2 ------------------------------------- Evaluating theorem mils_2 @@ -443,7 +443,7 @@ lib.real:119:62 Backends: warning : use default float value of 0.0 for operator theorem mils_2 is: TRUE -requirement : scheduling_1 +Processing requirement : scheduling_1 ------------------------------------- Evaluating theorem scheduling_1 diff --git a/src/backends/ocarina-backends-real.adb b/src/backends/ocarina-backends-real.adb index 727dbdc3..9665dd21 100644 --- a/src/backends/ocarina-backends-real.adb +++ b/src/backends/ocarina-backends-real.adb @@ -137,7 +137,8 @@ package body Ocarina.Backends.REAL is procedure Compute_Check_Subprogram_Call (E : Node_Id; T : out Return_Type; Result : out Value_Id); - function Apply_To_All_Elements (R : Node_Id) return Boolean; + function Apply_To_All_Elements + (R : Node_Id; Force_Result_To_False : Boolean := False) return Boolean; -- Test the theorem on all elements of the range set; -- return false if at least one of them fail @@ -291,7 +292,9 @@ package body Ocarina.Backends.REAL is Dummy := Apply_To_All_Elements (R); end Apply_To_All_Elements; - function Apply_To_All_Elements (R : Node_Id) return Boolean is + function Apply_To_All_Elements + (R : Node_Id; Force_Result_To_False : Boolean := False) return Boolean + is use Ocarina.ME_AADL.AADL_Instances.Nutils; pragma Assert (Kind (R) = K_Theorem); @@ -339,6 +342,10 @@ package body Ocarina.Backends.REAL is exit when not Success; end loop; + if Force_Result_To_False then + Success := False; + end if; + Write_Line ("theorem " & Get_Name_String (Name (Identifier (R))) & " is: "& Boolean'Image (Success)); Write_Line (""); @@ -517,29 +524,37 @@ package body Ocarina.Backends.REAL is Stored_Root : constant Node_Id := R; N : Node_Id; Success : Boolean := True; + Local_Success : Boolean; begin N := First_Node (Required_Theorems (R)); while Present (N) loop + Local_Success := True; RNU.REAL_Root := Related_Theorem (N); - Write_Line ("requirement : " & + Write_Line ("Processing requirement : " & Get_Name_String (Name (Identifier (RNU.REAL_Root)))); -- Requirements can also have requirements if not Check_Requirements (RNU.REAL_Root) then Display_Located_Error - (Loc (RNU.REAL_Root), "requirements are not fulfilled", + (Loc (RNU.REAL_Root), "requirements of " + & Get_Name_String (Name (Identifier (RNU.REAL_Root))) + &" are not fulfilled", Fatal => not Ocarina.Analyzer.REAL.Continue_Evaluation); - Success := False; + Local_Success := False; end if; -- Library theorems are already analyzed, so we proceed -- directly to execution Initialize_Sets_Table (RNU.REAL_Root); - Success := Apply_To_All_Elements (RNU.REAL_Root) and then Success; + + -- Note: if the requirements are not fulfilled, we flag the + -- theorem as wrong in all cases. + Success := Apply_To_All_Elements (RNU.REAL_Root, not Local_Success) + and then Success; Clean_Runtime; exit when (not Success) @@ -657,6 +672,7 @@ package body Ocarina.Backends.REAL is Ref : constant Node_Id := Referenced_Var (Var_Ref (E)); Local_Domain : constant Boolean := RNU.Is_Domain; Local_Domain_value : constant Result_Set := RNU.Domain; + Requirements_Checked : Boolean; begin Write_Line (" Evaluating " & Get_Name_String @@ -690,7 +706,9 @@ package body Ocarina.Backends.REAL is Clean_Runtime; REAL_Root := Related_Theorem (E); - if not Check_Requirements (RNU.REAL_Root) then + Requirements_Checked := Check_Requirements (RNU.REAL_Root); + + if not Requirements_Checked then Display_Located_Error (Loc (RNU.REAL_Root), "requirements are not fulfilled", Fatal => not Ocarina.Analyzer.REAL.Continue_Evaluation); diff --git a/tests/MANIFEST b/tests/MANIFEST index a9849bbb..8d6047bb 100644 --- a/tests/MANIFEST +++ b/tests/MANIFEST @@ -252,6 +252,7 @@ tests/real-annexes-execution-environment/test_real_exec_env_01.aadl tests/real_units/validation.aadl tests/real_requires/test.aadl tests/real_requires_2/test.aadl +tests/real_requires_3/test.aadl tests/ticket_46/test.aadl tests/ticket_48/test.aadl tests/package_annex/test.aadl diff --git a/tests/real_requires/test.aadl.out b/tests/real_requires/test.aadl.out index d2faae41..6710ced1 100644 --- a/tests/real_requires/test.aadl.out +++ b/tests/real_requires/test.aadl.out @@ -1,5 +1,5 @@ test_theorem execution -requirement : required_theorem +Processing requirement : required_theorem ------------------------------------- Evaluating theorem required_theorem diff --git a/tests/real_requires_2/test.aadl.out b/tests/real_requires_2/test.aadl.out index 0bf8a3f1..e5da446c 100644 --- a/tests/real_requires_2/test.aadl.out +++ b/tests/real_requires_2/test.aadl.out @@ -1,6 +1,6 @@ test execution -requirement : sub1 -requirement : sub2 +Processing requirement : sub1 +Processing requirement : sub2 ------------------------------------- Evaluating theorem sub2 @@ -10,14 +10,14 @@ theorems.real:9:10 Backends: error : Property is false for instance 6 (a.impl) theorem sub2 is: FALSE -theorems.real:1:01 Backends: error : requirements are not fulfilled +theorems.real:1:01 Backends: error : requirements of sub1 are not fulfilled ------------------------------------- Evaluating theorem sub1 * Iterate for variable: a.impl => Result: TRUE -theorem sub1 is: TRUE +theorem sub1 is: FALSE test.aadl:8:05 Backends: error : requirements are not fulfilled for theorem test -- GitLab