model.aadl.out 1.8 KB
Newer Older
jhugues's avatar
jhugues committed
1 2 3 4 5 6
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.
7
pok_safety execution
8
Processing requirement : check_error_handling
9 10 11 12
-------------------------------------
Evaluating theorem check_error_handling

 * Iterate for variable: node.impl_part1_thr1
13 14 15 16 17 18
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
19 20
     -> 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")
21
libsafety.real:32:46 Backends: error : Property is false for instance 69 (node.impl_part1_thr1)
22 23
 => Result: FALSE

24
theorem check_error_handling is: FALSE
25

26
model.aadl:118:07 Backends: fatal error : requirements are not fulfilled for theorem pok_safety