diff --git a/doc/aorai/example/README.md b/doc/aorai/example/README.md index ba51be2c35be160cc892ad4206140037cca0402a..7193041d206f40fce04d7ab5ca222bf849818096 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: