test_real_exec_env_01.aadl.out

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
Content of set a_set (test_real_exec_env_01.aadl:102:12) is 
  rma.erc32_node_a: 13 component instance test_real_exec_env_01.aadl:72:01
     -> value for y is 3
   Evaluating x
   value for x after evaluating sub_theorem_3 is 4.00000E+00
theorem test_env_subtheorem_call_multiple_parameters is: TRUE

test_env_subtheorem_call_with_domain execution
Content of set a_set (test_real_exec_env_01.aadl:112:12) is 
  rma.erc32_node_a_task1: 20 component instance test_real_exec_env_01.aadl:27:01
  rma.erc32_node_a_task2: 52 component instance test_real_exec_env_01.aadl:40:01
     -> value for y is 1
   Evaluating x
   value for x after evaluating sub_theorem_4 is 2.00000E+00
theorem test_env_subtheorem_call_with_domain is: TRUE

test_env_subtheorem_call_global_variable execution
Content of set a_set (test_real_exec_env_01.aadl:122:12) is 
  rma.erc32_node_a: 13 component instance test_real_exec_env_01.aadl:72:01
     -> value for y is 1
   Evaluating x
   value for x after evaluating sub_theorem_5 is 1.00000E+00
theorem test_env_subtheorem_call_global_variable is: TRUE

test_env_subtheorem_call_with_empty_domain execution
Content of set a_set (test_real_exec_env_01.aadl:133:12) is 
   Evaluating x
lib.real:38:01 Backends: warning : Empty range set, returned value is 0.0
   value for x after evaluating sub_theorem_6 is 0.00000E+00
theorem test_env_subtheorem_call_with_empty_domain is: TRUE