diff --git a/src/kernel_services/abstract_interp/int_set.ml b/src/kernel_services/abstract_interp/int_set.ml
index d4c45b4012f5f8d689e146ac34dcea3339bf10b4..9f640500ebaa1a1e474d7ba75933226ab4b72496 100644
--- a/src/kernel_services/abstract_interp/int_set.ml
+++ b/src/kernel_services/abstract_interp/int_set.ml
@@ -111,12 +111,56 @@ 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) + 1 in
+ (* If the interval is too small, uses a Set instead of Itv. *)
+ if nb > 3
+ then Itv (b, 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 (Int.pred curr)
+ then (acc, start, curr)
+ else (add_itv acc (start, prev), curr, curr)
+ in
+ let r = ref ([], s.(0), s.(0)) in
+ for i = 1 to Array.length s - 1 do
+ r := f !r s.(i)
+ done;
+ let list, start, curr = !r 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/oracle/ilevel.res.oracle b/tests/value/oracle/ilevel.res.oracle
index 042c98daaa39125f33b39a30cbfe8798a9b6d8b4..ccd33cb03cc2139805898fbdf5c29615b9dd90d7 100644
--- a/tests/value/oracle/ilevel.res.oracle
+++ b/tests/value/oracle/ilevel.res.oracle
@@ -58,7 +58,7 @@
[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
@@ -76,8 +76,8 @@
[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
@@ -95,10 +95,7 @@
[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]