Skip to content
Snippets Groups Projects
Commit 8ccfdbd5 authored by Virgile Prevosto's avatar Virgile Prevosto
Browse files

[aorai] update oracle

parent a6e57d66
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
src/plugins/aorai/tests/ya/oracle_prove/serial.res.oracle
+ 9
− 311
View file @ 8ccfdbd5
[kernel] Parsing tests/ya/serial.c (with preprocessing)
[kernel:annot:missing-spec] tests/ya/serial.c:43: Warning:
Neither code nor specification for function Frama_C_show_aorai_state, generating default assigns from the prototype
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
indefinitely ∈ [--..--]
buffer[0..4] ∈ {0}
n ∈ {0}
aorai_x1 ∈ {0}
aorai_x2 ∈ {0}
aorai_y1 ∈ {0}
aorai_y2 ∈ {0}
aorai_CurOperation ∈ {0}
aorai_CurOpStatus ∈ {0}
aorai_CurStates ∈ {19}
aorai_StatesHistory_1 ∈ {19}
aorai_StatesHistory_2 ∈ {19}
[eva] using specification for function Frama_C_interval
[eva] tests/ya/serial.c:45: starting to merge loop iterations
[eva] tests/ya/serial.c:50: Trace partitioning superposing up to 100 states
[eva] tests/ya/serial.c:50: Trace partitioning superposing up to 300 states
[aorai] tests/ya/serial.c:79: Wait1 <- Wait1 <- Complete
[aorai] tests/ya/serial.c:79: n in {5},x in [0..16383],y in [8192..16383]
[aorai] tests/ya/serial.c:79: Error <- Error <- Complete
[aorai] tests/ya/serial.c:79: n in {5},x in [0..16383],y in [8192..16383]
[aorai] tests/ya/serial.c:79: Complete <- Complete <- Complete
[aorai] tests/ya/serial.c:79: n in {5},x in [0..16383],y in [8192..16383]
[aorai] tests/ya/serial.c:79: Wait1 <- Wait1 <- Complete
[aorai] tests/ya/serial.c:79: n in {5},x in [0..16383],y in [0..8191]
[aorai] tests/ya/serial.c:79: Error <- Error <- Complete
[aorai] tests/ya/serial.c:79: n in {5},x in [0..16383],y in [0..8191]
[aorai] tests/ya/serial.c:79: Complete <- Complete <- Complete
[aorai] tests/ya/serial.c:79: n in {5},x in [0..16383],y in [0..8191]
[eva] tests/ya/serial.c:50: Trace partitioning superposing up to 500 states
[eva:alarm] tests/ya/serial.c:52: Warning:
accessing uninitialized left-value. assert \initialized(&status);
[eva] tests/ya/serial.c:50: Trace partitioning superposing up to 700 states
[eva] tests/ya/serial.c:50: Trace partitioning superposing up to 900 states
[eva] tests/ya/serial.c:50: Trace partitioning superposing up to 1200 states
[eva] tests/ya/serial.c:50: Trace partitioning superposing up to 1500 states
[aorai] tests/ya/serial.c:79: Error <- Error <- Error
[aorai] tests/ya/serial.c:79: n in {5},x in [0..16383],y in [8192..16383]
[aorai] tests/ya/serial.c:79: Error <- Error <- Error
[aorai] tests/ya/serial.c:79: n in {5},x in [0..16383],y in [0..8191]
[eva] tests/ya/serial.c:50: Trace partitioning superposing up to 1700 states
[eva] tests/ya/serial.c:50: Trace partitioning superposing up to 1900 states
[eva] tests/ya/serial.c:50: Trace partitioning superposing up to 2000 states
[eva] tests/ya/serial.c:50: Trace partitioning superposing up to 2100 states
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function input_data_post_func:
aorai_x1 ∈
{0; 1; 2; 3; 4; 5; 6; 7; 8; 9; 10; 11; 12; 13; 14; 15; 16; 17; 18;
19; 20; 21; 22; 23; 24; 25; 26; 27; 28; 29; 30; 31; 32; 33; 34;
35; 36; 37; 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; 86; 87; 88; 89; 90; 91; 92; 93; 94; 95; 96; 97; 98;
99; 100; 101; 102; 103; 104; 105; 106; 107; 108; 109; 110; 111;
112; 113; 114; 115; 116; 117; 118; 119; 120; 121; 122; 123; 124;
125; 126; 127}
aorai_x2 ∈
{0; 1; 2; 3; 4; 5; 6; 7; 8; 9; 10; 11; 12; 13; 14; 15; 16; 17; 18;
19; 20; 21; 22; 23; 24; 25; 26; 27; 28; 29; 30; 31; 32; 33; 34;
35; 36; 37; 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; 86; 87; 88; 89; 90; 91; 92; 93; 94; 95; 96; 97; 98;
99; 100; 101; 102; 103; 104; 105; 106; 107; 108; 109; 110; 111;
112; 113; 114; 115; 116; 117; 118; 119; 120; 121; 122; 123; 124;
125; 126; 127}
aorai_y1 ∈
{0; 1; 2; 3; 4; 5; 6; 7; 8; 9; 10; 11; 12; 13; 14; 15; 16; 17; 18;
19; 20; 21; 22; 23; 24; 25; 26; 27; 28; 29; 30; 31; 32; 33; 34;
35; 36; 37; 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; 86; 87; 88; 89; 90; 91; 92; 93; 94; 95; 96; 97; 98;
99; 100; 101; 102; 103; 104; 105; 106; 107; 108; 109; 110; 111;
112; 113; 114; 115; 116; 117; 118; 119; 120; 121; 122; 123; 124;
125; 126; 127}
aorai_y2 ∈ [0..2147483647]
aorai_CurOperation ∈ {2}
aorai_CurOpStatus ∈ {1}
aorai_CurStates ∈ {0; 7; 19; 20; 21; 22; 23}
aorai_StatesHistory_1 ∈ {1; 2; 3; 4; 5; 6; 7}
aorai_StatesHistory_2 ∈ {7; 8; 9; 10; 11; 12; 13}
[eva:final-states] Values at end of function input_data_pre_func:
aorai_CurOperation ∈ {2}
aorai_CurOpStatus ∈ {0}
aorai_CurStates ∈ {1; 2; 3; 4; 5; 6; 7}
aorai_StatesHistory_1 ∈ {7; 8; 9; 10; 11; 12; 13}
aorai_StatesHistory_2 ∈ {7; 14; 15; 16; 17; 18}
[eva:final-states] Values at end of function input_data:
Frama_C_entropy_source ∈ [--..--]
aorai_x1 ∈
{0; 1; 2; 3; 4; 5; 6; 7; 8; 9; 10; 11; 12; 13; 14; 15; 16; 17; 18;
19; 20; 21; 22; 23; 24; 25; 26; 27; 28; 29; 30; 31; 32; 33; 34;
35; 36; 37; 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; 86; 87; 88; 89; 90; 91; 92; 93; 94; 95; 96; 97; 98;
99; 100; 101; 102; 103; 104; 105; 106; 107; 108; 109; 110; 111;
112; 113; 114; 115; 116; 117; 118; 119; 120; 121; 122; 123; 124;
125; 126; 127}
aorai_x2 ∈
{0; 1; 2; 3; 4; 5; 6; 7; 8; 9; 10; 11; 12; 13; 14; 15; 16; 17; 18;
19; 20; 21; 22; 23; 24; 25; 26; 27; 28; 29; 30; 31; 32; 33; 34;
35; 36; 37; 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; 86; 87; 88; 89; 90; 91; 92; 93; 94; 95; 96; 97; 98;
99; 100; 101; 102; 103; 104; 105; 106; 107; 108; 109; 110; 111;
112; 113; 114; 115; 116; 117; 118; 119; 120; 121; 122; 123; 124;
125; 126; 127}
aorai_y1 ∈
{0; 1; 2; 3; 4; 5; 6; 7; 8; 9; 10; 11; 12; 13; 14; 15; 16; 17; 18;
19; 20; 21; 22; 23; 24; 25; 26; 27; 28; 29; 30; 31; 32; 33; 34;
35; 36; 37; 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; 86; 87; 88; 89; 90; 91; 92; 93; 94; 95; 96; 97; 98;
99; 100; 101; 102; 103; 104; 105; 106; 107; 108; 109; 110; 111;
112; 113; 114; 115; 116; 117; 118; 119; 120; 121; 122; 123; 124;
125; 126; 127}
aorai_y2 ∈ [0..2147483647]
aorai_CurOperation ∈ {2}
aorai_CurOpStatus ∈ {1}
aorai_CurStates ∈ {0; 7; 19; 20; 21; 22; 23}
aorai_StatesHistory_1 ∈ {1; 2; 3; 4; 5; 6; 7}
aorai_StatesHistory_2 ∈ {7; 8; 9; 10; 11; 12; 13}
[eva:final-states] Values at end of function input_status_post_func:
aorai_CurOperation ∈ {1}
aorai_CurOpStatus ∈ {1}
aorai_CurStates ∈ {7; 8; 9; 10; 11; 12; 13; 19; 20; 21; 22; 23}
aorai_StatesHistory_1 ∈ {7; 14; 15; 16; 17; 18}
aorai_StatesHistory_2 ∈ {0; 7; 19; 20; 21; 22; 23}
[eva:final-states] Values at end of function input_status_pre_func:
aorai_CurOperation ∈ {1}
aorai_CurOpStatus ∈ {0}
aorai_CurStates ∈ {7; 14; 15; 16; 17; 18}
aorai_StatesHistory_1 ∈ {0; 7; 19; 20; 21; 22; 23}
aorai_StatesHistory_2 ∈ {0; 1; 2; 3; 4; 5; 6; 7; 14; 15; 16; 17; 18; 19}
[eva:final-states] Values at end of function input_status:
Frama_C_entropy_source ∈ [--..--]
aorai_CurOperation ∈ {1}
aorai_CurOpStatus ∈ {1}
aorai_CurStates ∈ {7; 8; 9; 10; 11; 12; 13; 19; 20; 21; 22; 23}
aorai_StatesHistory_1 ∈ {7; 14; 15; 16; 17; 18}
aorai_StatesHistory_2 ∈ {0; 7; 19; 20; 21; 22; 23}
[eva:final-states] Values at end of function output_post_func:
aorai_CurOperation ∈ {0}
aorai_CurOpStatus ∈ {1}
aorai_CurStates ∈ {0; 7; 19}
aorai_StatesHistory_1 ∈ {0; 7; 19}
aorai_StatesHistory_2 ∈ {0; 7}
[eva:final-states] Values at end of function output_pre_func:
aorai_CurOperation ∈ {0}
aorai_CurOpStatus ∈ {0}
aorai_CurStates ∈ {0; 7; 19}
aorai_StatesHistory_1 ∈ {0; 7}
aorai_StatesHistory_2 ∈ {5; 7}
[eva:final-states] Values at end of function output:
aorai_CurOperation ∈ {0}
aorai_CurOpStatus ∈ {1}
aorai_CurStates ∈ {0; 7; 19}
aorai_StatesHistory_1 ∈ {0; 7; 19}
aorai_StatesHistory_2 ∈ {0; 7}
[eva:final-states] Values at end of function read:
Frama_C_entropy_source ∈ [--..--]
s ∈
{0; 1; 2; 3; 4; 5; 6; 7; 8; 9; 10; 11; 12; 13; 14; 15; 16; 17; 18; 19; 20;
21; 22; 23; 24; 25; 26; 27; 28; 29; 30; 31; 32; 33; 34; 35; 36; 37; 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; 86; 87; 88; 89; 90; 91; 92;
93; 94; 95; 96; 97; 98; 99; 100; 101; 102; 103; 104; 105; 106; 107; 108;
109; 110; 111; 112; 113; 114; 115; 116; 117; 118; 119; 120; 121; 122;
123; 124; 125; 126; 127; 128; 129; 130; 131; 132; 133; 134; 135; 136;
137; 138; 139; 140; 141; 142; 143; 144; 145; 146; 147; 148; 149; 150;
151; 152; 153; 154; 155; 156; 157; 158; 159; 160; 161; 162; 163; 164;
165; 166; 167; 168; 169; 170; 171; 172; 173; 174; 175; 176; 177; 178;
179; 180; 181; 182; 183; 184; 185; 186; 187; 188; 189; 190; 191; 192;
193; 194; 195; 196; 197; 198; 199; 200; 201; 202; 203; 204; 205; 206;
207; 208; 209; 210; 211; 212; 213; 214; 215; 216; 217; 218; 219; 220;
221; 222; 223; 224; 225; 226; 227; 228; 229; 230; 231; 232; 233; 234;
235; 236; 237; 238; 239; 240; 241; 242; 243; 244; 245; 246; 247; 248;
249; 250; 251; 252; 253; 254; 255}
status ∈ {0; 2; 4; 6; 8; 10; 12; 14} or UNINITIALIZED
__retres ∈ [-1..255]
aorai_x1 ∈
{0; 1; 2; 3; 4; 5; 6; 7; 8; 9; 10; 11; 12; 13; 14; 15; 16; 17; 18;
19; 20; 21; 22; 23; 24; 25; 26; 27; 28; 29; 30; 31; 32; 33; 34;
35; 36; 37; 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; 86; 87; 88; 89; 90; 91; 92; 93; 94; 95; 96; 97; 98;
99; 100; 101; 102; 103; 104; 105; 106; 107; 108; 109; 110; 111;
112; 113; 114; 115; 116; 117; 118; 119; 120; 121; 122; 123; 124;
125; 126; 127}
aorai_x2 ∈
{0; 1; 2; 3; 4; 5; 6; 7; 8; 9; 10; 11; 12; 13; 14; 15; 16; 17; 18;
19; 20; 21; 22; 23; 24; 25; 26; 27; 28; 29; 30; 31; 32; 33; 34;
35; 36; 37; 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; 86; 87; 88; 89; 90; 91; 92; 93; 94; 95; 96; 97; 98;
99; 100; 101; 102; 103; 104; 105; 106; 107; 108; 109; 110; 111;
112; 113; 114; 115; 116; 117; 118; 119; 120; 121; 122; 123; 124;
125; 126; 127}
aorai_y1 ∈
{0; 1; 2; 3; 4; 5; 6; 7; 8; 9; 10; 11; 12; 13; 14; 15; 16; 17; 18;
19; 20; 21; 22; 23; 24; 25; 26; 27; 28; 29; 30; 31; 32; 33; 34;
35; 36; 37; 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; 86; 87; 88; 89; 90; 91; 92; 93; 94; 95; 96; 97; 98;
99; 100; 101; 102; 103; 104; 105; 106; 107; 108; 109; 110; 111;
112; 113; 114; 115; 116; 117; 118; 119; 120; 121; 122; 123; 124;
125; 126; 127}
aorai_y2 ∈ [0..2147483647]
aorai_CurOperation ∈ {1; 2}
aorai_CurOpStatus ∈ {1}
aorai_CurStates ∈ {0; 7; 19; 20; 21; 22; 23}
aorai_StatesHistory_1 ∈ {1; 2; 3; 4; 5; 6; 7; 14; 15; 16; 17; 18}
aorai_StatesHistory_2 ∈ {0; 7; 8; 9; 10; 11; 12; 13; 19; 20; 21; 22; 23}
[eva:final-states] Values at end of function main:
Frama_C_entropy_source ∈ [--..--]
buffer[0] ∈
{0; 128; 129; 130; 131; 132; 133; 134; 135; 136; 137; 138; 139; 140;
141; 142; 143; 144; 145; 146; 147; 148; 149; 150; 151; 152; 153;
154; 155; 156; 157; 158; 159; 160; 161; 162; 163; 164; 165; 166;
167; 168; 169; 170; 171; 172; 173; 174; 175; 176; 177; 178; 179;
180; 181; 182; 183; 184; 185; 186; 187; 188; 189; 190; 191; 192;
193; 194; 195; 196; 197; 198; 199; 200; 201; 202; 203; 204; 205;
206; 207; 208; 209; 210; 211; 212; 213; 214; 215; 216; 217; 218;
219; 220; 221; 222; 223; 224; 225; 226; 227; 228; 229; 230; 231;
232; 233; 234; 235; 236; 237; 238; 239; 240; 241; 242; 243; 244;
245; 246; 247; 248; 249; 250; 251; 252; 253; 254; 255}
[1..2] ∈
{0; 1; 2; 3; 4; 5; 6; 7; 8; 9; 10; 11; 12; 13; 14; 15; 16; 17; 18;
19; 20; 21; 22; 23; 24; 25; 26; 27; 28; 29; 30; 31; 32; 33; 34; 35;
36; 37; 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; 86;
87; 88; 89; 90; 91; 92; 93; 94; 95; 96; 97; 98; 99; 100; 101; 102;
103; 104; 105; 106; 107; 108; 109; 110; 111; 112; 113; 114; 115;
116; 117; 118; 119; 120; 121; 122; 123; 124; 125; 126; 127}
[3..4] ∈ [0..2147483647]
n ∈ {0; 1; 2; 3; 4}
aorai_x1 ∈
{0; 1; 2; 3; 4; 5; 6; 7; 8; 9; 10; 11; 12; 13; 14; 15; 16; 17; 18;
19; 20; 21; 22; 23; 24; 25; 26; 27; 28; 29; 30; 31; 32; 33; 34;
35; 36; 37; 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; 86; 87; 88; 89; 90; 91; 92; 93; 94; 95; 96; 97; 98;
99; 100; 101; 102; 103; 104; 105; 106; 107; 108; 109; 110; 111;
112; 113; 114; 115; 116; 117; 118; 119; 120; 121; 122; 123; 124;
125; 126; 127}
aorai_x2 ∈
{0; 1; 2; 3; 4; 5; 6; 7; 8; 9; 10; 11; 12; 13; 14; 15; 16; 17; 18;
19; 20; 21; 22; 23; 24; 25; 26; 27; 28; 29; 30; 31; 32; 33; 34;
35; 36; 37; 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; 86; 87; 88; 89; 90; 91; 92; 93; 94; 95; 96; 97; 98;
99; 100; 101; 102; 103; 104; 105; 106; 107; 108; 109; 110; 111;
112; 113; 114; 115; 116; 117; 118; 119; 120; 121; 122; 123; 124;
125; 126; 127}
aorai_y1 ∈
{0; 1; 2; 3; 4; 5; 6; 7; 8; 9; 10; 11; 12; 13; 14; 15; 16; 17; 18;
19; 20; 21; 22; 23; 24; 25; 26; 27; 28; 29; 30; 31; 32; 33; 34;
35; 36; 37; 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; 86; 87; 88; 89; 90; 91; 92; 93; 94; 95; 96; 97; 98;
99; 100; 101; 102; 103; 104; 105; 106; 107; 108; 109; 110; 111;
112; 113; 114; 115; 116; 117; 118; 119; 120; 121; 122; 123; 124;
125; 126; 127}
aorai_y2 ∈ [0..2147483647]
aorai_CurOperation ∈ {0; 1; 2}
aorai_CurOpStatus ∈ {0; 1}
aorai_CurStates ∈ {0; 7; 19; 20; 21; 22; 23}
aorai_StatesHistory_1 ∈ {0; 1; 2; 3; 4; 5; 6; 7; 14; 15; 16; 17; 18; 19}
aorai_StatesHistory_2 ∈ {0; 7; 8; 9; 10; 11; 12; 13; 19; 20; 21; 22; 23}
[eva:summary] ====== ANALYSIS SUMMARY ======
----------------------------------------------------------------------------
11 functions analyzed (out of 11): 100% coverage.
In these functions, 216 statements reached (out of 255): 84% coverage.
----------------------------------------------------------------------------
Some errors and warnings have been raised during the analysis:
by the Eva analyzer: 0 errors 0 warnings
by the Frama-C kernel: 0 errors 1 warning
----------------------------------------------------------------------------
1 alarm generated by the analysis:
1 access to uninitialized left-values
----------------------------------------------------------------------------
Evaluation of the logical properties reached by the analysis:
Assertions 0 valid 0 unknown 0 invalid 0 total
Preconditions 2 valid 0 unknown 0 invalid 2 total
100% of the logical properties reached have been proven.
----------------------------------------------------------------------------
[aorai] tests/ya/serial.c:79: Warning:
Call to output not conforming to automaton (post-cond). Assuming it is on a dead path
[aorai] tests/ya/serial.c:25: Warning:
Call to output not conforming to automaton (pre-cond). Assuming it is on a dead path
[kernel] Parsing TMPDIR/aorai_serial_0.i (no preprocessing)
[kernel:typing:implicit-function-declaration] TMPDIR/aorai_serial_0.i:174: Warning:
[kernel:typing:implicit-function-declaration] TMPDIR/aorai_serial_0.i:98: Warning:
Calling undeclared function Frama_C_interval. Old style K&R code?
[wp] Warning: Missing RTE guards
[wp] Warning: No goal generated
[wp] Warning: No goal generated
[wp] Warning: No goal generated
[wp] Warning: No goal generated
[wp] Warning: No goal generated
[wp] Warning: No goal generated
[kernel:annot:missing-spec] TMPDIR/aorai_serial_0.i:125: Warning:
Neither code nor specification for function Frama_C_interval, generating default assigns from the prototype
[kernel:annot:missing-spec] TMPDIR/aorai_serial_0.i:125: Warning:
Neither code nor specification for function Frama_C_show_aorai_state, generating default assigns from the prototype
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