From a83d4c3129acc78b6397a0b64d380338ddee8c2b Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.maroneze@cea.fr>
Date: Mon, 1 Aug 2022 23:03:10 +0200
Subject: [PATCH] [Doc] update hello plugin tests
---
doc/developer/.gitignore | 4 +-
doc/developer/Makefile | 75 +++++++++++++++++++++-------
doc/developer/checks/README.md | 6 +++
doc/developer/checks/hello/v1.oracle | 1 +
doc/developer/checks/hello/v2.oracle | 1 +
doc/developer/checks/hello/v3.oracle | 2 +
doc/developer/checks/hello/v4.oracle | 1 +
doc/developer/checks/hello/v5.oracle | 1 +
doc/developer/checks/hello/v6.oracle | 12 +++++
doc/developer/checks/hello/v7.oracle | 1 +
doc/developer/tutorial.tex | 27 +++++++---
11 files changed, 105 insertions(+), 26 deletions(-)
create mode 100644 doc/developer/checks/README.md
create mode 100644 doc/developer/checks/hello/v1.oracle
create mode 100644 doc/developer/checks/hello/v2.oracle
create mode 100644 doc/developer/checks/hello/v3.oracle
create mode 100644 doc/developer/checks/hello/v4.oracle
create mode 100644 doc/developer/checks/hello/v5.oracle
create mode 100644 doc/developer/checks/hello/v6.oracle
create mode 100644 doc/developer/checks/hello/v7.oracle
diff --git a/doc/developer/.gitignore b/doc/developer/.gitignore
index 092d8112a26..b8344f6c7c6 100644
--- a/doc/developer/.gitignore
+++ b/doc/developer/.gitignore
@@ -8,7 +8,6 @@
/frama-c-affiliation.tex
/hello_world/
/tutorial/viewcfg/generated/
-/tutorial/hello/generated/
/examples/generated/
*.idx
*.out
@@ -17,3 +16,6 @@ developer.idxs
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/
diff --git a/doc/developer/Makefile b/doc/developer/Makefile
index 921c8589c6c..d74f5d54efd 100644
--- a/doc/developer/Makefile
+++ b/doc/developer/Makefile
@@ -32,14 +32,13 @@ SRC = developer \
SRC := $(addsuffix .tex, $(SRC))
SRC += macros.sty
-GENERATED= tutorial/viewcfg/generated \
- tutorial/hello/generated \
+GENERATED= \
examples/generated/callstack.ml \
examples/generated/use_callstack.ml \
examples/generated/syntactic_check.ml
DEPENDENCIES= $(FRAMAC_MODERN) $(GENERATED) frama-c-book.cls
-.PHONY: all check
+.PHONY: all check check-hello
all: developer.pdf # check << restore check later
@@ -47,14 +46,8 @@ all: developer.pdf # check << restore check later
# FC_BINDIR:=$(FRAMAC_ROOT_SRCDIR)/bin
# Thus TODO: use `dune exec -- frama-c` for the following commands
-.PHONY: clean-tuto
-clean-tuto:
- $(RM) ../../lib/plugins/META.frama-c-hello ../../lib/plugins/META.frama-c-viewcfg
- $(RM) ../../lib/plugins/top/Hello.* ../../lib/plugins/top/Viewcfg.*
-
# local plugin.cmi (if any) is in conflict with the one of Frama-C
-check: $(GENERATED)
- $(MAKE) clean-tuto
+check: $(GENERATED) check-hello
$(ECHO) Checking compilation of example scripts
$(FC_BINDIR)/frama-c \
-load-script ./examples/syntactic_check \
@@ -86,6 +79,46 @@ check: $(GENERATED)
PATH=$(FC_BINDIR):$$PATH; $(MAKE) DEVELOPMENT=no PTESTS_OPTS=-error-code -C tutorial/viewcfg/generated/split opt
$(MAKE) clean-tuto
+check-hello: check-hello-v1 check-hello-v2 check-hello-v3 check-hello-v4 check-hello-v5 check-hello-v6 check-hello-v7
+
+duneb := dune build --root .
+dunee := dune exec --root .
+
+check-hello-clean:
+ $(ECHO) Cleaning Hello tutorial files...
+ rm -rf tutorial/hello/v*/_build
+ rm -rf tutorial/hello/v*/hello.out
+
+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
+
+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
+
+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
+
+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
+
+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
+
+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
+
+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
+
check-all: developer.pdf
$(MAKE) -C ../.. check-devguide
@@ -98,9 +131,6 @@ install:
rm -f ../manuals/plugin-development-guide.pdf
cp developer.pdf ../manuals/plugin-development-guide.pdf
-tutorial/hello/generated:
- cd tutorial/hello && make
-
tutorial/viewcfg/generated:
cd tutorial/viewcfg && make
@@ -109,11 +139,20 @@ examples/generated/%.ml: examples/%.ml
cp $^ $@
headache -r $@
-archives: tutorial/hello/generated
- cd tutorial/hello/generated/; \
- mv with_doc/ hello-$(VERSION)/; \
- tar -zcvf ../../../hello-$(VERSION).tar.gz hello-$(VERSION)/*; \
- mv hello-$(VERSION)/ with_doc/
+archives: FILES=$(shell cd tutorial/hello/v7-doc && git ls-files)
+
+# - use 'git ls-files' to avoid including extraneous files in archive
+# - use several tar options to improve build reproducibility
+archives:
+ export VERSION="$(shell cat ../../VERSION)" && \
+ cd tutorial/hello && \
+ rm -rf hello-$$VERSION && \
+ cp -r v7-doc hello-$$VERSION && \
+ tar -cf - $(addprefix hello-$$VERSION/,$(FILES)) \
+ --numeric-owner --owner=0 --group=0 --sort=name \
+ --mtime="$$(date +"%F") Z" --mode='a+rw' | \
+ gzip -9 -n > ../../hello-$$VERSION.tar.gz && \
+ rm -rf hello-$$VERSION
.PHONY: tutorial/hello/generated tutorial/viewcfg/generated
diff --git a/doc/developer/checks/README.md b/doc/developer/checks/README.md
new file mode 100644
index 00000000000..fcf8eafc8e2
--- /dev/null
+++ b/doc/developer/checks/README.md
@@ -0,0 +1,6 @@
+# Test oracles for `make check` target of doc/developer
+
+This directory contains test oracles used by the `make check` target of the
+Plugin Developer guide Makefile.
+
+If any oracle needs to be changed, you have to manually update it.
diff --git a/doc/developer/checks/hello/v1.oracle b/doc/developer/checks/hello/v1.oracle
new file mode 100644
index 00000000000..af5626b4a11
--- /dev/null
+++ b/doc/developer/checks/hello/v1.oracle
@@ -0,0 +1 @@
+Hello, world!
diff --git a/doc/developer/checks/hello/v2.oracle b/doc/developer/checks/hello/v2.oracle
new file mode 100644
index 00000000000..821fa02b218
--- /dev/null
+++ b/doc/developer/checks/hello/v2.oracle
@@ -0,0 +1 @@
+Hello world output a warm welcome message to the user (-hello-h)
diff --git a/doc/developer/checks/hello/v3.oracle b/doc/developer/checks/hello/v3.oracle
new file mode 100644
index 00000000000..93cf0f55f6f
--- /dev/null
+++ b/doc/developer/checks/hello/v3.oracle
@@ -0,0 +1,2 @@
+[hello] Hello, world!
+[hello] 11 * 5 = 55
diff --git a/doc/developer/checks/hello/v4.oracle b/doc/developer/checks/hello/v4.oracle
new file mode 100644
index 00000000000..b0b28ee8b23
--- /dev/null
+++ b/doc/developer/checks/hello/v4.oracle
@@ -0,0 +1 @@
+[hello] Hello, world!
diff --git a/doc/developer/checks/hello/v5.oracle b/doc/developer/checks/hello/v5.oracle
new file mode 100644
index 00000000000..b0b28ee8b23
--- /dev/null
+++ b/doc/developer/checks/hello/v5.oracle
@@ -0,0 +1 @@
+[hello] Hello, world!
diff --git a/doc/developer/checks/hello/v6.oracle b/doc/developer/checks/hello/v6.oracle
new file mode 100644
index 00000000000..9c684ce00c7
--- /dev/null
+++ b/doc/developer/checks/hello/v6.oracle
@@ -0,0 +1,12 @@
+Files ../oracle/hello_test.res.oracle and hello_test.res.log differ
+% dune build @"tests/hello/result/hello_test.0.exec.wtests": diff failure on diff:
+ (cd _build/default/tests/hello/result && diff --new-file "hello_test.res.log" "../oracle/hello_test.res.oracle")
+File "tests/hello/oracle/hello_test.res.oracle", line 1, characters 0-0:
+diff --git a/_build/default/tests/hello/oracle/hello_test.res.oracle b/_build/default/tests/hello/result/hello_test.res.log
+index 5f6ab2389a..cf2e5c010c 100644
+--- a/_build/default/tests/hello/oracle/hello_test.res.oracle
++++ b/_build/default/tests/hello/result/hello_test.res.log
+@@ -1,2 +1,2 @@
+ [kernel] Parsing hello_test.c (with preprocessing)
+-[hello] Hello, world!
++[hello] Hello world!
diff --git a/doc/developer/checks/hello/v7.oracle b/doc/developer/checks/hello/v7.oracle
new file mode 100644
index 00000000000..fec4af84ca3
--- /dev/null
+++ b/doc/developer/checks/hello/v7.oracle
@@ -0,0 +1 @@
+welcome message
diff --git a/doc/developer/tutorial.tex b/doc/developer/tutorial.tex
index 9a6ca045345..bbc2322f6b2 100644
--- a/doc/developer/tutorial.tex
+++ b/doc/developer/tutorial.tex
@@ -550,7 +550,7 @@ Once \texttt{run.config} has been configured, it becomes possible to generate
Dune test files via the \ptests tool:
\begin{shell}[breaklines=true]
-\$ frama-c-ptests tests
+\$ frama-c-ptests
Test directory: tests
Total number of generated dune files: 2
\end{shell}
@@ -558,10 +558,20 @@ Total number of generated dune files: 2
This must be done each time a test configuration is modified or a test file or
directory is added.
-Then, one can execute the tests and get the output generated by the plug-in:
+Then, one can execute the tests and get the output generated by the plug-in,
+by running \verb|dune build @ptests|. Note that if you forget the intermediate
+step of running \verb|frama-c-ptests|, you may end up with the following error:
\begin{shell}[breaklines=true]
-\$ dune build @tests/ptests
+Error: Alias "ptests" specified on the command line is empty.
+It is not defined in tests or any of its descendants.
+\end{shell}
+
+But with the \texttt{dune} files generated by \verb|frama-c-ptests|, you can
+run the tests:
+
+\begin{shell}[breaklines=true]
+\$ dune build @ptests
Files ../oracle/hello_test.res.oracle and hello_test.res.log differ
% dune build @"tests/hello/result/hello_test.0.exec.wtests": diff failure on diff:
(cd _build/default/tests/hello/result && diff --new-file "hello_test.res.log"
@@ -631,12 +641,15 @@ After promoting tests, it is useful to remove empty oracles:
\$ frama-c-ptests -remove-empty-oracles tests
\end{shell}
+The new oracle should be committed to source control, for future testing.
+
\begin{important}
Once your plug-in has test files, the \verb|dune build| command presented
earlier will not only compile your plug-in, but also run its tests.
Therefore, if you want to simply compile it, you will have to run
\verb|dune build @install| instead. Despite the name, the command will
- {\em not} install your plug-in (that is performed by \verb|dune install|).
+ {\em not} install your plug-in (that is performed by
+ \verb|dune install|).
\end{important}
Now, let's introduce an error. Assume the plug-in has been modified as follows:
@@ -651,7 +664,7 @@ Running these commands:
\begin{shell}[breaklines=true]
\$ dune build @install
<...>
-\$ dune build @tests/ptests
+\$ dune build @ptests
Files ../oracle/hello_test.res.oracle and hello_test.res.log are different
% dune build @"tests/hello/result/hello_test.0.exec.wtests": diff failure on diff:
(cd _build/default/tests/hello/result && diff --new-file "hello_test.res.log" "../oracle/hello_test.res.oracle")
@@ -693,7 +706,7 @@ Here's a summarized list of operations in order to add a new test:
\item Add a \texttt{run.config} header to the test.
\item \verb|frama-c-ptests|
\item \verb|frama-c-ptests -create-missing-oracles|
-\item \verb|dune build @tests/ptests|
+\item \verb|dune build @ptests|
\item Manually inspect oracle diffs to check that they are ok.
\item \verb|dune promote|
\item \verb|frama-c-ptests -remove-empty-oracles|
@@ -703,7 +716,7 @@ Operations to perform when modifying the plug-in code:
\begin{enumerate}
\item \verb|dune build @install|
-\item \verb|dune build @tests/ptests|
+\item \verb|dune build @ptests|
\item If there are expected diffs, run \verb|dune promote|;
otherwise, fix code and re-run the first steps.
\end{enumerate}
--
GitLab