aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorYann Herklotz <git@yannherklotz.com>2021-09-20 10:02:03 +0100
committerYann Herklotz <git@yannherklotz.com>2021-09-20 10:02:03 +0100
commitd9f8dee1a294ee087f56c6e54b16ad3b0bf8d895 (patch)
tree099f61b28947f0bc441c632df8576cc4e28a59b3
parent5508c21e064276aa4d5146b3af5b6f6e9a4c2364 (diff)
downloadvericert-docs-d9f8dee1a294ee087f56c6e54b16ad3b0bf8d895.tar.gz
vericert-docs-d9f8dee1a294ee087f56c6e54b16ad3b0bf8d895.zip
Edit the current list of features
-rw-r--r--documentation.org4
1 files changed, 2 insertions, 2 deletions
diff --git a/documentation.org b/documentation.org
index b807b81..c9d1932 100644
--- a/documentation.org
+++ b/documentation.org
@@ -16,8 +16,8 @@ correctness.
** Features
-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:
+The project is currently a work in progress. Currently, the following C features are supported and
+have all been proven correct, providing a verified translation from C to Verilog:
- all int operations,
- non-recursive function calls,