all.aadl.out 5.16 KB
Newer Older
1
2
3
4
5
6
7
8
9
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
requirement : one_security_level_by_memory
hugues.jerome's avatar
hugues.jerome committed
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
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
30
31
32
33
34
35
36
37
theorem one_security_level_by_memory is: TRUE
requirement : bell_lapadula
theorem bell_lapadula is: TRUE
requirement : biba
theorem biba is: TRUE
requirement : mils_1
theorem mils_1 is: TRUE
requirement : mils_2
hugues.jerome's avatar
hugues.jerome committed
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
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
86
87
88
89
theorem mils_2 is: TRUE
requirement : scheduling_1
theorem scheduling_1 is: TRUE
theorem pok_security is: TRUE
hugues.jerome's avatar
hugues.jerome committed
90