Skip to content

Commit 84d9d27

Browse files
michael-schwarzmichael-schwarz
authored
Merge pull request #1695 from goblint/issue_1686
Unit tests: Remove usages of polymorphic equality
2 parents aa7e1d2 + 548a8fe commit 84d9d27

File tree

1 file changed

+146
-136
lines changed

1 file changed

+146
-136
lines changed

‎tests/unit/cdomains/intDomainTest.ml‎

Lines changed: 146 additions & 136 deletions
Original file line numberDiff line numberDiff line change
@@ -17,81 +17,85 @@ struct
1717
let itrue = I.of_bool true
1818
let ifalse = I.of_bool false
1919

20+
let assert_poly_equal = assert_equal
21+
let assert_equal x y =
22+
assert_equal ~cmp:I.equal ~printer:I.show x y
23+
2024

2125
let test_int_comp _ =
22-
assert_equal ~printer:I.show izero (I.of_int zero);
23-
assert_equal ~printer:I.show ione (I.of_int one);
24-
assert_equal ~printer:I.show itrue (I.of_bool true);
25-
assert_equal ~printer:I.show ifalse(I.of_bool false);
26-
assert_equal (Some one ) (I.to_int ione);
27-
assert_equal (Some zero) (I.to_int izero);
28-
assert_equal (Some zero) (I.to_int ifalse)
26+
assert_equal izero (I.of_int zero);
27+
assert_equal ione (I.of_int one);
28+
assert_equal itrue (I.of_bool true);
29+
assert_equal ifalse(I.of_bool false);
30+
assert_poly_equal (Some one ) (I.to_int ione);
31+
assert_poly_equal (Some zero) (I.to_int izero);
32+
assert_poly_equal (Some zero) (I.to_int ifalse)
2933

3034

3135
let test_bool _ =
32-
assert_equal (Some true ) (I.to_bool ione);
33-
assert_equal (Some false) (I.to_bool izero);
34-
assert_equal (Some true ) (I.to_bool itrue);
35-
assert_equal (Some false) (I.to_bool ifalse);
36-
assert_equal ~printer:I.show itrue (I.lt ione itwo);
37-
assert_equal ~printer:I.show ifalse (I.gt ione itwo);
38-
assert_equal ~printer:I.show itrue (I.le ione ione);
39-
assert_equal ~printer:I.show ifalse (I.ge izero itwo);
40-
assert_equal ~printer:I.show itrue (I.eq izero izero);
41-
assert_equal ~printer:I.show ifalse (I.ne ione ione)
36+
assert_poly_equal (Some true ) (I.to_bool ione);
37+
assert_poly_equal (Some false) (I.to_bool izero);
38+
assert_poly_equal (Some true ) (I.to_bool itrue);
39+
assert_poly_equal (Some false) (I.to_bool ifalse);
40+
assert_equal itrue (I.lt ione itwo);
41+
assert_equal ifalse (I.gt ione itwo);
42+
assert_equal itrue (I.le ione ione);
43+
assert_equal ifalse (I.ge izero itwo);
44+
assert_equal itrue (I.eq izero izero);
45+
assert_equal ifalse (I.ne ione ione)
4246

4347

4448
let test_neg _ =
45-
assert_equal ~printer:I.show in5 (I.neg i5);
46-
assert_equal ~printer:I.show i5 (I.neg (I.neg i5));
47-
assert_equal ~printer:I.show izero (I.neg izero)
49+
assert_equal in5 (I.neg i5);
50+
assert_equal i5 (I.neg (I.neg i5));
51+
assert_equal izero (I.neg izero)
4852

4953

5054
let test_add _ =
51-
assert_equal ~printer:I.show ione (I.add izero ione);
52-
assert_equal ~printer:I.show ione (I.add ione izero);
53-
assert_equal ~printer:I.show izero(I.add izero izero)
55+
assert_equal ione (I.add izero ione);
56+
assert_equal ione (I.add ione izero);
57+
assert_equal izero(I.add izero izero)
5458

5559

5660
let test_sub _ =
57-
assert_equal ~printer:I.show ione (I.sub izero iminus_one);
58-
assert_equal ~printer:I.show ione (I.sub ione izero);
59-
assert_equal ~printer:I.show izero(I.sub izero izero)
61+
assert_equal ione (I.sub izero iminus_one);
62+
assert_equal ione (I.sub ione izero);
63+
assert_equal izero(I.sub izero izero)
6064

6165

6266
let test_mul _ =
63-
assert_equal ~printer:I.show izero(I.mul izero iminus_one);
64-
assert_equal ~printer:I.show izero(I.mul izero izero);
65-
assert_equal ~printer:I.show ione (I.mul ione ione);
66-
assert_equal ~printer:I.show i42 (I.mul ione i42)
67+
assert_equal izero(I.mul izero iminus_one);
68+
assert_equal izero(I.mul izero izero);
69+
assert_equal ione (I.mul ione ione);
70+
assert_equal i42 (I.mul ione i42)
6771

6872

6973
let test_div _ =
70-
assert_equal ~printer:I.show ione (I.div ione ione);
71-
assert_equal ~printer:I.show ione (I.div i5 i5);
72-
assert_equal ~printer:I.show i5 (I.div i5 ione);
73-
assert_equal ~printer:I.show in5 (I.div i5 iminus_one);
74+
assert_equal ione (I.div ione ione);
75+
assert_equal ione (I.div i5 i5);
76+
assert_equal i5 (I.div i5 ione);
77+
assert_equal in5 (I.div i5 iminus_one);
7478
assert_bool "div_by_0" (try I.is_top (I.div i5 izero) with Division_by_zero -> true)
7579

7680

7781
let test_rem _ =
78-
assert_equal ~printer:I.show ione (I.rem ione i5);
79-
assert_equal ~printer:I.show izero(I.rem izero i5);
80-
assert_equal ~printer:I.show itwo (I.rem i42 i5);
81-
assert_equal ~printer:I.show itwo (I.rem i42 in5)
82+
assert_equal ione (I.rem ione i5);
83+
assert_equal izero(I.rem izero i5);
84+
assert_equal itwo (I.rem i42 i5);
85+
assert_equal itwo (I.rem i42 in5)
8286

8387

8488
let test_bit _ =
85-
assert_equal ~printer:I.show iminus_one (I.lognot izero);
86-
assert_equal ~printer:I.show iminus_two (I.lognot ione);
87-
assert_equal ~printer:I.show i5 (I.logand i5 i5);
88-
assert_equal ~printer:I.show i4 (I.logand i5 i4);
89-
assert_equal ~printer:I.show i5 (I.logor i4 ione);
90-
assert_equal ~printer:I.show ione (I.logxor i4 i5);
91-
assert_equal ~printer:I.show itwo (I.shift_left ione ione );
92-
assert_equal ~printer:I.show ione (I.shift_left ione izero);
93-
assert_equal ~printer:I.show ione (I.shift_right itwo ione);
94-
assert_equal ~printer:I.show izero(I.shift_right ione ione)
89+
assert_equal iminus_one (I.lognot izero);
90+
assert_equal iminus_two (I.lognot ione);
91+
assert_equal i5 (I.logand i5 i5);
92+
assert_equal i4 (I.logand i5 i4);
93+
assert_equal i5 (I.logor i4 ione);
94+
assert_equal ione (I.logxor i4 i5);
95+
assert_equal itwo (I.shift_left ione ione );
96+
assert_equal ione (I.shift_left ione izero);
97+
assert_equal ione (I.shift_right itwo ione);
98+
assert_equal izero(I.shift_right ione ione)
9599

96100

97101
let test () =
@@ -112,91 +116,97 @@ module Ikind = struct let ikind () = Cil.ILong end
112116
module A = IntTest (IntDomain.Integers (IntOps.BigIntOps))
113117
module B = IntTest (IntDomain.Flat (IntDomain.Integers (IntOps.BigIntOps)))
114118
module C = IntTest (IntDomainProperties.WithIkind (IntDomain.DefExc) (Ikind))
115-
module T = struct
116-
include IntDomainProperties.WithIkind (IntDomain.DefExc) (Ikind)
117-
let of_excl_list xs = of_excl_list Cil.ILong xs
118-
end
119119

120-
let tzero = T.of_int zero
121-
let tone = T.of_int one
122-
let tminus_one = T.of_int minus_one
123-
let ttwo = T.of_int (of_int 2)
124-
let tminus_two = T.of_int (of_int (-2))
125-
let t4 = T.of_int (of_int 4)
126-
let t5 = T.of_int (of_int 5)
127-
let tn5 = T.of_int (of_int (-5))
128-
let t42 = T.of_int (of_int 42)
129-
let ttrue = T.of_bool true
130-
let tfalse = T.of_bool false
131-
let ttop = T.top ()
132-
let tbot = T.bot ()
133-
let tex0 = T.of_excl_list [zero]
134-
let tex1 = T.of_excl_list [one ]
135-
let tex10 = T.of_excl_list [zero; one]
136-
let tex01 = T.of_excl_list [one; zero]
137-
138-
let test_bot _ =
139-
assert_bool "bot != bot" (T.is_bot tbot);
140-
assert_bool "top != top" (T.is_top ttop);
141-
assert_bool "top == bot" (not (T.is_bot ttop));
142-
assert_bool "bot == top" (not (T.is_top tbot));
143-
assert_bool "0 == top" (not (T.is_top tzero));
144-
assert_bool "1 == top" (not (T.is_top tone))
145-
146-
let test_join _ =
147-
assert_equal ~printer:T.show tone (T.join tbot tone);
148-
assert_equal ~printer:T.show tzero(T.join tbot tzero);
149-
assert_equal ~printer:T.show tone (T.join tone tbot);
150-
assert_equal ~printer:T.show tzero(T.join tzero tbot);
151-
assert_equal ~printer:T.show ttop (T.join ttop tone);
152-
assert_equal ~printer:T.show ttop (T.join ttop tzero);
153-
assert_equal ~printer:T.show ttop (T.join tone ttop);
154-
assert_equal ~printer:T.show ttop (T.join tzero ttop);
155-
assert_equal ~printer:T.show tbot (T.join tbot tbot);
156-
assert_equal ~printer:T.show tone (T.join tone tone);
157-
(* assert_equal ~printer:T.show tex0 (T.join tone ttwo); *) (* TODO: now more precise range *)
158-
(* assert_equal ~printer:T.show ttop (T.join tone tzero); *) (* TODO: now more precise range *)
159-
assert_equal ~printer:T.show tex0 (T.join tex0 tex0);
160-
assert_equal ~printer:T.show tex1 (T.join tex1 tex1);
161-
assert_equal ~printer:T.show ttop (T.join tex1 tex0);
162-
assert_equal ~printer:T.show ttop (T.join tex0 tex1);
163-
(* assert_equal ~printer:T.show tex0 (T.join tone ttwo); *) (* TODO: now more precise range *)
164-
assert_equal ~printer:T.show tex1 (T.join tex1 tzero);
165-
assert_equal ~printer:T.show tex0 (T.join tex0 tone );
166-
assert_equal ~printer:T.show tex1 (T.join tex1 tzero);
167-
assert_equal ~printer:T.show tex0 (T.join tex0 tone )
168-
169-
let test_meet _ =
170-
assert_equal ~printer:T.show tbot (T.meet tbot tone);
171-
assert_equal ~printer:T.show tbot (T.meet tbot tzero);
172-
assert_equal ~printer:T.show tbot (T.meet tone tbot);
173-
assert_equal ~printer:T.show tbot (T.meet tzero tbot);
174-
assert_equal ~printer:T.show tone (T.meet ttop tone);
175-
assert_equal ~printer:T.show tzero(T.meet ttop tzero);
176-
assert_equal ~printer:T.show tone (T.meet tone ttop);
177-
assert_equal ~printer:T.show tzero(T.meet tzero ttop);
178-
assert_equal ~printer:T.show tbot (T.meet tbot tbot);
179-
assert_equal ~printer:T.show tone (T.meet tone tone);
180-
assert_equal ~printer:T.show tbot (T.meet tone ttwo);
181-
assert_equal ~printer:T.show tbot (T.meet tone tzero);
182-
assert_equal ~printer:T.show tex0 (T.meet tex0 tex0);
183-
assert_equal ~printer:T.show tex1 (T.meet tex1 tex1);
184-
assert_equal ~printer:T.show tex10(T.meet tex1 tex0);
185-
assert_equal ~printer:T.show tex01(T.meet tex0 tex1);
186-
assert_equal ~printer:T.show tzero(T.meet tex1 tzero);
187-
assert_equal ~printer:T.show tone (T.meet tex0 tone );
188-
assert_equal ~printer:T.show tzero(T.meet tex1 tzero);
189-
assert_equal ~printer:T.show tone (T.meet tex0 tone )
190-
191-
let test_ex_set _ =
192-
assert_equal (Some [zero; one]) (T.to_excl_list tex10 |> Option.map fst);
193-
assert_equal (Some [zero; one]) (T.to_excl_list tex01 |> Option.map fst);
194-
assert_bool "Not [1;0] is not excl set" (T.is_excl_list tex10);
195-
assert_bool "bot is excl set" (not (T.is_excl_list tbot));
196-
assert_bool "42 is excl set" (not (T.is_excl_list t42));
197-
assert_equal (Some true) (T.to_bool tex0);
198-
assert_equal (Some true) (T.to_bool tex10);
199-
assert_equal None (T.to_bool tex1)
120+
module D = struct
121+
module T = struct
122+
include IntDomainProperties.WithIkind (IntDomain.DefExc) (Ikind)
123+
let of_excl_list xs = of_excl_list Cil.ILong xs
124+
end
125+
126+
let tzero = T.of_int zero
127+
let tone = T.of_int one
128+
let tminus_one = T.of_int minus_one
129+
let ttwo = T.of_int (of_int 2)
130+
let tminus_two = T.of_int (of_int (-2))
131+
let t4 = T.of_int (of_int 4)
132+
let t5 = T.of_int (of_int 5)
133+
let tn5 = T.of_int (of_int (-5))
134+
let t42 = T.of_int (of_int 42)
135+
let ttrue = T.of_bool true
136+
let tfalse = T.of_bool false
137+
let ttop = T.top ()
138+
let tbot = T.bot ()
139+
let tex0 = T.of_excl_list [zero]
140+
let tex1 = T.of_excl_list [one ]
141+
let tex10 = T.of_excl_list [zero; one]
142+
let tex01 = T.of_excl_list [one; zero]
143+
144+
let test_bot _ =
145+
assert_bool "bot != bot" (T.is_bot tbot);
146+
assert_bool "top != top" (T.is_top ttop);
147+
assert_bool "top == bot" (not (T.is_bot ttop));
148+
assert_bool "bot == top" (not (T.is_top tbot));
149+
assert_bool "0 == top" (not (T.is_top tzero));
150+
assert_bool "1 == top" (not (T.is_top tone))
151+
152+
let assert_poly_equal = assert_equal
153+
let assert_equal x y = assert_equal ~cmp: T.equal ~printer:T.show x y
154+
155+
let test_join _ =
156+
assert_equal tone (T.join tbot tone);
157+
assert_equal tzero(T.join tbot tzero);
158+
assert_equal tone (T.join tone tbot);
159+
assert_equal tzero(T.join tzero tbot);
160+
assert_equal ttop (T.join ttop tone);
161+
assert_equal ttop (T.join ttop tzero);
162+
assert_equal ttop (T.join tone ttop);
163+
assert_equal ttop (T.join tzero ttop);
164+
assert_equal tbot (T.join tbot tbot);
165+
assert_equal tone (T.join tone tone);
166+
(* assert_equal tex0 (T.join tone ttwo); *) (* TODO: now more precise range *)
167+
(* assert_equal ttop (T.join tone tzero); *) (* TODO: now more precise range *)
168+
assert_equal tex0 (T.join tex0 tex0);
169+
assert_equal tex1 (T.join tex1 tex1);
170+
assert_equal ttop (T.join tex1 tex0);
171+
assert_equal ttop (T.join tex0 tex1);
172+
(* assert_equal ~printer:T.show tex0 (T.join tone ttwo); *) (* TODO: now more precise range *)
173+
assert_equal tex1 (T.join tex1 tzero);
174+
assert_equal tex0 (T.join tex0 tone );
175+
assert_equal tex1 (T.join tex1 tzero);
176+
assert_equal tex0 (T.join tex0 tone )
177+
178+
let test_meet _ =
179+
assert_equal tbot (T.meet tbot tone);
180+
assert_equal tbot (T.meet tbot tzero);
181+
assert_equal tbot (T.meet tone tbot);
182+
assert_equal tbot (T.meet tzero tbot);
183+
assert_equal tone (T.meet ttop tone);
184+
assert_equal tzero(T.meet ttop tzero);
185+
assert_equal tone (T.meet tone ttop);
186+
assert_equal tzero(T.meet tzero ttop);
187+
assert_equal tbot (T.meet tbot tbot);
188+
assert_equal tone (T.meet tone tone);
189+
assert_equal tbot (T.meet tone ttwo);
190+
assert_equal tbot (T.meet tone tzero);
191+
assert_equal tex0 (T.meet tex0 tex0);
192+
assert_equal tex1 (T.meet tex1 tex1);
193+
assert_equal tex10(T.meet tex1 tex0);
194+
assert_equal tex01(T.meet tex0 tex1);
195+
assert_equal tzero(T.meet tex1 tzero);
196+
assert_equal tone (T.meet tex0 tone );
197+
assert_equal tzero(T.meet tex1 tzero);
198+
assert_equal tone (T.meet tex0 tone )
199+
200+
let test_ex_set _ =
201+
assert_poly_equal (Some [zero; one]) (T.to_excl_list tex10 |> Option.map fst);
202+
assert_poly_equal (Some [zero; one]) (T.to_excl_list tex01 |> Option.map fst);
203+
assert_bool "Not [1;0] is not excl set" (T.is_excl_list tex10);
204+
assert_bool "bot is excl set" (not (T.is_excl_list tbot));
205+
assert_bool "42 is excl set" (not (T.is_excl_list t42));
206+
assert_poly_equal (Some true) (T.to_bool tex0);
207+
assert_poly_equal (Some true) (T.to_bool tex10);
208+
assert_poly_equal None (T.to_bool tex1)
209+
end
200210

201211
module IntervalTest (I : IntDomain.SOverflow with type int_t = Z.t) =
202212
struct
@@ -996,10 +1006,10 @@ let test () =
9961006
"int_Integers" >::: A.test ();
9971007
"int_Flattened" >::: B.test ();
9981008
"int_DefExc" >::: C.test ();
999-
"test_bot" >:: test_bot;
1000-
"test_join" >:: test_join;
1001-
"test_meet" >:: test_meet;
1002-
"test_excl_list">:: test_ex_set;
1009+
"test_bot" >:: D.test_bot;
1010+
"test_join" >:: D.test_join;
1011+
"test_meet" >:: D.test_meet;
1012+
"test_excl_list">:: D.test_ex_set;
10031013
"interval" >::: Interval.test ();
10041014
"bitfield" >::: Bitfield.test ();
10051015
"intervalSet" >::: IntervalSet.test ();

0 commit comments

Comments
 (0)