From 26f42f6ac3207e9f286eee05d94c44a8a17a87d4 Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Fri, 14 Oct 2022 17:46:01 +0200
Subject: [PATCH] [aorai] clean up example files in the doc
---
doc/aorai/example/README | 25 ++++-----
doc/aorai/example/example.ltl | 6 ---
doc/aorai/example/example_loop.c | 54 +++++--------------
doc/aorai/example/example_loop.ltl | 13 -----
.../{example_loop2.ya => example_loop.ya} | 0
doc/aorai/example/example_loop2.c | 15 ------
6 files changed, 23 insertions(+), 90 deletions(-)
delete mode 100644 doc/aorai/example/example.ltl
delete mode 100644 doc/aorai/example/example_loop.ltl
rename doc/aorai/example/{example_loop2.ya => example_loop.ya} (100%)
delete mode 100644 doc/aorai/example/example_loop2.c
diff --git a/doc/aorai/example/README b/doc/aorai/example/README
index 8bfe2ea67a3..b2c416e266f 100644
--- a/doc/aorai/example/README
+++ b/doc/aorai/example/README
@@ -10,25 +10,24 @@ This directory contains 2 examples:
----------
* example.c - program to check
- * example.ltl - LTL formula to use
+ * example.ya - YA automaton
* example_annot.c - example of generated file
1.2) Usage
----------
-Each of the two following commands generate the example_annot.c file:
+The following commands generates the example_annot.c file:
frama-c example.c -aorai-automata example.ya
- or
- frama-c example.c -aorai-ltl example.ltl
-The generation process gives two warning, since an operation is never called in the code.
+The generation process gives two warnings, since an operation is never called in the code.
-Files example.ya and example.ltl are the description of the same property in two syntax.
+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 the property, it is sufficient to establish than the generated C is valid. For instance, with the Jessie plugin:
+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 -jessie -jessie-why-opt="-fast-wp"
+ frama-c example_annot.c -wp
2) Example 2 (with a loop)
==========================
@@ -37,7 +36,7 @@ In order to decide if the original program is correct wrt the property, it is su
----------
* example_loop.c - program to check
- * example_loop.ltl - LTL formula to use
+ * example_loop.ya - YA automaton
* example_loop_annot.c - example of generated file
2.2) Usage
@@ -45,11 +44,9 @@ In order to decide if the original program is correct wrt the property, it is su
The following command generates the example_loop_annot.c file:
- frama-c example_loop.c -aorai-ltl example_loop.ltl
+ 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 Jessie plugin:
-
- frama-c example_loop_annot.c -jessie -jessie-why-opt="-fast-wp"
-
+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/example.ltl b/doc/aorai/example/example.ltl
deleted file mode 100644
index 6df141a1475..00000000000
--- a/doc/aorai/example/example.ltl
+++ /dev/null
@@ -1,6 +0,0 @@
-CALL(main)
-&& _X_ (CALL(opa)
- && _X_ (!RETURN(opb)
- && _X_ (!CALL(opa)
- && _X_ (RETURN(opb)
- && _X_ (RETURN(main))))))
diff --git a/doc/aorai/example/example_loop.c b/doc/aorai/example/example_loop.c
index 507e443c621..907ed6c0560 100644
--- a/doc/aorai/example/example_loop.c
+++ b/doc/aorai/example/example_loop.c
@@ -1,45 +1,15 @@
-int cpt=3;
-//@ global invariant inv_cpt : 0<=cpt<=3;
-
-int status=0;
-//@ global invariant inv_status : 0<=status<=1;
-
-
-/*@ requires \true;
- @ behavior a :
- @ ensures 0<=\result<=1;
-*/
-int commit_trans() {
- return 1;
-}
-
-/*@ requires \true;
- @ behavior a :
- @ ensures 0<=\result<=1;
-*/
-int init_trans() {
- return 1;
-}
-
-/*@ requires \true;
- @ behavior a :
- @ ensures 0<=\result<=1;
-*/
-int main(){
- cpt=3;
- status=0;
- /*@ loop invariant i :
- @ 0<=status<=1
- @ && 0<=cpt<=3
- @ && (cpt==0 ==> status==0);
- */
- while (cpt>0) {
- status=init_trans();
- if (status && (status=commit_trans())) goto label_ok;
- cpt--;
+int f() {}
+
+int g() {}
+
+int main(int c) {
+ if (c<0) { c = 0; }
+ if (c>5) { c = 5; }
+ /*@ assert 0<=c<=5; */
+ while (c) {
+ f();
+ g();
+ c--;
}
return 0;
-
- label_ok:
- return 1;
}
diff --git a/doc/aorai/example/example_loop.ltl b/doc/aorai/example/example_loop.ltl
deleted file mode 100644
index d548c6b9311..00000000000
--- a/doc/aorai/example/example_loop.ltl
+++ /dev/null
@@ -1,13 +0,0 @@
-_G_(
- RETURN(main) ||
- (((_X_ CALL(commit_trans))
- =>
- (RETURN(init_trans) && status)
- )
- &&
- ((RETURN(init_trans) && status)
- =>
- (_X_ CALL(commit_trans))
- )
- )
-)
diff --git a/doc/aorai/example/example_loop2.ya b/doc/aorai/example/example_loop.ya
similarity index 100%
rename from doc/aorai/example/example_loop2.ya
rename to doc/aorai/example/example_loop.ya
diff --git a/doc/aorai/example/example_loop2.c b/doc/aorai/example/example_loop2.c
deleted file mode 100644
index 907ed6c0560..00000000000
--- a/doc/aorai/example/example_loop2.c
+++ /dev/null
@@ -1,15 +0,0 @@
-int f() {}
-
-int g() {}
-
-int main(int c) {
- if (c<0) { c = 0; }
- if (c>5) { c = 5; }
- /*@ assert 0<=c<=5; */
- while (c) {
- f();
- g();
- c--;
- }
- return 0;
-}
--
GitLab