diff --git a/src/kernel_services/abstract_interp/int_set.ml b/src/kernel_services/abstract_interp/int_set.ml
index d4c45b4012f5f8d689e146ac34dcea3339bf10b4..47c3b99595189fb6c8d3d028ffa649fba37b71c6 100644
--- a/src/kernel_services/abstract_interp/int_set.ml
+++ b/src/kernel_services/abstract_interp/int_set.ml
@@ -111,12 +111,52 @@ let compare s1 s2 =
let equal e1 e2 = compare e1 e2 = 0
+(* Used to print a compact representation of large integer sets. *)
+type set_or_itv =
+ | Set of Int.t array
+ | Itv of Int.t * Int.t
+
+(* Converts a set into an ordered list of sets and intervals, fusing adjacent
+ integers into intervals. *)
+let fuse_intervals s =
+ (* Add interval [b..e[ to the list [acc]. The interval can be a singleton. *)
+ let add_itv acc (b, e) =
+ let nb = Int.to_int_exn (Int.sub e b) in
+ (* If the interval is too small, uses a Set instead of Itv. *)
+ if nb > 3
+ then Itv (b, Int.pred e) :: acc
+ else
+ let a = Array.init nb (fun i -> Int.add b (Int.of_int i)) in
+ (* If the last element of [acc] is a Set, adds [a] at its end. *)
+ match acc with
+ | Set a' :: tl -> Set (Array.append a' a) :: tl
+ | _ -> Set a :: acc
+ in
+ (* [start..prev[ is the current interval being built. *)
+ let f (acc, start, prev) curr =
+ if Int.equal prev curr
+ then (acc, start, Int.succ curr)
+ else (add_itv acc (start, prev), curr, Int.succ curr)
+ in
+ let list, start, curr = Array.fold_left f ([], s.(0), s.(0)) s in
+ List.rev (add_itv list (start, curr))
+
+let pretty_array =
+ Pretty_utils.pp_iter ~pre:"@[<hov 1>{" ~suf:"}@]" ~sep:";@ "
+ Array.iter Int.pretty
+
+let pretty_set_or_itv fmt = function
+ | Set a -> pretty_array fmt a
+ | Itv (b, e) -> Format.fprintf fmt "[%a..%a]" Int.pretty b Int.pretty e
+
let pretty fmt s =
- Pretty_utils.pp_iter
- ~pre:"@[<hov 1>{"
- ~suf:"}@]"
- ~sep:";@ "
- Array.iter Int.pretty fmt s
+ if Array.length s < 10
+ then pretty_array fmt s
+ else
+ let union = Unicode.union_string () in
+ let sep = Scanf.format_from_string ("@ " ^ union ^ " ") "" in
+ Pretty_utils.pp_iter ~pre:"@[<hov 1>" ~suf:"@]" ~sep
+ List.iter pretty_set_or_itv fmt (fuse_intervals s)
include Datatype.Make_with_collections
(struct
diff --git a/src/plugins/aorai/tests/ya/oracle/serial.res.oracle b/src/plugins/aorai/tests/ya/oracle/serial.res.oracle
index f6cbbacc42cbecac9183de261ba17490eddb4cf3..fb69185c9377884bf38986c27bf55948689bb215 100644
--- a/src/plugins/aorai/tests/ya/oracle/serial.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/serial.res.oracle
@@ -38,36 +38,9 @@
[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_x1 ∈ [0..127]
+ aorai_x2 ∈ [0..127]
+ aorai_y1 ∈ [0..127]
aorai_y2 ∈ [0..2147483647]
aorai_CurOperation ∈ {2}
aorai_CurOpStatus ∈ {1}
@@ -82,36 +55,9 @@
aorai_StatesHistory_2 ∈ {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_x1 ∈ [0..127]
+ aorai_x2 ∈ [0..127]
+ aorai_y1 ∈ [0..127]
aorai_y2 ∈ [0..2147483647]
aorai_CurOperation ∈ {2}
aorai_CurOpStatus ∈ {1}
@@ -121,7 +67,7 @@
[eva:final-states] Values at end of function input_status_post_func:
aorai_CurOperation ∈ {1}
aorai_CurOpStatus ∈ {1}
- aorai_CurStates ∈ {8; 9; 10; 11; 12; 13; 19; 20; 21; 22; 23}
+ aorai_CurStates ∈ [8..13] ∪ [19..23]
aorai_StatesHistory_1 ∈ {14; 15; 16; 17; 18}
aorai_StatesHistory_2 ∈ {0; 19; 20; 21; 22; 23}
[eva:final-states] Values at end of function input_status_pre_func:
@@ -129,12 +75,12 @@
aorai_CurOpStatus ∈ {0}
aorai_CurStates ∈ {14; 15; 16; 17; 18}
aorai_StatesHistory_1 ∈ {0; 19; 20; 21; 22; 23}
- aorai_StatesHistory_2 ∈ {1; 2; 3; 4; 5; 6; 14; 15; 16; 17; 18; 19}
+ aorai_StatesHistory_2 ∈ [1..6] ∪ [14..19]
[eva:final-states] Values at end of function input_status:
Frama_C_entropy_source ∈ [--..--]
aorai_CurOperation ∈ {1}
aorai_CurOpStatus ∈ {1}
- aorai_CurStates ∈ {8; 9; 10; 11; 12; 13; 19; 20; 21; 22; 23}
+ aorai_CurStates ∈ [8..13] ∪ [19..23]
aorai_StatesHistory_1 ∈ {14; 15; 16; 17; 18}
aorai_StatesHistory_2 ∈ {0; 19; 20; 21; 22; 23}
[eva:final-states] Values at end of function output_post_func:
@@ -157,122 +103,33 @@
aorai_StatesHistory_2 ∈ {0}
[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}
+ s ∈ [0..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_x1 ∈ [0..127]
+ aorai_x2 ∈ [0..127]
+ aorai_y1 ∈ [0..127]
aorai_y2 ∈ [0..2147483647]
aorai_CurOperation ∈ {1; 2}
aorai_CurOpStatus ∈ {1}
aorai_CurStates ∈ {0; 19; 20; 21; 22; 23}
- aorai_StatesHistory_1 ∈ {1; 2; 3; 4; 5; 6; 14; 15; 16; 17; 18}
- aorai_StatesHistory_2 ∈ {0; 8; 9; 10; 11; 12; 13; 19; 20; 21; 22; 23}
+ aorai_StatesHistory_1 ∈ [1..6] ∪ [14..18]
+ aorai_StatesHistory_2 ∈ {0} ∪ [8..13] ∪ [19..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}
+ buffer[0] ∈ {0} ∪ [128..255]
+ [1..2] ∈ [0..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_x1 ∈ [0..127]
+ aorai_x2 ∈ [0..127]
+ aorai_y1 ∈ [0..127]
aorai_y2 ∈ [0..2147483647]
aorai_CurOperation ∈ {0; 1; 2}
aorai_CurOpStatus ∈ {0; 1}
aorai_CurStates ∈ {0; 19; 20; 21; 22; 23}
- aorai_StatesHistory_1 ∈ {1; 2; 3; 4; 5; 6; 14; 15; 16; 17; 18; 19}
- aorai_StatesHistory_2 ∈ {0; 8; 9; 10; 11; 12; 13; 19; 20; 21; 22; 23}
+ aorai_StatesHistory_1 ∈ [1..6] ∪ [14..19]
+ aorai_StatesHistory_2 ∈ {0} ∪ [8..13] ∪ [19..23]
[eva:summary] ====== ANALYSIS SUMMARY ======
----------------------------------------------------------------------------
11 functions analyzed (out of 11): 100% coverage.
diff --git a/tests/value/ilevel.c b/tests/value/ilevel.c
new file mode 100644
index 0000000000000000000000000000000000000000..cd68ed54ea80a0f2202a7373c2563e064534bfa7
--- /dev/null
+++ b/tests/value/ilevel.c
@@ -0,0 +1,48 @@
+/* run.config*
+ PLUGIN: @EVA_MAIN_PLUGINS@ inout,slicing
+ OPT: -eva @EVA_CONFIG@ -slice-return main -then-on "Slicing export" -eva -eva-ilevel 16 -eva-show-progress -then-on "default" -eva-ilevel 17 -then -eva-ilevel 48
+ STDOPT: +"-eva-ilevel 400 -main large_ilevel"
+*/
+
+// Test in particular that ilevel is by-project, even though it is an ocaml ref
+
+#include "__fc_builtin.h"
+
+volatile int nondet;
+int i, j, k, l;
+
+int main () {
+ do { i = nondet; }
+ while (! (0 <= i && i < 8));
+
+ do { j = nondet; }
+ while (! (0 <= j && j < 17));
+
+ k = j;
+ if (k == 16) k = 15;
+
+ l = nondet;
+ if (nondet) {
+ //@ assert 0 <= l <= 4;
+ } else {
+ //@ assert 6 <= l <= 9;
+ }
+ Frama_C_show_each(l); // Possible problem with cache on offsetmap join
+
+ return i+j+k+l;
+}
+
+/* Tests printing large integer sets. */
+void large_ilevel (void) {
+ int i = Frama_C_interval(0, 10);
+ int j = nondet ? i : i - 25;
+ int k = Frama_C_interval(100, 200);
+ if (k == 128) return;
+
+ int a[11] = {53, 17, 64, 99, 25, 12, 72, 81, 404, 303, -101};
+
+ int s2 = nondet ? 40 : (nondet ? 41 : 42);
+ int s1 = a[i];
+
+ int x = nondet ? (nondet ? j : k) : (nondet ? s1 : s2);
+}
diff --git a/tests/value/ilevel.i b/tests/value/ilevel.i
deleted file mode 100644
index 30aaf6a78b8fe2795a46249604b5e0e6f7028aa7..0000000000000000000000000000000000000000
--- a/tests/value/ilevel.i
+++ /dev/null
@@ -1,27 +0,0 @@
-/* run.config*
- PLUGIN: @EVA_MAIN_PLUGINS@ inout,slicing
- OPT: -eva @EVA_CONFIG@ -slice-return main -then-on "Slicing export" -eva -eva-ilevel 16 -eva-show-progress -then-on "default" -eva-ilevel 17 -then -eva-ilevel 48
-*/
-// Test in particular that ilevel is by-project, even though it is an ocaml ref
-volatile int v;
-int i, j, k, l;
-int main () {
- do { i = v; }
- while (! (0 <= i && i < 8));
-
- do { j = v; }
- while (! (0 <= j && j < 17));
-
- k = j;
- if (k == 16) k = 15;
-
- l = v;
- if (v) {
- //@ assert 0 <= l <= 4;
- } else {
- //@ assert 6 <= l <= 9;
- }
- Frama_C_show_each(l); // Possible problem with cache on offsetmap join
-
- return i+j+k+l;
-}
diff --git a/tests/value/oracle/ilevel.res.oracle b/tests/value/oracle/ilevel.0.res.oracle
similarity index 68%
rename from tests/value/oracle/ilevel.res.oracle
rename to tests/value/oracle/ilevel.0.res.oracle
index 042c98daaa39125f33b39a30cbfe8798a9b6d8b4..897c9e808ca3ad9d067d85a82e9051411385263d 100644
--- a/tests/value/oracle/ilevel.res.oracle
+++ b/tests/value/oracle/ilevel.0.res.oracle
@@ -1,18 +1,18 @@
-[kernel] Parsing ilevel.i (no preprocessing)
+[kernel] Parsing ilevel.c (with preprocessing)
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
- v ∈ [--..--]
+ nondet ∈ [--..--]
i ∈ {0}
j ∈ {0}
k ∈ {0}
l ∈ {0}
-[eva] ilevel.i:9: starting to merge loop iterations
-[eva] ilevel.i:12: starting to merge loop iterations
-[eva:alarm] ilevel.i:20: Warning: assertion got status unknown.
-[eva:alarm] ilevel.i:22: Warning: assertion got status unknown.
-[eva] ilevel.i:24: Frama_C_show_each: [0..9]
+[eva] ilevel.c:15: starting to merge loop iterations
+[eva] ilevel.c:18: starting to merge loop iterations
+[eva:alarm] ilevel.c:26: Warning: assertion got status unknown.
+[eva:alarm] ilevel.c:28: Warning: assertion got status unknown.
+[eva] ilevel.c:30: Frama_C_show_each: [0..9]
[eva] Recording results for main
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
@@ -43,14 +43,14 @@
[eva] Computing initial state
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
- v ∈ [--..--]
+ nondet ∈ [--..--]
i ∈ {0}
j ∈ {0}
k ∈ {0}
l ∈ {0}
-[eva] ilevel.i:9: starting to merge loop iterations
-[eva] ilevel.i:12: starting to merge loop iterations
-[eva:alarm] ilevel.i:26: Warning:
+[eva] ilevel.c:15: starting to merge loop iterations
+[eva] ilevel.c:18: starting to merge loop iterations
+[eva:alarm] ilevel.c:32: Warning:
signed overflow. assert (int)((int)(i + j) + k) + l ≤ 2147483647;
[eva] Recording results for main
[eva] done for function main
@@ -58,47 +58,44 @@
[eva:final-states] Values at end of function main:
i ∈ {0; 1; 2; 3; 4; 5; 6; 7}
j ∈ [0..16]
- k ∈ {0; 1; 2; 3; 4; 5; 6; 7; 8; 9; 10; 11; 12; 13; 14; 15}
+ k ∈ [0..15]
l ∈ [--..--]
__retres ∈ [--..--]
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
- v ∈ [--..--]
+ nondet ∈ [--..--]
i ∈ {0}
j ∈ {0}
k ∈ {0}
l ∈ {0}
-[eva] ilevel.i:24: Frama_C_show_each: {0; 1; 2; 3; 4; 6; 7; 8; 9}
+[eva] ilevel.c:30: Frama_C_show_each: {0; 1; 2; 3; 4; 6; 7; 8; 9}
[eva] Recording results for main
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function main:
i ∈ {0; 1; 2; 3; 4; 5; 6; 7}
- j ∈ {0; 1; 2; 3; 4; 5; 6; 7; 8; 9; 10; 11; 12; 13; 14; 15; 16}
- k ∈ {0; 1; 2; 3; 4; 5; 6; 7; 8; 9; 10; 11; 12; 13; 14; 15}
+ j ∈ [0..16]
+ k ∈ [0..15]
l ∈ {0; 1; 2; 3; 4; 6; 7; 8; 9}
__retres ∈ [0..47]
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
- v ∈ [--..--]
+ nondet ∈ [--..--]
i ∈ {0}
j ∈ {0}
k ∈ {0}
l ∈ {0}
-[eva] ilevel.i:24: Frama_C_show_each: {0; 1; 2; 3; 4; 6; 7; 8; 9}
+[eva] ilevel.c:30: Frama_C_show_each: {0; 1; 2; 3; 4; 6; 7; 8; 9}
[eva] Recording results for main
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function main:
i ∈ {0; 1; 2; 3; 4; 5; 6; 7}
- j ∈ {0; 1; 2; 3; 4; 5; 6; 7; 8; 9; 10; 11; 12; 13; 14; 15; 16}
- k ∈ {0; 1; 2; 3; 4; 5; 6; 7; 8; 9; 10; 11; 12; 13; 14; 15}
+ j ∈ [0..16]
+ k ∈ [0..15]
l ∈ {0; 1; 2; 3; 4; 6; 7; 8; 9}
- __retres ∈
- {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}
+ __retres ∈ [0..47]
diff --git a/tests/value/oracle/ilevel.1.res.oracle b/tests/value/oracle/ilevel.1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..af0704f7b5dc3605bcf5703ca05d7133098127fb
--- /dev/null
+++ b/tests/value/oracle/ilevel.1.res.oracle
@@ -0,0 +1,63 @@
+[kernel] Parsing ilevel.c (with preprocessing)
+[eva] Analyzing a complete application starting at large_ilevel
+[eva] Computing initial state
+[eva] Initial state computed
+[eva:initial-state] Values of globals at initialization
+ nondet ∈ [--..--]
+ i ∈ {0}
+ j ∈ {0}
+ k ∈ {0}
+ l ∈ {0}
+[eva] computing for function Frama_C_interval <- large_ilevel.
+ Called from ilevel.c:37.
+[eva] using specification for function Frama_C_interval
+[eva] ilevel.c:37:
+ function Frama_C_interval: precondition 'order' got status valid.
+[eva] Done for function Frama_C_interval
+[eva] computing for function Frama_C_interval <- large_ilevel.
+ Called from ilevel.c:39.
+[eva] ilevel.c:39:
+ function Frama_C_interval: precondition 'order' got status valid.
+[eva] Done for function Frama_C_interval
+[eva] Recording results for large_ilevel
+[eva] done for function large_ilevel
+[eva] ====== VALUES COMPUTED ======
+[eva:final-states] Values at end of function large_ilevel:
+ Frama_C_entropy_source ∈ [--..--]
+ i_0 ∈ [0..10]
+ j_0 ∈ [-25..-15] ∪ [0..10]
+ k_0 ∈ [100..200]
+ a[0] ∈ {53}
+ [1] ∈ {17}
+ [2] ∈ {64}
+ [3] ∈ {99}
+ [4] ∈ {25}
+ [5] ∈ {12}
+ [6] ∈ {72}
+ [7] ∈ {81}
+ [8] ∈ {404}
+ [9] ∈ {303}
+ [10] ∈ {-101}
+ s2 ∈ {40; 41; 42}
+ s1 ∈ {-101; 12; 17; 25; 53; 64; 72; 81; 99; 303; 404}
+ x ∈
+ {-101} ∪ [-25..-15] ∪ [0..10]
+ ∪ {12; 17; 25; 40; 41; 42; 53; 64; 72; 81} ∪ [99..127] ∪ [129..200]
+ ∪ {303; 404}
+[from] Computing for function large_ilevel
+[from] Computing for function Frama_C_interval <-large_ilevel
+[from] Done for function Frama_C_interval
+[from] Done for function large_ilevel
+[from] ====== DEPENDENCIES COMPUTED ======
+ These dependencies hold at termination for the executions that terminate:
+[from] Function Frama_C_interval:
+ Frama_C_entropy_source FROM Frama_C_entropy_source (and SELF)
+ \result FROM Frama_C_entropy_source; min; max
+[from] Function large_ilevel:
+ Frama_C_entropy_source FROM Frama_C_entropy_source (and SELF)
+[from] ====== END OF DEPENDENCIES ======
+[inout] Out (internal) for function large_ilevel:
+ Frama_C_entropy_source; i_0; j_0; tmp_0; k_0; a[0..10]; s2; tmp_2;
+ tmp_3; s1; x; tmp_4; tmp_5; tmp_6
+[inout] Inputs for function large_ilevel:
+ Frama_C_entropy_source; nondet