Commit 9843d9d8 authored by jhugues's avatar jhugues

* 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
parent fa81181d
......@@ -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
......
......@@ -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
......
......@@ -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);
......
......@@ -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
......
test_theorem execution
requirement : required_theorem
Processing requirement : required_theorem
-------------------------------------
Evaluating theorem required_theorem
......
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
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment