Source

cil-template / test / tut11.tex

\noindent
\ttfamily
\hlstd{}\section{\texttt{test/tut11.c}}\hlstd{}\hltscom{This C source file contains an example function that we \hlstd{}will use to demonstrate the features developed in\hlstd{}\texttt{tut11.ml}. In particular we will verify that a function \hlstd{}will successfully initialize an integer array to contain the \hlstd{}number 4 at each entry.}\hlstd{}\hlbegincode{}\hlstd{}\hspace*{\fill}\\
\hldir{\#include\ $<$ciltut.h$>$\ }\hlslc{//\ For\ the\ pre,\ post\ and\ invariant\ annotations.}\hspace*{\fill}\\
\hldir{}\hlstd{}\hlendcode{}\hlstd{}\hltscom{The function \texttt{arr\_init} loops over the given \hlstd{}array setting each element to 4. The precondition to the function \hlstd{}states that the parameter \texttt{n} must be positive. The \hlstd{}postcondition states that each element of the array is 4. The\hlstd{}loop invariant states that the loop index stays in bounds, and\hlstd{}that the array up to the value of the loop index is initialized \hlstd{}to be 4.}\hlstd{}\hlbegincode{}\hlstd{}\hspace*{\fill}\\
\hlkwb{void\ }\hlstd{}\hlsym{(}\hlstd{}\hlkwd{pre}\hlstd{}\hlsym{(}\hlstd{n\ }\hlsym{$>$\ }\hlstd{}\hlnum{0}\hlstd{}\hlsym{)}\hspace*{\fill}\\
\hlstd{}\hlstd{\ \ \ \ \ \ }\hlstd{}\hlkwd{post}\hlstd{}\hlsym{(}\hlstd{}\hlkwd{forall}\hlstd{}\hlsym{(}\hlstd{j}\hlsym{,}\hlstd{}\hlkwd{implies}\hlstd{}\hlsym{(}\hlstd{j}\hlsym{$>$=}\hlstd{}\hlnum{0\ }\hlstd{}\hlsym{\&\&\ }\hlstd{j\ }\hlsym{$<$\ }\hlstd{n}\hlsym{,{*}(}\hlstd{a}\hlsym{+}\hlstd{j}\hlsym{)==}\hlstd{}\hlnum{4}\hlstd{}\hlsym{)))}\hspace*{\fill}\\
\hlstd{}\hlstd{\ \ \ \ \ \ }\hlstd{arr\textunderscore init}\hlsym{)(}\hlstd{}\hlkwb{int\ }\hlstd{}\hlsym{{*}}\hlstd{a}\hlsym{,\ }\hlstd{}\hlkwb{int\ }\hlstd{n}\hlsym{)}\hspace*{\fill}\\
\hlstd{}\hlsym{\{}\hspace*{\fill}\\
\hlstd{}\hlstd{\ \ }\hlstd{}\hlkwb{int\ }\hlstd{i}\hlsym{;}\hspace*{\fill}\\
\hlstd{\hspace*{\fill}\\
}\hlstd{\ \ }\hlstd{}\hlkwa{for\ }\hlstd{}\hlsym{(}\hlstd{i\ }\hlsym{=\ }\hlstd{}\hlnum{0}\hlstd{}\hlsym{;\ }\hlstd{i\ }\hlsym{$<$\ }\hlstd{n}\hlsym{;\ }\hlstd{i}\hlsym{++)}\hspace*{\fill}\\
\hlstd{}\hlstd{\ \ }\hlstd{}\hlsym{\{\ }\hlstd{}\hlkwd{invariant}\hlstd{}\hlsym{(}\hlstd{i\ }\hlsym{!=\ }\hlstd{n}\hlsym{,}\hspace*{\fill}\\
\hlstd{}\hlstd{\ \ \ \ \ \ \ \ \ \ \ \ \ \ }\hlstd{i\ }\hlsym{$>$=\ }\hlstd{}\hlnum{0\ }\hlstd{}\hlsym{\&\&\ }\hlstd{i\ }\hlsym{$<$=\ }\hlstd{n\ }\hlsym{\&\&\ }\hlstd{}\hlkwd{forall}\hlstd{}\hlsym{(}\hlstd{j}\hlsym{,\ }\hlstd{}\hlkwd{implies}\hlstd{}\hlsym{(}\hlstd{j}\hlsym{$>$=}\hlstd{}\hlnum{0\ }\hlstd{}\hlsym{\&\&\ }\hlstd{j}\hlsym{$<$}\hlstd{i}\hlsym{,\ {*}(}\hlstd{a}\hlsym{+}\hlstd{j}\hlsym{)\ ==\ }\hlstd{}\hlnum{4}\hlstd{}\hlsym{)),}\hspace*{\fill}\\
\hlstd{}\hlstd{\ \ \ \ \ \ \ \ \ \ \ \ \ \ }\hlstd{i}\hlsym{)}\hspace*{\fill}\\
\hlstd{}\hlstd{\ \ \ \ }\hlstd{a}\hlsym{{[}}\hlstd{i}\hlsym{{]}\ =\ }\hlstd{}\hlnum{4}\hlstd{}\hlsym{;}\hspace*{\fill}\\
\hlstd{}\hlstd{\ \ }\hlstd{}\hlsym{\}}\hspace*{\fill}\\
\hlstd{\hspace*{\fill}\\
}\hlstd{\ \ }\hlstd{}\hlkwa{return}\hlstd{}\hlsym{;}\hspace*{\fill}\\
\hlstd{}\hlsym{\}}\hspace*{\fill}\\
\hlstd{}\hlendcode{}\hlstd{}\hltscom{The \texttt{main} function simply invokes the \hlstd{}\texttt{arr\_init} function on a local array. \hlstd{}\exercise{Extend the checking in \texttt{tut11.ml} to also verify \hlstd{}that function preconditions are satisfied.}\hlstd{}The annotations we have added have no runtime effects.}\hlstd{}\hlbegincode{}\hlstd{}\hspace*{\fill}\\
\hlkwb{int\ }\hlstd{}\hlkwd{main}\hlstd{}\hlsym{()}\hspace*{\fill}\\
\hlstd{}\hlsym{\{}\hspace*{\fill}\\
\hlstd{}\hlstd{\ \ }\hlstd{}\hlkwb{int\ }\hlstd{arr}\hlsym{{[}}\hlstd{}\hlnum{5}\hlstd{}\hlsym{{]};}\hspace*{\fill}\\
\hlstd{\hspace*{\fill}\\
}\hlstd{\ \ }\hlstd{}\hlkwd{arr\textunderscore init}\hlstd{}\hlsym{(\&}\hlstd{arr}\hlsym{{[}}\hlstd{}\hlnum{0}\hlstd{}\hlsym{{]},\ }\hlstd{}\hlnum{5}\hlstd{}\hlsym{);}\hspace*{\fill}\\
\hlstd{\hspace*{\fill}\\
}\hlstd{\ \ }\hlstd{}\hlkwa{return\ }\hlstd{}\hlnum{0}\hlstd{}\hlsym{;}\hspace*{\fill}\\
\hlstd{}\hlsym{\}}\hspace*{\fill}\\
\hlstd{}\hlendcode{}\hlstd{}\hspace*{\fill}\\
\mbox{}
\normalfont
Tip: Filter by directory path e.g. /media app.js to search for public/media/app.js.
Tip: Use camelCasing e.g. ProjME to search for ProjectModifiedEvent.java.
Tip: Filter by extension type e.g. /repo .js to search for all .js files in the /repo directory.
Tip: Separate your search with spaces e.g. /ssh pom.xml to search for src/ssh/pom.xml.
Tip: Use ↑ and ↓ arrow keys to navigate and return to view the file.
Tip: You can also navigate files with Ctrl+j (next) and Ctrl+k (previous) and view the file with Ctrl+o.
Tip: You can also navigate files with Alt+j (next) and Alt+k (previous) and view the file with Alt+o.