# Changeset 3311 for Papers/fopara2013

Ignore:
Timestamp:
Jun 4, 2013, 6:37:44 PM (7 years ago)
Message:

...

File:
1 edited

### Legend:

Unmodified
 r3310 \begin{figure}[t] \begin{tabular}{l@{\hspace{0.2cm}}|l} \begin{lstlisting} char a[] = {3, 2, 7, -4}; int main() { char j; char *p = a; int found = 0; for (j=0; j < 4; j++) { if (*p <= treshold) { found++; } p++; } return found; char j; char *p = a; int found = 0; for (j=0; j < 4; j++) { if (*p <= treshold) { found++; } p++; } return found; } \end{lstlisting} \caption{A simple C program.} & $\vcenter{\includegraphics[width=7.5cm]{interaction_diagram.pdf}}$ \end{tabular} \caption{On the left: a C program that counts the array's elements greater or equal to the treshold. On the right: CerCo's interaction diagram.} \label{test1} \end{figure} }| unsigned char a[4] = { 3, 2, 7, 252, }; unsigned char treshold = 4; char a[4] = { 3, 2, 7, 252, }; char treshold = 4; /*@ behavior stack_cost: } \end{lstlisting} \caption{The instrumented version of the program in \autoref{test1}.} \caption{The instrumented version of the program in \autoref{test1}. Lines in red are instrumentation added by the CerCo compiler. The cost invariants in blue are added by the Frama-C plugin and automatically verified by CVC3 in 8s. The time costs are in clock cycles. Being non recursive, the main function uses no stack (all the variables are kept in registers). The global data occupies 5 bytes and 33 clock cycles for the initialization (before calling \texttt{main}). } \label{itest1} \end{figure} \begin{figure} \includegraphics[width=7.5cm]{interaction_diagram.pdf} \caption{The interaction diagram of CerCo.} \end{figure} \bibliography{fopara13.bib}