Commit 04192a21 authored by hugues.jerome's avatar hugues.jerome
Browse files

* Various updates for REAL: add Abstract_Set as additional

          pre-defined set, add support for properties that refer to
          classifier, add debug information reporting on the content
          of sets being built.



git-svn-id: https://tecsw.estec.esa.int/svn/taste/trunk/ocarina@2306 129961e7-ef38-4bb5-a8f7-c9a525a55882
parent 6966c89b
...@@ -7,13 +7,45 @@ all.aadl:127:03: warning: ram_2 references a component type ...@@ -7,13 +7,45 @@ all.aadl:127:03: warning: ram_2 references a component type
ocarina: Total: 0 error and 6 warnings ocarina: Total: 0 error and 6 warnings
resources execution resources execution
requirement : connections requirement : connections
Content of set proc_set (lib.real:25:18) is
shared.impl_sn: 13 component instance all.aadl:302:01
Content of set cnx_set (lib.real:27:14) is
shared.impl_tr: 200 component instance all.aadl:279:01
Content of set proc_set (lib.real:25:18) is
shared.impl_tr: 200 component instance all.aadl:279:01
Content of set cnx_set (lib.real:27:14) is
shared.impl_sn: 13 component instance all.aadl:302:01
theorem connections is: TRUE theorem connections is: TRUE
requirement : memory_size requirement : memory_size
Content of set proc_set (lib.real:42:18) is
shared.impl_sn: 13 component instance all.aadl:302:01
Content of set threads (lib.real:44:14) is
shared.impl_sn_th1: 43 component instance all.aadl:209:01
shared.impl_sn_th2: 112 component instance all.aadl:233:01
Content of set mem_set (lib.real:46:17) is
shared.impl_ram: 586 component instance all.aadl:93:01
Content of set proc_set (lib.real:42:18) is
shared.impl_tr: 200 component instance all.aadl:279:01
Content of set threads (lib.real:44:14) is
shared.impl_tr_th1: 219 component instance all.aadl:259:01
shared.impl_tr_th2: 371 component instance all.aadl:259:01
Content of set mem_set (lib.real:46:17) is
shared.impl_ram_2: 597 component instance all.aadl:93:01
theorem memory_size is: TRUE theorem memory_size is: TRUE
requirement : mutexes requirement : mutexes
Content of set proc_set (lib.real:63:18) is
shared.impl_sn: 13 component instance all.aadl:302:01
Content of set protected_data_set (lib.real:65:25) is
Content of set proc_set (lib.real:63:18) is
shared.impl_tr: 200 component instance all.aadl:279:01
Content of set protected_data_set (lib.real:65:25) is
theorem mutexes is: TRUE theorem mutexes is: TRUE
requirement : latency requirement : latency
requirement : buses_rate requirement : buses_rate
Content of set cnx_set (lib.real:8:17) is
shared.impl_cnx_1: 614 connection instance all.aadl:130:03
shared.impl_cnx_2: 626 connection instance all.aadl:131:03
Content of set connected_data_set (lib.real:10:25) is
lib.real:12:33 Backends: warning : property "assert_properties::access_bandwidth" is not defined on element 607 (shared.impl_a_bus) all.aadl:104:01Bus_Set lib.real:12:33 Backends: warning : property "assert_properties::access_bandwidth" is not defined on element 607 (shared.impl_a_bus) all.aadl:104:01Bus_Set
lib.real:12:72 Backends: error : Property is false for instance 607 (shared.impl_a_bus) lib.real:12:72 Backends: error : Property is false for instance 607 (shared.impl_a_bus)
theorem buses_rate is: FALSE theorem buses_rate is: FALSE
......
pok_safety execution pok_safety execution
requirement : check_error_handling requirement : check_error_handling
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 errors is Not implemented yet
-> value for actual_errors is Not implemented yet -> value for actual_errors is Not implemented yet
libsafety.real:32:46 Backends: error : Property is false for instance 69 (node.impl_part1_thr1) libsafety.real:32:46 Backends: error : Property is false for instance 69 (node.impl_part1_thr1)
......
...@@ -7,34 +7,226 @@ all.aadl:197:07: warning: layer_unclassified references a component type ...@@ -7,34 +7,226 @@ all.aadl:197:07: warning: layer_unclassified references a component type
ocarina: Total: 0 error and 6 warnings ocarina: Total: 0 error and 6 warnings
pok_security execution pok_security execution
requirement : one_security_level_by_memory requirement : one_security_level_by_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:23 Backends: warning : cardinal of set b is null
lib.real:15:11 Backends: warning : use default boolean value of true for operator '=' lib.real:15:11 Backends: warning : use default boolean value of true for operator '='
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:23 Backends: warning : cardinal of set b is null
lib.real:15:11 Backends: warning : use default boolean value of true for operator '=' lib.real:15:11 Backends: warning : use default boolean value of true for operator '='
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:23 Backends: warning : cardinal of set b is null
lib.real:15:11 Backends: warning : use default boolean value of true for operator '=' lib.real:15:11 Backends: warning : use default boolean value of true for operator '='
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:23 Backends: warning : cardinal of set b is null
lib.real:15:11 Backends: warning : use default boolean value of true for operator '=' lib.real:15:11 Backends: warning : use default boolean value of true for operator '='
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:23 Backends: warning : cardinal of set b is null
lib.real:15:11 Backends: warning : use default boolean value of true for operator '=' lib.real:15:11 Backends: warning : use default boolean value of true for operator '='
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:23 Backends: warning : cardinal of set b is null
lib.real:15:11 Backends: warning : use default boolean value of true for operator '=' lib.real:15:11 Backends: warning : use default boolean value of true for operator '='
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:23 Backends: warning : cardinal of set b is null
lib.real:15:11 Backends: warning : use default boolean value of true for operator '=' lib.real:15:11 Backends: warning : use default boolean value of true for operator '='
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:23 Backends: warning : cardinal of set b is null
lib.real:15:11 Backends: warning : use default boolean value of true for operator '=' lib.real:15:11 Backends: warning : use default boolean value of true for operator '='
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:23 Backends: warning : cardinal of set b is null
lib.real:15:11 Backends: warning : use default boolean value of true for operator '=' lib.real:15:11 Backends: warning : use default boolean value of true for operator '='
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:23 Backends: warning : cardinal of set b is null
lib.real:15:11 Backends: warning : use default boolean value of true for operator '=' lib.real:15:11 Backends: warning : use default boolean value of true for operator '='
theorem one_security_level_by_memory is: TRUE theorem one_security_level_by_memory is: TRUE
requirement : bell_lapadula requirement : bell_lapadula
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
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
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
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
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
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
theorem bell_lapadula is: TRUE theorem bell_lapadula is: TRUE
requirement : biba requirement : biba
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
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
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
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
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
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
theorem biba is: TRUE theorem biba is: TRUE
requirement : mils_1 requirement : mils_1
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
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
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
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
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
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
theorem mils_1 is: TRUE theorem mils_1 is: TRUE
requirement : mils_2 requirement : mils_2
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: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: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:118:20 Backends: warning : cardinal of set b_cnx is null
...@@ -43,6 +235,15 @@ lib.real:119:20 Backends: warning : cardinal of set b_dst is null ...@@ -43,6 +235,15 @@ 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: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: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 lib.real:119:62 Backends: warning : use default float value of 0.0 for operator Max
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: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: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:118:20 Backends: warning : cardinal of set b_cnx is null
...@@ -51,6 +252,15 @@ lib.real:119:20 Backends: warning : cardinal of set b_dst is null ...@@ -51,6 +252,15 @@ 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: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: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 lib.real:119:62 Backends: warning : use default float value of 0.0 for operator Max
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: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: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:118:20 Backends: warning : cardinal of set b_cnx is null
...@@ -59,6 +269,15 @@ lib.real:119:20 Backends: warning : cardinal of set b_dst is null ...@@ -59,6 +269,15 @@ 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: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: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 lib.real:119:62 Backends: warning : use default float value of 0.0 for operator Max
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: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: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:118:20 Backends: warning : cardinal of set b_cnx is null
...@@ -67,6 +286,15 @@ lib.real:119:20 Backends: warning : cardinal of set b_dst is null ...@@ -67,6 +286,15 @@ 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: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: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 lib.real:119:62 Backends: warning : use default float value of 0.0 for operator Max
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: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: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:118:20 Backends: warning : cardinal of set b_cnx is null
...@@ -75,6 +303,15 @@ lib.real:119:20 Backends: warning : cardinal of set b_dst is null ...@@ -75,6 +303,15 @@ 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: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: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 lib.real:119:62 Backends: warning : use default float value of 0.0 for operator Max
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: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: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:118:20 Backends: warning : cardinal of set b_cnx is null
......
...@@ -6,7 +6,7 @@ ...@@ -6,7 +6,7 @@
-- -- -- --
-- B o d y -- -- B o d y --
-- -- -- --
-- Copyright (C) 2009-2011, GET-Telecom Paris. -- -- Copyright (C) 2009-2011, European Space Agency (ESA). --
-- -- -- --
-- Ocarina is free software; you can redistribute it and/or modify -- -- Ocarina is free software; you can redistribute it and/or modify --
-- it under terms of the GNU General Public License as published by the -- -- it under terms of the GNU General Public License as published by the --
...@@ -766,9 +766,9 @@ package body Ocarina.Backends.REAL is ...@@ -766,9 +766,9 @@ package body Ocarina.Backends.REAL is
-- Iterate on the local set -- Iterate on the local set
for I in 1 .. Cardinal (R) loop for J in 1 .. Cardinal (R) loop
declare declare
V : constant Value_Id := New_Elem_Value (Get (R, I)); V : constant Value_Id := New_Elem_Value (Get (R, J));
Ret : Return_Type := RT_Error; Ret : Return_Type := RT_Error;
Result : Value_Id := No_Value; Result : Value_Id := No_Value;
begin begin
...@@ -788,7 +788,7 @@ package body Ocarina.Backends.REAL is ...@@ -788,7 +788,7 @@ package body Ocarina.Backends.REAL is
end if; end if;
if Get_Value_Type (Result).BVal then if Get_Value_Type (Result).BVal then
Add (R2, Get (R, I)); Add (R2, Get (R, J));
end if; end if;
end; end;
end loop; end loop;
...@@ -801,6 +801,14 @@ package body Ocarina.Backends.REAL is ...@@ -801,6 +801,14 @@ package body Ocarina.Backends.REAL is
-- Bind it in the set table, -- Bind it in the set table,
Set_Array (Integer (Index (Annotation (G)))) := R2; Set_Array (Integer (Index (Annotation (G)))) := R2;
Write_Line
("Content of set "
& Get_Name_String (Name (Identifier (Parametrized_Expr (E))))
& " (" & Image (Loc (E)) & ") is ");
Increment_Indentation;
Display_Set (R2);
Decrement_Indentation;
end Manage_Set_Declaration; end Manage_Set_Declaration;
----------------------------- -----------------------------
...@@ -895,17 +903,22 @@ package body Ocarina.Backends.REAL is ...@@ -895,17 +903,22 @@ package body Ocarina.Backends.REAL is
procedure Compute_Check_Expression procedure Compute_Check_Expression
(E : Node_Id; Ret : out Return_Type; Result : out Value_Id) (E : Node_Id; Ret : out Return_Type; Result : out Value_Id)
is is
pragma Assert (Kind (E) = K_Check_Expression or else pragma Assert (Kind (E) = K_Check_Expression
Kind (E) = K_Ternary_Expression or else or else Kind (E) = K_Ternary_Expression
Kind (E) = K_Literal or else or else Kind (E) = K_Literal
Kind (E) = K_Var_Reference or else or else Kind (E) = K_Var_Reference
Kind (E) = K_Check_Subprogram_Call); or else Kind (E) = K_Check_Subprogram_Call);
T1, T2 : Return_Type := RT_Unknown; T1, T2 : Return_Type := RT_Unknown;
R1, R2 : Value_Id := No_Value; R1, R2 : Value_Id := No_Value;
V, V2 : Value_Type; V, V2 : Value_Type;
begin begin
case Kind (E) is case Kind (E) is
when K_Identifier =>
Write_Line (Get_Name_String (Name (E)));
raise Program_Error;
when K_Var_Reference => when K_Var_Reference =>
Ret := Var_Type (Referenced_Var (E)); Ret := Var_Type (Referenced_Var (E));
Result := Var_Value (Referenced_Var (E)); Result := Var_Value (Referenced_Var (E));
...@@ -1742,10 +1755,10 @@ package body Ocarina.Backends.REAL is ...@@ -1742,10 +1755,10 @@ package body Ocarina.Backends.REAL is
(Referenced_Sets (E))))))); (Referenced_Sets (E)))))));
begin begin
if Cardinal (R1) > 0 then if Cardinal (R1) > 0 then
for I in 1 .. Cardinal (R1) loop for J in 1 .. Cardinal (R1) loop
V := Get_Property_Value_Function V := Get_Property_Value_Function
(Value (First_Node (True_Parameters (E))), (Value (First_Node (True_Parameters (E))),
Returned_Type (E), Get (R1, I)); Returned_Type (E), Get (R1, J));
if V /= No_Value then if V /= No_Value then
VT := Get_Value_Type (V); VT := Get_Value_Type (V);
if VT.T /= LT_List then if VT.T /= LT_List then
...@@ -1833,9 +1846,9 @@ package body Ocarina.Backends.REAL is ...@@ -1833,9 +1846,9 @@ package body Ocarina.Backends.REAL is
else else
Result := New_Boolean_Value (False); Result := New_Boolean_Value (False);
end if; end if;
else else
if Present (First_Node (Referenced_Sets (E))) then if Present (First_Node (Referenced_Sets (E))) then
-- The first parameter is a set -- The first parameter is a set
declare declare
...@@ -2745,8 +2758,8 @@ package body Ocarina.Backends.REAL is ...@@ -2745,8 +2758,8 @@ package body Ocarina.Backends.REAL is
end if; end if;
if T1 /= T2 then if T1 /= T2 then
Display_Located_Error Display_Located_Error
(Loc (P), "Is_in must be called on lists " (Loc (P), "Is_In must be called on lists "
& "of same type", & "of same type" & T1'Img & " " & T2'Img,
Fatal => True); Fatal => True);
end if; end if;
...@@ -2912,6 +2925,9 @@ package body Ocarina.Backends.REAL is ...@@ -2912,6 +2925,9 @@ package body Ocarina.Backends.REAL is
when SV_System_Set => when SV_System_Set =>
return Get_Instances_Of_Component_Type (C_System); return Get_Instances_Of_Component_Type (C_System);
when SV_Abstract_Set =>
return Get_Instances_Of_Component_Type (C_Abstract);
when SV_End_To_End_Flows_Set => when SV_End_To_End_Flows_Set =>
return Get_Instances_Of_End_To_End_Flows; return Get_Instances_Of_End_To_End_Flows;
......
...@@ -6,7 +6,7 @@ ...@@ -6,7 +6,7 @@
-- -- -- --
-- B o d y -- -- B o d y --
-- -- -- --
-- Copyright (C) 2009-2010, GET-Telecom Paris. -- -- Copyright (C) 2009-2011, European Space Agency (ESA). --
-- -- -- --
-- Ocarina is free software; you can redistribute it and/or modify -- -- Ocarina is free software; you can redistribute it and/or modify --
-- it under terms of the GNU General Public License as published by the -- -- it under terms of the GNU General Public License as published by the --
...@@ -42,6 +42,7 @@ with Ocarina.ME_AADL; ...@@ -42,6 +42,7 @@ with Ocarina.ME_AADL;
with Ocarina.ME_AADL.AADL_Instances.Debug; with Ocarina.ME_AADL.AADL_Instances.Debug;
with Ocarina.ME_AADL.AADL_Instances.Nutils; with Ocarina.ME_AADL.AADL_Instances.Nutils;
with Namet; use Namet; with Namet; use Namet;
with Output; use Output;
package body Ocarina.Instances.REAL_Checker.Queries is package body Ocarina.Instances.REAL_Checker.Queries is
use Ocarina.ME_AADL.AADL_Instances.Entities; use Ocarina.ME_AADL.AADL_Instances.Entities;
...@@ -108,6 +109,8 @@ package body Ocarina.Instances.REAL_Checker.Queries is ...@@ -108,6 +109,8 @@ package body Ocarina.Instances.REAL_Checker.Queries is
return (Component_T = C_Virtual_Bus); return (Component_T = C_Virtual_Bus);
when CC_Device => when CC_Device =>
return (Component_T = C_Device);