Changeset 3311


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

...

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Papers/fopara2013/fopara13.tex

    r3310 r3311  
    237237
    238238\begin{figure}[t]
     239\begin{tabular}{l@{\hspace{0.2cm}}|l}
    239240\begin{lstlisting}
    240241char a[] = {3, 2, 7, -4};
     
    242243
    243244int main() {
    244         char j;
    245         char *p = a;
    246         int found = 0;
    247         for (j=0; j < 4; j++) {
    248                 if (*p <= treshold) { found++; }
    249                 p++;
    250         }
    251         return found;
     245  char j;
     246  char *p = a;
     247  int found = 0;
     248  for (j=0; j < 4; j++) {
     249    if (*p <= treshold)
     250      { found++; }
     251    p++;
     252  }
     253  return found;
    252254}
    253255\end{lstlisting}
    254 \caption{A simple C program.}
     256&
     257 $\vcenter{\includegraphics[width=7.5cm]{interaction_diagram.pdf}}$
     258\end{tabular}
     259\caption{On the left: a C program that counts the array's elements
     260 greater or equal to the treshold. On the right: CerCo's interaction
     261 diagram.}
    255262\label{test1}
    256263\end{figure}
     
    274281}|
    275282
    276 unsigned char a[4] = { 3, 2, 7, 252, };
    277 unsigned char treshold = 4;
     283char a[4] = { 3, 2, 7, 252, };
     284char treshold = 4;
    278285
    279286/*@ behavior stack_cost:
     
    315322}
    316323\end{lstlisting}
    317 \caption{The instrumented version of the program in \autoref{test1}.}
     324\caption{The instrumented version of the program in \autoref{test1}.
     325 Lines in red are instrumentation added by the CerCo compiler. The
     326 cost invariants in blue are added by the Frama-C plugin and automatically
     327 verified by CVC3 in 8s. The time costs are in clock cycles. Being non recursive, the
     328 main function uses no stack (all the variables are kept in registers).
     329 The global data occupies 5 bytes and 33 clock
     330 cycles for the initialization (before calling \texttt{main}).
     331}
    318332\label{itest1}
    319333\end{figure}
    320334
     335\begin{figure}
     336 \includegraphics[width=7.5cm]{interaction_diagram.pdf}
     337 \caption{The interaction diagram of CerCo.}
     338\end{figure}
     339
    321340
    322341\bibliography{fopara13.bib}
Note: See TracChangeset for help on using the changeset viewer.