From 26fbe3803507fb95f658a888cb225a298644a77b Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Mon, 27 Sep 2021 18:14:33 +0100 Subject: Add empty title --- README.org | 2 ++ 1 file changed, 2 insertions(+) (limited to 'README.org') diff --git a/README.org b/README.org index 4426561..e899bde 100644 --- a/README.org +++ b/README.org @@ -1,3 +1,5 @@ +#+title: + #+html: #+html:

 

-- cgit From d7a08d9b3523aadc10b0d32baa6ec2d8508ef9a3 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Mon, 27 Sep 2021 20:12:21 +0100 Subject: Update README on the status of Vericert --- README.org | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'README.org') diff --git a/README.org b/README.org index e899bde..faee0cc 100644 --- a/README.org +++ b/README.org @@ -13,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, -- cgit From 1cb470d7b34a6e4fba73e0c57e51c44a220912bb Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Fri, 1 Oct 2021 19:42:17 +0100 Subject: Fix citation file and README --- README.org | 1 - 1 file changed, 1 deletion(-) (limited to 'README.org') diff --git a/README.org b/README.org index faee0cc..09e2968 100644 --- a/README.org +++ b/README.org @@ -34,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. -- cgit From 0b6938e44cde14ed66e6b7af943d3176b5c559cd Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Fri, 1 Oct 2021 20:11:17 +0100 Subject: Update README with checkout instructions --- README.org | 22 ++++++++++++---------- 1 file changed, 12 insertions(+), 10 deletions(-) (limited to 'README.org') diff --git a/README.org b/README.org index 09e2968..cf8bd34 100644 --- a/README.org +++ b/README.org @@ -42,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 @@ -71,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. @@ -84,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: @@ -104,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 -- cgit