From 2c6fbce219530d49d90c9e142a8d77d4f46e0caf Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Wed, 7 Oct 2020 11:14:45 +0200
Subject: [PATCH] Deactivate pedantic assigns warning in WP
---
Makefile | 1 +
configure.ac | 1 +
frama_Clang_register.ml | 4 ++++
3 files changed, 6 insertions(+)
diff --git a/Makefile b/Makefile
index 66999186..b965f9d5 100644
--- a/Makefile
+++ b/Makefile
@@ -45,6 +45,7 @@ PLUGIN_GENERATED:= \
else
PLUGIN_GENERATED:=
endif
+PLUGIN_DEPENDENCIES:= wp
ifeq ("$(RUN_TESTS)","yes")
PLUGIN_TESTS_DIRS:=basic stl class val_analysis template specs exn pp ppwp bugs da
else
diff --git a/configure.ac b/configure.ac
index 41df9339..aed9b95d 100644
--- a/configure.ac
+++ b/configure.ac
@@ -37,6 +37,7 @@ check_plugin([frama_clang],PLUGIN_RELATIVE_PATH(plugin_file),
[C++ front-end for Frama-C],yes)
plugin_require_external(frama_clang,camlp5o)
+plugin_use(frama_clang,wp)
# check for system C++ compiler, as we can't rely on clang++ itself because
# of potential incompatibilities with GNU libstdc++ v5.
diff --git a/frama_Clang_register.ml b/frama_Clang_register.ml
index 1af18d65..37f0ada6 100644
--- a/frama_Clang_register.ml
+++ b/frama_Clang_register.ml
@@ -176,6 +176,10 @@ let parse_cxx file =
let cxx_suffixes = [ ".cpp"; ".C"; ".cxx"; ".c++"; ".cc"; ".ii" ]
+let remove_wp_assigns_warning () =
+ Wp.Wp_parameters.set_warn_status Wp.AssignsCompleteness.wkey_pedantic Log.Winactive
+
let () =
+ remove_wp_assigns_warning () ;
List.iter
(fun suf -> File.new_file_type suf parse_cxx) cxx_suffixes
--
GitLab