From dcad7213b0fd4b568b99609c932cb3ad294836f2 Mon Sep 17 00:00:00 2001 From: Valentin Perrelle <valentin.perrelle@cea.fr> Date: Wed, 26 Oct 2022 13:08:29 +0000 Subject: [PATCH] fix md syntax --- doc/aorai/example/README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/doc/aorai/example/README.md b/doc/aorai/example/README.md index ba51be2c35b..7193041d206 100644 --- a/doc/aorai/example/README.md +++ b/doc/aorai/example/README.md @@ -44,7 +44,7 @@ frama-c example.c -aorai-automata example.ya -then-last -wp The following command generates the `example_loop_annot.c` file ```sh -frama-c example_loop.c -aorai-automata example_loop.ya -then-last -ocode example_loop_annot.c` file +frama-c example_loop.c -aorai-automata example_loop.ya -then-last -ocode example_loop_annot.c file ``` In order to decide if the original program is correct wrt the property, it is sufficient to establish than the generated C is valid. For instance, with the WP plugin: -- GitLab