adbrucker
/
lh-l4v
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

autocorres: point C parser links to GitHub 

TS C parser web page has been retired.

Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
This commit is contained in:
Gerwin Klein 2024-01-16 10:11:25 +11:00 committed by Achim D. Brucker
parent 77050f3034
commit d5fcddecfd
4 changed files with 6 additions and 6 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
tools/autocorres/README.md
View File

@ -16,7 +16,7 @@ abstracts the result to produce a result that is (hopefully)
more pleasant to reason about. more pleasant to reason about.
[1]: https://isabelle.in.tum.de [1]: https://isabelle.in.tum.de
[2]: https://trustworthy.systems/software/TS/c-parser/ [2]: https://github.com/seL4/l4v/blob/master/tools/c-parser/README.md

4
tools/autocorres/doc/quickstart/Chapter1_MinMax.thy
View File

@ -69,8 +69,8 @@ text \<open>
As mentioned earlier, AutoCorres does not handle C code directly. The first As mentioned earlier, AutoCorres does not handle C code directly. The first
step is to apply the step is to apply the
C-Parser\footnote{\url{https://trustworthy.systems/software/TS/c-parser}} to C-Parser\footnote{\url{https://github.com/seL4/l4v/blob/master/tools/c-parser/README.md}}
obtain a SIMPL translation. We do this using the \texttt{install-C-file} to obtain a SIMPL translation. We do this using the \texttt{install-C-file}
command in Isabelle, as shown. command in Isabelle, as shown.
\<close> \<close>

2
tools/autocorres/doc/quickstart/document/root.bib
View File

@ -25,7 +25,7 @@
title = {{C-to-Isabelle} Parser, version 1.13.0}, title = {{C-to-Isabelle} Parser, version 1.13.0},
year = 2013, year = 2013,
month = may, month = may,
url = {https://trustworthy.systems/software/TS/c-parser/}, url = {https://github.com/seL4/l4v/blob/master/tools/c-parser/README.md},
note = {Accessed May 2016} note = {Accessed May 2016}
} }

4
tools/autocorres/tools/release_files/README
View File

@ -8,7 +8,7 @@ abstracts the result to produce a result that is (hopefully)
more pleasant to reason about. more pleasant to reason about.
[1]: https://isabelle.in.tum.de/ [1]: https://isabelle.in.tum.de/
[2]: https://trustworthy.systems/software/TS/c-parser/ [2]: https://github.com/seL4/l4v/blob/master/tools/c-parser/README.md
@ -107,7 +107,7 @@ This package contains:
* Michael Norrish's C parser, used to translate C code into Isabelle: * Michael Norrish's C parser, used to translate C code into Isabelle:
https://trustworthy.systems/software/TS/c-parser/ https://github.com/seL4/l4v/blob/master/tools/c-parser/README.md
* Norbert Schirmer's Simpl language and associated VCG tool. The * Norbert Schirmer's Simpl language and associated VCG tool. The
C parser translates C into Schirmer's Simpl language: C parser translates C into Schirmer's Simpl language: