# Changeset 3310 for Papers

Ignore:
Timestamp:
Jun 4, 2013, 6:19:47 PM (6 years ago)
Message:

An example.

File:
1 edited

### Legend:

Unmodified
 r3309 \usepackage{color} \usepackage{fancybox} \usepackage{fancyvrb} \usepackage{graphicx} \usepackage[colorlinks]{hyperref} %\def\lstlanguagefiles{lst-grafite.tex} %\lstset{language=Grafite} \lstset{language=C} \newlength{\mylength} I/O operations can be performed in the prefix of the run, but not in the measurable sub-run. Therefore we prove that we can predict reaction times, but not I/O times, as it should be. \begin{figure}[t] \begin{lstlisting} char a[] = {3, 2, 7, -4}; char treshold = 4; int main() { 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.} \label{test1} \end{figure} \fvset{commandchars=\\\{\}} \lstset{morecomment=[s][\color{blue}]{/*@}{*/}, moredelim=[is][\color{blue}]{$}{$}, moredelim=[is][\color{red}]{|}{|}} \begin{figure}[!p] \begin{lstlisting} |int __cost = 33; int __stack = 5, __stack_max = 5;| |void __cost_incr(int incr) { __cost = __cost + incr; }| |void __stack_incr(int incr) { __stack = __stack + incr; __stack_max = __stack_max < __stack ? __stack : __stack_max; }| unsigned char a[4] = { 3, 2, 7, 252, }; unsigned char treshold = 4; /*@ behavior stack_cost: ensures __stack_max <= __max(\old(__stack_max), \old(__stack)); ensures __stack == \old(__stack); behavior time_cost: ensures __cost <= \old(__cost)+1228; */ int main(void) { char j; char *p; int found; |__stack_incr(0); __cost_incr(91);| p = a; found = 0; $__l: /* internal */$ /*@ for time_cost: loop invariant __cost <= \at(__cost,__l)+220*(__max(\at(5-j,__l), 0)-__max (5-j, 0)); for stack_cost: loop invariant __stack_max == \at(__stack_max,__l); for stack_cost: loop invariant __stack == \at(__stack,__l); loop variant 4-j; */ for (j = 0; j < 4; j++) { |__cost_incr(76);| if (*p <= treshold) { |__cost_incr(144);| found++; } else { |__cost_incr(122);| } p++; } |__cost_incr(37); __stack_incr(-0);| return found; } \end{lstlisting} \caption{The instrumented version of the program in \autoref{test1}.} \label{itest1} \end{figure} \bibliography{fopara13.bib}