From 7c9a21dff7ee65a8ef4f4d3b65fbabb7c2a6eb48 Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Fri, 14 Oct 2022 18:30:56 +0200
Subject: [PATCH] [aorai] clean up generation of example archive

---
 doc/aorai/Makefile          |  7 ++---
 doc/aorai/example/README    | 52 --------------------------------
 doc/aorai/example/README.md | 60 +++++++++++++++++++++++++++++++++++++
 3 files changed, 63 insertions(+), 56 deletions(-)
 delete mode 100644 doc/aorai/example/README
 create mode 100644 doc/aorai/example/README.md

diff --git a/doc/aorai/Makefile b/doc/aorai/Makefile
index bb56a790d23..6a5f48cf367 100644
--- a/doc/aorai/Makefile
+++ b/doc/aorai/Makefile
@@ -28,10 +28,9 @@
 DWNLDDIR=../manuals
 DOCNAME=aorai-manual.pdf
 ARCHIVENAME=aorai-example
-EXAMPLES=example.c example.ltl example.ya \
-         example_loop.c example_loop.ltl \
-         example_loop2.c example_loop2.ya \
-         README
+EXAMPLES=example.c example.ya \
+         example_loop.c example_loop.ya \
+         README.md
 
 BNF=ya_file.bnf basic_ya.bnf extended_ya.bnf ya_variables.bnf
 
diff --git a/doc/aorai/example/README b/doc/aorai/example/README
deleted file mode 100644
index b2c416e266f..00000000000
--- a/doc/aorai/example/README
+++ /dev/null
@@ -1,52 +0,0 @@
-               READ ME file for the Aorai example
-               ==================================
-
-This directory contains 2 examples:
-
-1) Example 1 (with many goto)
-=============================
-
-1.1) Files
-----------
-
-  * example.c - program to check
-  * example.ya - YA automaton
-  * example_annot.c - example of generated file
-
-1.2) Usage
-----------
-
-The following commands generates the example_annot.c file:
-
-     frama-c example.c -aorai-automata example.ya
-
-The generation process gives two warnings, since an operation is never called in the code.
-
-File example.ya is the automaton that describes the sequences of function calls that are allowed for the program.
-
-In order to decide if the original program is correct wrt this automaton, it is sufficient to establish than the generated C is valid with respect to the generated ACSL annotations.
-For instance, with the WP plugin:
-
-     frama-c example_annot.c -wp
-
-2) Example 2 (with a loop)
-==========================
-
-2.1) Files
-----------
-
-  * example_loop.c - program to check
-  * example_loop.ya - YA automaton
-  * example_loop_annot.c - example of generated file
-
-2.2) Usage
-----------
-
-The following command generates the example_loop_annot.c file: 
-
-     frama-c example_loop.c -aorai-automaton example_loop.ya
-
-
-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:
-
-     frama-c example_loop_annot.c  -wp
diff --git a/doc/aorai/example/README.md b/doc/aorai/example/README.md
new file mode 100644
index 00000000000..ba51be2c35b
--- /dev/null
+++ b/doc/aorai/example/README.md
@@ -0,0 +1,60 @@
+# Aoraï usage example
+
+This directory contains 2 examples:
+
+## Example 1 (with many goto)
+
+### Files
+
+- `example.c`: program to check
+- `example.ya`: YA automaton
+
+### Usage
+
+The following commands generates the `example_annot.c` file containing the instrumented code
+
+```sh
+frama-c example.c -aorai-automata example.ya -then-last -ocode example_annot.c -print
+```
+
+File `example.ya` is the automaton that describes the sequences of function calls that are allowed for the program.
+
+In order to decide if the original program is correct wrt this automaton, it is sufficient to establish than the generated C is valid with respect to the generated ACSL annotations.
+For instance, with the WP plugin:
+
+```sh
+frama-c example_annot.c -wp
+```
+
+It is also possible to run Aoraï and WP in a single Frama-C run with
+
+```sh
+frama-c example.c -aorai-automata example.ya -then-last -wp
+```
+
+## Example 2 (with a loop)
+
+### Files
+
+- `example_loop.c`: program to check
+- `example_loop.ya`: YA automaton
+
+### Usage
+
+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
+```
+
+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:
+
+```sh
+frama-c example_loop_annot.c  -wp
+```
+
+Again, it is possible to run Aoraï and WP in a single Frama-C run:
+
+```sh
+frama-c example_loop.c -aorai-automata example_loop.ya -then-last -wp
+```
-- 
GitLab