From 89c4cd447367b59c6be828528bd25b278e35857d Mon Sep 17 00:00:00 2001 From: jhugues Date: Mon, 2 Jan 2012 18:17:02 +0000 Subject: [PATCH] * 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 --- examples/real/safety/model.aadl.out | 11 +- examples/real/security/all.aadl.out | 139 ++++++++++++++++ src/backends/ocarina-backends-real.adb | 33 ++-- src/core/model/ocarina-analyzer-real.adb | 3 +- src/core/model/ocarina-analyzer-real.ads | 4 + src/core/tree/ocarina-real_values.adb | 23 ++- src/frontends/real/ocarina-fe_real-parser.adb | 8 +- src/frontends/real/ocarina-fe_real.adb | 2 + .../test_real_exec_env_01.aadl.out | 42 +++++ .../test_real_exec_01.aadl.out | 14 ++ .../test_real_exec_02.aadl.out | 153 ++++++++++++++++++ .../test_real_exec_03.aadl.out | 21 +++ .../test_real_exec_04.aadl.out | 77 ++++++++- .../test_real_exec_05.aadl.out | 110 ++++++++++++- tests/real_units/validation.aadl.out | 28 ++++ tests/test_ocarina_help/dummy.aadl.out | 1 + 16 files changed, 641 insertions(+), 28 deletions(-) diff --git a/examples/real/safety/model.aadl.out b/examples/real/safety/model.aadl.out index 246f40c4..177ed0e8 100644 --- a/examples/real/safety/model.aadl.out +++ b/examples/real/safety/model.aadl.out @@ -1,13 +1,20 @@ 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 diff --git a/examples/real/security/all.aadl.out b/examples/real/security/all.aadl.out index 3143f4d6..ce77f28e 100644 --- a/examples/real/security/all.aadl.out +++ b/examples/real/security/all.aadl.out @@ -7,58 +7,96 @@ 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 +------------------------------------- +Evaluating theorem one_security_level_by_memory + + * Iterate for variable: main.i_node1_memory Content of set p (lib.real:9:12) is Content of set vp (lib.real:11:13) is Content of set b (lib.real:13:12) is lib.real:15:23 Backends: warning : cardinal of set b is null lib.real:15:11 Backends: warning : use default boolean value of true for operator '=' + => Result: TRUE + + * Iterate for variable: main.i_node1_memory_topsecret Content of set p (lib.real:9:12) is Content of set vp (lib.real:11:13) is Content of set b (lib.real:13:12) is lib.real:15:23 Backends: warning : cardinal of set b is null lib.real:15:11 Backends: warning : use default boolean value of true for operator '=' + => Result: TRUE + + * Iterate for variable: main.i_node1_memory_secret Content of set p (lib.real:9:12) is Content of set vp (lib.real:11:13) is Content of set b (lib.real:13:12) is lib.real:15:23 Backends: warning : cardinal of set b is null lib.real:15:11 Backends: warning : use default boolean value of true for operator '=' + => Result: TRUE + + * Iterate for variable: main.i_node1_memory_unclassified Content of set p (lib.real:9:12) is Content of set vp (lib.real:11:13) is Content of set b (lib.real:13:12) is lib.real:15:23 Backends: warning : cardinal of set b is null lib.real:15:11 Backends: warning : use default boolean value of true for operator '=' + => Result: TRUE + + * Iterate for variable: main.i_node1_memory_driver Content of set p (lib.real:9:12) is Content of set vp (lib.real:11:13) is Content of set b (lib.real:13:12) is lib.real:15:23 Backends: warning : cardinal of set b is null lib.real:15:11 Backends: warning : use default boolean value of true for operator '=' + => Result: TRUE + + * Iterate for variable: main.i_node2_memory Content of set p (lib.real:9:12) is Content of set vp (lib.real:11:13) is Content of set b (lib.real:13:12) is lib.real:15:23 Backends: warning : cardinal of set b is null lib.real:15:11 Backends: warning : use default boolean value of true for operator '=' + => Result: TRUE + + * Iterate for variable: main.i_node2_memory_topsecret Content of set p (lib.real:9:12) is Content of set vp (lib.real:11:13) is Content of set b (lib.real:13:12) is lib.real:15:23 Backends: warning : cardinal of set b is null lib.real:15:11 Backends: warning : use default boolean value of true for operator '=' + => Result: TRUE + + * Iterate for variable: main.i_node2_memory_secret Content of set p (lib.real:9:12) is Content of set vp (lib.real:11:13) is Content of set b (lib.real:13:12) is lib.real:15:23 Backends: warning : cardinal of set b is null lib.real:15:11 Backends: warning : use default boolean value of true for operator '=' + => Result: TRUE + + * Iterate for variable: main.i_node2_memory_unclassified Content of set p (lib.real:9:12) is Content of set vp (lib.real:11:13) is Content of set b (lib.real:13:12) is lib.real:15:23 Backends: warning : cardinal of set b is null lib.real:15:11 Backends: warning : use default boolean value of true for operator '=' + => Result: TRUE + + * Iterate for variable: main.i_node2_memory_driver Content of set p (lib.real:9:12) is Content of set vp (lib.real:11:13) is Content of set b (lib.real:13:12) is lib.real:15:23 Backends: warning : cardinal of set b is null lib.real:15:11 Backends: warning : use default boolean value of true for operator '=' + => Result: TRUE + theorem one_security_level_by_memory is: TRUE + requirement : bell_lapadula +------------------------------------- +Evaluating theorem bell_lapadula + + * Iterate for variable: main.i_node1_partition_topsecret Content of set vp1 (lib.real:27:14) is main.i_node1_runtime_topsecret: 48 component instance all.aadl:156:04 Content of set b_src (lib.real:29:16) is @@ -69,6 +107,9 @@ Content of set vp2 (lib.real:33:14) is main.i_node2_runtime_topsecret: 139 component instance all.aadl:156:04 Content of set b_dst (lib.real:35:16) is main.i_rtbus_layer_topsecret: 727 component instance all.aadl:15:04 + => Result: TRUE + + * Iterate for variable: main.i_node1_partition_secret Content of set vp1 (lib.real:27:14) is main.i_node1_runtime_secret: 28 component instance all.aadl:156:04 Content of set b_src (lib.real:29:16) is @@ -79,6 +120,9 @@ Content of set vp2 (lib.real:33:14) is main.i_node2_runtime_secret: 124 component instance all.aadl:156:04 Content of set b_dst (lib.real:35:16) is main.i_rtbus_layer_secret: 735 component instance all.aadl:10:04 + => Result: TRUE + + * Iterate for variable: main.i_node1_partition_unclassified Content of set vp1 (lib.real:27:14) is main.i_node1_runtime_unclassified: 64 component instance all.aadl:156:04 Content of set b_src (lib.real:29:16) is @@ -89,6 +133,9 @@ Content of set vp2 (lib.real:33:14) is main.i_node2_runtime_unclassified: 154 component instance all.aadl:156:04 Content of set b_dst (lib.real:35:16) is main.i_rtbus_layer_unclassified: 743 component instance all.aadl:5:04 + => Result: TRUE + + * Iterate for variable: main.i_node2_partition_topsecret Content of set vp1 (lib.real:27:14) is main.i_node2_runtime_topsecret: 139 component instance all.aadl:156:04 Content of set b_src (lib.real:29:16) is @@ -96,6 +143,9 @@ Content of set b_src (lib.real:29:16) is Content of set p_dest (lib.real:31:17) is Content of set vp2 (lib.real:33:14) is Content of set b_dst (lib.real:35:16) is + => Result: TRUE + + * Iterate for variable: main.i_node2_partition_secret Content of set vp1 (lib.real:27:14) is main.i_node2_runtime_secret: 124 component instance all.aadl:156:04 Content of set b_src (lib.real:29:16) is @@ -103,6 +153,9 @@ Content of set b_src (lib.real:29:16) is Content of set p_dest (lib.real:31:17) is Content of set vp2 (lib.real:33:14) is Content of set b_dst (lib.real:35:16) is + => Result: TRUE + + * Iterate for variable: main.i_node2_partition_unclassified Content of set vp1 (lib.real:27:14) is main.i_node2_runtime_unclassified: 154 component instance all.aadl:156:04 Content of set b_src (lib.real:29:16) is @@ -110,8 +163,15 @@ Content of set b_src (lib.real:29:16) is Content of set p_dest (lib.real:31:17) is Content of set vp2 (lib.real:33:14) is Content of set b_dst (lib.real:35:16) is + => Result: TRUE + theorem bell_lapadula is: TRUE + requirement : biba +------------------------------------- +Evaluating theorem biba + + * Iterate for variable: main.i_node1_partition_topsecret Content of set vp1 (lib.real:51:14) is main.i_node1_runtime_topsecret: 48 component instance all.aadl:156:04 Content of set b_src (lib.real:53:16) is @@ -122,6 +182,9 @@ Content of set vp2 (lib.real:57:14) is main.i_node2_runtime_topsecret: 139 component instance all.aadl:156:04 Content of set b_dst (lib.real:59:16) is main.i_rtbus_layer_topsecret: 727 component instance all.aadl:15:04 + => Result: TRUE + + * Iterate for variable: main.i_node1_partition_secret Content of set vp1 (lib.real:51:14) is main.i_node1_runtime_secret: 28 component instance all.aadl:156:04 Content of set b_src (lib.real:53:16) is @@ -132,6 +195,9 @@ Content of set vp2 (lib.real:57:14) is main.i_node2_runtime_secret: 124 component instance all.aadl:156:04 Content of set b_dst (lib.real:59:16) is main.i_rtbus_layer_secret: 735 component instance all.aadl:10:04 + => Result: TRUE + + * Iterate for variable: main.i_node1_partition_unclassified Content of set vp1 (lib.real:51:14) is main.i_node1_runtime_unclassified: 64 component instance all.aadl:156:04 Content of set b_src (lib.real:53:16) is @@ -142,6 +208,9 @@ Content of set vp2 (lib.real:57:14) is main.i_node2_runtime_unclassified: 154 component instance all.aadl:156:04 Content of set b_dst (lib.real:59:16) is main.i_rtbus_layer_unclassified: 743 component instance all.aadl:5:04 + => Result: TRUE + + * Iterate for variable: main.i_node2_partition_topsecret Content of set vp1 (lib.real:51:14) is main.i_node2_runtime_topsecret: 139 component instance all.aadl:156:04 Content of set b_src (lib.real:53:16) is @@ -149,6 +218,9 @@ Content of set b_src (lib.real:53:16) is Content of set p_dest (lib.real:55:17) is Content of set vp2 (lib.real:57:14) is Content of set b_dst (lib.real:59:16) is + => Result: TRUE + + * Iterate for variable: main.i_node2_partition_secret Content of set vp1 (lib.real:51:14) is main.i_node2_runtime_secret: 124 component instance all.aadl:156:04 Content of set b_src (lib.real:53:16) is @@ -156,6 +228,9 @@ Content of set b_src (lib.real:53:16) is Content of set p_dest (lib.real:55:17) is Content of set vp2 (lib.real:57:14) is Content of set b_dst (lib.real:59:16) is + => Result: TRUE + + * Iterate for variable: main.i_node2_partition_unclassified Content of set vp1 (lib.real:51:14) is main.i_node2_runtime_unclassified: 154 component instance all.aadl:156:04 Content of set b_src (lib.real:53:16) is @@ -163,8 +238,15 @@ Content of set b_src (lib.real:53:16) is Content of set p_dest (lib.real:55:17) is Content of set vp2 (lib.real:57:14) is Content of set b_dst (lib.real:59:16) is + => Result: TRUE + theorem biba is: TRUE + requirement : mils_1 +------------------------------------- +Evaluating theorem mils_1 + + * Iterate for variable: main.i_node1_partition_topsecret Content of set vp1 (lib.real:73:14) is main.i_node1_runtime_topsecret: 48 component instance all.aadl:156:04 Content of set b_src (lib.real:75:16) is @@ -175,6 +257,9 @@ Content of set vp2 (lib.real:79:14) is main.i_node2_runtime_topsecret: 139 component instance all.aadl:156:04 Content of set b_dst (lib.real:81:16) is main.i_rtbus_layer_topsecret: 727 component instance all.aadl:15:04 + => Result: TRUE + + * Iterate for variable: main.i_node1_partition_secret Content of set vp1 (lib.real:73:14) is main.i_node1_runtime_secret: 28 component instance all.aadl:156:04 Content of set b_src (lib.real:75:16) is @@ -185,6 +270,9 @@ Content of set vp2 (lib.real:79:14) is main.i_node2_runtime_secret: 124 component instance all.aadl:156:04 Content of set b_dst (lib.real:81:16) is main.i_rtbus_layer_secret: 735 component instance all.aadl:10:04 + => Result: TRUE + + * Iterate for variable: main.i_node1_partition_unclassified Content of set vp1 (lib.real:73:14) is main.i_node1_runtime_unclassified: 64 component instance all.aadl:156:04 Content of set b_src (lib.real:75:16) is @@ -195,6 +283,9 @@ Content of set vp2 (lib.real:79:14) is main.i_node2_runtime_unclassified: 154 component instance all.aadl:156:04 Content of set b_dst (lib.real:81:16) is main.i_rtbus_layer_unclassified: 743 component instance all.aadl:5:04 + => Result: TRUE + + * Iterate for variable: main.i_node2_partition_topsecret Content of set vp1 (lib.real:73:14) is main.i_node2_runtime_topsecret: 139 component instance all.aadl:156:04 Content of set b_src (lib.real:75:16) is @@ -202,6 +293,9 @@ Content of set b_src (lib.real:75:16) is Content of set p_dest (lib.real:77:17) is Content of set vp2 (lib.real:79:14) is Content of set b_dst (lib.real:81:16) is + => Result: TRUE + + * Iterate for variable: main.i_node2_partition_secret Content of set vp1 (lib.real:73:14) is main.i_node2_runtime_secret: 124 component instance all.aadl:156:04 Content of set b_src (lib.real:75:16) is @@ -209,6 +303,9 @@ Content of set b_src (lib.real:75:16) is Content of set p_dest (lib.real:77:17) is Content of set vp2 (lib.real:79:14) is Content of set b_dst (lib.real:81:16) is + => Result: TRUE + + * Iterate for variable: main.i_node2_partition_unclassified Content of set vp1 (lib.real:73:14) is main.i_node2_runtime_unclassified: 154 component instance all.aadl:156:04 Content of set b_src (lib.real:75:16) is @@ -216,8 +313,15 @@ Content of set b_src (lib.real:75:16) is Content of set p_dest (lib.real:77:17) is Content of set vp2 (lib.real:79:14) is Content of set b_dst (lib.real:81:16) is + => Result: TRUE + theorem mils_1 is: TRUE + requirement : mils_2 +------------------------------------- +Evaluating theorem mils_2 + + * Iterate for variable: main.i_node1_partition_topsecret Content of set vp1 (lib.real:98:14) is main.i_node1_runtime_topsecret: 48 component instance all.aadl:156:04 Content of set b_src (lib.real:100:16) is @@ -235,6 +339,9 @@ lib.real:119:20 Backends: warning : cardinal of set b_dst is null lib.real:119:15 Backends: warning : use default float value of 0.0 for operator Max lib.real:120:20 Backends: warning : cardinal of set b_cnx is null lib.real:119:62 Backends: warning : use default float value of 0.0 for operator Max + => Result: TRUE + + * Iterate for variable: main.i_node1_partition_secret Content of set vp1 (lib.real:98:14) is main.i_node1_runtime_secret: 28 component instance all.aadl:156:04 Content of set b_src (lib.real:100:16) is @@ -252,6 +359,9 @@ lib.real:119:20 Backends: warning : cardinal of set b_dst is null lib.real:119:15 Backends: warning : use default float value of 0.0 for operator Max lib.real:120:20 Backends: warning : cardinal of set b_cnx is null lib.real:119:62 Backends: warning : use default float value of 0.0 for operator Max + => Result: TRUE + + * Iterate for variable: main.i_node1_partition_unclassified Content of set vp1 (lib.real:98:14) is main.i_node1_runtime_unclassified: 64 component instance all.aadl:156:04 Content of set b_src (lib.real:100:16) is @@ -269,6 +379,9 @@ lib.real:119:20 Backends: warning : cardinal of set b_dst is null lib.real:119:15 Backends: warning : use default float value of 0.0 for operator Max lib.real:120:20 Backends: warning : cardinal of set b_cnx is null lib.real:119:62 Backends: warning : use default float value of 0.0 for operator Max + => Result: TRUE + + * Iterate for variable: main.i_node2_partition_topsecret Content of set vp1 (lib.real:98:14) is main.i_node2_runtime_topsecret: 139 component instance all.aadl:156:04 Content of set b_src (lib.real:100:16) is @@ -286,6 +399,9 @@ lib.real:119:20 Backends: warning : cardinal of set b_dst is null lib.real:119:15 Backends: warning : use default float value of 0.0 for operator Max lib.real:120:20 Backends: warning : cardinal of set b_cnx is null lib.real:119:62 Backends: warning : use default float value of 0.0 for operator Max + => Result: TRUE + + * Iterate for variable: main.i_node2_partition_secret Content of set vp1 (lib.real:98:14) is main.i_node2_runtime_secret: 124 component instance all.aadl:156:04 Content of set b_src (lib.real:100:16) is @@ -303,6 +419,9 @@ lib.real:119:20 Backends: warning : cardinal of set b_dst is null lib.real:119:15 Backends: warning : use default float value of 0.0 for operator Max lib.real:120:20 Backends: warning : cardinal of set b_cnx is null lib.real:119:62 Backends: warning : use default float value of 0.0 for operator Max + => Result: TRUE + + * Iterate for variable: main.i_node2_partition_unclassified Content of set vp1 (lib.real:98:14) is main.i_node2_runtime_unclassified: 154 component instance all.aadl:156:04 Content of set b_src (lib.real:100:16) is @@ -320,8 +439,28 @@ lib.real:119:20 Backends: warning : cardinal of set b_dst is null lib.real:119:15 Backends: warning : use default float value of 0.0 for operator Max lib.real:120:20 Backends: warning : cardinal of set b_cnx is null lib.real:119:62 Backends: warning : use default float value of 0.0 for operator Max + => Result: TRUE + theorem mils_2 is: TRUE + requirement : scheduling_1 +------------------------------------- +Evaluating theorem scheduling_1 + + * Iterate for variable: main.i_node1 + => Result: TRUE + + * Iterate for variable: main.i_node2 + => Result: TRUE + theorem scheduling_1 is: TRUE + +------------------------------------- +Evaluating theorem pok_security + + * Iterate for variable: main.i + => Result: TRUE + theorem pok_security is: TRUE + diff --git a/src/backends/ocarina-backends-real.adb b/src/backends/ocarina-backends-real.adb index 1e4486a4..fbfbd80a 100644 --- a/src/backends/ocarina-backends-real.adb +++ b/src/backends/ocarina-backends-real.adb @@ -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 diff --git a/src/core/model/ocarina-analyzer-real.adb b/src/core/model/ocarina-analyzer-real.adb index ed3aac75..d9368902 100644 --- a/src/core/model/ocarina-analyzer-real.adb +++ b/src/core/model/ocarina-analyzer-real.adb @@ -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 diff --git a/src/core/model/ocarina-analyzer-real.ads b/src/core/model/ocarina-analyzer-real.ads index 8a0dd0b0..5724762f 100644 --- a/src/core/model/ocarina-analyzer-real.ads +++ b/src/core/model/ocarina-analyzer-real.ads @@ -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; diff --git a/src/core/tree/ocarina-real_values.adb b/src/core/tree/ocarina-real_values.adb index dc6a1929..07147076 100644 --- a/src/core/tree/ocarina-real_values.adb +++ b/src/core/tree/ocarina-real_values.adb @@ -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 ('-'); diff --git a/src/frontends/real/ocarina-fe_real-parser.adb b/src/frontends/real/ocarina-fe_real-parser.adb index e8310686..2194cec4 100644 --- a/src/frontends/real/ocarina-fe_real-parser.adb +++ b/src/frontends/real/ocarina-fe_real-parser.adb @@ -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; diff --git a/src/frontends/real/ocarina-fe_real.adb b/src/frontends/real/ocarina-fe_real.adb index e59eab2a..63f89088 100644 --- a/src/frontends/real/ocarina-fe_real.adb +++ b/src/frontends/real/ocarina-fe_real.adb @@ -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 Evaluate only theorem"); + Write_Line + (" -real_continue_eval Continue evaluation in case of failures"); end Usage; end Ocarina.FE_REAL; diff --git a/tests/real-annexes-execution-environment/test_real_exec_env_01.aadl.out b/tests/real-annexes-execution-environment/test_real_exec_env_01.aadl.out index 1c764baf..a91ca841 100644 --- a/tests/real-annexes-execution-environment/test_real_exec_env_01.aadl.out +++ b/tests/real-annexes-execution-environment/test_real_exec_env_01.aadl.out @@ -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 + diff --git a/tests/real-annexes-execution/test_real_exec_01.aadl.out b/tests/real-annexes-execution/test_real_exec_01.aadl.out index 676a41f9..89f6699d 100644 --- a/tests/real-annexes-execution/test_real_exec_01.aadl.out +++ b/tests/real-annexes-execution/test_real_exec_01.aadl.out @@ -1,6 +1,20 @@ 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 + diff --git a/tests/real-annexes-execution/test_real_exec_02.aadl.out b/tests/real-annexes-execution/test_real_exec_02.aadl.out index 36b178b2..60be209f 100644 --- a/tests/real-annexes-execution/test_real_exec_02.aadl.out +++ b/tests/real-annexes-execution/test_real_exec_02.aadl.out @@ -1,97 +1,226 @@ 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 + diff --git a/tests/real-annexes-execution/test_real_exec_03.aadl.out b/tests/real-annexes-execution/test_real_exec_03.aadl.out index 47675665..681bf30f 100644 --- a/tests/real-annexes-execution/test_real_exec_03.aadl.out +++ b/tests/real-annexes-execution/test_real_exec_03.aadl.out @@ -1,9 +1,30 @@ 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 + diff --git a/tests/real-annexes-execution/test_real_exec_04.aadl.out b/tests/real-annexes-execution/test_real_exec_04.aadl.out index bc2d00d1..62be6eee 100644 --- a/tests/real-annexes-execution/test_real_exec_04.aadl.out +++ b/tests/real-annexes-execution/test_real_exec_04.aadl.out @@ -1,48 +1,121 @@ 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 + + * Iterate for variable: rma.erc32 + -> value for var_list is (2, 4, 6) + => Result: TRUE + theorem check_expression_gcd is: TRUE + check_expression_gcd_var execution +------------------------------------- +Evaluating theorem check_expression_gcd_var + + * Iterate for variable: rma.erc32 -> value for v1 is 2 -> value for v2 is 4 -> value for v3 is 6 + => Result: TRUE + theorem check_expression_gcd_var is: TRUE + check_expression_non_null execution +------------------------------------- +Evaluating theorem check_expression_non_null + + * Iterate for variable: rma.erc32 -> value for v0 is 0 -> value for v1 is 42 + => Result: TRUE + theorem check_expression_non_null is: TRUE + check_is_in execution +------------------------------------- +Evaluating theorem check_is_in + + * Iterate for variable: rma.erc32_node_a Content of set set (test_real_exec_04.aadl:218:12) 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_is_in is: TRUE + diff --git a/tests/real-annexes-execution/test_real_exec_05.aadl.out b/tests/real-annexes-execution/test_real_exec_05.aadl.out index f7ff7e2b..8bcf5990 100644 --- a/tests/real-annexes-execution/test_real_exec_05.aadl.out +++ b/tests/real-annexes-execution/test_real_exec_05.aadl.out @@ -1,88 +1,186 @@ variables_basis execution +------------------------------------- +Evaluating theorem variables_basis + + * Iterate for variable: rma.erc32_cpu_rm -> value for bla is 2 + => Result: TRUE + theorem variables_basis is: TRUE + variables_with_expression execution +------------------------------------- +Evaluating theorem variables_with_expression + + * Iterate for variable: rma.erc32_cpu_rm -> value for bla is 3 + => Result: TRUE + theorem variables_with_expression is: TRUE + variables_dependant execution +------------------------------------- +Evaluating theorem variables_dependant + + * Iterate for variable: rma.erc32_cpu_rm -> value for x1 is 1 -> value for x2 is 3 + => Result: TRUE + theorem variables_dependant is: TRUE + variables_set_dependants execution +------------------------------------- +Evaluating theorem variables_set_dependants + + * Iterate for variable: rma.erc32_cpu_rm Content of set a_set (test_real_exec_05.aadl:125:12) is rma.erc32_node_a: 13 component instance test_real_exec_05.aadl:72:01 -> value for x2 is 3 + => Result: TRUE + theorem variables_set_dependants is: TRUE + variables_iterative_expressions execution +------------------------------------- +Evaluating theorem variables_iterative_expressions + + * Iterate for variable: rma.erc32_cpu_rm Content of set proc_set (test_real_exec_05.aadl:139:18) is rma.erc32_node_a: 13 component instance test_real_exec_05.aadl:72:01 Content of set threads (test_real_exec_05.aadl:141:14) is rma.erc32_node_a_task1: 20 component instance test_real_exec_05.aadl:27:01 rma.erc32_node_a_task2: 52 component instance test_real_exec_05.aadl:40:01 -> value for y is 6.0 + => Result: TRUE + theorem variables_iterative_expressions is: TRUE + variables_imbricated_iterative_expressions execution +------------------------------------- +Evaluating theorem variables_imbricated_iterative_expressions + + * Iterate for variable: rma.erc32_cpu_rm Content of set proc_set (test_real_exec_05.aadl:156:18) is rma.erc32_node_a: 13 component instance test_real_exec_05.aadl:72:01 Content of set threads (test_real_exec_05.aadl:158:14) is rma.erc32_node_a_task1: 20 component instance test_real_exec_05.aadl:27:01 rma.erc32_node_a_task2: 52 component instance test_real_exec_05.aadl:40:01 -> value for y is 4000000003.0 + => Result: TRUE + theorem variables_imbricated_iterative_expressions is: TRUE + variables_product_expression execution +------------------------------------- +Evaluating theorem variables_product_expression + + * Iterate for variable: rma.erc32_node_a Content of set new_set (test_real_exec_05.aadl:179:20) is rma.erc32_node_a_task1: 20 component instance test_real_exec_05.aadl:27:01 rma.erc32_node_a_task2: 52 component instance test_real_exec_05.aadl:40:01 -> value for x is 500000000000000000.0 + => Result: TRUE + theorem variables_product_expression is: TRUE + element_list_expression execution +------------------------------------- +Evaluating theorem element_list_expression + + * Iterate for variable: rma.erc32_node_a Content of set new_set (test_real_exec_05.aadl:192:18) is rma.erc32_node_a_task1: 20 component instance test_real_exec_05.aadl:27:01 rma.erc32_node_a_task2: 52 component instance test_real_exec_05.aadl:40:01 + => Result: TRUE + theorem element_list_expression is: TRUE + element_list_static_declaration execution +------------------------------------- +Evaluating theorem element_list_static_declaration + + * Iterate for variable: rma.erc32_node_a Content of set new_set (test_real_exec_05.aadl:203:18) is rma.erc32_node_a_task1: 20 component instance test_real_exec_05.aadl:27:01 rma.erc32_node_a_task2: 52 component instance test_real_exec_05.aadl:40:01 - -> value for period is Not implemented yet + -> value for period is (500000000000, 1000000000000, 2000000000000) + => Result: TRUE + theorem element_list_static_declaration is: TRUE + list_concat execution - -> value for lst1 is Not implemented yet - -> value for lst2 is Not implemented yet - -> value for lst3 is Not implemented yet +------------------------------------- +Evaluating theorem list_concat + + * Iterate for variable: rma.erc32_node_a + -> value for lst1 is ("test1", "test2") + -> value for lst2 is ("test3") + -> value for lst3 is ("test1", "test2", "test3") + => Result: TRUE + theorem list_concat is: TRUE + is_in_list_and_set_expression execution +------------------------------------- +Evaluating theorem is_in_list_and_set_expression + + * Iterate for variable: rma.erc32_node_a Content of set new_set (test_real_exec_05.aadl:229:18) is rma.erc32_node_a_task1: 20 component instance test_real_exec_05.aadl:27:01 rma.erc32_node_a_task2: 52 component instance test_real_exec_05.aadl:40:01 + => Result: TRUE + theorem is_in_list_and_set_expression is: TRUE + if_then_else_expression execution +------------------------------------- +Evaluating theorem if_then_else_expression + + * Iterate for variable: rma.erc32_node_a -> value for v1 is 1 -> value for v2 is 2 -> value for v3 is 0 + => Result: TRUE + theorem if_then_else_expression is: TRUE + test_head_and_queue execution +------------------------------------- +Evaluating theorem test_head_and_queue + + * Iterate for variable: rma.erc32 Content of set threads (test_real_exec_05.aadl:255:16) is rma.erc32_node_a_task1: 20 component instance test_real_exec_05.aadl:27:01 rma.erc32_node_a_task2: 52 component instance test_real_exec_05.aadl:40:01 - -> value for period_list is Not implemented yet - -> value for poped_list is Not implemented yet + -> value for period_list is (1000000000000, 500000000000) + -> value for poped_list is (500000000000) + => Result: TRUE + theorem test_head_and_queue is: TRUE + test_reference_property execution +------------------------------------- +Evaluating theorem test_reference_property + + * Iterate for variable: rma.erc32_cpu_rm Content of set set (test_real_exec_05.aadl:270:12) is rma.erc32_node_a: 13 component instance test_real_exec_05.aadl:72:01 + => Result: TRUE + theorem test_reference_property is: TRUE + diff --git a/tests/real_units/validation.aadl.out b/tests/real_units/validation.aadl.out index a8651bcc..e650800d 100644 --- a/tests/real_units/validation.aadl.out +++ b/tests/real_units/validation.aadl.out @@ -1,26 +1,54 @@ contains_memories execution +------------------------------------- +Evaluating theorem contains_memories + + * Iterate for variable: mysystem.local Content of set mainmem (validation.aadl:123:28) is mysystem.local_ram: 122 component instance validation.aadl:99:01 + => Result: TRUE + theorem contains_memories is: TRUE + check_memory_and_process_mem execution +------------------------------------- +Evaluating theorem check_memory_and_process_mem + + * Iterate for variable: mysystem.local_ram Content of set prs (validation.aadl:133:28) is mysystem.local_node: 13 component instance validation.aadl:87:01 validation.aadl:135:99 Backends: error : Property is false for instance 122 (mysystem.local_ram) + => Result: FALSE + theorem check_memory_and_process_mem is: FALSE + check_thread_and_process_mem execution +------------------------------------- +Evaluating theorem check_thread_and_process_mem + + * Iterate for variable: mysystem.local_node Content of set thrs (validation.aadl:144:28) is mysystem.local_node_p1: 20 component instance validation.aadl:32:01 mysystem.local_node_p2: 60 component instance validation.aadl:51:01 validation.aadl:151:16 Backends: error : Property is false for instance 13 (mysystem.local_node) + => Result: FALSE + theorem check_thread_and_process_mem is: FALSE + check_processor_compliance execution +------------------------------------- +Evaluating theorem check_processor_compliance + + * Iterate for variable: mysystem.local_cpu Content of set prs (validation.aadl:160:28) is mysystem.local_node: 13 component instance validation.aadl:87:01 Content of set thrs (validation.aadl:161:28) is mysystem.local_node_p1: 20 component instance validation.aadl:32:01 mysystem.local_node_p2: 60 component instance validation.aadl:51:01 + => Result: TRUE + theorem check_processor_compliance is: TRUE + diff --git a/tests/test_ocarina_help/dummy.aadl.out b/tests/test_ocarina_help/dummy.aadl.out index 41ef5c20..b7d3ddd8 100644 --- a/tests/test_ocarina_help/dummy.aadl.out +++ b/tests/test_ocarina_help/dummy.aadl.out @@ -35,6 +35,7 @@ Usage: -aadlv2 Use AADL v2 standard -real_lib Add a REAL file to be used as a theorem library by REAL annexes -real_theorem Evaluate only theorem + -real_continue_eval Continue evaluation in case of failures -g Generate code from the AADL instance tree Registered backends: arinc653_conf -- GitLab