From 13da19e870555eea85eb166589fdaf469cc1f2ed Mon Sep 17 00:00:00 2001 From: yoogx Date: Sat, 16 May 2015 13:04:41 +0200 Subject: [PATCH] * Update reference output --- examples/petri_net/robot/robot.aadl.out | 6 +- examples/real/resources/all.aadl.out | 1 - examples/real/safety/model.aadl.out | 28 +- examples/real/security/all.aadl.out | 468 +++++++++++++++++++++++- tests/github/issue_10/test.aadl.out | 3 +- tests/github/issue_10/test2.aadl.out | 3 +- tests/real_units/validation.aadl.out | 60 ++- 7 files changed, 556 insertions(+), 13 deletions(-) diff --git a/examples/petri_net/robot/robot.aadl.out b/examples/petri_net/robot/robot.aadl.out index 54eeb4e3..e2168801 100644 --- a/examples/petri_net/robot/robot.aadl.out +++ b/examples/petri_net/robot/robot.aadl.out @@ -1,2 +1,4 @@ -taste_properties.aadl:19:08: (record type element) points to Supported_Source_Language (property definition declaration) , which is not a property type -Cannot analyze AADL specifications +robot.aadl:170:05: warning: CPU1 references a component type +ocarina: Total: 0 error and 1 warning +robot.aadl:170:05: warning: CPU1 references a component type +ocarina: Total: 0 error and 1 warning diff --git a/examples/real/resources/all.aadl.out b/examples/real/resources/all.aadl.out index 9591a878..06b10cc2 100644 --- a/examples/real/resources/all.aadl.out +++ b/examples/real/resources/all.aadl.out @@ -1,4 +1,3 @@ -taste_properties.aadl:19:08: (record type element) points to Supported_Source_Language (property definition declaration) , which is not a property type all.aadl:11:03: Criticity (property definition declaration) does not point to anything all.aadl:18:03: Actual_Subprogram_Type (property definition declaration) does not point to anything Cannot analyze AADL specifications diff --git a/examples/real/safety/model.aadl.out b/examples/real/safety/model.aadl.out index 54eeb4e3..b95e2e0a 100644 --- a/examples/real/safety/model.aadl.out +++ b/examples/real/safety/model.aadl.out @@ -1,2 +1,26 @@ -taste_properties.aadl:19:08: (record type element) points to Supported_Source_Language (property definition declaration) , which is not a property type -Cannot analyze AADL specifications +model.aadl:85:04: Warning: source_language is not a list while the corresponding property name at programming_properties.aadl:61:02 is a list. +model.aadl:85:04: Warning: The value of source_language has been converted into a list. +model.aadl:92:04: Warning: source_language is not a list while the corresponding property name at programming_properties.aadl:61:02 is a list. +model.aadl:92:04: Warning: The value of source_language has been converted into a list. +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 +Processing 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 ("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 for theorem pok_safety diff --git a/examples/real/security/all.aadl.out b/examples/real/security/all.aadl.out index 54eeb4e3..8d0259ec 100644 --- a/examples/real/security/all.aadl.out +++ b/examples/real/security/all.aadl.out @@ -1,2 +1,466 @@ -taste_properties.aadl:19:08: (record type element) points to Supported_Source_Language (property definition declaration) , which is not a property type -Cannot analyze AADL specifications +all.aadl:195:07: warning: layer_topsecret references a component type +all.aadl:196:07: warning: layer_secret references a component type +all.aadl:197:07: warning: layer_unclassified references a component type +all.aadl:195:07: warning: layer_topsecret references a component type +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 +Processing 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 + +Processing 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 + main.i_rtbus_layer_topsecret: 727 component instance all.aadl:15:04 +Content of set p_dest (lib.real:31:17) is + main.i_node2_partition_topsecret: 416 component instance all.aadl:138:04 +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 + main.i_rtbus_layer_secret: 735 component instance all.aadl:10:04 +Content of set p_dest (lib.real:31:17) is + main.i_node2_partition_secret: 483 component instance all.aadl:138:04 +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 + main.i_rtbus_layer_unclassified: 743 component instance all.aadl:5:04 +Content of set p_dest (lib.real:31:17) is + main.i_node2_partition_unclassified: 547 component instance all.aadl:138:04 +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 + main.i_rtbus_layer_topsecret: 727 component instance all.aadl:15:04 +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 + main.i_rtbus_layer_secret: 735 component instance all.aadl:10:04 +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 + main.i_rtbus_layer_unclassified: 743 component instance all.aadl:5:04 +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 + +Processing 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 + main.i_rtbus_layer_topsecret: 727 component instance all.aadl:15:04 +Content of set p_dest (lib.real:55:17) is + main.i_node2_partition_topsecret: 416 component instance all.aadl:138:04 +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 + main.i_rtbus_layer_secret: 735 component instance all.aadl:10:04 +Content of set p_dest (lib.real:55:17) is + main.i_node2_partition_secret: 483 component instance all.aadl:138:04 +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 + main.i_rtbus_layer_unclassified: 743 component instance all.aadl:5:04 +Content of set p_dest (lib.real:55:17) is + main.i_node2_partition_unclassified: 547 component instance all.aadl:138:04 +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 + main.i_rtbus_layer_topsecret: 727 component instance all.aadl:15:04 +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 + main.i_rtbus_layer_secret: 735 component instance all.aadl:10:04 +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 + main.i_rtbus_layer_unclassified: 743 component instance all.aadl:5:04 +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 + +Processing 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 + main.i_rtbus_layer_topsecret: 727 component instance all.aadl:15:04 +Content of set p_dest (lib.real:77:17) is + main.i_node2_partition_topsecret: 416 component instance all.aadl:138:04 +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 + main.i_rtbus_layer_secret: 735 component instance all.aadl:10:04 +Content of set p_dest (lib.real:77:17) is + main.i_node2_partition_secret: 483 component instance all.aadl:138:04 +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 + main.i_rtbus_layer_unclassified: 743 component instance all.aadl:5:04 +Content of set p_dest (lib.real:77:17) is + main.i_node2_partition_unclassified: 547 component instance all.aadl:138:04 +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 + main.i_rtbus_layer_topsecret: 727 component instance all.aadl:15:04 +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 + main.i_rtbus_layer_secret: 735 component instance all.aadl:10:04 +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 + main.i_rtbus_layer_unclassified: 743 component instance all.aadl:5:04 +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 + +Processing 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 + main.i_rtbus_layer_topsecret: 727 component instance all.aadl:15:04 +Content of set cnx (lib.real:102:14) is +Content of set p_dest (lib.real:104:17) is +Content of set vp2 (lib.real:106:14) is +Content of set b_dst (lib.real:108:16) is +Content of set b_cnx (lib.real:110:16) is +lib.real:117:20 Backends: warning : cardinal of set b_dst is null +lib.real:117:15 Backends: warning : unknown value, use default value of 0.0 for operator Min +lib.real:118:20 Backends: warning : cardinal of set b_cnx is null +lib.real:117:62 Backends: warning : unknown value, use default value of 0.0 for operator Min +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 + main.i_rtbus_layer_secret: 735 component instance all.aadl:10:04 +Content of set cnx (lib.real:102:14) is +Content of set p_dest (lib.real:104:17) is +Content of set vp2 (lib.real:106:14) is +Content of set b_dst (lib.real:108:16) is +Content of set b_cnx (lib.real:110:16) is +lib.real:117:20 Backends: warning : cardinal of set b_dst is null +lib.real:117:15 Backends: warning : unknown value, use default value of 0.0 for operator Min +lib.real:118:20 Backends: warning : cardinal of set b_cnx is null +lib.real:117:62 Backends: warning : unknown value, use default value of 0.0 for operator Min +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 + main.i_rtbus_layer_unclassified: 743 component instance all.aadl:5:04 +Content of set cnx (lib.real:102:14) is +Content of set p_dest (lib.real:104:17) is +Content of set vp2 (lib.real:106:14) is +Content of set b_dst (lib.real:108:16) is +Content of set b_cnx (lib.real:110:16) is +lib.real:117:20 Backends: warning : cardinal of set b_dst is null +lib.real:117:15 Backends: warning : unknown value, use default value of 0.0 for operator Min +lib.real:118:20 Backends: warning : cardinal of set b_cnx is null +lib.real:117:62 Backends: warning : unknown value, use default value of 0.0 for operator Min +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 + main.i_rtbus_layer_topsecret: 727 component instance all.aadl:15:04 +Content of set cnx (lib.real:102:14) is +Content of set p_dest (lib.real:104:17) is +Content of set vp2 (lib.real:106:14) is +Content of set b_dst (lib.real:108:16) is +Content of set b_cnx (lib.real:110:16) is +lib.real:117:20 Backends: warning : cardinal of set b_dst is null +lib.real:117:15 Backends: warning : unknown value, use default value of 0.0 for operator Min +lib.real:118:20 Backends: warning : cardinal of set b_cnx is null +lib.real:117:62 Backends: warning : unknown value, use default value of 0.0 for operator Min +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 + main.i_rtbus_layer_secret: 735 component instance all.aadl:10:04 +Content of set cnx (lib.real:102:14) is +Content of set p_dest (lib.real:104:17) is +Content of set vp2 (lib.real:106:14) is +Content of set b_dst (lib.real:108:16) is +Content of set b_cnx (lib.real:110:16) is +lib.real:117:20 Backends: warning : cardinal of set b_dst is null +lib.real:117:15 Backends: warning : unknown value, use default value of 0.0 for operator Min +lib.real:118:20 Backends: warning : cardinal of set b_cnx is null +lib.real:117:62 Backends: warning : unknown value, use default value of 0.0 for operator Min +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 + main.i_rtbus_layer_unclassified: 743 component instance all.aadl:5:04 +Content of set cnx (lib.real:102:14) is +Content of set p_dest (lib.real:104:17) is +Content of set vp2 (lib.real:106:14) is +Content of set b_dst (lib.real:108:16) is +Content of set b_cnx (lib.real:110:16) is +lib.real:117:20 Backends: warning : cardinal of set b_dst is null +lib.real:117:15 Backends: warning : unknown value, use default value of 0.0 for operator Min +lib.real:118:20 Backends: warning : cardinal of set b_cnx is null +lib.real:117:62 Backends: warning : unknown value, use default value of 0.0 for operator Min +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 + +Processing 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/tests/github/issue_10/test.aadl.out b/tests/github/issue_10/test.aadl.out index 54eeb4e3..a8e4d279 100644 --- a/tests/github/issue_10/test.aadl.out +++ b/tests/github/issue_10/test.aadl.out @@ -1,2 +1 @@ -taste_properties.aadl:19:08: (record type element) points to Supported_Source_Language (property definition declaration) , which is not a property type -Cannot analyze AADL specifications +Backends: fatal error : Petri Net backend : incomplete AADL model diff --git a/tests/github/issue_10/test2.aadl.out b/tests/github/issue_10/test2.aadl.out index 54eeb4e3..ca50eee2 100644 --- a/tests/github/issue_10/test2.aadl.out +++ b/tests/github/issue_10/test2.aadl.out @@ -1,2 +1 @@ -taste_properties.aadl:19:08: (record type element) points to Supported_Source_Language (property definition declaration) , which is not a property type -Cannot analyze AADL specifications +test2.aadl:24:09 Backends: fatal error : This IN port is not connected to any destination diff --git a/tests/real_units/validation.aadl.out b/tests/real_units/validation.aadl.out index 54eeb4e3..1776a5f7 100644 --- a/tests/real_units/validation.aadl.out +++ b/tests/real_units/validation.aadl.out @@ -1,2 +1,58 @@ -taste_properties.aadl:19:08: (record type element) points to Supported_Source_Language (property definition declaration) , which is not a property type -Cannot analyze AADL specifications +validation.aadl:13:03: Warning: source_language is not a list while the corresponding property name at programming_properties.aadl:61:02 is a list. +validation.aadl:13:03: Warning: The value of source_language has been converted into a list. +validation.aadl:20:03: Warning: source_language is not a list while the corresponding property name at programming_properties.aadl:61:02 is a list. +validation.aadl:20:03: Warning: The value of source_language has been converted into a list. +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 + + -- GitLab