diff options
Diffstat (limited to 'README.org')
| -rw-r--r-- | README.org | 29 |
1 files changed, 16 insertions, 13 deletions
@@ -1,3 +1,5 @@ +#+title: + #+html: <a href="https://vericert.ymhg.org"><img src="https://vericert.ymhg.org/vericert-main.svg" width="100%" height="144" /></a> #+html: <p align=center><a href="https://github.com/ymherklotz/vericert/actions"><img src="https://github.com/ymherklotz/vericert/workflows/CI/badge.svg" /></a> <a href="https://vericert.ymhg.org/"><img src="https://github.com/ymherklotz/vericert-docs/workflows/docs/badge.svg" /></a></p> @@ -11,8 +13,8 @@ correctness. :PROPERTIES: :CUSTOM_ID: features :END: -The project is currently a work in progress, so proofs remain to be finished. Currently, the -following C features are supported, but are not all proven correct yet: + +Currently all proofs of the following features have been completed. - all int operations, - non-recursive function calls, @@ -32,7 +34,6 @@ compiled and executed. The dependencies of this project are the following: - [[https://coq.inria.fr/][Coq]]: theorem prover that is used to also program the HLS tool. - [[https://ocaml.org/][OCaml]]: the OCaml compiler to compile the extracted files. -- [[https://github.com/mit-plv/bbv][bbv]]: an efficient bit vector library. - [[https://github.com/ocaml/dune][dune]]: build tool for ocaml projects to gather all the ocaml files and compile them in the right order. - [[http://gallium.inria.fr/~fpottier/menhir/][menhir]]: parser generator for ocaml. @@ -41,23 +42,25 @@ compiled and executed. The dependencies of this project are the following: These dependencies can be installed manually, or automatically through Nix. -*** Downloading CompCert +*** Downloading Vericert and CompCert :PROPERTIES: :CUSTOM_ID: downloading-compcert :END: CompCert is added as a submodule in the =lib/CompCert= directory. It is needed to run the build process below, as it is the one dependency that is not downloaded by nix, and has to be downloaded -together with the repository. To clone CompCert together with this project, you can run: +together with the repository. To clone CompCert together with this project, and check it out at the +correct revision, you can run: #+begin_src shell - git clone --recursive https://github.com/ymherklotz/vericert +git clone -b v1.2.2 --recursive https://github.com/ymherklotz/vericert #+end_src If the repository is already cloned, you can run the following command to make sure that CompCert is -also downloaded: +also downloaded and the correct branch is checked out: #+begin_src shell - git submodule update --init +git checkout v1.2.2 +git submodule update --init #+end_src *** Setting up Nix @@ -70,7 +73,7 @@ reproducible. Once nix is installed, it can be used in the following way. To open a shell which includes all the necessary dependencies, one can use: #+begin_src shell - nix-shell +nix-shell #+end_src which will open a shell that has all the dependencies loaded. @@ -83,7 +86,7 @@ If the dependencies were installed manually, or if one is in the =nix-shell=, th by running: #+begin_src shell - make -j8 +make -j8 #+end_src and installed locally, or under the =PREFIX= location using: @@ -103,9 +106,9 @@ To test out =vericert= you can try the following examples which are in the test following: #+begin_src shell - ./bin/vericert test/loop.c -o loop.v - ./bin/vericert test/conditional.c -o conditional.v - ./bin/vericert test/add.c -o add.v +./bin/vericert test/loop.c -o loop.v +./bin/vericert test/conditional.c -o conditional.v +./bin/vericert test/add.c -o add.v #+end_src ** Citation |