diff --git a/examples/real/safety/model.aadl.out b/examples/real/safety/model.aadl.out index a91d796944abf38e9826929ed2cd851905ce0ffb..b95e2e0aff765d484ba281eef4e976cbcc5b5eca 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 ce77f28ee8840aaf20ae51a442456e5b700d0bce..8d0259ec104013ccd3f9350debdc0924448d9809 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 727dbdc35df720c0bd7d93a95ac2c38e473ce78c..9665dd21037fd75ba71a835fb3114c16dddd6c48 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 a9849bbb96a55d76dba99cfc4f9ed9b20e96ee76..8d6047bb6e1eeadfabecd73ad2f3cc12ee94b6e7 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 d2faae41f3cc602f50a4f28603ab87dfadead2c0..6710ced114002c6a9e71b73ae2fdbd440f10f27e 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 0bf8a3f16331babb6a28bbd0e2c98936261610b7..e5da446cab9f6dd7f052cd00c03a62ec43559dde 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