HCoop / bpt / coccinelle.git / blame
? search:
summary | shortlog | log | commit | commitdiff | tree
blob | blame (incremental) | history | HEAD
Coccinelle release 0.2.5-rc3
[bpt/coccinelle.git] / engine / tests / test1.tex
CommitLineData
34e49164
C		 1\documentclass{article}
2\usepackage{fullpage}
3
4\newcommand{\U}{\,\mbox{\sf{U}}\,}
5\newcommand{\A}{\mbox{\sf{A}}}
6\newcommand{\E}{\mbox{\sf{E}}}
7\newcommand{\AX}{\mbox{\sf{AX}}}
8\newcommand{\EX}{\mbox{\sf{EX}}}
9\newcommand{\AF}{\mbox{\sf{AF}}}
10\newcommand{\EF}{\mbox{\sf{EF}}}
11\newcommand{\AG}{\mbox{\sf{AG}}}
12\newcommand{\EG}{\mbox{\sf{EG}}}
13
14\newcommand{\mita}[1]{\mbox{\it{{#1}}}}
15\newcommand{\mtt}[1]{\mbox{\tt{{#1}}}}
16\newcommand{\msf}[1]{\mbox{\sf{{#1}}}}
17\newcommand{\mrm}[1]{\mbox{\rm{{#1}}}}
18\newcommand{\mth}[1]{\({#1}\)}
19
20\newcommand{\ttlb}{\mbox{\tt \char'173}}
21\newcommand{\ttrb}{\mbox{\tt \char'175}}
22
23\begin{document}
24
25\begin{quote}\begin{verbatim}
26
27@@
28@@
29
30f();
31...
32?g();
33...
34h();
35\end{verbatim}\end{quote}
36
37\[\begin{array}{l}
38\mita{\sf{let}} \, \mita{l9} = \mita{f();} \, \mita{\sf{in}} \, \mita{l9} \wedge (\AX(\mita{\sf{let}} \, \mita{l0} = \mita{g();} \, \mita{\sf{in}} \, \A[\neg (\mita{l0} \vee \mita{l9}) \U (\mita{\sf{let}} \, \mita{l7} = \msf{After}\\\mbox{} \vee \msf{ErrorExit} \, \mita{\sf{in}} \, (\mita{\sf{let}} \, \mita{l10} = (\mita{\sf{let}} \, \mita{l5} = \mita{h();} \, \mita{\sf{in}} \, \A[\neg (\mita{l5} \vee \mita{l0}) \U (\mita{l5} \vee \mita{l7})]
39
40) \, \mita{\sf{in}} \, (\mita{\sf{let}} \, \mita{l3} = \mita{l0}\\\mbox{} \wedge (\AX\mita{l10}) \, \mita{\sf{in}} \, \mita{l3} \vee ((\neg \mita{l3}) \wedge \mita{l10})
41)
42) \vee \mita{l7}
43)]
44
45))
46
47\end{array}\]
48
49\begin{quote}\begin{verbatim}
50
51@@
52@@
53
54foo(...) {
55
56(
57 -f-(-3-, -E-)-;
58 >>> f(3, 3, E);
59
60|
61 -f-(-E-, -4-)-;
62 >>> f(E, 4, 4);
63
64|
65 -E-;
66 >>> g(E);
67
68)
69
70(
71 -f-(-3-, -X-)-;
72 >>> f(3, 3, X);
73
74|
75 -f-(-Y-, -4-)-;
76 >>> f(Y, 4, 4);
77
78|
79 -Z-;
80 >>> g(Z);
81
82)
83
84(
85 -f-(-3-)-;
86 >>> f(3, 3);
87
88|
89 -f-(-4-)-;
90 >>> f(4, 4);
91
92)
93}
94\end{verbatim}\end{quote}
95
96\[\begin{array}{l}
97(\exists \mita{foo} . \mita{foo(...) }) \wedge (\AX(\exists \mita{p0} . (\mita{\sf{let}} \, \mita{l17} = \msf{Paren}(p0) \, \mita{\sf{in}} \, \mita{{\ttlb}
98 } \wedge \mita{l17} \wedge (\AX(\mita{\sf{let}} \, \mita{l32} = \AX(\mita{\sf{let}} \, \mita{l2} = \AX(\mita{\sf{let}} \, \mita{l12} = \AX(\mita{
99{\ttrb}}\\\mbox{} \wedge \mita{l17}) \, \mita{\sf{in}} \, ((\exists \mita{v0} . \mita{-f-(-3-)-;
100 \mth{>}\mth{>}\mth{>} f(3, 3);}_{\mita{v0}}) \wedge \mita{l12}) \vee ((\exists \mita{v0} . \mita{-f-(-4-)-;
101 \mth{>}\mth{>}\mth{>} f(4, 4);}_{\mita{v0}})\\\mbox{} \wedge \mita{l12})
102) \, \mita{\sf{in}} \, (\mita{\sf{let}} \, \mita{l7} = \exists \mita{X} . \exists \mita{v0} . \mita{-f-(-3-, -X-)-;
103 \mth{>}\mth{>}\mth{>} f(3, 3, X);}_{\mita{v0}} \, \mita{\sf{in}} \, (\mita{l7}\\\mbox{} \wedge \mita{l2}) \vee (\mita{\sf{let}} \, \mita{l21} = \neg \mita{l7} \, \mita{\sf{in}} \, (\mita{\sf{let}} \, \mita{l6} = \exists \mita{Y} . \exists \mita{v0} . \mita{-f-(-Y-, -4-)-;
104 \mth{>}\mth{>}\mth{>} f(Y, 4, 4);}_{\mita{v0}}\\\mbox{} \, \mita{\sf{in}} \, (\mita{l21} \wedge \mita{l6} \wedge \mita{l2}) \vee ((\neg \mita{l6}) \wedge \mita{l21} \wedge (\exists \mita{Z} . \exists \mita{v0} . \mita{-Z-;
105 \mth{>}\mth{>}\mth{>} g(Z);}_{\mita{v0}}) \wedge \mita{l2})
106)
107)
108)
109) \, \mita{\sf{in}} \, (\mita{\sf{let}} \, \mita{l8} = \exists \mita{E}\\\mbox{} . \exists \mita{v0} . \mita{-f-(-3-, -E-)-;
110 \mth{>}\mth{>}\mth{>} f(3, 3, E);}_{\mita{v0}} \, \mita{\sf{in}} \, (\mita{l8} \wedge \mita{l32}) \vee (\mita{\sf{let}} \, \mita{l19} = \neg \mita{l8}\\\mbox{} \, \mita{\sf{in}} \, (\mita{\sf{let}} \, \mita{l4} = \exists \mita{E} . \exists \mita{v0} . \mita{-f-(-E-, -4-)-;
111 \mth{>}\mth{>}\mth{>} f(E, 4, 4);}_{\mita{v0}} \, \mita{\sf{in}} \, (\mita{l19} \wedge \mita{l4}\\\mbox{} \wedge \mita{l32}) \vee ((\neg \mita{l4}) \wedge \mita{l19} \wedge (\exists \mita{E} . \exists \mita{v0} . \mita{-E-;
112 \mth{>}\mth{>}\mth{>} g(E);}_{\mita{v0}}) \wedge \mita{l32})
113)
114)
115)
116))
117)))
118\end{array}\]
119
120\begin{quote}\begin{verbatim}
121
122@@
123@@
124
125p(
126 <<< int hostptr,
127 char buffer) {
128 -int -hostptr-;
129}
130\end{verbatim}\end{quote}
131
132\[\begin{array}{l}
133\exists \mita{hostptr} . ((\exists \mita{buffer} . \exists \mita{v0} . \mita{p(
134 <<< int hostptr,
135 char buffer) }_{\mita{v0}})\\\mbox{} \wedge (\AX(\exists \mita{p0} . (\mita{\sf{let}} \, \mita{l0} = \msf{Paren}(p0) \, \mita{\sf{in}} \, \mita{{\ttlb}
136 } \wedge \mita{l0} \wedge (\AX((\exists \mita{v0} . \mita{-int -hostptr-;}_{\mita{v0}})\\\mbox{} \wedge (\AX(\mita{
137{\ttrb}} \wedge \mita{l0}))))
138))))
139\end{array}\]
140
141\begin{quote}\begin{verbatim}
142
143@@
144@@
145
146f(X);
147-... WHEN != -h-(-X-)
148g(Y);
149\end{verbatim}\end{quote}
150
151\[\begin{array}{l}
152\exists \mita{X} . (\mita{\sf{let}} \, \mita{l1} = \mita{f(X);} \, \mita{\sf{in}} \, \mita{l1} \wedge (\AX(\mita{\sf{let}} \, \mita{l0} = \exists \mita{Y} . \mita{g(Y);} \, \mita{\sf{in}} \, \A[((\exists \mita{v0} . \mita{-\_S0}_{\mita{v0}}) \wedge (\neg (\exists \mita{v0}\\\mbox{} . \mita{-h-(-X-)}_{\mita{v0}})) \wedge (\neg (\mita{l0} \vee \mita{l1}))) \U (\mita{l0} \vee \msf{After} \vee \msf{ErrorExit})]
153
154))
155)
156\end{array}\]
157
158\begin{quote}\begin{verbatim}
159
160@@
161@@
162
163f(X);
164-...
165g(Y);
166\end{verbatim}\end{quote}
167
168\[\begin{array}{l}
169\mita{\sf{let}} \, \mita{l1} = \exists \mita{X} . \mita{f(X);} \, \mita{\sf{in}} \, \mita{l1} \wedge (\AX(\mita{\sf{let}} \, \mita{l2} = \exists \mita{Y} . \mita{g(Y);} \, \mita{\sf{in}} \, \A[((\exists \mita{v0} . \mita{-\_S0}_{\mita{v0}}) \wedge (\neg (\mita{l2}\\\mbox{} \vee \mita{l1}))) \U (\mita{l2} \vee \msf{After} \vee \msf{ErrorExit})]
170
171))
172
173\end{array}\]
174
175\begin{quote}\begin{verbatim}
176
177@@
178@@
179
180f(X);
181g(Y);
182h(X);
183f(Y);
184g(X);
185h(Y);
186\end{verbatim}\end{quote}
187
188\[\begin{array}{l}
189\exists \mita{X} . (\mita{f(X);} \wedge (\AX(\exists \mita{Y} . (\mita{g(Y);} \wedge (\AX(\mita{h(X);} \wedge (\AX(\mita{f(Y);} \wedge (\AX(\mita{g(X);} \wedge (\AX(\mita{h(Y);}))))))))))))
190\end{array}\]
191
192\begin{quote}\begin{verbatim}
193
194@@
195@@
196
197f(X);
198...
199g(X);
200h(X);
201\end{verbatim}\end{quote}
202
203\[\begin{array}{l}
204\exists \mita{X} . (\mita{\sf{let}} \, \mita{l0} = \mita{f(X);} \, \mita{\sf{in}} \, \mita{l0} \wedge (\AX(\mita{\sf{let}} \, \mita{l1} = \mita{g(X);} \, \mita{\sf{in}} \, \A[\neg (\mita{l1} \vee \mita{l0}) \U ((\mita{l1} \wedge (\AX(\mita{h(X);})))\\\mbox{} \vee \msf{After} \vee \msf{ErrorExit})]
205
206))
207)
208\end{array}\]
209
210\begin{quote}\begin{verbatim}
211
212@@
213@@
214
215if (X) {
216 ...
217} else {
218 ...
219}
220f(X);
221\end{verbatim}\end{quote}
222
223\[\begin{array}{l}
224\exists \mita{X} . (\mita{\sf{let}} \, \mita{l0} = \msf{FalseBranch} \, \mita{\sf{in}} \, (\mita{\sf{let}} \, \mita{l1} = \msf{After} \, \mita{\sf{in}} \, \mita{if (X) } \wedge (\AX(\mita{\sf{let}} \, \mita{l15} = \AX(\exists \mita{p0}\\\mbox{} . (\mita{\sf{let}} \, \mita{l7} = \msf{Paren}(p0) \, \mita{\sf{in}} \, (\mita{\sf{let}} \, \mita{l14} = \mita{{\ttlb}
225 } \wedge \mita{l7} \, \mita{\sf{in}} \, \mita{l14} \wedge (\AX(\mita{\sf{let}} \, \mita{l13} = \mita{
226{\ttrb}} \wedge \mita{l7}\\\mbox{} \, \mita{\sf{in}} \, \A[\neg (\mita{l13} \vee \mita{l14}) \U (\mita{l13} \vee \mita{l1} \vee \msf{ErrorExit})]
227
228))
229)
230)) \, \mita{\sf{in}} \, (\msf{TrueBranch} \wedge \mita{l15}) \vee (\mita{l0}\\\mbox{} \wedge \mita{l15}) \vee (\mita{l1} \wedge (\AX(\mita{f(X);})))
231)) \wedge (\EX\mita{l0}) \wedge (\EX\mita{l1})
232)
233)
234\end{array}\]
235
236\begin{quote}\begin{verbatim}
237
238@@
239@@
240
241if (X) {
242 ...
243}
244f(X);
245\end{verbatim}\end{quote}
246
247\[\begin{array}{l}
248\exists \mita{X} . (\mita{\sf{let}} \, \mita{l0} = \msf{After} \, \mita{\sf{in}} \, \mita{if (X) } \wedge (\AX((\msf{TrueBranch} \wedge (\AX(\exists \mita{p0} . (\mita{\sf{let}} \, \mita{l2} = \msf{Paren}(p0)\\\mbox{} \, \mita{\sf{in}} \, (\mita{\sf{let}} \, \mita{l4} = \mita{{\ttlb}
249 } \wedge \mita{l2} \, \mita{\sf{in}} \, \mita{l4} \wedge (\AX(\mita{\sf{let}} \, \mita{l3} = \mita{
250{\ttrb}} \wedge \mita{l2} \, \mita{\sf{in}} \, \A[\neg (\mita{l3} \vee \mita{l4}) \U (\mita{l3} \vee \mita{l0}\\\mbox{} \vee \msf{ErrorExit})]
251
252))
253)
254)))) \vee \msf{FallThrough} \vee (\mita{l0} \wedge (\AX(\mita{f(X);}))))) \wedge (\EX\mita{l0})
255)
256\end{array}\]
257
258\begin{quote}\begin{verbatim}
259
260@@
261@@
262
263while (X) {
264 ...
265}
266f(X);
267\end{verbatim}\end{quote}
268
269\[\begin{array}{l}
270\exists \mita{X} . (\mita{while (X) } \wedge (\mita{\sf{let}} \, \mita{l0} = \msf{After} \, \mita{\sf{in}} \, (\AX((\msf{TrueBranch} \rightarrow (\AX(\exists \mita{p0} . (\mita{\sf{let}} \, \mita{l3} = \msf{Paren}(p0)\\\mbox{} \, \mita{\sf{in}} \, (\mita{\sf{let}} \, \mita{l5} = \mita{{\ttlb}
271 } \wedge \mita{l3} \, \mita{\sf{in}} \, \mita{l5} \wedge (\AX(\mita{\sf{let}} \, \mita{l4} = \mita{
272{\ttrb}} \wedge \mita{l3} \, \mita{\sf{in}} \, \A[\neg (\mita{l4} \vee \mita{l5}) \U (\mita{l4} \vee \mita{l0}\\\mbox{} \vee \msf{ErrorExit})]
273
274))
275)
276)))) \wedge (\mita{l0} \rightarrow (\AX(\mita{f(X);}))))) \wedge (\EX\mita{l0})
277))
278\end{array}\]
279
280\begin{quote}\begin{verbatim}
281
282@@
283@@
284
285while (X) {
286 ...
287}
288\end{verbatim}\end{quote}
289
290\[\begin{array}{l}
291(\exists \mita{X} . \mita{while (X) }) \wedge (\AX(\msf{TrueBranch} \rightarrow (\AX(\exists \mita{p0} . (\mita{\sf{let}} \, \mita{l1} = \msf{Paren}(p0) \, \mita{\sf{in}} \, (\mita{\sf{let}} \, \mita{l4} = \mita{{\ttlb}
292 }\\\mbox{} \wedge \mita{l1} \, \mita{\sf{in}} \, \mita{l4} \wedge (\AX(\mita{\sf{let}} \, \mita{l3} = \mita{
293{\ttrb}} \wedge \mita{l1} \, \mita{\sf{in}} \, \A[\neg (\mita{l3} \vee \mita{l4}) \U (\mita{l3} \vee \msf{After} \vee \msf{ErrorExit})]
294\\\mbox{}
295))
296)
297)))))
298\end{array}\]
299
300\begin{quote}\begin{verbatim}
301
302@@
303@@
304
305{
306 ... WHEN != g(Y)
307 f(X);
308 ... WHEN != h(Y)
309}
310\end{verbatim}\end{quote}
311
312\[\begin{array}{l}
313\exists \mita{p0} . (\mita{\sf{let}} \, \mita{l6} = \msf{Paren}(p0) \, \mita{\sf{in}} \, (\mita{\sf{let}} \, \mita{l9} = \mita{{\ttlb}
314 } \wedge \mita{l6} \, \mita{\sf{in}} \, \mita{l9} \wedge (\AX(\exists \mita{Y} . (\mita{\sf{let}} \, \mita{l3} = \exists \mita{X} . \mita{f(X);}\\\mbox{} \, \mita{\sf{in}} \, \A[((\neg \mita{g(Y)}) \wedge (\neg (\mita{l3} \vee \mita{l9}))) \U (\mita{\sf{let}} \, \mita{l5} = \msf{After} \vee \msf{ErrorExit} \, \mita{\sf{in}} \, (\mita{l3} \wedge (\AX(\mita{\sf{let}} \, \mita{l8} = \mita{
315{\ttrb}}\\\mbox{} \wedge \mita{l6} \, \mita{\sf{in}} \, \A[((\neg \mita{h(Y)}) \wedge (\neg (\mita{l8} \vee \mita{l3}))) \U (\mita{l8} \vee \mita{l5})]
316
317))) \vee \mita{l5}
318)]
319
320)))
321)
322)
323\end{array}\]
324
325\begin{quote}\begin{verbatim}
326
327@@
328@@
329
330f(X);
331...
332-g-(-Y-)-;
333 >>> h(X, Y);
334
335\end{verbatim}\end{quote}
336
337\[\begin{array}{l}
338\exists \mita{X} . (\mita{\sf{let}} \, \mita{l0} = \mita{f(X);} \, \mita{\sf{in}} \, \mita{l0} \wedge (\AX\A[\neg ((\exists \mita{Y} . \mita{-g-(-Y-)-;
339 \mth{>}\mth{>}\mth{>} h(X, Y);}) \vee \mita{l0})\\\mbox{} \U ((\exists \mita{Y} . \exists \mita{v0} . \mita{-g-(-Y-)-;
340 \mth{>}\mth{>}\mth{>} h(X, Y);}_{\mita{v0}}) \vee \msf{After} \vee \msf{ErrorExit})]
341)
342)
343\end{array}\]
344
345\begin{quote}\begin{verbatim}
346
347@@
348@@
349
350-f-(-X-)-;
351 >>> f(Z);
352
353-...
354g(Y);
355h(Z);
356\end{verbatim}\end{quote}
357
358\[\begin{array}{l}
359\exists \mita{Z} . ((\exists \mita{X} . \exists \mita{v0} . \mita{-f-(-X-)-;
360 \mth{>}\mth{>}\mth{>} f(Z);}_{\mita{v0}}) \wedge (\AX(\mita{\sf{let}} \, \mita{l0} = \exists \mita{Y} . \mita{g(Y);} \, \mita{\sf{in}} \, \A[((\exists \mita{v0}\\\mbox{} . \mita{-\_S0}_{\mita{v0}}) \wedge (\neg (\mita{l0} \vee (\exists \mita{X} . \mita{-f-(-X-)-;
361 \mth{>}\mth{>}\mth{>} f(Z);})))) \U ((\mita{l0} \wedge (\AX(\mita{h(Z);})))\\\mbox{} \vee \msf{After} \vee \msf{ErrorExit})]
362
363)))
364\end{array}\]
365
366\begin{quote}\begin{verbatim}
367
368@@
369@@
370
371-f-(-X-)-;
372 >>> f(Z);
373
374...
375g(Y);
376h(Z);
377\end{verbatim}\end{quote}
378
379\[\begin{array}{l}
380\exists \mita{Z} . ((\exists \mita{X} . \exists \mita{v0} . \mita{-f-(-X-)-;
381 \mth{>}\mth{>}\mth{>} f(Z);}_{\mita{v0}}) \wedge (\AX(\mita{\sf{let}} \, \mita{l0} = \exists \mita{Y} . \mita{g(Y);} \, \mita{\sf{in}} \, \A[\neg (\mita{l0}\\\mbox{} \vee (\exists \mita{X} . \mita{-f-(-X-)-;
382 \mth{>}\mth{>}\mth{>} f(Z);})) \U ((\mita{l0} \wedge (\AX(\mita{h(Z);}))) \vee \msf{After} \vee \msf{ErrorExit})]
383\\\mbox{}
384)))
385\end{array}\]
386
387\begin{quote}\begin{verbatim}
388
389@@
390@@
391
392f(X);
393...
394g(Y);
395h(Z);
396\end{verbatim}\end{quote}
397
398\[\begin{array}{l}
399\mita{\sf{let}} \, \mita{l1} = \exists \mita{X} . \mita{f(X);} \, \mita{\sf{in}} \, \mita{l1} \wedge (\AX(\mita{\sf{let}} \, \mita{l2} = \exists \mita{Y} . \mita{g(Y);} \, \mita{\sf{in}} \, \A[\neg (\mita{l2} \vee \mita{l1}) \U ((\mita{l2} \wedge (\AX(\exists \mita{Z}\\\mbox{} . \mita{h(Z);}))) \vee \msf{After} \vee \msf{ErrorExit})]
400
401))
402
403\end{array}\]
404
405\begin{quote}\begin{verbatim}
406
407@@
408@@
409
410f(X);
411... WHEN != h(Z)
412g(Y);
413h(Z);
414\end{verbatim}\end{quote}
415
416\[\begin{array}{l}
417\mita{\sf{let}} \, \mita{l1} = \exists \mita{X} . \mita{f(X);} \, \mita{\sf{in}} \, \mita{l1} \wedge (\AX(\exists \mita{Z} . (\mita{\sf{let}} \, \mita{l2} = \exists \mita{Y} . \mita{g(Y);} \, \mita{\sf{in}} \, \A[((\neg \mita{h(Z)}) \wedge (\neg (\mita{l2} \vee \mita{l1})))\\\mbox{} \U ((\mita{l2} \wedge (\AX(\mita{h(Z);}))) \vee \msf{After} \vee \msf{ErrorExit})]
418
419)))
420
421\end{array}\]
422
423\begin{quote}\begin{verbatim}
424
425@@
426@@
427
428f(X);
429... WHEN != h(Q)
430g(Y);
431h(Z);
432\end{verbatim}\end{quote}
433
434\[\begin{array}{l}
435\mita{\sf{let}} \, \mita{l1} = \exists \mita{X} . \mita{f(X);} \, \mita{\sf{in}} \, \mita{l1} \wedge (\AX(\mita{\sf{let}} \, \mita{l2} = \exists \mita{Y} . \mita{g(Y);} \, \mita{\sf{in}} \, \A[((\neg (\exists \mita{Q} . \mita{h(Q)})) \wedge (\neg (\mita{l2}\\\mbox{} \vee \mita{l1}))) \U ((\mita{l2} \wedge (\AX(\exists \mita{Z} . \mita{h(Z);}))) \vee \msf{After} \vee \msf{ErrorExit})]
436
437))
438
439\end{array}\]
440
441\begin{quote}\begin{verbatim}
442
443@@
444@@
445
446if (X) {
447 ...
448} else {
449 g(X);
450}
451h(Z);
452\end{verbatim}\end{quote}
453
454\[\begin{array}{l}
455\exists \mita{X} . (\mita{\sf{let}} \, \mita{l0} = \msf{FalseBranch} \, \mita{\sf{in}} \, (\mita{\sf{let}} \, \mita{l1} = \msf{After} \, \mita{\sf{in}} \, \mita{if (X) } \wedge (\AX(\mita{\sf{let}} \, \mita{l2} = \msf{Paren}(p0)\\\mbox{} \, \mita{\sf{in}} \, (\msf{TrueBranch} \wedge (\AX(\exists \mita{p0} . (\mita{\sf{let}} \, \mita{l6} = \mita{{\ttlb}
456 } \wedge \mita{l2} \, \mita{\sf{in}} \, \mita{l6} \wedge (\AX(\mita{\sf{let}} \, \mita{l5} = \mita{
457{\ttrb}} \wedge \mita{l2} \, \mita{\sf{in}} \, \A[\neg (\mita{l5}\\\mbox{} \vee \mita{l6}) \U (\mita{l5} \vee \mita{l1} \vee \msf{ErrorExit})]
458
459))
460)))) \vee (\mita{l0} \wedge (\AX(\exists \mita{p0} . (\mita{{\ttlb}
461 } \wedge \mita{l2} \wedge (\AX(\mita{g(X);} \wedge (\AX(\mita{
462{\ttrb}}\\\mbox{} \wedge \mita{l2})))))))) \vee (\mita{l1} \wedge (\AX(\exists \mita{Z} . \mita{h(Z);})))
463)) \wedge (\EX\mita{l0}) \wedge (\EX\mita{l1})
464)
465)
466\end{array}\]
467
468\begin{quote}\begin{verbatim}
469
470@@
471@@
472
473<...
474
475(
476 h(X)
477|
478 g(Y)
479)
480...>
481\end{verbatim}\end{quote}
482
483\[\begin{array}{l}
484\AG(\mita{\sf{let}} \, \mita{l2} = \exists \mita{Y} . \exists \mita{X} . \mita{
485(
486h(X)
487|
488g(Y)
489)} \, \mita{\sf{in}} \, \mita{l2} \vee (\neg \mita{l2})
490)
491\end{array}\]
492
493\begin{quote}\begin{verbatim}
494
495@@
496@@
497
498<...
499
500(
501 h(X)
502|
503 g(Y)
504)
505...>
506r(X);
507\end{verbatim}\end{quote}
508
509\[\begin{array}{l}
510\exists \mita{X} . (\mita{\sf{let}} \, \mita{l1} = \mita{r(X);} \, \mita{\sf{in}} \, \A[((\neg \mita{l1}) \wedge (\mita{\sf{let}} \, \mita{l0} = \exists \mita{Y} . \mita{
511(
512h(X)
513|
514g(Y)
515)} \, \mita{\sf{in}} \, \mita{l0} \vee (\neg \mita{l0})\\\mbox{}
516)) \U (\mita{l1} \vee \msf{After} \vee \msf{ErrorExit})]
517
518)
519\end{array}\]
520
521\begin{quote}\begin{verbatim}
522
523@@
524@@
525
526
527(
528h(X)
529|
530g(Y)
531)
532\end{verbatim}\end{quote}
533
534\[\begin{array}{l}
535\exists \mita{Y} . \exists \mita{X} . \mita{
536(
537h(X)
538|
539g(Y)
540)}
541\end{array}\]
542
543\begin{quote}\begin{verbatim}
544
545@@
546@@
547
548m(Y);
549?h(X);
550g(Y);
551\end{verbatim}\end{quote}
552
553\[\begin{array}{l}
554\exists \mita{Y} . (\mita{m(Y);} \wedge (\AX(\mita{\sf{let}} \, \mita{l0} = \mita{g(Y);} \, \mita{\sf{in}} \, ((\exists \mita{X} . \mita{h(X);}) \wedge (\AX\mita{l0})) \vee \mita{l0}
555)))
556\end{array}\]
557
558\begin{quote}\begin{verbatim}
559
560@@
561@@
562
563sht/*struct Scsi_Host_Template */.proc_info = proc_info_func;
564\end{verbatim}\end{quote}
565
566\[\begin{array}{l}
567\exists \mita{proc\_info\_func} . \exists \mita{sht} . \mita{sht/*struct Scsi\_Host\_Template */.proc\_info = proc\_info\_func;}
568\end{array}\]
569
570\begin{quote}\begin{verbatim}
571
572@@
573@@
574
575proc_info_func(char *buffer, char **start, off_t offset, int length,
576 int hostno, int inout) {
577 ...
578 struct Scsi_Host *hostptr;
579 ...
580 hostptr = scsi_host_hn_get(hostno);
581 ...
582 ?if (hostptr == NULL) ?{
583 ?...
584 ?}
585 ...
586 ?scsi_host_put(hostptr);
587 ...
588}
589\end{verbatim}\end{quote}
590
591\[\begin{array}{l}
592\exists \mita{hostno} . ((\exists \mita{buffer} . \exists \mita{start} . \exists \mita{offset} . \exists \mita{length} . \exists \mita{inout} . \mita{proc\_info\_func(char *buffer, char **start, off\_t offset, int length,
593 int hostno, int inout) })\\\mbox{} \wedge (\AX(\exists \mita{p1} . (\mita{\sf{let}} \, \mita{l33} = \msf{Paren}(p1) \, \mita{\sf{in}} \, (\mita{\sf{let}} \, \mita{l5} = \mita{{\ttlb}
594 } \wedge \mita{l33} \, \mita{\sf{in}} \, \mita{l5} \wedge (\AX(\mita{\sf{let}} \, \mita{l53} = \mita{struct Scsi\_Host *hostptr;}\\\mbox{} \, \mita{\sf{in}} \, \A[\neg ((\exists \mita{hostptr} . \mita{l53}) \vee \mita{l5}) \U (\mita{\sf{let}} \, \mita{l1} = \msf{After} \, \mita{\sf{in}} \, (\mita{\sf{let}} \, \mita{l6} = \mita{l1} \vee \msf{ErrorExit}\\\mbox{} \, \mita{\sf{in}} \, (\exists \mita{hostptr} . (\mita{l53} \wedge (\AX(\mita{\sf{let}} \, \mita{l30} = \mita{hostptr = scsi\_host\_hn\_get(hostno);}\\\mbox{} \, \mita{\sf{in}} \, \A[\neg (\mita{l30} \vee \mita{l53}) \U ((\mita{l30} \wedge (\AX(\mita{\sf{let}} \, \mita{l32} = \msf{Paren}(p0) \, \mita{\sf{in}} \, (\mita{\sf{let}} \, \mita{l50} = \mita{
595{\ttrb}} \wedge \mita{l32}\\\mbox{} \, \mita{\sf{in}} \, (\mita{\sf{let}} \, \mita{l14} = \mita{l50} \vee \mita{l6} \, \mita{\sf{in}} \, (\mita{\sf{let}} \, \mita{l2} = \msf{FallThrough} \, \mita{\sf{in}} \, (\mita{\sf{let}} \, \mita{l29} = \mita{l2} \vee \mita{l1} \, \mita{\sf{in}} \, (\mita{\sf{let}} \, \mita{l51} = \mita{{\ttlb}
596 }\\\mbox{} \wedge \mita{l32} \, \mita{\sf{in}} \, (\mita{\sf{let}} \, \mita{l0} = \msf{TrueBranch} \, \mita{\sf{in}} \, (\mita{\sf{let}} \, \mita{l52} = \mita{if (hostptr == NULL) } \, \mita{\sf{in}} \, (\mita{\sf{let}} \, \mita{l20} = \mita{l52}\\\mbox{} \wedge (\AX((\mita{l0} \wedge (\AX(\exists \mita{p0} . (\mita{l51} \wedge (\AX\AF\mita{l14}))))) \vee \mita{l29})) \, \mita{\sf{in}} \, \A[\neg (\mita{l20} \vee \mita{l30}) \U ((\mita{\sf{let}} \, \mita{l8} = \mita{scsi\_host\_put(hostptr);}\\\mbox{} \, \mita{\sf{in}} \, (\mita{\sf{let}} \, \mita{l11} = \A[\neg \mita{l8} \U \mita{l6}]
597 \, \mita{\sf{in}} \, (\mita{\sf{let}} \, \mita{l25} = \mita{l8} \wedge (\AX\mita{l11}) \, \mita{\sf{in}} \, (\mita{\sf{let}} \, \mita{l39} = \neg \mita{l25} \, \mita{\sf{in}} \, (\mita{\sf{let}} \, \mita{l13} = (\mita{\sf{let}} \, \mita{l48} = (\mita{\sf{let}} \, \mita{l4} = \mita{
598{\ttrb}}\\\mbox{} \wedge \mita{l33} \, \mita{\sf{in}} \, \A[\neg (\mita{l4} \vee \mita{l8}) \U (\mita{l4} \vee \mita{l6})]
599
600) \, \mita{\sf{in}} \, (\mita{l8} \wedge (\AX\mita{l48})) \vee (\mita{l39} \wedge \mita{l48})
601) \vee \mita{l6} \, \mita{\sf{in}} \, (\mita{\sf{let}} \, \mita{l36} = \neg (\mita{l8}\\\mbox{} \vee \mita{l20}) \, \mita{\sf{in}} \, (\mita{\sf{let}} \, \mita{l34} = \mita{l0} \wedge (\AX(\exists \mita{p0} . (\mita{l51} \wedge (\AX\A[\neg (\mita{l50} \vee \mita{l51}) \U \mita{l14}]
602)))) \, \mita{\sf{in}} \, (\mita{\sf{let}} \, \mita{l16} = \EX\mita{l1}\\\mbox{} \, \mita{\sf{in}} \, (\mita{l52} \wedge (\AX(\mita{l34} \vee \mita{l2} \vee (\mita{l1} \wedge (\AX\A[\mita{l36} \U \mita{l13}]
603)))) \wedge \mita{l16}) \vee ((\neg (\mita{l52} \wedge (\AX(\mita{l34}\\\mbox{} \vee \mita{l2} \vee (\mita{l1} \wedge (\AX\A[\mita{l36} \U (\mita{l25} \vee (\mita{l39} \wedge \mita{l11}) \vee \mita{l6})]
604)))) \wedge \mita{l16})) \wedge (\A[\neg (\mita{l8} \vee (\mita{l52} \wedge (\AX(\mita{l34}\\\mbox{} \vee \mita{l29})))) \U \mita{l13}]
605))
606)
607)
608)
609)
610)
611)
612)
613) \vee \mita{l6})]
614
615)
616)
617)
618)
619)
620)
621)
622)
623))) \vee \mita{l6})]
624
625)))) \vee \mita{l6}
626)
627)]
628
629))
630)
631))))
632\end{array}\]
633
634\begin{quote}\begin{verbatim}
635
636@@
637@@
638
639proc_info_func(...) {
640 <...
641
642(
643 E->host_no == hostno
644|
645 hostno
646)
647 ...>
648}
649\end{verbatim}\end{quote}
650
651\[\begin{array}{l}
652\mita{proc\_info\_func(...) } \wedge (\AX(\exists \mita{p0} . (\mita{\sf{let}} \, \mita{l3} = \msf{Paren}(p0) \, \mita{\sf{in}} \, (\mita{\sf{let}} \, \mita{l6} = \mita{{\ttlb}
653 } \wedge \mita{l3}\\\mbox{} \, \mita{\sf{in}} \, \mita{l6} \wedge (\AX(\mita{\sf{let}} \, \mita{l5} = \mita{
654{\ttrb}} \wedge \mita{l3} \, \mita{\sf{in}} \, \A[((\neg (\mita{l5} \vee \mita{l6})) \wedge (\mita{\sf{let}} \, \mita{l2} = \exists \mita{E} . \mita{
655(
656E-\mth{>}host\_no == hostno
657|
658hostno
659)}\\\mbox{} \, \mita{\sf{in}} \, \mita{l2} \vee (\neg \mita{l2})
660)) \U (\mita{l5} \vee \msf{After} \vee \msf{ErrorExit})]
661
662))
663)
664)))
665\end{array}\]
666
667\end{document}
Unnamed repository; edit this file 'description' to name the repository.