autocorres: fix code inclusion in quickstart doc
The AutoCorres quickstart document includes code from `*.c` files from a given line number, to avoid including license headers and other details that aren't useful in the document. This updates the line numbers for the current license headers. Signed-off-by: Matthew Brecknell <Matthew.Brecknell@data61.csiro.au>
This commit is contained in:
parent
bb90c7541e
commit
13ca552d67
|
@ -55,7 +55,7 @@ text \<open>
|
|||
which (we expect) return the minimum and maximum respectively of two unsigned
|
||||
integers.
|
||||
|
||||
\lstinputlisting[language=C, firstline=17]{../../minmax.c}
|
||||
\lstinputlisting[language=C, firstline=13]{../../minmax.c}
|
||||
|
||||
It is easy to see that \texttt{min} is correct, but perhaps less obvious why
|
||||
\texttt{max} is correct. AutoCorres will hopefully allow us to prove these
|
||||
|
|
|
@ -34,7 +34,7 @@ text \<open>
|
|||
Our C function \texttt{mult\_by\_add} implements a multiply operation
|
||||
by successive additions:
|
||||
|
||||
\lstinputlisting[language=C, firstline=15]{../../mult_by_add.c}
|
||||
\lstinputlisting[language=C, firstline=11]{../../mult_by_add.c}
|
||||
|
||||
We start by translating the program using the C parser and AutoCorres,
|
||||
and entering the generated locale \texttt{mult\_by\_add}.
|
||||
|
|
|
@ -19,7 +19,7 @@ text \<open>
|
|||
Here, we use AutoCorres to verify a C program that reads and writes to the heap.
|
||||
Our C function, \texttt{swap}, swaps two words in memory:
|
||||
|
||||
\lstinputlisting[language=C, firstline=15]{../../swap.c}
|
||||
\lstinputlisting[language=C, firstline=11]{../../swap.c}
|
||||
|
||||
Again, we translate the program using the C parser and AutoCorres.
|
||||
\<close>
|
||||
|
|
Loading…
Reference in New Issue