Commit 89c4cd44 authored by jhugues's avatar jhugues

* Enhance the output of the REAL backend

	* Add new flag -real_continue_eval to continue evaluation of
	 theorems in case of failures



git-svn-id: https://tecsw.estec.esa.int/svn/taste/trunk/ocarina@3585 129961e7-ef38-4bb5-a8f7-c9a525a55882
parent e9e2838d
pok_safety execution
requirement : check_error_handling
-------------------------------------
Evaluating theorem check_error_handling
* Iterate for variable: node.impl_part1_thr1
Content of set prs (libsafety.real:6:15) is
node.impl_part1: 62 component instance model.aadl:40:01
Content of set vp (libsafety.real:8:14) is
node.impl_cpu_part1: 20 component instance model.aadl:16:01
Content of set cpu (libsafety.real:10:15) is
node.impl_cpu: 13 component instance model.aadl:22:01
-> value for errors is Not implemented yet
-> value for actual_errors is Not implemented yet
-> value for errors is ("module_config", "module_init", "module_scheduling", "partition_scheduling", "partition_config", "partition_handler", "partition_init", "deadline_miss", "application_error", "numeric_error", "illegal_request", "stack_overflow", "memory_violation", "hardware_fault", "power_fail")
-> value for actual_errors is ("module_config", "partition_init", "illegal_request")
libsafety.real:32:46 Backends: error : Property is false for instance 69 (node.impl_part1_thr1)
=> Result: FALSE
theorem check_error_handling is: FALSE
model.aadl:118:07 Backends: fatal error : requirements are not fulfilled
This diff is collapsed.
......@@ -35,6 +35,7 @@ with Namet;
with Output;
with Locations; use Locations;
with Ocarina.Analyzer.REAL;
with Ocarina.ME_REAL.REAL_Tree.Nodes;
with Ocarina.ME_REAL.REAL_Tree.Nutils;
with Ocarina.ME_REAL.REAL_Tree.Utils;
......@@ -285,11 +286,8 @@ package body Ocarina.Backends.REAL is
Dummy := Apply_To_All_Elements (R);
end Apply_To_All_Elements;
---------------------------
-- Apply_To_All_Elements --
---------------------------
function Apply_To_All_Elements (R : Node_Id) return Boolean is
use Ocarina.ME_AADL.AADL_Instances.Nutils;
pragma Assert (Kind (R) = K_Theorem);
Range_Set : constant Result_Set := Set_Array
......@@ -302,12 +300,23 @@ package body Ocarina.Backends.REAL is
(Range_Declaration (R))))))));
Success : Boolean := True;
begin
-- For each element of the global ("range") set,
-- we build the dependant sets and then
-- we check the verification expression
-- For each element of the global ("range") set, we build the
-- dependant sets and then we check the verification expression
Write_Line ("-------------------------------------");
Write_Line ("Evaluating theorem "
& Get_Name_String (Name (Identifier (R))));
Write_Line ("");
for J in 1 .. Cardinal (Range_Set) loop
Current_Range_Variable := Get (Range_Set, J);
begin
Write_Line (" * Iterate for variable: "
& Get_Name_String (Compute_Full_Name_Of_Instance
(Current_Range_Variable)));
exception
when others =>
null;
end;
Set_Var_Value
(Referenced_Var (Variable_Ref (Range_Declaration (R))),
New_Elem_Value (Current_Range_Variable));
......@@ -315,13 +324,14 @@ package body Ocarina.Backends.REAL is
if Success then
Success := Manage_Check_Expression (R);
end if;
Write_Line (" => Result: " & Success'Img);
Write_Line ("");
exit when not Success;
end loop;
Write_Line ("theorem " & Get_Name_String (Name (Identifier (R)))
& " is: "& Boolean'Image (Success));
Write_Line ("");
return Success;
end Apply_To_All_Elements;
......@@ -521,7 +531,8 @@ package body Ocarina.Backends.REAL is
Success := Apply_To_All_Elements (RNU.REAL_Root);
Clean_Runtime;
exit when not Success;
exit when (not Success)
and then (not Ocarina.Analyzer.REAL.Continue_Evaluation);
N := Next_Node (N);
end loop;
......@@ -1448,7 +1459,7 @@ package body Ocarina.Backends.REAL is
Success : Boolean;
begin
case (Code (E)) is
case Code (E) is
when FC_Is_Called_By =>
Extract_Parameters_Sets (E, R1, R2, Success);
if not Success then
......
......@@ -1464,8 +1464,7 @@ package body Ocarina.Analyzer.REAL is
end if;
when FC_Get_Property_Value =>
if Present (N) and then
Present (Next_Node (N)) then
if Present (N) and then Present (Next_Node (N)) then
declare
Is_Set : Boolean;
begin
......
......@@ -61,4 +61,8 @@ package Ocarina.Analyzer.REAL is
-- Name of the main theorem to be evaluated, by default evaluate
-- all theorems.
Continue_Evaluation : Boolean := False;
-- In case of a theorem evaluates to false, continue the
-- evaluation.
end Ocarina.Analyzer.REAL;
......@@ -157,8 +157,25 @@ package body Ocarina.REAL_Values is
end if;
when LT_List =>
-- XXX FIXME :
return "Not implemented yet";
declare
N : Node_Id;
Name : Name_Id;
begin
N := First_Node (Value.LVal);
if Present (N) then
Name := Get_String_Name ("(" & Image (Item_Val (N)));
N := Next_Node (N);
else
Name := Get_String_Name ("(");
end if;
while Present (N) loop
Name := Get_String_Name
(Get_Name_String (Name)
& ", " & Image (Item_Val (N)));
N := Next_Node (N);
end loop;
Add_Str_To_Name_Buffer (")");
end;
when LT_Range =>
if Value.RSign_Left then
......@@ -167,7 +184,7 @@ package body Ocarina.REAL_Values is
Add_Str_To_Name_Buffer
(Image (Value.RVal_Left, Value.RVBase, Value.RVExp));
Add_Str_To_Name_Buffer (" - ");
Add_Str_To_Name_Buffer (" .. ");
if Value.RSign_Right then
Set_Char_To_Name_Buffer ('-');
......
......@@ -702,7 +702,7 @@ package body Ocarina.FE_REAL.Parser is
begin
-- Read enough expressions to push as first expression a binary
-- operator with no right expressio
-- operator with no right expression
Expr := P_Expression_Part;
if No (Expr) then
......@@ -1936,7 +1936,7 @@ package body Ocarina.FE_REAL.Parser is
Initialize_Option_Scan;
loop
C := Getopt ("* real_lib: real_theorem:");
C := Getopt ("* real_lib: real_theorem: real_continue_eval");
case C is
when ASCII.NUL =>
exit;
......@@ -1950,6 +1950,10 @@ package body Ocarina.FE_REAL.Parser is
Main_Theorem := Get_String_Name (Parameter);
end if;
if Full_Switch = "real_continue_eval" then
Continue_Evaluation := True;
end if;
when others =>
null;
end case;
......
......@@ -70,6 +70,8 @@ package body Ocarina.FE_REAL is
Write_Line (" -real_lib Add a REAL file to be used as a theorem "&
"library by REAL annexes");
Write_Line (" -real_theorem <theorem> Evaluate only theorem");
Write_Line
(" -real_continue_eval Continue evaluation in case of failures");
end Usage;
end Ocarina.FE_REAL;
......@@ -2,44 +2,86 @@ lib.real:12:17: warning: Unable to determine actualy returned type.
lib.real:19:24: warning: Unable to determine actualy returned type.
lib.real:33:03: warning: Returned integer value will be cast to a float at runtime
test_env_subtheorem_call_no_parameter execution
-------------------------------------
Evaluating theorem test_env_subtheorem_call_no_parameter
* Iterate for variable: rma.erc32_cpu_rm
Evaluating x
value for x after evaluating sub_theorem_1 is 2.00000E+00
=> Result: TRUE
theorem test_env_subtheorem_call_no_parameter is: TRUE
test_env_subtheorem_call_one_parameter execution
-------------------------------------
Evaluating theorem test_env_subtheorem_call_one_parameter
* Iterate for variable: rma.erc32_cpu_rm
Evaluating x
value for x after evaluating sub_theorem_2 is 2.00000E+00
=> Result: TRUE
theorem test_env_subtheorem_call_one_parameter is: TRUE
test_env_subtheorem_call_multiple_parameters execution
-------------------------------------
Evaluating theorem test_env_subtheorem_call_multiple_parameters
* Iterate for variable: rma.erc32_cpu_rm
Content of set a_set (test_real_exec_env_01.aadl:102:12) is
rma.erc32_node_a: 13 component instance test_real_exec_env_01.aadl:72:01
-> value for y is 3
Evaluating x
value for x after evaluating sub_theorem_3 is 4.00000E+00
=> Result: TRUE
theorem test_env_subtheorem_call_multiple_parameters is: TRUE
test_env_subtheorem_call_with_domain execution
-------------------------------------
Evaluating theorem test_env_subtheorem_call_with_domain
* Iterate for variable: rma.erc32_node_a
Content of set a_set (test_real_exec_env_01.aadl:112:12) is
rma.erc32_node_a_task1: 20 component instance test_real_exec_env_01.aadl:27:01
rma.erc32_node_a_task2: 52 component instance test_real_exec_env_01.aadl:40:01
-> value for y is 1
Evaluating x
value for x after evaluating sub_theorem_4 is 1.00000E+09
=> Result: TRUE
theorem test_env_subtheorem_call_with_domain is: TRUE
test_env_subtheorem_call_global_variable execution
-------------------------------------
Evaluating theorem test_env_subtheorem_call_global_variable
* Iterate for variable: rma.erc32_cpu_rm
Content of set a_set (test_real_exec_env_01.aadl:122:12) is
rma.erc32_node_a: 13 component instance test_real_exec_env_01.aadl:72:01
-> value for y is 1
Evaluating x
value for x after evaluating sub_theorem_5 is 1.00000E+00
=> Result: TRUE
theorem test_env_subtheorem_call_global_variable is: TRUE
test_env_subtheorem_call_with_empty_domain execution
-------------------------------------
Evaluating theorem test_env_subtheorem_call_with_empty_domain
* Iterate for variable: rma.erc32_node_a
Content of set a_set (test_real_exec_env_01.aadl:133:12) is
Evaluating x
lib.real:38:01 Backends: warning : Empty range set, returned value is 0.0
value for x after evaluating sub_theorem_6 is 0.00000E+00
=> Result: TRUE
theorem test_env_subtheorem_call_with_empty_domain is: TRUE
integer_and_binaries_operators execution
-------------------------------------
Evaluating theorem integer_and_binaries_operators
* Iterate for variable: rma.erc32_cpu_rm
=> Result: TRUE
theorem integer_and_binaries_operators is: TRUE
modulo_operator execution
-------------------------------------
Evaluating theorem modulo_operator
* Iterate for variable: rma.erc32_cpu_rm
=> Result: TRUE
theorem modulo_operator is: TRUE
test_real_exec_02.aadl:81:04: warning: obj references a component type
ocarina: Total: 0 error and 1 warning
set_declaration_is_bound_to execution
-------------------------------------
Evaluating theorem set_declaration_is_bound_to
* Iterate for variable: rma.erc32_cpu_rm
Content of set proc_set (test_real_exec_02.aadl:148:19) is
rma.erc32_node_a: 13 component instance test_real_exec_02.aadl:130:01
=> Result: TRUE
theorem set_declaration_is_bound_to is: TRUE
set_declaration_is_connected_to execution
-------------------------------------
Evaluating theorem set_declaration_is_connected_to
* Iterate for variable: rma.erc32_node_a_task_1
Content of set cnx_set (test_real_exec_02.aadl:160:14) is
=> Result: TRUE
* Iterate for variable: rma.erc32_node_a_task_2
Content of set cnx_set (test_real_exec_02.aadl:160:14) is
rma.erc32_node_a_task_1: 20 component instance test_real_exec_02.aadl:44:01
=> Result: TRUE
* Iterate for variable: rma.erc32_node_a_task_12
Content of set cnx_set (test_real_exec_02.aadl:160:14) is
=> Result: TRUE
* Iterate for variable: rma.erc32_node_a_task_22
Content of set cnx_set (test_real_exec_02.aadl:160:14) is
rma.erc32_node_a_task_12: 142 component instance test_real_exec_02.aadl:59:01
=> Result: TRUE
theorem set_declaration_is_connected_to is: TRUE
set_declaration_is_subcomponent_of execution
-------------------------------------
Evaluating theorem set_declaration_is_subcomponent_of
* Iterate for variable: rma.erc32_node_a
Content of set threads (test_real_exec_02.aadl:172:14) is
rma.erc32_node_a_task_1: 20 component instance test_real_exec_02.aadl:44:01
rma.erc32_node_a_task_2: 80 component instance test_real_exec_02.aadl:79:01
rma.erc32_node_a_task_12: 142 component instance test_real_exec_02.aadl:59:01
rma.erc32_node_a_task_22: 194 component instance test_real_exec_02.aadl:96:01
=> Result: TRUE
theorem set_declaration_is_subcomponent_of is: TRUE
set_declaration_is_accessed_by execution
-------------------------------------
Evaluating theorem set_declaration_is_accessed_by
* Iterate for variable: rma.erc32_node_a_task_2_obj
Content of set accessors (test_real_exec_02.aadl:184:16) is
=> Result: TRUE
theorem set_declaration_is_accessed_by is: TRUE
set_declaration_is_accessing_to execution
-------------------------------------
Evaluating theorem set_declaration_is_accessing_to
* Iterate for variable: rma.erc32_node_a_task_2_obj
Content of set accessors (test_real_exec_02.aadl:196:16) is
=> Result: TRUE
theorem set_declaration_is_accessing_to is: TRUE
set_declaration_is_called_by_1 execution
-------------------------------------
Evaluating theorem set_declaration_is_called_by_1
* Iterate for variable: rma.erc32_node_a_task_1_mycalls_p_spg
Content of set callers (test_real_exec_02.aadl:211:19) is
rma.erc32_node_a_task_1: 20 component instance test_real_exec_02.aadl:44:01
=> Result: TRUE
* Iterate for variable: rma.erc32_node_a_task_2_mycall_p_spg
Content of set callers (test_real_exec_02.aadl:211:19) is
rma.erc32_node_a_task_2: 80 component instance test_real_exec_02.aadl:79:01
=> Result: TRUE
* Iterate for variable: rma.erc32_node_a_task_12_mycalls_p_spg
Content of set callers (test_real_exec_02.aadl:211:19) is
rma.erc32_node_a_task_12: 142 component instance test_real_exec_02.aadl:59:01
=> Result: TRUE
* Iterate for variable: rma.erc32_node_a_task_22_mycall_p_spg
Content of set callers (test_real_exec_02.aadl:211:19) is
rma.erc32_node_a_task_22: 194 component instance test_real_exec_02.aadl:96:01
=> Result: TRUE
theorem set_declaration_is_called_by_1 is: TRUE
set_declaration_is_called_by_2 execution
-------------------------------------
Evaluating theorem set_declaration_is_called_by_2
* Iterate for variable: test2_real_hello_spg_1
Content of set callers (test_real_exec_02.aadl:226:19) is
rma.erc32_node_a_task_1: 20 component instance test_real_exec_02.aadl:44:01
rma.erc32_node_a_task_12: 142 component instance test_real_exec_02.aadl:59:01
=> Result: TRUE
* Iterate for variable: test2_real_hello_spg_2
Content of set callers (test_real_exec_02.aadl:226:19) is
rma.erc32_node_a_task_2: 80 component instance test_real_exec_02.aadl:79:01
rma.erc32_node_a_task_22: 194 component instance test_real_exec_02.aadl:96:01
=> Result: TRUE
theorem set_declaration_is_called_by_2 is: TRUE
set_declaration_is_connecting_to execution
-------------------------------------
Evaluating theorem set_declaration_is_connecting_to
* Iterate for variable: rma.erc32_node_a_task_1
Content of set cnx_threads (test_real_exec_02.aadl:239:22) is
=> Result: TRUE
* Iterate for variable: rma.erc32_node_a_task_2
Content of set cnx_threads (test_real_exec_02.aadl:239:22) is
rma.erc32_node_a_task_1: 20 component instance test_real_exec_02.aadl:44:01
=> Result: TRUE
* Iterate for variable: rma.erc32_node_a_task_12
Content of set cnx_threads (test_real_exec_02.aadl:239:22) is
=> Result: TRUE
* Iterate for variable: rma.erc32_node_a_task_22
Content of set cnx_threads (test_real_exec_02.aadl:239:22) is
rma.erc32_node_a_task_12: 142 component instance test_real_exec_02.aadl:59:01
=> Result: TRUE
theorem set_declaration_is_connecting_to is: TRUE
set_declaration_is_passing_through execution
-------------------------------------
Evaluating theorem set_declaration_is_passing_through
* Iterate for variable: rma.erc32_node_a_task_1
Content of set accessor_flows (test_real_exec_02.aadl:251:21) is
anonymous end to end flow :3449 end to end flow spec
=> Result: TRUE
* Iterate for variable: rma.erc32_node_a_task_2
Content of set accessor_flows (test_real_exec_02.aadl:251:21) is
anonymous end to end flow :3449 end to end flow spec
=> Result: TRUE
* Iterate for variable: rma.erc32_node_a_task_12
Content of set accessor_flows (test_real_exec_02.aadl:251:21) is
anonymous end to end flow :3450 end to end flow spec
=> Result: TRUE
* Iterate for variable: rma.erc32_node_a_task_22
Content of set accessor_flows (test_real_exec_02.aadl:251:21) is
anonymous end to end flow :3450 end to end flow spec
=> Result: TRUE
theorem set_declaration_is_passing_through is: TRUE
set_declaration_is_predecessor_of execution
-------------------------------------
Evaluating theorem set_declaration_is_predecessor_of
* Iterate for variable: rma.erc32_node_a_task_1
Content of set pred (test_real_exec_02.aadl:264:13) is
Content of set inv_pred (test_real_exec_02.aadl:266:17) is
rma.erc32_node_a_task_2: 80 component instance test_real_exec_02.aadl:79:01
=> Result: TRUE
* Iterate for variable: rma.erc32_node_a_task_2
Content of set pred (test_real_exec_02.aadl:264:13) is
rma.erc32_node_a_task_1: 20 component instance test_real_exec_02.aadl:44:01
Content of set inv_pred (test_real_exec_02.aadl:266:17) is
=> Result: TRUE
* Iterate for variable: rma.erc32_node_a_task_12
Content of set pred (test_real_exec_02.aadl:264:13) is
Content of set inv_pred (test_real_exec_02.aadl:266:17) is
rma.erc32_node_a_task_22: 194 component instance test_real_exec_02.aadl:96:01
=> Result: TRUE
* Iterate for variable: rma.erc32_node_a_task_22
Content of set pred (test_real_exec_02.aadl:264:13) is
rma.erc32_node_a_task_12: 142 component instance test_real_exec_02.aadl:59:01
Content of set inv_pred (test_real_exec_02.aadl:266:17) is
=> Result: TRUE
theorem set_declaration_is_predecessor_of is: TRUE
set_declaration_compare_property_value execution
-------------------------------------
Evaluating theorem set_declaration_compare_property_value
* Iterate for variable: rma.erc32_cpu_rm
Content of set pure_subprograms (test_real_exec_02.aadl:280:24) is
test2_real_hello_spg_1: 41 component instance test_real_exec_02.aadl:19:01
test2_real_hello_spg_2: 103 component instance test_real_exec_02.aadl:27:01
=> Result: TRUE
theorem set_declaration_compare_property_value is: TRUE
set_declaration_set_composition execution
-------------------------------------
Evaluating theorem set_declaration_set_composition
* Iterate for variable: rma.erc32_cpu_rm
Content of set proc_set (test_real_exec_02.aadl:295:19) is
rma.erc32_node_a: 13 component instance test_real_exec_02.aadl:130:01
Content of set new_set (test_real_exec_02.aadl:297:15) is
......@@ -99,22 +228,46 @@ Content of set new_set (test_real_exec_02.aadl:297:15) is
rma.erc32_node_a_task_2: 80 component instance test_real_exec_02.aadl:79:01
rma.erc32_node_a_task_12: 142 component instance test_real_exec_02.aadl:59:01
rma.erc32_node_a_task_22: 194 component instance test_real_exec_02.aadl:96:01
=> Result: TRUE
theorem set_declaration_set_composition is: TRUE
set_declaration_and_operator execution
-------------------------------------
Evaluating theorem set_declaration_and_operator
* Iterate for variable: rma.erc32_node_a
Content of set protected_data (test_real_exec_02.aadl:309:21) is
rma.erc32_node_a_task_2_obj: 92 component instance test_real_exec_02.aadl:10:01
=> Result: TRUE
theorem set_declaration_and_operator is: TRUE
set_declaration_or_operator execution
-------------------------------------
Evaluating theorem set_declaration_or_operator
* Iterate for variable: rma.erc32_node_a
Content of set a_set (test_real_exec_02.aadl:325:14) is
rma.erc32_node_a_task_1: 20 component instance test_real_exec_02.aadl:44:01
rma.erc32_node_a_task_2: 80 component instance test_real_exec_02.aadl:79:01
rma.erc32_node_a_task_12: 142 component instance test_real_exec_02.aadl:59:01
rma.erc32_node_a_task_22: 194 component instance test_real_exec_02.aadl:96:01
=> Result: TRUE
theorem set_declaration_or_operator is: TRUE
set_declaration_predefined_sets execution
-------------------------------------
Evaluating theorem set_declaration_predefined_sets
* Iterate for variable: rma.erc32_cpu_rm
-> value for x is 4
=> Result: TRUE
theorem set_declaration_predefined_sets is: TRUE
type_issues_1 execution
-------------------------------------
Evaluating theorem type_issues_1
* Iterate for variable: rma.erc32_cpu_rm
=> Result: TRUE
theorem type_issues_1 is: TRUE
type_issues_2 execution
-------------------------------------
Evaluating theorem type_issues_2
* Iterate for variable: rma.erc32_cpu_rm
=> Result: TRUE
theorem type_issues_2 is: TRUE
type_issues_3 execution
-------------------------------------
Evaluating theorem type_issues_3
* Iterate for variable: rma.erc32_cpu_rm
=> Result: TRUE
theorem type_issues_3 is: TRUE
check_expression_max execution
-------------------------------------
Evaluating theorem check_expression_max
* Iterate for variable: rma.erc32_node_a
Content of set new_set (test_real_exec_04.aadl:86:18) is
rma.erc32_node_a_task1: 20 component instance test_real_exec_04.aadl:27:01
rma.erc32_node_a_task2: 52 component instance test_real_exec_04.aadl:40:01
=> Result: TRUE
theorem check_expression_max is: TRUE
check_expression_sum execution
-------------------------------------
Evaluating theorem check_expression_sum
* Iterate for variable: rma.erc32_node_a
Content of set new_set (test_real_exec_04.aadl:98:18) is
rma.erc32_node_a_task1: 20 component instance test_real_exec_04.aadl:27:01
rma.erc32_node_a_task2: 52 component instance test_real_exec_04.aadl:40:01
=> Result: TRUE
theorem check_expression_sum is: TRUE
check_expression_not execution
-------------------------------------
Evaluating theorem check_expression_not
* Iterate for variable: rma.erc32_cpu_rm
=> Result: TRUE
theorem check_expression_not is: TRUE
check_expression_complex execution
-------------------------------------
Evaluating theorem check_expression_complex
* Iterate for variable: rma.erc32_cpu_rm
Content of set test_set (test_real_exec_04.aadl:136:15) is
rma.erc32_node_a: 13 component instance test_real_exec_04.aadl:72:01
=> Result: TRUE
theorem check_expression_complex is: TRUE
check_expression_range execution
-------------------------------------
Evaluating theorem check_expression_range
* Iterate for variable: rma.erc32_node_a_task1
=> Result: TRUE
* Iterate for variable: rma.erc32_node_a_task2
=> Result: TRUE
theorem check_expression_range is: TRUE
check_expression_lcm execution
-> value for var_list is Not implemented yet
-------------------------------------
Evaluating theorem check_expression_lcm
* Iterate for variable: rma.erc32
-> value for var_list is (2, 4, 6)
=> Result: TRUE
theorem check_expression_lcm is: TRUE
check_expression_gcd execution
-> value for var_list is Not implemented yet
-------------------------------------
Evaluating theorem check_expression_gcd