Commit 57c7af69 authored by hugues.jerome's avatar hugues.jerome

* Update all outputs



git-svn-id: https://tecsw.estec.esa.int/svn/taste/trunk/ocarina@1102 129961e7-ef38-4bb5-a8f7-c9a525a55882
parent 8beb47ee
all.aadl:66:03: warning: Field references a component type
all.aadl:124:03: warning: proc_1 references a component type
all.aadl:125:03: warning: proc_2 references a component type
all.aadl:126:03: warning: ram references a component type
all.aadl:127:03: warning: ram_2 references a component type
ocarina: Total: 0 error and 5 warnings
resources execution
requirement : connections
theorem connections is: TRUE
requirement : memory_size
theorem memory_size is: TRUE
requirement : mutexes
theorem mutexes is: TRUE
requirement : latency
requirement : buses_rate
lib.real:12:33 Backends: warning : property "assert_properties::access_bandwidth" is not defined on this single element.
lib.real:12:72 Backends: error : Property is false for instance 582 (shared.impl_a_bus)
theorem buses_rate is: FALSE
lib.real:85:01 Backends: fatal error : requirements are not fulfilled
pok_safety execution
requirement : check_error_handling
-> value for 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)
theorem check_error_handling is: FALSE
model.aadl:118:07 Backends: fatal error : requirements are not fulfilled
......@@ -7,6 +7,26 @@ 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
lib.real:15:23 Backends: warning : cardinal of set is null
lib.real:15:11 Backends: warning : use default boolean value of true
lib.real:15:23 Backends: warning : cardinal of set is null
lib.real:15:11 Backends: warning : use default boolean value of true
lib.real:15:23 Backends: warning : cardinal of set is null
lib.real:15:11 Backends: warning : use default boolean value of true
lib.real:15:23 Backends: warning : cardinal of set is null
lib.real:15:11 Backends: warning : use default boolean value of true
lib.real:15:23 Backends: warning : cardinal of set is null
lib.real:15:11 Backends: warning : use default boolean value of true
lib.real:15:23 Backends: warning : cardinal of set is null
lib.real:15:11 Backends: warning : use default boolean value of true
lib.real:15:23 Backends: warning : cardinal of set is null
lib.real:15:11 Backends: warning : use default boolean value of true
lib.real:15:23 Backends: warning : cardinal of set is null
lib.real:15:11 Backends: warning : use default boolean value of true
lib.real:15:23 Backends: warning : cardinal of set is null
lib.real:15:11 Backends: warning : use default boolean value of true
lib.real:15:23 Backends: warning : cardinal of set is null
lib.real:15:11 Backends: warning : use default boolean value of true
theorem one_security_level_by_memory is: TRUE
requirement : bell_lapadula
theorem bell_lapadula is: TRUE
......@@ -15,7 +35,56 @@ theorem biba is: TRUE
requirement : mils_1
theorem mils_1 is: TRUE
requirement : mils_2
lib.real:117:20 Backends: warning : cardinal of set is null
lib.real:117:15 Backends: warning : unknown value, use default value of 0.0
lib.real:118:20 Backends: warning : cardinal of set is null
lib.real:117:62 Backends: warning : unknown value, use default value of 0.0
lib.real:119:20 Backends: warning : cardinal of set is null
lib.real:119:15 Backends: warning : use default float value of 0.0
lib.real:120:20 Backends: warning : cardinal of set is null
lib.real:119:62 Backends: warning : use default float value of 0.0
lib.real:117:20 Backends: warning : cardinal of set is null
lib.real:117:15 Backends: warning : unknown value, use default value of 0.0
lib.real:118:20 Backends: warning : cardinal of set is null
lib.real:117:62 Backends: warning : unknown value, use default value of 0.0
lib.real:119:20 Backends: warning : cardinal of set is null
lib.real:119:15 Backends: warning : use default float value of 0.0
lib.real:120:20 Backends: warning : cardinal of set is null
lib.real:119:62 Backends: warning : use default float value of 0.0
lib.real:117:20 Backends: warning : cardinal of set is null
lib.real:117:15 Backends: warning : unknown value, use default value of 0.0
lib.real:118:20 Backends: warning : cardinal of set is null
lib.real:117:62 Backends: warning : unknown value, use default value of 0.0
lib.real:119:20 Backends: warning : cardinal of set is null
lib.real:119:15 Backends: warning : use default float value of 0.0
lib.real:120:20 Backends: warning : cardinal of set is null
lib.real:119:62 Backends: warning : use default float value of 0.0
lib.real:117:20 Backends: warning : cardinal of set is null
lib.real:117:15 Backends: warning : unknown value, use default value of 0.0
lib.real:118:20 Backends: warning : cardinal of set is null
lib.real:117:62 Backends: warning : unknown value, use default value of 0.0
lib.real:119:20 Backends: warning : cardinal of set is null
lib.real:119:15 Backends: warning : use default float value of 0.0
lib.real:120:20 Backends: warning : cardinal of set is null
lib.real:119:62 Backends: warning : use default float value of 0.0
lib.real:117:20 Backends: warning : cardinal of set is null
lib.real:117:15 Backends: warning : unknown value, use default value of 0.0
lib.real:118:20 Backends: warning : cardinal of set is null
lib.real:117:62 Backends: warning : unknown value, use default value of 0.0
lib.real:119:20 Backends: warning : cardinal of set is null
lib.real:119:15 Backends: warning : use default float value of 0.0
lib.real:120:20 Backends: warning : cardinal of set is null
lib.real:119:62 Backends: warning : use default float value of 0.0
lib.real:117:20 Backends: warning : cardinal of set is null
lib.real:117:15 Backends: warning : unknown value, use default value of 0.0
lib.real:118:20 Backends: warning : cardinal of set is null
lib.real:117:62 Backends: warning : unknown value, use default value of 0.0
lib.real:119:20 Backends: warning : cardinal of set is null
lib.real:119:15 Backends: warning : use default float value of 0.0
lib.real:120:20 Backends: warning : cardinal of set is null
lib.real:119:62 Backends: warning : use default float value of 0.0
theorem mils_2 is: TRUE
requirement : scheduling_1
theorem scheduling_1 is: TRUE
theorem pok_security is: TRUE
......@@ -264,8 +264,10 @@ tests/ocarina/test004/ocarina_script.aadl
tests/bound-t/rma.aadl
# Test for the Petri Net backend
tests/pn/test001/test.aadl
examples/petri_net/robot/robot.aadl
# Test for the REAL backend
examples/real/security/all.aadl
#examples/real/resources/all.aadl
examples/real/resources/all.aadl
examples/real/safety/model.aadl
examples/petri_net/robot/robot.aadl
......@@ -2,21 +2,35 @@ 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 boolean value will be casted to a float at runtime
test_env_subtheorem_call_no_parameter execution
Evaluating x
value for x after evaluating sub_theorem_1 is 2.00000E+00
theorem test_env_subtheorem_call_no_parameter is: TRUE
test_env_subtheorem_call_one_parameter execution
Evaluating x
value for x after evaluating sub_theorem_2 is 2.00000E+00
theorem test_env_subtheorem_call_one_parameter is: TRUE
test_env_subtheorem_call_multiple_parameters execution
-> value for y is 3
Evaluating x
value for x after evaluating sub_theorem_3 is 4.00000E+00
theorem test_env_subtheorem_call_multiple_parameters is: TRUE
test_env_subtheorem_call_with_domain execution
-> value for y is 1
Evaluating x
value for x after evaluating sub_theorem_4 is 2.00000E+00
theorem test_env_subtheorem_call_with_domain is: TRUE
test_env_subtheorem_call_global_variable execution
-> value for y is 1
Evaluating x
value for x after evaluating sub_theorem_5 is 1.00000E+00
theorem test_env_subtheorem_call_global_variable is: TRUE
test_env_subtheorem_call_with_empty_domain execution
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
theorem test_env_subtheorem_call_with_empty_domain is: TRUE
......@@ -43,5 +43,6 @@ set_declaration_or_operator execution
theorem set_declaration_or_operator is: TRUE
set_declaration_predefined_sets execution
-> value for x is 4
theorem set_declaration_predefined_sets is: TRUE
......@@ -17,15 +17,22 @@ check_expression_range execution
theorem check_expression_range is: TRUE
check_expression_lcm execution
-> value for var_list is Not implemented yet
theorem check_expression_lcm is: TRUE
check_expression_gcd execution
-> value for var_list is Not implemented yet
theorem check_expression_gcd is: TRUE
check_expression_gcd_var execution
-> value for v1 is 2
-> value for v2 is 4
-> value for v3 is 6
theorem check_expression_gcd_var is: TRUE
check_expression_non_null execution
-> value for v0 is 0
-> value for v1 is 42
theorem check_expression_non_null is: TRUE
check_is_in execution
......
variables_basis execution
-> value for bla is 2
theorem variables_basis is: TRUE
variables_with_expression execution
-> value for bla is 3
theorem variables_with_expression is: TRUE
variables_dependant execution
-> value for x1 is 1
-> value for x2 is 3
theorem variables_dependant is: TRUE
variables_set_dependants execution
-> value for x2 is 3
theorem variables_set_dependants is: TRUE
variables_iterative_expressions execution
-> value for y is 6.0
theorem variables_iterative_expressions is: TRUE
variables_imbricated_iterative_expressions execution
-> value for y is 7.0
theorem variables_imbricated_iterative_expressions is: TRUE
variables_product_expression execution
-> value for x is 0.5
theorem variables_product_expression is: TRUE
element_list_expression execution
theorem element_list_expression is: TRUE
element_list_static_declaration execution
-> value for period is Not implemented yet
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
theorem list_concat is: TRUE
is_in_list_and_set_expression execution
theorem is_in_list_and_set_expression is: TRUE
if_then_else_expression execution
-> value for v1 is 1
-> value for v2 is 2
-> value for v3 is 0
theorem if_then_else_expression is: TRUE
test_head_and_queue execution
-> value for period_list is Not implemented yet
-> value for poped_list is Not implemented yet
theorem test_head_and_queue is: TRUE
test_reference_property execution
theorem test_reference_property is: TRUE
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment