diff --git a/Changelog b/Changelog
index 6a3abe5f41ef3d49357e25758fef1e2003155583..be1909122a14b0668ac9f196e247de2ea4d253fb 100644
--- a/Changelog
+++ b/Changelog
@@ -19,6 +19,8 @@ Open Source Release <next-release>
##################################
-! Kernel [2023-01-25] Add support for C11's _Generic. Modifies Cabs AST.
+- Logic [2023-01-16] Accept \ghost attribute in logic annotations (##2638)
+- Logic [2023-01-10] Fix issue in pretty-printing ranges (##2639)
###############################
Open Source Release 26.0 (Iron)
diff --git a/doc/pdg/Makefile b/doc/pdg/Makefile
index ae4b91825f7218745a76191d48d909771a198a4e..88886fbc89fc18241c5b6ba1c53c7a167c402985 100644
--- a/doc/pdg/Makefile
+++ b/doc/pdg/Makefile
@@ -30,7 +30,7 @@ include ../MakeLaTeXModern
DWNLDDIR=../manuals
DOCNAME=pdg-documentation-fr.pdf
-TEST_DIR=../../tests/pdg/
+TEST_DIR=../../tests/pdg
BIB_FILE = ../slicing/bib-slicing.bib
main.bbl : $(BIB_FILE)
@@ -56,13 +56,12 @@ GENERATED+=call-f.pdf call-g.pdf
fig2dev -L pdf $< $@
GENERATED+=call-f.dot call-g.dot
-call-%.dot : $(TEST_DIR)/call.%.dot
+call-%.dot : $(TEST_DIR)/oracle/call.%.dot
cp $< $@
call-%.dot :
@echo
- @echo "ERROR : $@ not found : you should run PDG tests to have it"
- @echo " Run : cd ../.. ; make pdg_tests ; cd - "
+ @echo "ERROR : $@ not found : this file cannot be generated from an oracle of the PDD test 'tests/pdg/call.c'"
@echo
exit 1
diff --git a/doc/pdg/main.tex b/doc/pdg/main.tex
index 4bedb8ab5526ec481c2cdff9db8afebfd5d0f031..c31cbb3dbb613c11cdac4d7492dc48c31d61dccd 100644
--- a/doc/pdg/main.tex
+++ b/doc/pdg/main.tex
@@ -19,7 +19,7 @@
\end{tabular}
\vfill
\begin{flushleft}
- \textcopyright 2007-2022 CEA LIST
+ \textcopyright 2007-2023 CEA LIST
\end{flushleft}
\end{titlepage}
diff --git a/share/Makefile.installation b/share/Makefile.installation
index 5796f19796bdefba7d1a0facb2623f3a7a65e791..8e10270d351afcd7068e7b87159fa69a827ab8d0 100644
--- a/share/Makefile.installation
+++ b/share/Makefile.installation
@@ -62,15 +62,18 @@ ifndef PREFIX
@echo " (recommendation: include FRAMAC/share/Makefile.common)"
@exit 1
else
+ifeq ($(patsubst ~%,,$(PREFIX)),)
+$(error "PREFIX cannot start with '~'; use $$HOME instead")
+endif
ifeq ($(PREFIX),$(OPAM_SWITCH_PREFIX))
@echo "Installing $(INSTALL_TARGET)to current Opam switch"
@printf " Copying and relocating files..."
- dune install ${MANDIR_OPT} 2> /dev/null
+ dune install --root . ${MANDIR_OPT} 2> /dev/null
@echo " (done)"
else
@echo "Installing $(INSTALL_TARGET)to ${PREFIX}"
@printf " Copying and relocating files..."
- dune install --prefix ${PREFIX} ${MANDIR_OPT} 2> /dev/null
+ dune install --root . --prefix ${PREFIX} ${MANDIR_OPT} 2> /dev/null
@echo " (done)"
@echo 'DO NOT FORGET TO EXPAND YOUR OCAMLPATH VARIABLE:'
@echo ' export OCAMLPATH="${PREFIX}/lib:$$OCAMLPATH"'
@@ -80,5 +83,5 @@ endif
ifdef PREFIX
uninstall::
@echo "Uninstalling $(INSTALL_TARGET)"
- dune uninstall --prefix ${PREFIX} ${MANDIR_OPT} 2> /dev/null
+ dune uninstall --root . --prefix ${PREFIX} ${MANDIR_OPT} 2> /dev/null
endif
diff --git a/src/init/dune b/src/init/dune
index 08a3450ef5df30197a45739f3b558cf0fa44b01e..034e06a38dc904efff9f4b5981ea9a1a4003e74a 100644
--- a/src/init/dune
+++ b/src/init/dune
@@ -25,6 +25,7 @@
(public_name frama-c.init)
(modules frama_c_init gui_init)
(virtual_modules gui_init)
+ (libraries threads)
)
(include_subdirs no)
diff --git a/src/plugins/wp/Changelog b/src/plugins/wp/Changelog
index 174873b3019c281b3d86afbe536c5f6687d7da80..339dbc71af35924adb98ed50291d3351b7a7f2d4 100644
--- a/src/plugins/wp/Changelog
+++ b/src/plugins/wp/Changelog
@@ -26,6 +26,8 @@ Plugin WP <next-release>
- WP [2023-02-03] new option -wp-why3-extra-config for providing
additional Why3 configuration files
+- WP [2022-12-02] Fixes 'terminates' goals generation when some
+ 'terminates' or 'decreases' clauses are missing.
#####################
Plugin WP 26.0 (Iron)
diff --git a/tests/pdg/call.c b/tests/pdg/call.c
index 2b5d7ef5e264bf4fa9dd84e1d8f7ad67d0da98d9..f8385c40f0cddb126886ab18ab73e11698af64e8 100644
--- a/tests/pdg/call.c
+++ b/tests/pdg/call.c
@@ -1,9 +1,9 @@
/* run.config
-
+ LOG: call.f.dot call.g.dot
STDOPT: +"-lib-entry -main g -pdg -pdg-dot ./call "
*/
-/* Ne pas modifier : exemple utilisé dans le rapport. */
+/* Ne pas modifier : exemple utilisé dans le manuel du PDG. */
/*BDOC*/
struct {int a; int b; } G;
diff --git a/tests/pdg/oracle/call.f.dot b/tests/pdg/oracle/call.f.dot
new file mode 100644
index 0000000000000000000000000000000000000000..6069991160613f9dc1bb4eaeea0e4dda95d7f71f
--- /dev/null
+++ b/tests/pdg/oracle/call.f.dot
@@ -0,0 +1,31 @@
+digraph G {
+ rankdir=TB;
+ node [style="filled", ];
+ 2 [label="Decl a", fillcolor="#FFEFD5", shape=box, ];
+ 3 [label="In1", fillcolor="#6495ED", shape=box, ];
+ 4 [label="Decl b", fillcolor="#FFEFD5", shape=box, ];
+ 5 [label="In2", fillcolor="#6495ED", shape=box, ];
+ 6 [label="Decl __retres", fillcolor="#FFEFD5", shape=box, ];
+ 7 [label="G.b = b;", fillcolor="#CCCCCC", shape=box, ];
+ 8 [label="__retres = a + G.a;", fillcolor="#CCCCCC", shape=box, ];
+ 9 [label="return __retres;", fillcolor="#CCCCCC", shape=box, ];
+ 10 [label="OutRet", fillcolor="#90EE90", shape=box, ];
+ 11 [label="In(G.a)", fillcolor="#6495ED", shape=box, ];
+
+
+ edge [dir=back, ];
+ 3 -> 2 [color="#000000", style="dotted", ];
+ 2 -> 3 [color="#000000", style="dotted", ];
+ 5 -> 4 [color="#000000", style="dotted", ];
+ 4 -> 5 [color="#000000", style="dotted", ];
+ 4 -> 7 [color="#0000FF", ];
+ 5 -> 7 [color="#0000FF", ];
+ 2 -> 8 [color="#0000FF", ];
+ 3 -> 8 [color="#0000FF", ];
+ 6 -> 8 [color="#000000", style="dotted", ];
+ 11 -> 8 [color="#0000FF", ];
+ 6 -> 9 [color="#0000FF", ];
+ 8 -> 9 [color="#0000FF", ];
+ 9 -> 10 [color="#0000FF", ];
+
+ }
\ No newline at end of file
diff --git a/tests/pdg/oracle/call.g.dot b/tests/pdg/oracle/call.g.dot
new file mode 100644
index 0000000000000000000000000000000000000000..f0da71f1413380c06107d64436516841851b4eba
--- /dev/null
+++ b/tests/pdg/oracle/call.g.dot
@@ -0,0 +1,48 @@
+digraph G {
+ rankdir=TB;
+ node [style="filled", ];
+ 13 [label="Decl x", fillcolor="#FFEFD5", shape=box, ];
+ 14 [label="In1", fillcolor="#6495ED", shape=box, ];
+ 15 [label="Decl y", fillcolor="#FFEFD5", shape=box, ];
+ 16 [label="In2", fillcolor="#6495ED", shape=box, ];
+ 17 [label="Decl z", fillcolor="#FFEFD5", shape=box, ];
+ 18 [label="In3", fillcolor="#6495ED", shape=box, ];
+ 19 [label="Decl r", fillcolor="#FFEFD5", shape=box, ];
+ 21 [label="In1", fillcolor="#FFCA6E", shape=box, ];
+ 22 [label="In2", fillcolor="#FFCA6E", shape=box, ];
+ 23 [label="Out(G.b)", fillcolor="#FFCA6E", shape=box, ];
+ 24 [label="OutRet", fillcolor="#FFCA6E", shape=box, ];
+ 25 [label="A = G.a;", fillcolor="#CCCCCC", shape=box, ];
+ 26 [label="B = G.b;", fillcolor="#CCCCCC", shape=box, ];
+ 27 [label="return r;", fillcolor="#CCCCCC", shape=box, ];
+ 28 [label="OutRet", fillcolor="#90EE90", shape=box, ];
+ 29 [label="In(G.a)", fillcolor="#6495ED", shape=box, ];
+
+ subgraph cluster_Call5 { label="Call5 : /*@ assert Eva: signed_overflow: -2147483648 \226\137\164 x + y; */\n/*@ assert Eva: signed_overflow: x + y \226\137\164 2147483647; */\nint r = f(x + y,z);";
+ fillcolor="#B38B4D"; style="filled"; 24;23;22;21;
+ };
+
+ edge [dir=back, ];
+ 14 -> 13 [color="#000000", style="dotted", ];
+ 13 -> 14 [color="#000000", style="dotted", ];
+ 16 -> 15 [color="#000000", style="dotted", ];
+ 15 -> 16 [color="#000000", style="dotted", ];
+ 18 -> 17 [color="#000000", style="dotted", ];
+ 17 -> 18 [color="#000000", style="dotted", ];
+ 13 -> 21 [color="#0000FF", ];
+ 14 -> 21 [color="#0000FF", ];
+ 15 -> 21 [color="#0000FF", ];
+ 16 -> 21 [color="#0000FF", ];
+ 17 -> 22 [color="#0000FF", ];
+ 18 -> 22 [color="#0000FF", ];
+ 22 -> 23 [color="#0000FF", ];
+ 19 -> 24 [color="#000000", style="dotted", ];
+ 21 -> 24 [color="#0000FF", ];
+ 29 -> 24 [color="#0000FF", ];
+ 29 -> 25 [color="#0000FF", ];
+ 23 -> 26 [label="G.b", color="#0000FF", ];
+ 19 -> 27 [color="#0000FF", ];
+ 24 -> 27 [color="#0000FF", ];
+ 27 -> 28 [color="#0000FF", ];
+
+ }
\ No newline at end of file