Lines Matching refs:vc
32 VC vc; in TEST() local
35 vc = vc_createValidityChecker(); in TEST()
37 vc_setFlags(vc, 'd'); in TEST()
41 Expr x00000003 = vc_varExpr(vc, "x00000003", vc_bvType(vc, 16)); in TEST()
42 Expr hex00FF = vc_bvConstExprFromInt(vc, 16, 0x00FF); in TEST()
44 Expr query1 = vc_eqExpr(vc, x00000003, hex00FF); in TEST()
45 Expr query2 = vc_notExpr(vc, query1); in TEST()
48 vc_push(vc); in TEST()
49 query_result = vc_query(vc, query1); in TEST()
51 vc_pop(vc); in TEST()
54 vc_push(vc); in TEST()
55 query_result = vc_query(vc, query2); in TEST()
57 vc_pop(vc); in TEST()
59 Expr x00000005 = vc_varExpr(vc, "x00000005", vc_bvType(vc, 16)); in TEST()
60 Expr query3 = vc_eqExpr(vc, x00000005, hex00FF); in TEST()
61 Expr query4 = vc_notExpr(vc, query3); in TEST()
64 vc_push(vc); in TEST()
65 vc_assertFormula(vc, query1); in TEST()
66 query_result = vc_query(vc, query3); in TEST()
68 vc_pop(vc); in TEST()
71 vc_push(vc); in TEST()
72 vc_assertFormula(vc, query1); in TEST()
73 query_result = vc_query(vc, query4); in TEST()
75 vc_pop(vc); in TEST()
77 Expr x00000007 = vc_varExpr(vc, "x00000007", vc_bvType(vc, 16)); in TEST()
78 Expr query5 = vc_eqExpr(vc, x00000007, hex00FF); in TEST()
79 Expr query6 = vc_notExpr(vc, query5); in TEST()
83 vc_push(vc); in TEST()
84 vc_assertFormula(vc, query3); in TEST()
85 vc_assertFormula(vc, query1); in TEST()
86 query_result = vc_query(vc, query5); in TEST()
88 vc_pop(vc); in TEST()
91 vc_push(vc); in TEST()
92 vc_assertFormula(vc, query3); in TEST()
93 vc_assertFormula(vc, query1); in TEST()
94 query_result = vc_query(vc, query6); in TEST()
96 vc_pop(vc); in TEST()
98 Expr x00000009 = vc_varExpr(vc, "x00000009", vc_bvType(vc, 32)); in TEST()
99 Expr ct_0_32 = vc_bvConstExprFromInt(vc, 32, 0x0); in TEST()
100 Expr query8 = vc_eqExpr(vc, x00000009, ct_0_32); in TEST()
101 Expr query7 = vc_notExpr(vc, query8); in TEST()
104 vc_push(vc); in TEST()
105 vc_assertFormula(vc, query5); in TEST()
106 vc_assertFormula(vc, query3); in TEST()
107 vc_assertFormula(vc, query1); in TEST()
108 query_result = vc_query(vc, query7); in TEST()
110 vc_pop(vc); in TEST()
113 vc_push(vc); in TEST()
114 vc_assertFormula(vc, query5); in TEST()
115 vc_assertFormula(vc, query3); in TEST()
116 vc_assertFormula(vc, query1); in TEST()
117 query_result = vc_query(vc, query8); in TEST()
119 vc_pop(vc); in TEST()
121 Expr x0000000b = vc_varExpr(vc, "x0000000b", vc_bvType(vc, 32)); in TEST()
122 Expr query9 = vc_eqExpr(vc, x0000000b, ct_0_32); in TEST()
123 Expr query10 = vc_notExpr(vc, query9); in TEST()
126 vc_push(vc); in TEST()
127 vc_assertFormula(vc, query7); in TEST()
128 vc_assertFormula(vc, query5); in TEST()
129 vc_assertFormula(vc, query3); in TEST()
130 vc_assertFormula(vc, query1); in TEST()
131 query_result = vc_query(vc, query9); in TEST()
133 vc_pop(vc); in TEST()
136 vc_push(vc); in TEST()
137 vc_assertFormula(vc, query7); in TEST()
138 vc_assertFormula(vc, query5); in TEST()
139 vc_assertFormula(vc, query3); in TEST()
140 vc_assertFormula(vc, query1); in TEST()
141 query_result = vc_query(vc, query10); in TEST()
143 vc_pop(vc); in TEST()
145 Expr x0000000d = vc_varExpr(vc, "x0000000d", vc_bvType(vc, 32)); in TEST()
146 Expr query11 = vc_eqExpr(vc, x0000000d, ct_0_32); in TEST()
147 Expr query12 = vc_notExpr(vc, query11); in TEST()
150 vc_push(vc); in TEST()
151 vc_assertFormula(vc, query2); in TEST()
152 query_result = vc_query(vc, query11); in TEST()
154 vc_pop(vc); in TEST()
157 vc_push(vc); in TEST()
158 vc_assertFormula(vc, query2); in TEST()
159 query_result = vc_query(vc, query12); in TEST()
161 vc_pop(vc); in TEST()
163 Expr x00000075 = vc_varExpr(vc, "x00000075", vc_bvType(vc, 8)); in TEST()
164 Expr ct_0_8 = vc_bvConstExprFromInt(vc, 8, 0x0); in TEST()
165 Expr query14 = vc_eqExpr(vc, x00000075, ct_0_8); in TEST()
166 Expr query13 = vc_notExpr(vc, query14); in TEST()
169 vc_push(vc); in TEST()
170 vc_assertFormula(vc, query12); in TEST()
171 vc_assertFormula(vc, query2); in TEST()
172 query_result = vc_query(vc, query13); in TEST()
174 vc_pop(vc); in TEST()
177 vc_push(vc); in TEST()
178 vc_assertFormula(vc, query12); in TEST()
179 vc_assertFormula(vc, query2); in TEST()
180 query_result = vc_query(vc, query14); in TEST()
182 vc_pop(vc); in TEST()
184 Expr x00000015 = vc_varExpr(vc, "x00000015", vc_bv32Type(vc)); in TEST()
185 Expr x0000001b = vc_varExpr(vc, "x0000001b", vc_bv32Type(vc)); in TEST()
186 Expr x00000021 = vc_varExpr(vc, "x00000021", vc_bv32Type(vc)); in TEST()
187 Expr x00000010 = vc_varExpr(vc, "x00000010", vc_bv32Type(vc)); in TEST()
188 Expr x00000017 = vc_varExpr(vc, "x00000017", vc_bv32Type(vc)); in TEST()
189 Expr ct_F_32 = vc_bvConstExprFromInt(vc, 32, 0xFFFFFFFF); in TEST()
190 Expr x1b_sub_x21 = vc_bvMinusExpr(vc, 32, x0000001b, x00000021); // Q1 in TEST()
191 Expr Q1_plus_x15 = vc_bvPlusExpr(vc, 32, x1b_sub_x21, x00000015); // Q2 in TEST()
192 Expr Q2_plus_FF = vc_bvPlusExpr(vc, 32, Q1_plus_x15, ct_F_32); // Q3 in TEST()
193 Expr Q3_div_x15 = vc_bvDivExpr(vc, 32, Q2_plus_FF, x00000015); // T1 in TEST()
194 Expr x10_sub_x17 = vc_bvMinusExpr(vc, 32, x00000010, x00000017); // Q4 in TEST()
195 Expr Q4_div_x15 = vc_bvDivExpr(vc, 32, x10_sub_x17, x00000015); // T2 in TEST()
196 Expr query15 = vc_sbvGtExpr(vc, Q3_div_x15, Q4_div_x15); in TEST()
197 Expr query16 = vc_notExpr(vc, query15); in TEST()
200 vc_push(vc); in TEST()
201 Expr query15_0 = vc_eqExpr(vc, x00000015, ct_0_32); in TEST()
202 Expr query15_1 = vc_notExpr(vc, query15_0); in TEST()
203 vc_assertFormula(vc, query15_1); in TEST()
204 vc_assertFormula(vc, query13); in TEST()
205 vc_assertFormula(vc, query12); in TEST()
206 vc_assertFormula(vc, query2); in TEST()
207 query_result = vc_query(vc, query15); in TEST()
209 vc_pop(vc); in TEST()
212 vc_push(vc); in TEST()
213 vc_assertFormula(vc, query13); in TEST()
214 vc_assertFormula(vc, query12); in TEST()
215 vc_assertFormula(vc, query2); in TEST()
216 query_result = vc_query(vc, query16); in TEST()
218 vc_pop(vc); in TEST()
220 Expr x00000032 = vc_varExpr(vc, "x00000032", vc_bv32Type(vc)); in TEST()
221 Expr x00000038 = vc_varExpr(vc, "x00000038", vc_bv32Type(vc)); in TEST()
222 Expr x00000028 = vc_varExpr(vc, "x00000028", vc_bv32Type(vc)); in TEST()
223 Expr x0000002e = vc_varExpr(vc, "x0000002e", vc_bv32Type(vc)); in TEST()
224 Expr x32_sub_x38 = vc_bvMinusExpr(vc, 32, x00000032, x00000038); // A1 in TEST()
225 Expr A1_plus_x15 = vc_bvPlusExpr(vc, 32, x32_sub_x38, x00000015); // A2 in TEST()
226 Expr A2_plus_FF = vc_bvPlusExpr(vc, 32, A1_plus_x15, ct_F_32); // A3 in TEST()
227 Expr A3_div_x15 = vc_bvDivExpr(vc, 32, A2_plus_FF, x00000015); // A4 in TEST()
228 Expr x28_sub_x2e = vc_bvMinusExpr(vc, 32, x00000028, x0000002e); // A5 in TEST()
229 Expr A5_div_x15 = vc_bvDivExpr(vc, 32, x28_sub_x2e, x00000015); // A6 in TEST()
230 Expr A4_sub_A6 = vc_bvMinusExpr(vc, 32, A3_div_x15, A5_div_x15); // A7 in TEST()
231 Expr query17 = vc_sbvGtExpr(vc, A4_sub_A6, ct_0_32); in TEST()
232 Expr query18 = vc_notExpr(vc, query17); in TEST()
235 vc_push(vc); in TEST()
236 vc_assertFormula(vc, query15); in TEST()
237 vc_assertFormula(vc, query13); in TEST()
238 vc_assertFormula(vc, query12); in TEST()
239 vc_assertFormula(vc, query2); in TEST()
240 query_result = vc_query(vc, query17); in TEST()
242 vc_pop(vc); in TEST()
245 vc_push(vc); in TEST()
246 vc_assertFormula(vc, query15); in TEST()
247 vc_assertFormula(vc, query13); in TEST()
248 vc_assertFormula(vc, query12); in TEST()
249 vc_assertFormula(vc, query2); in TEST()
250 query_result = vc_query(vc, query18); in TEST()
252 vc_pop(vc); in TEST()
254 Expr query19 = vc_bvLtExpr(vc, ct_0_32, x00000015); in TEST()
257 vc_push(vc); in TEST()
258 vc_assertFormula(vc, query17); in TEST()
259 vc_assertFormula(vc, query15); in TEST()
260 vc_assertFormula(vc, query13); in TEST()
261 vc_assertFormula(vc, query12); in TEST()
262 vc_assertFormula(vc, query2); in TEST()
263 query_result = vc_query(vc, query19); in TEST()
265 vc_pop(vc); in TEST()
267 vc_Destroy(vc); in TEST()