diff --git a/doc/developer/.gitignore b/doc/developer/.gitignore
index b8344f6c7c60d73ddd53c5daf71a3d80305c2979..2a5270788248055f10119ae94c106e82f525eff7 100644
--- a/doc/developer/.gitignore
+++ b/doc/developer/.gitignore
@@ -17,5 +17,5 @@ mecanism.eps
pp
pp.ml
/checks/hello/*.res
-/tutorial/hello/v6-test-with-bug/tests/hello/oracle/
-/tutorial/hello/v6-test-with-bug/tests/hello/result/
+/**/tests/**/result*/
+/**/tests/**/oracle*/dune
diff --git a/doc/developer/Makefile b/doc/developer/Makefile
index d74f5d54efd8f2d876c95c05e548668c1a7bac56..7825f1cba79ffb3cb0a7502133f8b29788940abe 100644
--- a/doc/developer/Makefile
+++ b/doc/developer/Makefile
@@ -47,7 +47,7 @@ all: developer.pdf # check << restore check later
# Thus TODO: use `dune exec -- frama-c` for the following commands
# local plugin.cmi (if any) is in conflict with the one of Frama-C
-check: $(GENERATED) check-hello
+check: $(GENERATED) check-hello check-examples
$(ECHO) Checking compilation of example scripts
$(FC_BINDIR)/frama-c \
-load-script ./examples/syntactic_check \
@@ -91,33 +91,56 @@ check-hello-clean:
check-hello-v1: check-hello-clean
(cd tutorial/hello/v1-* && $(duneb) && $(dunee) -- frama-c && cat hello.out) 2>&1 > checks/hello/v1.res
- diff checks/hello/v1.res checks/hello/v1.oracle
+ diff checks/hello/v1.oracle checks/hello/v1.res
check-hello-v2: check-hello-clean
(cd tutorial/hello/v2-* && $(duneb) && $(dunee) -- frama-c -plugins | grep Hello) 2>&1 > checks/hello/v2.res
- diff checks/hello/v2.res checks/hello/v2.oracle
+ diff checks/hello/v2.oracle checks/hello/v2.res
check-hello-v3: check-hello-clean
(cd tutorial/hello/v3-* && $(duneb) && $(dunee) -- frama-c) 2>&1 > checks/hello/v3.res
- diff checks/hello/v3.res checks/hello/v3.oracle
+ diff checks/hello/v3.oracle checks/hello/v3.res
check-hello-v4: check-hello-clean
(cd tutorial/hello/v4-* && $(duneb) && $(dunee) -- frama-c -hello) 2>&1 > checks/hello/v4.res
- diff checks/hello/v4.res checks/hello/v4.oracle
+ diff checks/hello/v4.oracle checks/hello/v4.res
check-hello-v5:check-hello-clean
(cd tutorial/hello/v5-* && $(duneb) && $(dunee) -- frama-c -hello) 2>&1 > checks/hello/v5.res
- diff checks/hello/v5.res checks/hello/v5.oracle
+ diff checks/hello/v5.oracle checks/hello/v5.res
check-hello-v6: check-hello-clean
(cd tutorial/hello/v6-* && $(duneb) @install && $(duneb) @ptests 2>&1 || true) > checks/hello/v6.res
- diff checks/hello/v6.res checks/hello/v6.oracle
+ diff checks/hello/v6.oracle checks/hello/v6.res
check-hello-v7: check-hello-clean
#redirect the stderr of 'dune build @doc' because of warnings 'Couldn't find ... Frama_c_kernel__Plugin'
#checks that a specific generated HTML file exists and contains something related to the source code
(cd tutorial/hello/v7-* && $(duneb) @install && ($(duneb) @doc 2>/dev/null) && grep -o "welcome message" _build/default/_doc/_html/frama-c-hello/Hello/Hello_options/index.html) 2>&1 > checks/hello/v7.res
- diff checks/hello/v7.res checks/hello/v7.oracle
+ diff checks/hello/v7.oracle checks/hello/v7.res
+
+# For check-examples, we perform no explicit oracle comparisons:
+# we simply build the code and run tests (which must always succeed).
+check-examples: check-examples-acsl_extension_foo check-examples-acsl_extension_ext_types \
+ check-examples-callstack check-examples-syntactic_check
+
+check-examples-clean:
+ $(ECHO) Cleaning example files...
+ rm -rf examples/*/_build
+
+check-examples-acsl_extension_foo: check-examples-clean
+ cd examples/acsl_extension_foo && $(duneb) @install && $(duneb) @ptests
+
+check-examples-acsl_extension_ext_types: check-examples-clean
+ cd examples/acsl_extension_ext_types && $(duneb) @install && $(duneb) @ptests
+
+check-examples-callstack: check-examples-clean
+ # no test oracles; just check that the code compiles
+ cd examples/callstack && $(duneb) @install
+
+check-examples-syntactic_check: check-examples-clean
+ cd examples/syntactic_check && $(duneb) @install && $(duneb) @ptests 2>&1
+
check-all: developer.pdf
$(MAKE) -C ../.. check-devguide
diff --git a/doc/developer/advance.tex b/doc/developer/advance.tex
index 6647eca22ae390d903e3ed76bb1019beb8aa6ac2..d1d30f0ce9484330eaaaa8ed320428330c9dcd6e 100644
--- a/doc/developer/advance.tex
+++ b/doc/developer/advance.tex
@@ -2293,7 +2293,7 @@ plug-in which provides a dynamic API for callstacks as follows.
\scodeidx{Cil\_datatype}{Stmt}
\scodeidx{Cil}{dummyStmt}
\scodeidx{Datatype}{Serializable\_undefined}
-\ocamlinput{./examples/generated/callstack.ml}
+\ocamlinput{./examples/callstack/callstack.ml}
You have to use the functor \texttt{Type.Abstract} to access to the type value
corresponding to the type of callstacks (and thus to access to the above
@@ -2307,7 +2307,7 @@ dynamically registered functions).
\scodeidx{Datatype}{func}
\scodeidx{Datatype}{func3}
\scodeidx{Datatype}{unit}
-\ocamlinput{./examples/generated/use_callstack.ml}
+\ocamlinput{./examples/callstack/use_callstack.ml}
\end{example}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
@@ -3901,7 +3901,7 @@ division in the program, stating that the divisor is not zero:
\scodeidx{Ast}{self}
\sscodeidx{Cil}{cilVisitor}{current\_kinstr}
\sscodeidx{Visitor}{frama\_c\_visitor}{current\_kf}
-\ocamlinput{./examples/generated/syntactic_check.ml}
+\ocamlinput{./examples/syntactic_check/syntactic_check.ml}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
@@ -4067,7 +4067,7 @@ recognize only subtrees of an otherwise normal ACSL predicate or term. For
instance, the following code will let extension \verb|foo| replace all
occurrences of \verb|\foo| by \verb|42|.
-\ocamlinput{./examples/acsl_extension_foo.ml}
+\ocamlinput{./examples/acsl_extension_foo/acsl_extension_foo.ml}
With this extension enabled, \framac will interpret the following clause in
a given source file:
@@ -4146,7 +4146,7 @@ The following code shows a more complete extension example. It provides the
user a way to load some types (assumed to be external to Frama-C) so that they
can be used in ACSL specification.
-\ocamlinput{./examples/acsl_extension_ext_types.ml}
+\ocamlinput{./examples/acsl_extension_ext_types/acsl_extension_ext_types.ml}
Namely, specification:
@@ -4163,7 +4163,7 @@ Namely, specification:
is correctly parsed and typed by Frama-C and leads to the following displayed
version in the interface:
-\includegraphics[width=\textwidth]{examples/acsl_extension_ext_types}
+\includegraphics[width=\textwidth]{examples/acsl_extension_ext_types/acsl_extension_ext_types}
diff --git a/doc/developer/examples/acsl_extension_ext_types/Example.ml b/doc/developer/examples/acsl_extension_ext_types/Example.ml
new file mode 100644
index 0000000000000000000000000000000000000000..5dfbd652e6173d203594b0612b6ff5bc82ca036b
--- /dev/null
+++ b/doc/developer/examples/acsl_extension_ext_types/Example.ml
@@ -0,0 +1,3 @@
+(** Self-contained example for Plugin Developer Guide.
+
+ Nothing is exported. *)
diff --git a/doc/developer/examples/acsl_extension_ext_types.ml b/doc/developer/examples/acsl_extension_ext_types/acsl_extension_ext_types.ml
similarity index 87%
rename from doc/developer/examples/acsl_extension_ext_types.ml
rename to doc/developer/examples/acsl_extension_ext_types/acsl_extension_ext_types.ml
index bd8efcd6e7672dbd4835a5baad3ecef8759e85d7..3bf92db73e4d6ddfff76b7662da4c9ada6cf1df6 100644
--- a/doc/developer/examples/acsl_extension_ext_types.ml
+++ b/doc/developer/examples/acsl_extension_ext_types/acsl_extension_ext_types.ml
@@ -4,7 +4,7 @@ open Cil_types
let preprocessor =
List.map (fun e -> begin match e with
- | { lexpr_node = PLnamed ("load", { lexpr_node = PLvar s}) } ->
+ | { lexpr_node = PLnamed ("load", { lexpr_node = PLvar s; _ }) ; _ } ->
if not (Logic_env.is_logic_type s) then Logic_env.add_typename s
else Kernel.error "Type already exists %s" s
| _ -> ()
@@ -19,7 +19,7 @@ module Ts = struct
end
let typer ctxt loc = function
- | [ { lexpr_node = PLnamed ("load", { lexpr_node = PLvar s}) } ] ->
+ | [ { lexpr_node = PLnamed ("load", { lexpr_node = PLvar s; _ }) ; _ } ] ->
let ti = { lt_name = s ; lt_params = [] ; lt_def = None ; lt_attr = []} in
ctxt.add_logic_type s ti ;
Ext_id (Ts.add ti)
diff --git a/doc/developer/examples/acsl_extension_ext_types.png b/doc/developer/examples/acsl_extension_ext_types/acsl_extension_ext_types.png
similarity index 100%
rename from doc/developer/examples/acsl_extension_ext_types.png
rename to doc/developer/examples/acsl_extension_ext_types/acsl_extension_ext_types.png
diff --git a/doc/developer/examples/acsl_extension_ext_types/dune b/doc/developer/examples/acsl_extension_ext_types/dune
new file mode 100644
index 0000000000000000000000000000000000000000..52d08afb2c980670ddd0fe5c3056c1bd847985a1
--- /dev/null
+++ b/doc/developer/examples/acsl_extension_ext_types/dune
@@ -0,0 +1,12 @@
+(library
+ (name Example)
+ (public_name frama-c-example.core)
+ (flags -open Frama_c_kernel :standard)
+ (libraries frama-c.kernel)
+)
+
+(plugin
+ (optional)
+ (name example)
+ (libraries frama-c-example.core)
+ (site (frama-c plugins)))
diff --git a/doc/developer/examples/acsl_extension_ext_types/dune-project b/doc/developer/examples/acsl_extension_ext_types/dune-project
new file mode 100644
index 0000000000000000000000000000000000000000..ee82a6cf3583c620586b5c40e672a4d730ee48aa
--- /dev/null
+++ b/doc/developer/examples/acsl_extension_ext_types/dune-project
@@ -0,0 +1,5 @@
+(lang dune 3.0)
+(using dune_site 0.1)
+
+(name frama-c-example)
+(package (name frama-c-example))
diff --git a/doc/developer/examples/acsl_extension_ext_types/tests/example/ext_type_foo.c b/doc/developer/examples/acsl_extension_ext_types/tests/example/ext_type_foo.c
new file mode 100644
index 0000000000000000000000000000000000000000..f68b0544f40a3d6cf5b7b7297916fca2fea53cff
--- /dev/null
+++ b/doc/developer/examples/acsl_extension_ext_types/tests/example/ext_type_foo.c
@@ -0,0 +1,10 @@
+/* run.config
+ OPT: -check -print
+ */
+/*@ ext_type load: foo ; */
+/*@
+ axiomatic Pred {
+ predicate P(foo f) reads \nothing ;
+ }
+*/
+/*@ lemma X: \forall foo f ; P(f) ; */
diff --git a/doc/developer/examples/acsl_extension_ext_types/tests/example/oracle/ext_type_foo.res.oracle b/doc/developer/examples/acsl_extension_ext_types/tests/example/oracle/ext_type_foo.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e748bf40f3cb6b59c8773f8a87f27a2d84cbdbd2
--- /dev/null
+++ b/doc/developer/examples/acsl_extension_ext_types/tests/example/oracle/ext_type_foo.res.oracle
@@ -0,0 +1,12 @@
+[kernel] Parsing ext_type_foo.c (with preprocessing)
+/* Generated by Frama-C */
+/*@ ext_type load: foo; */
+/*@ axiomatic Pred {
+ predicate P(foo f)
+ reads \nothing;
+
+ }
+ */
+/*@ lemma X: ∀ foo f; P(f);
+ */
+
diff --git a/doc/developer/examples/acsl_extension_ext_types/tests/ptests_config b/doc/developer/examples/acsl_extension_ext_types/tests/ptests_config
new file mode 100644
index 0000000000000000000000000000000000000000..bd7f109d72b0645ed197a88e5e50e70c07138c5d
--- /dev/null
+++ b/doc/developer/examples/acsl_extension_ext_types/tests/ptests_config
@@ -0,0 +1 @@
+DEFAULT_SUITES= example
diff --git a/doc/developer/examples/acsl_extension_ext_types/tests/test_config b/doc/developer/examples/acsl_extension_ext_types/tests/test_config
new file mode 100644
index 0000000000000000000000000000000000000000..b10e94352e9f3006d726c7ad2004041f8714202b
--- /dev/null
+++ b/doc/developer/examples/acsl_extension_ext_types/tests/test_config
@@ -0,0 +1 @@
+PLUGIN: example
diff --git a/doc/developer/examples/acsl_extension_foo/Example.ml b/doc/developer/examples/acsl_extension_foo/Example.ml
new file mode 100644
index 0000000000000000000000000000000000000000..5dfbd652e6173d203594b0612b6ff5bc82ca036b
--- /dev/null
+++ b/doc/developer/examples/acsl_extension_foo/Example.ml
@@ -0,0 +1,3 @@
+(** Self-contained example for Plugin Developer Guide.
+
+ Nothing is exported. *)
diff --git a/doc/developer/examples/acsl_extension_foo.ml b/doc/developer/examples/acsl_extension_foo/acsl_extension_foo.ml
similarity index 100%
rename from doc/developer/examples/acsl_extension_foo.ml
rename to doc/developer/examples/acsl_extension_foo/acsl_extension_foo.ml
diff --git a/doc/developer/examples/acsl_extension_foo/dune b/doc/developer/examples/acsl_extension_foo/dune
new file mode 100644
index 0000000000000000000000000000000000000000..52d08afb2c980670ddd0fe5c3056c1bd847985a1
--- /dev/null
+++ b/doc/developer/examples/acsl_extension_foo/dune
@@ -0,0 +1,12 @@
+(library
+ (name Example)
+ (public_name frama-c-example.core)
+ (flags -open Frama_c_kernel :standard)
+ (libraries frama-c.kernel)
+)
+
+(plugin
+ (optional)
+ (name example)
+ (libraries frama-c-example.core)
+ (site (frama-c plugins)))
diff --git a/doc/developer/examples/acsl_extension_foo/dune-project b/doc/developer/examples/acsl_extension_foo/dune-project
new file mode 100644
index 0000000000000000000000000000000000000000..ee82a6cf3583c620586b5c40e672a4d730ee48aa
--- /dev/null
+++ b/doc/developer/examples/acsl_extension_foo/dune-project
@@ -0,0 +1,5 @@
+(lang dune 3.0)
+(using dune_site 0.1)
+
+(name frama-c-example)
+(package (name frama-c-example))
diff --git a/doc/developer/examples/acsl_extension_foo/tests/example/foo.c b/doc/developer/examples/acsl_extension_foo/tests/example/foo.c
new file mode 100644
index 0000000000000000000000000000000000000000..33dd17810dafa57bc4c6d78db49a7b8c2299c73d
--- /dev/null
+++ b/doc/developer/examples/acsl_extension_foo/tests/example/foo.c
@@ -0,0 +1,7 @@
+/* run.config
+ OPT: -check -print
+ */
+int main() {
+ /*@ foo 84 == \foo + \foo; */
+ return 0;
+}
diff --git a/doc/developer/examples/acsl_extension_foo/tests/example/oracle/foo.res.oracle b/doc/developer/examples/acsl_extension_foo/tests/example/oracle/foo.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..5b1a105e7ddce8442960fd8a9ca4636032eb6f80
--- /dev/null
+++ b/doc/developer/examples/acsl_extension_foo/tests/example/oracle/foo.res.oracle
@@ -0,0 +1,14 @@
+[kernel] Parsing foo.c (with preprocessing)
+/* Generated by Frama-C */
+int main(void)
+{
+ int __retres;
+ /*@ foo 84 ≡ 42 + 42; */
+ {
+ __retres = 0;
+ goto return_label;
+ }
+ return_label: return __retres;
+}
+
+
diff --git a/doc/developer/examples/acsl_extension_foo/tests/ptests_config b/doc/developer/examples/acsl_extension_foo/tests/ptests_config
new file mode 100644
index 0000000000000000000000000000000000000000..bd7f109d72b0645ed197a88e5e50e70c07138c5d
--- /dev/null
+++ b/doc/developer/examples/acsl_extension_foo/tests/ptests_config
@@ -0,0 +1 @@
+DEFAULT_SUITES= example
diff --git a/doc/developer/examples/acsl_extension_foo/tests/test_config b/doc/developer/examples/acsl_extension_foo/tests/test_config
new file mode 100644
index 0000000000000000000000000000000000000000..b10e94352e9f3006d726c7ad2004041f8714202b
--- /dev/null
+++ b/doc/developer/examples/acsl_extension_foo/tests/test_config
@@ -0,0 +1 @@
+PLUGIN: example
diff --git a/doc/developer/examples/callstack.ml b/doc/developer/examples/callstack.ml
deleted file mode 100644
index 74e25f7fee63af89a140bec3e63b7916f2a7cca1..0000000000000000000000000000000000000000
--- a/doc/developer/examples/callstack.ml
+++ /dev/null
@@ -1,68 +0,0 @@
-(**************************************************************************)
-(* *)
-(* This file is part of Frama-C. *)
-(* *)
-(* Copyright (C) 2007-2022 *)
-(* CEA (Commissariat à l'énergie atomique et aux énergies *)
-(* alternatives) *)
-(* *)
-(* you can redistribute it and/or modify it under the terms of the GNU *)
-(* Lesser General Public License as published by the Free Software *)
-(* Foundation, version 2.1. *)
-(* *)
-(* It is distributed in the hope that it will be useful, *)
-(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
-(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
-(* GNU Lesser General Public License for more details. *)
-(* *)
-(* See the GNU Lesser General Public License version 2.1 *)
-(* for more details (enclosed in the file licenses/LGPLv2.1). *)
-(* *)
-(**************************************************************************)
-
-module P =
- Plugin.Register
- (struct
- let name = "Callstack"
- let shortname = "Callstack"
- let help = "callstack library"
- end)
-
-(* A callstack is a list of a pair (kf * stmt) where [kf] is the kernel
- function called at statement [stmt]. Building the datatype also creates the
- corresponding type value [ty]. *)
-type callstack = (Kernel_function.t * Cil_datatype.Stmt.t) list
-
-(* Implementation *)
-let empty = []
-let push kf stmt stack = (kf, stmt) :: stack
-let pop = function [] -> [] | _ :: stack -> stack
-let rec print = function
- | [] -> P.feedback ""
- | (kf, stmt) :: stack ->
- P.feedback "function %a called at stmt %a"
- Kernel_function.pretty kf
- Cil_datatype.Stmt.pretty stmt;
- print stack
-
-(* Type values *)
-let kf_ty = Kernel_function.ty
-let stmt_ty = Cil_datatype.Stmt.ty
-
-module D =
- Datatype.Make
- (struct
- type t = callstack
- let name = "Callstack.t"
- let reprs = [ empty; [ Kernel_function.dummy (), Cil.dummyStmt ] ]
- include Datatype.Serializable_undefined
- end)
-
-(* Dynamic API registration *)
-let register name ty =
- Dynamic.register ~plugin:"Callstack" name ty
-
-let empty = register "empty" D.ty empty
-let push = register "push" (Datatype.func3 kf_ty stmt_ty D.ty D.ty) push
-let pop = register "pop" (Datatype.func D.ty D.ty) pop
-let print = register "print" (Datatype.func D.ty Datatype.unit) print
diff --git a/doc/developer/examples/callstack/Example.ml b/doc/developer/examples/callstack/Example.ml
new file mode 100644
index 0000000000000000000000000000000000000000..5dfbd652e6173d203594b0612b6ff5bc82ca036b
--- /dev/null
+++ b/doc/developer/examples/callstack/Example.ml
@@ -0,0 +1,3 @@
+(** Self-contained example for Plugin Developer Guide.
+
+ Nothing is exported. *)
diff --git a/doc/developer/examples/callstack/callstack.ml b/doc/developer/examples/callstack/callstack.ml
new file mode 100644
index 0000000000000000000000000000000000000000..4ef550b94769a896f446ff8fe7d3edd3afa121b5
--- /dev/null
+++ b/doc/developer/examples/callstack/callstack.ml
@@ -0,0 +1,46 @@
+module P =
+ Plugin.Register
+ (struct
+ let name = "Callstack"
+ let shortname = "Callstack"
+ let help = "callstack library"
+ end)
+
+(* A callstack is a list of a pair (kf * stmt) where [kf] is the kernel
+ function called at statement [stmt]. Building the datatype also creates the
+ corresponding type value [ty]. *)
+type callstack = (Kernel_function.t * Cil_datatype.Stmt.t) list
+
+(* Implementation *)
+let empty = []
+let push kf stmt stack = (kf, stmt) :: stack
+let pop = function [] -> [] | _ :: stack -> stack
+let rec print = function
+ | [] -> P.feedback ""
+ | (kf, stmt) :: stack ->
+ P.feedback "function %a called at stmt %a"
+ Kernel_function.pretty kf
+ Cil_datatype.Stmt.pretty stmt;
+ print stack
+
+(* Type values *)
+let kf_ty = Kernel_function.ty
+let stmt_ty = Cil_datatype.Stmt.ty
+
+module D =
+ Datatype.Make
+ (struct
+ type t = callstack
+ let name = "Callstack.t"
+ let reprs = [ empty; [ Kernel_function.dummy (), Cil.dummyStmt ] ]
+ include Datatype.Serializable_undefined
+ end)
+
+(* Dynamic API registration *)
+let register name ty =
+ Dynamic.register ~plugin:"Callstack" name ty
+
+let empty = register "empty" D.ty empty
+let push = register "push" (Datatype.func3 kf_ty stmt_ty D.ty D.ty) push
+let pop = register "pop" (Datatype.func D.ty D.ty) pop
+let print = register "print" (Datatype.func D.ty Datatype.unit) print
diff --git a/doc/developer/examples/callstack/dune b/doc/developer/examples/callstack/dune
new file mode 100644
index 0000000000000000000000000000000000000000..52d08afb2c980670ddd0fe5c3056c1bd847985a1
--- /dev/null
+++ b/doc/developer/examples/callstack/dune
@@ -0,0 +1,12 @@
+(library
+ (name Example)
+ (public_name frama-c-example.core)
+ (flags -open Frama_c_kernel :standard)
+ (libraries frama-c.kernel)
+)
+
+(plugin
+ (optional)
+ (name example)
+ (libraries frama-c-example.core)
+ (site (frama-c plugins)))
diff --git a/doc/developer/examples/callstack/dune-project b/doc/developer/examples/callstack/dune-project
new file mode 100644
index 0000000000000000000000000000000000000000..ee82a6cf3583c620586b5c40e672a4d730ee48aa
--- /dev/null
+++ b/doc/developer/examples/callstack/dune-project
@@ -0,0 +1,5 @@
+(lang dune 3.0)
+(using dune_site 0.1)
+
+(name frama-c-example)
+(package (name frama-c-example))
diff --git a/doc/developer/examples/callstack/use_callstack.ml b/doc/developer/examples/callstack/use_callstack.ml
new file mode 100644
index 0000000000000000000000000000000000000000..2af8893af690d83eb8abd9d3e92be8607d0fb744
--- /dev/null
+++ b/doc/developer/examples/callstack/use_callstack.ml
@@ -0,0 +1,30 @@
+(* Type values *)
+let kf_ty = Kernel_function.ty
+let stmt_ty = Cil_datatype.Stmt.ty
+
+(* Access to the type value for abstract callstacks *)
+module C = Type.Abstract(struct let name = "Callstack.t" end)
+
+let get name ty = Dynamic.get ~plugin:"Callstack" name ty
+
+(* mutable callstack *)
+let callstack_ref = ref (get "empty" C.ty)
+
+(* operations over this mutable callstack *)
+
+let push_callstack =
+ (* getting the function outside the closure is more efficient *)
+ let push = get "push" (Datatype.func3 kf_ty stmt_ty C.ty C.ty) in
+ fun kf stmt -> callstack_ref := push kf stmt !callstack_ref
+
+let pop_callstack =
+ (* getting the function outside the closure is more efficient *)
+ let pop = get "pop" (Datatype.func C.ty C.ty) in
+ fun () -> callstack_ref := pop !callstack_ref
+
+let print_callstack =
+ (* getting the function outside the closure is more efficient *)
+ let print = get "print" (Datatype.func C.ty Datatype.unit) in
+ fun () -> print !callstack_ref
+
+(* ... algorithm using the callstack ... *)
diff --git a/doc/developer/examples/syntactic_check/Example.ml b/doc/developer/examples/syntactic_check/Example.ml
new file mode 100644
index 0000000000000000000000000000000000000000..5dfbd652e6173d203594b0612b6ff5bc82ca036b
--- /dev/null
+++ b/doc/developer/examples/syntactic_check/Example.ml
@@ -0,0 +1,3 @@
+(** Self-contained example for Plugin Developer Guide.
+
+ Nothing is exported. *)
diff --git a/doc/developer/examples/syntactic_check/dune b/doc/developer/examples/syntactic_check/dune
new file mode 100644
index 0000000000000000000000000000000000000000..52d08afb2c980670ddd0fe5c3056c1bd847985a1
--- /dev/null
+++ b/doc/developer/examples/syntactic_check/dune
@@ -0,0 +1,12 @@
+(library
+ (name Example)
+ (public_name frama-c-example.core)
+ (flags -open Frama_c_kernel :standard)
+ (libraries frama-c.kernel)
+)
+
+(plugin
+ (optional)
+ (name example)
+ (libraries frama-c-example.core)
+ (site (frama-c plugins)))
diff --git a/doc/developer/examples/syntactic_check/dune-project b/doc/developer/examples/syntactic_check/dune-project
new file mode 100644
index 0000000000000000000000000000000000000000..ee82a6cf3583c620586b5c40e672a4d730ee48aa
--- /dev/null
+++ b/doc/developer/examples/syntactic_check/dune-project
@@ -0,0 +1,5 @@
+(lang dune 3.0)
+(using dune_site 0.1)
+
+(name frama-c-example)
+(package (name frama-c-example))
diff --git a/doc/developer/examples/syntactic_check.ml b/doc/developer/examples/syntactic_check/syntactic_check.ml
similarity index 66%
rename from doc/developer/examples/syntactic_check.ml
rename to doc/developer/examples/syntactic_check/syntactic_check.ml
index 28090a74480b78bb0abe64ca78323cd82a541177..9b2d02ce56dab7c43f114a00b7b3780898f9aa4d 100644
--- a/doc/developer/examples/syntactic_check.ml
+++ b/doc/developer/examples/syntactic_check/syntactic_check.ml
@@ -1,25 +1,3 @@
-(**************************************************************************)
-(* *)
-(* This file is part of Frama-C. *)
-(* *)
-(* Copyright (C) 2007-2022 *)
-(* CEA (Commissariat à l'énergie atomique et aux énergies *)
-(* alternatives) *)
-(* *)
-(* you can redistribute it and/or modify it under the terms of the GNU *)
-(* Lesser General Public License as published by the Free Software *)
-(* Foundation, version 2.1. *)
-(* *)
-(* It is distributed in the hope that it will be useful, *)
-(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
-(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
-(* GNU Lesser General Public License for more details. *)
-(* *)
-(* See the GNU Lesser General Public License version 2.1 *)
-(* for more details (enclosed in the file licenses/LGPLv2.1). *)
-(* *)
-(**************************************************************************)
-
open Cil_types
open Cil
diff --git a/doc/developer/examples/syntactic_check/tests/example/div.c b/doc/developer/examples/syntactic_check/tests/example/div.c
new file mode 100644
index 0000000000000000000000000000000000000000..b6a48956ace2ae33e1906504a453417cdf43b263
--- /dev/null
+++ b/doc/developer/examples/syntactic_check/tests/example/div.c
@@ -0,0 +1,11 @@
+/* run.config
+ OPT: -check -then-last -print
+*/
+
+int main() {
+ int a, b, c;
+ a = 1;
+ b = 2;
+ c = a/b;
+ return c;
+}
diff --git a/doc/developer/examples/syntactic_check/tests/example/oracle/div.res.oracle b/doc/developer/examples/syntactic_check/tests/example/oracle/div.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..db8bc412f377ff014b2d64f1abf10e024a2c343c
--- /dev/null
+++ b/doc/developer/examples/syntactic_check/tests/example/oracle/div.res.oracle
@@ -0,0 +1,15 @@
+[kernel] Parsing div.c (with preprocessing)
+/* Generated by Frama-C */
+int main(void)
+{
+ int a;
+ int b;
+ int c;
+ a = 1;
+ b = 2;
+ /*@ assert b ≢ 0; */
+ c = a / b;
+ return c;
+}
+
+
diff --git a/doc/developer/examples/syntactic_check/tests/ptests_config b/doc/developer/examples/syntactic_check/tests/ptests_config
new file mode 100644
index 0000000000000000000000000000000000000000..bd7f109d72b0645ed197a88e5e50e70c07138c5d
--- /dev/null
+++ b/doc/developer/examples/syntactic_check/tests/ptests_config
@@ -0,0 +1 @@
+DEFAULT_SUITES= example
diff --git a/doc/developer/examples/syntactic_check/tests/test_config b/doc/developer/examples/syntactic_check/tests/test_config
new file mode 100644
index 0000000000000000000000000000000000000000..b10e94352e9f3006d726c7ad2004041f8714202b
--- /dev/null
+++ b/doc/developer/examples/syntactic_check/tests/test_config
@@ -0,0 +1 @@
+PLUGIN: example
diff --git a/doc/developer/examples/use_callstack.ml b/doc/developer/examples/use_callstack.ml
deleted file mode 100644
index c6e179f0da8c1ac6d6f9e84d0d33b0f021b543f6..0000000000000000000000000000000000000000
--- a/doc/developer/examples/use_callstack.ml
+++ /dev/null
@@ -1,52 +0,0 @@
-(**************************************************************************)
-(* *)
-(* This file is part of Frama-C. *)
-(* *)
-(* Copyright (C) 2007-2022 *)
-(* CEA (Commissariat à l'énergie atomique et aux énergies *)
-(* alternatives) *)
-(* *)
-(* you can redistribute it and/or modify it under the terms of the GNU *)
-(* Lesser General Public License as published by the Free Software *)
-(* Foundation, version 2.1. *)
-(* *)
-(* It is distributed in the hope that it will be useful, *)
-(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
-(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
-(* GNU Lesser General Public License for more details. *)
-(* *)
-(* See the GNU Lesser General Public License version 2.1 *)
-(* for more details (enclosed in the file licenses/LGPLv2.1). *)
-(* *)
-(**************************************************************************)
-
-(* Type values *)
-let kf_ty = Kernel_function.ty
-let stmt_ty = Cil_datatype.Stmt.ty
-
-(* Access to the type value for abstract callstacks *)
-module C = Type.Abstract(struct let name = "Callstack.t" end)
-
-let get name ty = Dynamic.get ~plugin:"Callstack" name ty
-
-(* mutable callstack *)
-let callstack_ref = ref (get "empty" C.ty)
-
-(* operations over this mutable callstack *)
-
-let push_callstack =
- (* getting the function outside the closure is more efficient *)
- let push = get "push" (Datatype.func3 kf_ty stmt_ty C.ty C.ty) in
- fun kf stmt -> callstack_ref := push kf stmt !callstack_ref
-
-let pop_callstack =
- (* getting the function outside the closure is more efficient *)
- let pop = get "pop" (Datatype.func C.ty C.ty) in
- fun () -> callstack_ref := pop !callstack_ref
-
-let print_callstack =
- (* getting the function outside the closure is more efficient *)
- let print = get "print" (Datatype.func C.ty Datatype.unit) in
- fun () -> print !callstack_ref
-
-(* ... algorithm using the callstack ... *)