qsym

A symbolic executor for the QBE intermediate language

git clone https://git.8pit.net/qsym.git

  1[jnz] Exploring path for label 'if_true.11'
  2[jnz] Exploring path for label 'logic_right.13'
  3[jnz] Exploring path for label 'for_body.4'
  4[jnz] Exploring path for label 'if_true.7'
  5[jnz] Exploring path for label 'if_false.16'
  6Local variables:
  7	.1 = |main:.1|
  8	.10 = (ite (= |main:.1| #x00000002) #x00000001 #x00000000)
  9	.11 = (ite (= |main:.1| #x00000002) #x00000001 #x00000000)
 10	.12 = (ite (= |main:.1| #x00000002) #x00000001 #x00000000)
 11	.2 = #x000000000000000c
 12	.3 = |main:.1|
 13	.4 = (ite (and (= ((_ extract 31 4) |main:.1|) #x0000000)
 14          (bvule ((_ extract 3 0) |main:.1|) #xa))
 15     #x00000001
 16     #x00000000)
 17	.5 = |main:.1|
 18	.6 = (ite (= ((_ extract 31 1) |main:.1|) #b0000000000000000000000000000000)
 19     #x00000000
 20     #x00000001)
 21	.7 = |main:.1|
 22	.8 = #x00000002
 23	.9 = |main:.1|
 24Symbolic variable values:
 25	main:.1 -> #x00000008
 26	
 27[jnz] Exploring path for label 'if_false.8'
 28[jnz] Exploring path for label 'for_cond.3'
 29[jnz] Exploring path for label 'for_body.4'
 30[jnz] Exploring path for label 'if_true.7'
 31[jnz] Exploring path for label 'if_false.16'
 32Local variables:
 33	.1 = |main:.1|
 34	.10 = (ite (= |main:.1| #x00000003) #x00000001 #x00000000)
 35	.11 = (ite (= |main:.1| #x00000003) #x00000001 #x00000000)
 36	.12 = (ite (= |main:.1| #x00000003) #x00000001 #x00000000)
 37	.2 = #x000000000000000c
 38	.3 = |main:.1|
 39	.4 = (ite (and (= ((_ extract 31 4) |main:.1|) #x0000000)
 40          (bvule ((_ extract 3 0) |main:.1|) #xa))
 41     #x00000001
 42     #x00000000)
 43	.5 = |main:.1|
 44	.6 = (ite (= ((_ extract 31 1) |main:.1|) #b0000000000000000000000000000000)
 45     #x00000000
 46     #x00000001)
 47	.7 = |main:.1|
 48	.8 = #x00000003
 49	.9 = |main:.1|
 50Symbolic variable values:
 51	main:.1 -> #x00000009
 52	
 53[jnz] Exploring path for label 'if_false.8'
 54[jnz] Exploring path for label 'for_cond.3'
 55[jnz] Exploring path for label 'for_body.4'
 56[jnz] Exploring path for label 'if_false.8'
 57[jnz] Exploring path for label 'for_cond.3'
 58[jnz] Exploring path for label 'for_body.4'
 59[jnz] Exploring path for label 'if_false.8'
 60[jnz] Exploring path for label 'for_cond.3'
 61[jnz] Exploring path for label 'for_body.4'
 62[jnz] Exploring path for label 'if_false.8'
 63[jnz] Exploring path for label 'for_cond.3'
 64[jnz] Exploring path for label 'for_join.6'
 65[jnz] Exploring path for label 'if_true.15'
 66Halting executing
 67Local variables:
 68	.1 = |main:.1|
 69	.10 = #x00000001
 70	.11 = #x00000001
 71	.12 = #x00000001
 72	.2 = #x000000000000000c
 73	.3 = |main:.1|
 74	.4 = (ite (and (= ((_ extract 31 4) |main:.1|) #x0000000)
 75          (bvule ((_ extract 3 0) |main:.1|) #xa))
 76     #x00000001
 77     #x00000000)
 78	.5 = |main:.1|
 79	.6 = (ite (= ((_ extract 31 1) |main:.1|) #b0000000000000000000000000000000)
 80     #x00000000
 81     #x00000001)
 82	.7 = |main:.1|
 83	.8 = |main:.1|
 84	.9 = |main:.1|
 85Symbolic variable values:
 86	main:.1 -> #x00000007
 87	
 88[jnz] Exploring path for label 'for_join.6'
 89[jnz] Exploring path for label 'if_true.15'
 90Halting executing
 91Local variables:
 92	.1 = |main:.1|
 93	.10 = #x00000001
 94	.11 = #x00000001
 95	.12 = #x00000001
 96	.2 = #x000000000000000c
 97	.3 = |main:.1|
 98	.4 = (ite (and (= ((_ extract 31 4) |main:.1|) #x0000000)
 99          (bvule ((_ extract 3 0) |main:.1|) #xa))
100     #x00000001
101     #x00000000)
102	.5 = |main:.1|
103	.6 = (ite (= ((_ extract 31 1) |main:.1|) #b0000000000000000000000000000000)
104     #x00000000
105     #x00000001)
106	.7 = |main:.1|
107	.8 = |main:.1|
108	.9 = |main:.1|
109Symbolic variable values:
110	main:.1 -> #x00000005
111	
112[jnz] Exploring path for label 'for_join.6'
113[jnz] Exploring path for label 'if_true.15'
114Halting executing
115Local variables:
116	.1 = |main:.1|
117	.10 = #x00000001
118	.11 = #x00000001
119	.12 = #x00000001
120	.2 = #x000000000000000c
121	.3 = |main:.1|
122	.4 = (ite (and (= ((_ extract 31 4) |main:.1|) #x0000000)
123          (bvule ((_ extract 3 0) |main:.1|) #xa))
124     #x00000001
125     #x00000000)
126	.5 = |main:.1|
127	.6 = (ite (= ((_ extract 31 1) |main:.1|) #b0000000000000000000000000000000)
128     #x00000000
129     #x00000001)
130	.7 = |main:.1|
131	.8 = |main:.1|
132	.9 = |main:.1|
133Symbolic variable values:
134	main:.1 -> #x00000003
135	
136[jnz] Exploring path for label 'for_join.6'
137[jnz] Exploring path for label 'if_true.15'
138Halting executing
139Local variables:
140	.1 = |main:.1|
141	.10 = #x00000001
142	.11 = #x00000001
143	.12 = #x00000001
144	.2 = #x000000000000000c
145	.3 = |main:.1|
146	.4 = (ite (and (= ((_ extract 31 4) |main:.1|) #x0000000)
147          (bvule ((_ extract 3 0) |main:.1|) #xa))
148     #x00000001
149     #x00000000)
150	.5 = |main:.1|
151	.6 = (ite (= ((_ extract 31 1) |main:.1|) #b0000000000000000000000000000000)
152     #x00000000
153     #x00000001)
154	.7 = |main:.1|
155	.8 = |main:.1|
156	.9 = |main:.1|
157Symbolic variable values:
158	main:.1 -> #x00000002
159	
160[jnz] Exploring path for label 'logic_join.14'
161[jnz] Exploring path for label 'if_false.16'
162Local variables:
163	.1 = |main:.1|
164	.12 = #x00000000
165	.2 = #x000000000000000c
166	.3 = |main:.1|
167	.4 = (ite (and (= ((_ extract 31 4) |main:.1|) #x0000000)
168          (bvule ((_ extract 3 0) |main:.1|) #xa))
169     #x00000001
170     #x00000000)
171	.5 = |main:.1|
172	.6 = (ite (= ((_ extract 31 1) |main:.1|) #b0000000000000000000000000000000)
173     #x00000000
174     #x00000001)
175Symbolic variable values:
176	main:.1 -> #x00000000
177	
178[jnz] Exploring path for label 'if_false.12'
179Local variables:
180	.1 = |main:.1|
181	.2 = #x000000000000000c
182	.3 = |main:.1|
183	.4 = (ite (and (= ((_ extract 31 4) |main:.1|) #x0000000)
184          (bvule ((_ extract 3 0) |main:.1|) #xa))
185     #x00000001
186     #x00000000)
187Symbolic variable values:
188	main:.1 -> #x0000000c
189