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
|
\appendix
\chapter{Analysis tool results}
In the following output a min-cost flow operator is presented as
{\tt MCF<supplies,edges>(costs)}. This represents the solution to a
min-cost flow problem where each node has a cost from ``supplies'',
``edges'' indicates the topology of the directed graph and ``costs''
indicates costs of the edges (which are the arguments to the
operator).
As an example, {\tt MCF<[1,0,-1],[2:1,2:3,1:2]>(x1, x2, x3)} is a
representation of the flow network shown in Figure
\ref{fig:results-min-cost-flow}. The minimum cost flow of this network
is {\tt x2 + x3}, unless {\tt x1 = $-\infty$}, in which case the
system is infeasible and the result is $-\infty$.
\begin{figure}[H]
\begin{tikzpicture}[->,>=stealth',shorten >=1pt,auto,node
distance=2cm,main node/.style={circle,fill=blue!20,draw},every
loop/.style={min distance=1.5cm}]
\node[main node] (2) {$0$};
\node[main node] (1) [above left of=V] {$1$};
\node[main node] (3) [above right of=V] {$-1$};
\path[every node/.style={fill=none}]
(2) edge [bend left] node{x1} (1)
(2) edge node [anchor=north west] {x2} (3)
(1) edge [bend left] node {x3} (2);
\end{tikzpicture}
\caption{An example flow network for which a min-cost flow must be
found}
\label{fig:results-min-cost-flow}
\end{figure}
The output below consists of a CFG dumped by the Clang framework,
followed by the generated equation system for the CFG. Finally the
equation system is solved and the bounds for each abstract variable at
each block is printed.
\lstset{basicstyle=\ttfamily\scriptsize,breaklines=true,breakatwhitespace=true,frame=lrtb}
\pagebreak
\section{Chain construction}
\lstinputlisting{implementation/experiments/chain-output}
In this example we show
\pagebreak
\section{Counter}
\lstinputlisting{implementation/experiments/counter-output}
\lstinputlisting{implementation/experiments/backwards_counter-output}
\pagebreak
\section{Nested Loops}
\lstinputlisting{implementation/experiments/nested-output}
\pagebreak
\section{Double counting}
\lstinputlisting{implementation/experiments/example-output}
In this example
\pagebreak
\section{Fibonacci}
\lstinputlisting{implementation/experiments/fib-output}
\pagebreak
\section{Unreachable}
\lstinputlisting{implementation/experiments/irreducible-output}
|
