Commit 78b0160b authored by yoogx's avatar yoogx
Browse files

* Update reference output, to be later checked when issue #17

          is solved
parent a5ceddeb
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
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
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
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
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
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
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
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
......@@ -151,22 +151,22 @@ 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 :3884 end to end flow spec
anonymous end to end flow :3964 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 :3884 end to end flow spec
anonymous end to end flow :3964 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 :3885 end to end flow spec
anonymous end to end flow :3965 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 :3885 end to end flow spec
anonymous end to end flow :3965 end to end flow spec
=> Result: TRUE
theorem set_declaration_is_passing_through is: TRUE
......
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
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
......@@ -16,7 +16,6 @@ Usage:
-er Execute the generated application code and
verify that there is no regression
-p Only parse and instantiate the application model
-c Only perform schedulability analysis
Advanced user options:
-d Debug mode for developpers
......
......@@ -3227,16 +3227,16 @@ Declarations List_Id 7
Backend_Node Node_Id 0
Entity Node_Id 1838
Property_Set_Identifier Node_Id 0
Expanded_Type_Designator Node_Id 2519
2519 range type timing_properties.aadl:9:19
Number_Type Node_Id 2520
2520 integer type timing_properties.aadl:7:13
Type_Range Node_Id 2521
2521 number range timing_properties.aadl:7:25
Lower_Bound Node_Id 2522
2522 signed aadlnumber timing_properties.aadl:7:25
Number_Value Node_Id 2523
2523 literal timing_properties.aadl:7:25
Expanded_Type_Designator Node_Id 2529
2529 range type timing_properties.aadl:9:19
Number_Type Node_Id 2530
2530 integer type timing_properties.aadl:7:13
Type_Range Node_Id 2531
2531 number range timing_properties.aadl:7:25