From b99bc0985cc0714dd27d12672dd6dc418d412f7e Mon Sep 17 00:00:00 2001
From: Valentin Perrelle <valentin.perrelle@cea.fr>
Date: Tue, 18 Dec 2018 19:37:58 +0100
Subject: [PATCH] [Aorai] Add a complete test for aorai + eva combination
---
.../aorai/tests/ya/oracle/serial.res.oracle | 691 ++++++++++++++++++
.../tests/ya/oracle_prove/serial.res.oracle | 310 ++++++++
src/plugins/aorai/tests/ya/serial.c | 88 +++
src/plugins/aorai/tests/ya/serial.ya | 160 ++++
4 files changed, 1249 insertions(+)
create mode 100644 src/plugins/aorai/tests/ya/oracle/serial.res.oracle
create mode 100644 src/plugins/aorai/tests/ya/oracle_prove/serial.res.oracle
create mode 100644 src/plugins/aorai/tests/ya/serial.c
create mode 100644 src/plugins/aorai/tests/ya/serial.ya
diff --git a/src/plugins/aorai/tests/ya/oracle/serial.res.oracle b/src/plugins/aorai/tests/ya/oracle/serial.res.oracle
new file mode 100644
index 00000000000..0a57509c1c6
--- /dev/null
+++ b/src/plugins/aorai/tests/ya/oracle/serial.res.oracle
@@ -0,0 +1,691 @@
+[kernel] Parsing tests/ya/serial.c (with preprocessing)
+[kernel:typing:implicit-function-declaration] tests/ya/serial.c:81: Warning:
+ Calling undeclared function Frama_C_show_aorai_state. Old style K&R code?
+[aorai] Welcome to the Aorai plugin
+[kernel:annot:missing-spec] tests/ya/serial.c:45: 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:47: starting to merge loop iterations
+[eva] tests/ya/serial.c:52: Trace partitioning superposing up to 100 states
+[eva] tests/ya/serial.c:52: Trace partitioning superposing up to 300 states
+[aorai] tests/ya/serial.c:81: Wait1 <- Wait1 <- Complete
+[aorai] tests/ya/serial.c:81: Error <- Error <- Complete
+[aorai] tests/ya/serial.c:81: Complete <- Complete <- Complete
+[aorai] tests/ya/serial.c:81: Wait1 <- Wait1 <- Complete
+[aorai] tests/ya/serial.c:81: Error <- Error <- Complete
+[aorai] tests/ya/serial.c:81: Complete <- Complete <- Complete
+[eva] tests/ya/serial.c:52: Trace partitioning superposing up to 500 states
+[eva:alarm] tests/ya/serial.c:54: Warning:
+ accessing uninitialized left-value. assert \initialized(&status);
+[eva] tests/ya/serial.c:52: Trace partitioning superposing up to 700 states
+[eva] tests/ya/serial.c:52: Trace partitioning superposing up to 900 states
+[eva] tests/ya/serial.c:52: Trace partitioning superposing up to 1200 states
+[eva] tests/ya/serial.c:52: Trace partitioning superposing up to 1500 states
+[aorai] tests/ya/serial.c:81: Error <- Error <- Error
+[aorai] tests/ya/serial.c:81: Error <- Error <- Error
+[eva] tests/ya/serial.c:52: Trace partitioning superposing up to 1700 states
+[eva] tests/ya/serial.c:52: Trace partitioning superposing up to 1900 states
+[eva] tests/ya/serial.c:52: Trace partitioning superposing up to 2000 states
+[eva] tests/ya/serial.c:52: 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.
+ ----------------------------------------------------------------------------
+[kernel] Parsing TMPDIR/aorai_serial_0.i (no preprocessing)
+[kernel:typing:implicit-function-declaration] TMPDIR/aorai_serial_0.i:176: Warning:
+ Calling undeclared function Frama_C_interval. Old style K&R code?
+/* Generated by Frama-C */
+enum aorai_States {
+ aorai_reject_state = -2,
+ Complete = 0,
+ DataReq1 = 1,
+ DataReq2 = 2,
+ DataReq3 = 3,
+ DataReq4 = 4,
+ DataReq5 = 5,
+ DataReqE = 6,
+ Error = 7,
+ StatusError = 8,
+ StatusOk1 = 9,
+ StatusOk2 = 10,
+ StatusOk3 = 11,
+ StatusOk4 = 12,
+ StatusOk5 = 13,
+ StatusReq1 = 14,
+ StatusReq2 = 15,
+ StatusReq3 = 16,
+ StatusReq4 = 17,
+ StatusReq5 = 18,
+ Wait1 = 19,
+ Wait2 = 20,
+ Wait3 = 21,
+ Wait4 = 22,
+ Wait5 = 23
+};
+enum aorai_ListOper {
+ op_input_data = 2,
+ op_input_status = 1,
+ op_output = 0
+};
+enum aorai_OpStatusList {
+ aorai_Terminated = 1,
+ aorai_Called = 0
+};
+int volatile indefinitely;
+int buffer[5];
+int n = 0;
+/*@ assigns \result;
+ assigns \result \from \nothing; */
+extern int Frama_C_show_aorai_state(void);
+
+/*@ ghost enum aorai_ListOper aorai_CurOperation; */
+/*@ ghost enum aorai_OpStatusList aorai_CurOpStatus; */
+/*@ ghost int aorai_CurStates = Wait1; */
+/*@ ghost int aorai_StatesHistory_1 = Wait1; */
+/*@ ghost int aorai_StatesHistory_2 = Wait1; */
+/*@ ghost int aorai_x1 = 0; */
+/*@ ghost int aorai_x2 = 0; */
+/*@ ghost int aorai_y1 = 0; */
+/*@ ghost int aorai_y2 = 0; */
+/*@ ghost
+ void input_status_pre_func(void)
+ {
+ /@ slevel full; @/
+ aorai_CurOpStatus = aorai_Called;
+ aorai_CurOperation = op_input_status;
+ aorai_StatesHistory_2 = aorai_StatesHistory_1;
+ aorai_StatesHistory_1 = aorai_CurStates;
+ if (19 == aorai_CurStates) aorai_CurStates = StatusReq1;
+ else
+ if (9 == aorai_CurStates) aorai_CurStates = StatusReq1;
+ else
+ if (8 == aorai_CurStates) aorai_CurStates = StatusReq1;
+ else
+ if (0 == aorai_CurStates) aorai_CurStates = StatusReq1;
+ else
+ if (20 == aorai_CurStates) aorai_CurStates = StatusReq2;
+ else
+ if (10 == aorai_CurStates) aorai_CurStates = StatusReq2;
+ else
+ if (21 == aorai_CurStates) aorai_CurStates = StatusReq3;
+ else
+ if (11 == aorai_CurStates) aorai_CurStates = StatusReq3;
+ else
+ if (22 == aorai_CurStates) aorai_CurStates = StatusReq4;
+ else
+ if (12 == aorai_CurStates) aorai_CurStates = StatusReq4;
+ else
+ if (23 == aorai_CurStates) aorai_CurStates = StatusReq5;
+ else
+ if (13 == aorai_CurStates) aorai_CurStates = StatusReq5;
+ return;
+ }
+
+*/
+
+/*@ ghost
+ void input_status_post_func(int res)
+ {
+ /@ slevel full; @/
+ aorai_CurOpStatus = aorai_Terminated;
+ aorai_CurOperation = op_input_status;
+ aorai_StatesHistory_2 = aorai_StatesHistory_1;
+ aorai_StatesHistory_1 = aorai_CurStates;
+ if (18 == aorai_CurStates && ((res & 15) != 1 && (res & 1) != 0))
+ aorai_CurStates = StatusError;
+ else
+ if (17 == aorai_CurStates && ((res & 15) != 1 && (res & 1) != 0))
+ aorai_CurStates = StatusError;
+ else
+ if (16 == aorai_CurStates && ((res & 15) != 1 && (res & 1) != 0))
+ aorai_CurStates = StatusError;
+ else
+ if (15 == aorai_CurStates && ((res & 15) != 1 && (res & 1) != 0))
+ aorai_CurStates = StatusError;
+ else
+ if (14 == aorai_CurStates && ((res & 15) != 1 && (res & 1) != 0))
+ aorai_CurStates = StatusError;
+ else
+ if (14 == aorai_CurStates && (res & 15) == 1) aorai_CurStates = StatusOk1;
+ else
+ if (15 == aorai_CurStates && (res & 15) == 1) aorai_CurStates = StatusOk2;
+ else
+ if (16 == aorai_CurStates && (res & 15) == 1) aorai_CurStates = StatusOk3;
+ else
+ if (17 == aorai_CurStates && (res & 15) == 1) aorai_CurStates = StatusOk4;
+ else
+ if (18 == aorai_CurStates && (res & 15) == 1) aorai_CurStates = StatusOk5;
+ else
+ if (14 == aorai_CurStates && (res & 1) == 0)
+ aorai_CurStates = Wait1;
+ else
+ if (15 == aorai_CurStates && (res & 1) == 0)
+ aorai_CurStates = Wait2;
+ else
+ if (16 == aorai_CurStates && (res & 1) == 0)
+ aorai_CurStates = Wait3;
+ else
+ if (17 == aorai_CurStates && (res & 1) == 0)
+ aorai_CurStates = Wait4;
+ else
+ if (18 == aorai_CurStates && (res & 1) == 0)
+ aorai_CurStates = Wait5;
+ return;
+ }
+
+*/
+
+extern int ( /* missing proto */ Frama_C_interval)(int x_0, int x_1);
+
+/*@ ensures 0 ≤ \result < 0x100;
+ assigns \result;
+ assigns \result \from \nothing;
+ */
+int input_status(void)
+{
+ int tmp;
+ /*@ ghost input_status_pre_func(); */
+ tmp = Frama_C_interval(0x00,0xff);
+ /*@ ghost input_status_post_func(tmp); */
+ return tmp;
+}
+
+/*@ ghost
+ void input_data_pre_func(void)
+ {
+ /@ slevel full; @/
+ aorai_CurOpStatus = aorai_Called;
+ aorai_CurOperation = op_input_data;
+ aorai_StatesHistory_2 = aorai_StatesHistory_1;
+ aorai_StatesHistory_1 = aorai_CurStates;
+ if (9 == aorai_CurStates) aorai_CurStates = DataReq1;
+ else
+ if (10 == aorai_CurStates) aorai_CurStates = DataReq2;
+ else
+ if (11 == aorai_CurStates) aorai_CurStates = DataReq3;
+ else
+ if (12 == aorai_CurStates) aorai_CurStates = DataReq4;
+ else
+ if (13 == aorai_CurStates) aorai_CurStates = DataReq5;
+ else
+ if (8 == aorai_CurStates) aorai_CurStates = DataReqE;
+ else
+ if (23 == aorai_CurStates) aorai_CurStates = Error;
+ else
+ if (22 == aorai_CurStates) aorai_CurStates = Error;
+ else
+ if (21 == aorai_CurStates) aorai_CurStates = Error;
+ else
+ if (20 == aorai_CurStates) aorai_CurStates = Error;
+ else
+ if (19 == aorai_CurStates) aorai_CurStates = Error;
+ return;
+ }
+
+*/
+
+/*@ ghost
+ void input_data_post_func(int res)
+ {
+ /@ slevel full; @/
+ aorai_CurOpStatus = aorai_Terminated;
+ aorai_CurOperation = op_input_data;
+ aorai_StatesHistory_2 = aorai_StatesHistory_1;
+ aorai_StatesHistory_1 = aorai_CurStates;
+ if (5 == aorai_CurStates && (res & 128) == 0) {
+ aorai_CurStates = Complete;
+ aorai_y2 = res;
+ }
+ else
+ if (6 == aorai_CurStates) aorai_CurStates = Wait1;
+ else
+ if (5 == aorai_CurStates && (res & 192) == 192) aorai_CurStates = Wait1;
+ else
+ if (4 == aorai_CurStates && (res & 192) == 192) aorai_CurStates = Wait1;
+ else
+ if (3 == aorai_CurStates && (res & 192) == 192) aorai_CurStates = Wait1;
+ else
+ if (2 == aorai_CurStates && (res & 192) == 192) aorai_CurStates = Wait1;
+ else
+ if (1 == aorai_CurStates && (res & 128) == 0) aorai_CurStates = Wait1;
+ else
+ if (1 == aorai_CurStates && (res & 192) == 192) aorai_CurStates = Wait1;
+ else
+ if (5 == aorai_CurStates && (res & 192) == 128) aorai_CurStates = Wait2;
+ else
+ if (4 == aorai_CurStates && (res & 192) == 128)
+ aorai_CurStates = Wait2;
+ else
+ if (3 == aorai_CurStates && (res & 192) == 128)
+ aorai_CurStates = Wait2;
+ else
+ if (2 == aorai_CurStates && (res & 192) == 128)
+ aorai_CurStates = Wait2;
+ else
+ if (1 == aorai_CurStates && (res & 192) == 128)
+ aorai_CurStates = Wait2;
+ else
+ if (2 == aorai_CurStates && (res & 128) == 0) {
+ aorai_CurStates = Wait3;
+ aorai_x1 = res;
+ }
+ else
+ if (3 == aorai_CurStates && (res & 128) == 0) {
+ aorai_CurStates = Wait4;
+ aorai_x2 = res;
+ }
+ else
+ if (4 == aorai_CurStates && (res & 128) == 0) {
+ aorai_CurStates = Wait5;
+ aorai_y1 = res;
+ }
+ return;
+ }
+
+*/
+
+/*@ ensures 0 ≤ \result < 0x100;
+ assigns \result;
+ assigns \result \from \nothing;
+ */
+int input_data(void)
+{
+ int tmp;
+ /*@ ghost input_data_pre_func(); */
+ tmp = Frama_C_interval(0x00,0xff);
+ /*@ ghost input_data_post_func(tmp); */
+ return tmp;
+}
+
+/*@ ghost
+ void output_pre_func(int x, int y)
+ {
+ /@ slevel full; @/
+ aorai_CurOpStatus = aorai_Called;
+ aorai_CurOperation = op_output;
+ aorai_StatesHistory_2 = aorai_StatesHistory_1;
+ aorai_StatesHistory_1 = aorai_CurStates;
+ if (23 == aorai_CurStates) aorai_CurStates = Error;
+ else
+ if (22 == aorai_CurStates) aorai_CurStates = Error;
+ else
+ if (21 == aorai_CurStates) aorai_CurStates = Error;
+ else
+ if (20 == aorai_CurStates) aorai_CurStates = Error;
+ else
+ if (19 == aorai_CurStates) aorai_CurStates = Error;
+ else
+ if (13 == aorai_CurStates) aorai_CurStates = Error;
+ else
+ if (12 == aorai_CurStates) aorai_CurStates = Error;
+ else
+ if (11 == aorai_CurStates) aorai_CurStates = Error;
+ else
+ if (10 == aorai_CurStates) aorai_CurStates = Error;
+ else
+ if (9 == aorai_CurStates) aorai_CurStates = Error;
+ else
+ if (8 == aorai_CurStates) aorai_CurStates = Error;
+ else
+ if (0 == aorai_CurStates && (y != aorai_y1 +
+ 128 * aorai_y2 ||
+ x != aorai_x1 +
+ 128 * aorai_x2))
+ aorai_CurStates = Error;
+ else
+ if (0 == aorai_CurStates && (x == aorai_x1 +
+ 128 * aorai_x2 &&
+ y == aorai_y1 +
+ 128 * aorai_y2))
+ aorai_CurStates = Wait1;
+ return;
+ }
+
+*/
+
+/*@ ghost
+ void output_post_func(void)
+ {
+ /@ slevel full; @/
+ aorai_CurOpStatus = aorai_Terminated;
+ aorai_CurOperation = op_output;
+ aorai_StatesHistory_2 = aorai_StatesHistory_1;
+ aorai_StatesHistory_1 = aorai_CurStates;
+ if (19 == aorai_CurStates) aorai_CurStates = Wait1;
+ return;
+ }
+
+*/
+
+/*@ assigns \nothing; */
+void output(int x, int y)
+{
+ /*@ ghost output_pre_func(x,y); */
+ /*@ ghost output_post_func(); */
+ return;
+}
+
+int read(int *status)
+{
+ int __retres;
+ int s = input_status();
+ if (s & 0x01) {
+ int tmp_0;
+ *status = s & 0x0e;
+ tmp_0 = input_data();
+ __retres = tmp_0;
+ goto return_label;
+ }
+ __retres = -1;
+ return_label: ;
+ return __retres;
+}
+
+void main(void)
+{
+ /*@ ghost int aorai_Loop_Init_18; */
+ while (indefinitely) {
+ int status;
+ int data = read(& status);
+ if (data != -1) {
+ int tmp_0;
+ /*@ assert Eva: initialization: \initialized(&status); */ ;
+ if (status != 0) {
+ n = 0;
+ continue;
+ }
+ if (data & 0x80) {
+ if (n != 0) {
+ n = 0;
+ continue;
+ }
+ }
+ else {
+ /*@ split data & 0x40; */ ;
+ if (n == 0) continue;
+ }
+ tmp_0 = n;
+ n ++;
+ buffer[tmp_0] = data;
+ if (n == 5) {
+ if ((buffer[0] & 0x40) == 0) {
+ int x = buffer[1] + 0x80 * buffer[2];
+ int y = buffer[3] + 0x80 * buffer[4];
+ output(x,y);
+ Frama_C_show_aorai_state();
+ }
+ n = 0;
+ }
+ }
+ }
+ return;
+}
+
+
diff --git a/src/plugins/aorai/tests/ya/oracle_prove/serial.res.oracle b/src/plugins/aorai/tests/ya/oracle_prove/serial.res.oracle
new file mode 100644
index 00000000000..2572e58edad
--- /dev/null
+++ b/src/plugins/aorai/tests/ya/oracle_prove/serial.res.oracle
@@ -0,0 +1,310 @@
+[kernel] Parsing tests/ya/serial.c (with preprocessing)
+[kernel:typing:implicit-function-declaration] tests/ya/serial.c:81: Warning:
+ Calling undeclared function Frama_C_show_aorai_state. Old style K&R code?
+[aorai] Welcome to the Aorai plugin
+[kernel:annot:missing-spec] tests/ya/serial.c:45: 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:47: starting to merge loop iterations
+[eva] tests/ya/serial.c:52: Trace partitioning superposing up to 100 states
+[eva] tests/ya/serial.c:52: Trace partitioning superposing up to 300 states
+[aorai] tests/ya/serial.c:81: Wait1 <- Wait1 <- Complete
+[aorai] tests/ya/serial.c:81: Error <- Error <- Complete
+[aorai] tests/ya/serial.c:81: Complete <- Complete <- Complete
+[aorai] tests/ya/serial.c:81: Wait1 <- Wait1 <- Complete
+[aorai] tests/ya/serial.c:81: Error <- Error <- Complete
+[aorai] tests/ya/serial.c:81: Complete <- Complete <- Complete
+[eva] tests/ya/serial.c:52: Trace partitioning superposing up to 500 states
+[eva:alarm] tests/ya/serial.c:54: Warning:
+ accessing uninitialized left-value. assert \initialized(&status);
+[eva] tests/ya/serial.c:52: Trace partitioning superposing up to 700 states
+[eva] tests/ya/serial.c:52: Trace partitioning superposing up to 900 states
+[eva] tests/ya/serial.c:52: Trace partitioning superposing up to 1200 states
+[eva] tests/ya/serial.c:52: Trace partitioning superposing up to 1500 states
+[aorai] tests/ya/serial.c:81: Error <- Error <- Error
+[aorai] tests/ya/serial.c:81: Error <- Error <- Error
+[eva] tests/ya/serial.c:52: Trace partitioning superposing up to 1700 states
+[eva] tests/ya/serial.c:52: Trace partitioning superposing up to 1900 states
+[eva] tests/ya/serial.c:52: Trace partitioning superposing up to 2000 states
+[eva] tests/ya/serial.c:52: 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.
+ ----------------------------------------------------------------------------
+[kernel] Parsing TMPDIR/aorai_serial_0.i (no preprocessing)
+[kernel:typing:implicit-function-declaration] TMPDIR/aorai_serial_0.i:176: 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
diff --git a/src/plugins/aorai/tests/ya/serial.c b/src/plugins/aorai/tests/ya/serial.c
new file mode 100644
index 00000000000..2e8b8bc3d45
--- /dev/null
+++ b/src/plugins/aorai/tests/ya/serial.c
@@ -0,0 +1,88 @@
+/* run.config*
+ OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -aorai-test 1 -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@ -aorai-no-acceptance -aorai-instrumentation-history 2 -aorai-no-generate-annotations -aorai-no-generate-deterministic-lemmas -then-last -eva -eva-partition-value n -eva-ilevel 256
+*/
+
+#include "__fc_builtin.h"
+#include "aorai/aorai.h"
+
+
+/*@ assigns \result \from \nothing;
+ ensures 0 <= \result < 0x100; */
+int input_status(void) {
+ return Frama_C_interval(0x00, 0xff);
+}
+
+/*@ assigns \result \from \nothing;
+ ensures 0 <= \result < 0x100; */
+int input_data(void) {
+ return Frama_C_interval(0x00, 0xff);
+}
+
+/*@ assigns \nothing; */
+void output(int x, int y) {
+ // do nothing
+}
+
+
+int read(int *status)
+{
+ int s = input_status();
+
+ if (s & 0x01) {
+ *status = s & 0x0e;
+ return input_data();
+ }
+
+ return -1;
+}
+
+
+volatile int indefinitely;
+
+int buffer[5]; // buffer to store bytes
+int n = 0; // number of bytes received
+
+void main(void)
+{
+ while (indefinitely)
+ {
+ int status;
+ int data = read(&status);
+
+ if (data != -1) { // data is present
+
+ if (status != 0) { // read issue
+ n = 0;
+ continue;
+ }
+ if (data & 0x80) { // status received
+ if (n != 0) { // but data was expected
+ n = 0;
+ continue;
+ }
+ //@ split data & 0x40;
+ }
+ else { // data receieved
+ if (n == 0) { // but status was expected}
+ continue;
+ }
+ }
+
+ buffer[n++] = data;
+
+ if (n == 5) { // the packet is completely read
+ if ((buffer[0] & 0x40) == 0) // it is a release action
+ {
+ int x = buffer[1] + 0x80 * buffer[2];
+ int y = buffer[3] + 0x80 * buffer[4];
+ output(x, y);
+ /* "Error" state should show up as, for now, it is hard to prove
+ the metavariable équation in the input automaton */
+ Frama_C_show_aorai_state();
+ }
+
+ n = 0;
+ }
+ }
+ }
+}
diff --git a/src/plugins/aorai/tests/ya/serial.ya b/src/plugins/aorai/tests/ya/serial.ya
new file mode 100644
index 00000000000..8fde0de6e29
--- /dev/null
+++ b/src/plugins/aorai/tests/ya/serial.ya
@@ -0,0 +1,160 @@
+%init : Wait1;
+%deterministic;
+%observables: input_status, input_data, output;
+
+$x1 : int;
+$x2 : int;
+$y1 : int;
+$y2 : int;
+
+Error : { 0 } -> Error;
+
+Wait1 :
+ { CALL(input_status) } -> StatusReq1
+| { CALL(input_data) } -> Error
+| { CALL(output) } -> Error
+| other -> Wait1
+;
+
+Wait2 :
+ { CALL(input_status) } -> StatusReq2
+| { CALL(input_data) } -> Error
+| { CALL(output) } -> Error
+| other -> Wait2
+;
+
+Wait3 :
+ { CALL(input_status) } -> StatusReq3
+| { CALL(input_data) } -> Error
+| { CALL(output) } -> Error
+| other -> Wait3
+;
+
+Wait4 :
+ { CALL(input_status) } -> StatusReq4
+| { CALL(input_data) } -> Error
+| { CALL(output) } -> Error
+| other -> Wait4
+;
+
+Wait5 :
+ { CALL(input_status) } -> StatusReq5
+| { CALL(input_data) } -> Error
+| { CALL(output) } -> Error
+| other -> Wait5
+;
+
+StatusReq1 :
+ { input_status().\result & 1 == 0 } -> Wait1
+| { input_status().\result & 15 == 1 } -> StatusOk1
+| other -> StatusError
+;
+
+StatusReq2 :
+ { input_status().\result & 1 == 0 } -> Wait2
+| { input_status().\result & 15 == 1 } -> StatusOk2
+| other -> StatusError
+;
+
+StatusReq3 :
+ { input_status().\result & 1 == 0 } -> Wait3
+| { input_status().\result & 15 == 1 } -> StatusOk3
+| other -> StatusError
+;
+
+StatusReq4 :
+ { input_status().\result & 1 == 0 } -> Wait4
+| { input_status().\result & 15 == 1 } -> StatusOk4
+| other -> StatusError
+;
+
+StatusReq5 :
+ { input_status().\result & 1 == 0 } -> Wait5
+| { input_status().\result & 15 == 1 } -> StatusOk5
+| other -> StatusError
+;
+
+StatusError :
+ { CALL(input_status) } -> StatusReq1
+| { CALL(input_data) } -> DataReqE
+| { CALL(output) } -> Error
+| other -> StatusError
+;
+
+StatusOk1 :
+ { CALL(input_status) } -> StatusReq1
+| { CALL(input_data) } -> DataReq1
+| { CALL(output) } -> Error
+| other -> StatusOk1
+;
+
+StatusOk2 :
+ { CALL(input_status) } -> StatusReq2
+| { CALL(input_data) } -> DataReq2
+| { CALL(output) } -> Error
+| other -> StatusOk2
+;
+
+StatusOk3 :
+ { CALL(input_status) } -> StatusReq3
+| { CALL(input_data) } -> DataReq3
+| { CALL(output) } -> Error
+| other -> StatusOk3
+;
+
+StatusOk4 :
+ { CALL(input_status) } -> StatusReq4
+| { CALL(input_data) } -> DataReq4
+| { CALL(output) } -> Error
+| other -> StatusOk4
+;
+
+StatusOk5 :
+ { CALL(input_status) } -> StatusReq5
+| { CALL(input_data) } -> DataReq5
+| { CALL(output) } -> Error
+| other -> StatusOk5
+;
+
+DataReqE :
+ { RETURN(input_data) } -> Wait1
+;
+
+DataReq1 :
+ { input_data().\result & 192 == 128 } -> Wait2
+| { input_data().\result & 192 == 192 } -> Wait1
+| { input_data().\result & 128 == 0 } -> Wait1
+;
+
+DataReq2 :
+ { input_data().\result & 192 == 128 } -> Wait2
+| { input_data().\result & 192 == 192 } -> Wait1
+| { input_data().\result & 128 == 0 } $x1 := \result -> Wait3
+;
+
+DataReq3 :
+ { input_data().\result & 192 == 128 } -> Wait2
+| { input_data().\result & 192 == 192 } -> Wait1
+| { input_data().\result & 128 == 0 } $x2 := \result -> Wait4
+;
+
+DataReq4 :
+ { input_data().\result & 192 == 128 } -> Wait2
+| { input_data().\result & 192 == 192 } -> Wait1
+| { input_data().\result & 128 == 0 } $y1 := \result -> Wait5
+;
+
+DataReq5 :
+ { input_data().\result & 192 == 128 } -> Wait2
+| { input_data().\result & 192 == 192 } -> Wait1
+| { input_data().\result & 128 == 0 } $y2 := \result -> Complete
+;
+
+Complete :
+ { CALL(output) && output().x == $x1 + 128 * $x2 && output().y == $y1 + 128 * $y2 } -> Wait1
+| { CALL(output) && (output().x != $x1 + 128 * $x2 || output().y != $y1 + 128 * $y2) } -> Error
+| { CALL(input_status) } -> StatusReq1
+| { CALL(input_data) } -> Error
+| other -> Complete
+;
+
--
GitLab