diff --git a/src/plugins/wp/AssignsCompleteness.ml b/src/plugins/wp/AssignsCompleteness.ml
new file mode 100644
index 0000000000000000000000000000000000000000..25db9a6e85e9a6a4157343361a9aaeca4d4a7ffe
--- /dev/null
+++ b/src/plugins/wp/AssignsCompleteness.ml
@@ -0,0 +1,166 @@
+(**************************************************************************)
+(* *)
+(* This file is part of WP plug-in of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2020 *)
+(* CEA (Commissariat a l'energie atomique et aux energies *)
+(* 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
+
+module Completeness = struct
+ module KfParam = struct
+ include Cil_datatype.Kf
+ let label = None
+ end
+
+ module Data =
+ Datatype.Pair
+ (Datatype.Bool)
+ (Datatype.Function(KfParam)(Datatype.Unit))
+
+ include State_builder.Hashtbl
+ (Cil_datatype.Kf.Hashtbl)
+ (Data)
+ (struct
+ let name = "RefUsage.AssignsCompleteness.Callbacks"
+ let size = 17
+ let dependencies = [ Ast.self ]
+ end)
+end
+
+exception Incomplete_assigns of (string list * string)
+
+let wkey_pedantic = Wp_parameters.register_warn_category "pedantic-assigns"
+
+type ('a, 'b) result = Ok of 'a | Error of 'b
+
+let collect_assigns kf =
+ let opt_try f p = function None -> f p | Some x -> Some x in
+ let fold_assigns bhv =
+ let folder _ a acc = match a, acc with
+ | WritesAny, _ -> None
+ | _, None -> Some a
+ | _, Some acc -> Some (Logic_utils.concat_assigns acc a)
+ in
+ Annotations.fold_assigns folder kf bhv None
+ in
+ let find_default () =
+ match fold_assigns Cil.default_behavior_name with
+ | None -> None
+ | Some x -> Some [x]
+ in
+ let incompletes = ref [] in
+ let find_complete () =
+ let fold_behaviors names =
+ let folder l name = match (fold_assigns name) with
+ | None -> raise (Incomplete_assigns(names, name))
+ | Some a -> a :: l
+ in
+ try Some (List.fold_left folder [] names)
+ with Incomplete_assigns(bhv_l,b) ->
+ incompletes := (bhv_l, b) :: !incompletes ;
+ None
+ in
+ Annotations.fold_complete (fun _ -> opt_try fold_behaviors) kf None
+ in
+ (* First:
+ - try to find default behavior assigns, if we cannot get it
+ - try to find a "complete behaviors" set where each behavior has assigns
+ As assigns and froms are over-approximations, the result (if it exists)
+ must cover all assigned memory locations and all data dependencies.
+ *)
+ match opt_try find_complete () (opt_try find_default () None) with
+ | None -> Error !incompletes
+ | Some r -> Ok r
+
+let pretty_behaviors_errors fmt l =
+ let pp_complete =
+ Pretty_utils.pp_list ~pre:"{" ~suf:"}" ~sep:", " Format.pp_print_string
+ in
+ let pp_bhv_error fmt (bhv_l, name) =
+ Format.fprintf fmt
+ "- in complete behaviors: %a@\n No assigns for (at least) '%s'@\n"
+ pp_complete bhv_l name
+ in
+ match l with
+ | [] -> Format.fprintf fmt ""
+ | l -> Format.fprintf fmt "%a" (Pretty_utils.pp_list pp_bhv_error) l
+
+let check_assigns kf assigns =
+ let complete = (true, fun _ -> ()) in
+ let incomplete (_status, current) warning =
+ let new_warning kf =
+ current kf ;
+ warning kf ;
+ in
+ (false, new_warning)
+ in
+ let vassigns acc a =
+ let res_t = Kernel_function.get_return_type kf in
+ let assigns_result ({ it_content=t }, _) = Logic_utils.is_result t in
+ let froms = match a with WritesAny -> [] | Writes l -> l in
+ let acc =
+ if Cil.isPointerType res_t && not (List.exists assigns_result froms) then
+ incomplete acc
+ begin fun kf ->
+ Wp_parameters.warning ~wkey:wkey_pedantic
+ ~once:true ~source:(fst (Kernel_function.get_location kf))
+ "No 'assigns \\result \\from ...' specification for function '%a'\
+ returning pointer type.@ Callers assumptions might be imprecise."
+ Kernel_function.pretty kf ;
+ end
+ else acc
+ in
+ let vfrom acc = function
+ | t, FromAny when Logic_typing.is_pointer_type t.it_content.term_type ->
+ incomplete acc
+ begin fun _kf ->
+ Wp_parameters.warning ~wkey:wkey_pedantic
+ ~once:true ~source:(fst t.it_content.term_loc)
+ "No \\from specification for assigned pointer '%a'.@ \
+ Callers assumptions might be imprecise."
+ Cil_printer.pp_identified_term t
+ end
+ | _ -> acc
+ in List.fold_left vfrom acc froms
+ in
+ match assigns with
+ | Error l ->
+ false,
+ begin fun kf ->
+ Wp_parameters.warning ~wkey:wkey_pedantic
+ ~once:true ~source:(fst (Kernel_function.get_location kf))
+ "No 'assigns' specification for function '%a'.@\n%a\
+ Callers assumptions might be imprecise."
+ Kernel_function.pretty kf
+ pretty_behaviors_errors l
+ end
+ | Ok l ->
+ List.fold_left vassigns complete l
+
+let memo_compute kf =
+ Completeness.memo (fun kf -> check_assigns kf (collect_assigns kf)) kf
+
+let compute kf =
+ ignore (memo_compute kf)
+
+let is_complete kf =
+ fst(memo_compute kf)
+
+let warn kf =
+ snd(memo_compute kf) kf
diff --git a/src/plugins/wp/AssignsCompleteness.mli b/src/plugins/wp/AssignsCompleteness.mli
new file mode 100644
index 0000000000000000000000000000000000000000..8fa55bec1d546c61fddd6cdd9e6a7bc65c2ee968
--- /dev/null
+++ b/src/plugins/wp/AssignsCompleteness.mli
@@ -0,0 +1,38 @@
+(**************************************************************************)
+(* *)
+(* This file is part of WP plug-in of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2020 *)
+(* CEA (Commissariat a l'energie atomique et aux energies *)
+(* 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). *)
+(* *)
+(**************************************************************************)
+
+(** This module is used to check the assigns specification of a given function
+ so that if it is not precise enough to enable precise memory models
+ hypotheses computation, the assigns specification is considered incomplete.
+
+ All these functions are memoized.
+*)
+
+val compute: Kernel_function.t -> unit
+
+val is_complete: Kernel_function.t -> bool
+
+val warn: Kernel_function.t -> unit
+(** Displays a warning if the given kernel function has incomplete assigns.
+ Note that the warning is configured with [~once] set to [true]. *)
+
+val wkey_pedantic: Wp_parameters.warn_category
diff --git a/src/plugins/wp/Makefile.in b/src/plugins/wp/Makefile.in
index 2ab8ab0e65898a650b80a0e9f5b4db42800298ba..1d5323096b59b43fd323217981be3315320eb9e1 100644
--- a/src/plugins/wp/Makefile.in
+++ b/src/plugins/wp/Makefile.in
@@ -63,7 +63,7 @@ PLUGIN_CMO:= \
wp_parameters wp_error \
dyncall ctypes clabels \
Why3Provers \
- Context Warning MemoryContext wpContext \
+ Context Warning AssignsCompleteness MemoryContext wpContext \
LogicUsage RefUsage \
Layout Region \
RegionAnnot RegionAccess RegionDump RegionAnalysis \
@@ -234,7 +234,7 @@ WP_API_BASE= \
LogicUsage.mli RefUsage.mli \
normAtLabels.mli \
wpPropId.mli mcfg.ml \
- Context.mli Warning.mli wpContext.mli \
+ Context.mli Warning.mli AssignsCompleteness.mli wpContext.mli \
Lang.mli Repr.mli Passive.mli Splitter.mli \
LogicBuiltins.mli Definitions.mli \
Cint.mli Cfloat.mli Vset.mli Cstring.mli \
diff --git a/src/plugins/wp/tests/test_config b/src/plugins/wp/tests/test_config
index 14ca1f7d9cc68b971448022ebc5ee6df17ae822a..0181ba49e1a2fd88c7a229e8b3b44bd8a11b95ea 100644
--- a/src/plugins/wp/tests/test_config
+++ b/src/plugins/wp/tests/test_config
@@ -1,3 +1,3 @@
PLUGIN: rtegen,wp
-CMD: @frama-c@ -wp -wp-prover none -wp-print -wp-msg-key shell @OPTIONS@
+CMD: @frama-c@ -wp -wp-prover none -wp-print -wp-msg-key shell -wp-warn-key "pedantic-assigns=inactive" @OPTIONS@
OPT:
diff --git a/src/plugins/wp/tests/test_config_qualif b/src/plugins/wp/tests/test_config_qualif
index 8e0f64feca8e0f9e9d690c12e88122aebb2af27a..039d6269182c1d6e61b2a70c250610b3d3cd9dd8 100644
--- a/src/plugins/wp/tests/test_config_qualif
+++ b/src/plugins/wp/tests/test_config_qualif
@@ -1,4 +1,4 @@
PLUGIN: rtegen,wp
-MACRO: WP_OPTIONS -wp -wp-par 1 -wp-share ../../../share -wp-msg-key shell -wp-report %{dep:../../qualif.report} -wp-session ../oracle@PTEST_CONFIG@/@PTEST_NAME@.@PTEST_NUMBER@.session -wp-cache-env -wp-cache replay -wp-coq-timeout 120
+MACRO: WP_OPTIONS -wp -wp-par 1 -wp-share ../../../share -wp-msg-key shell -wp-warn-key pedantic-assigns=inactive -wp-report %{dep:../../qualif.report} -wp-session ../oracle@PTEST_CONFIG@/@PTEST_NAME@.@PTEST_NUMBER@.session -wp-cache-env -wp-cache replay -wp-coq-timeout 120
CMD: @frama-c@ @WP_OPTIONS@ @OPTIONS@
OPT:
diff --git a/src/plugins/wp/tests/wp_bts/bts_2110.i b/src/plugins/wp/tests/wp_bts/bts_2110.i
index 6ea65e502859f5e5e4ad31023383e0793e49fce4..431bd45052e4d02e8b1aa005223fcaed306612b9 100644
--- a/src/plugins/wp/tests/wp_bts/bts_2110.i
+++ b/src/plugins/wp/tests/wp_bts/bts_2110.i
@@ -1,5 +1,5 @@
/* run.config
- CMD: @frama-c@ -wp -wp-msg-key shell,cluster,print-generated -wp-prover why3 -wp-gen @OPTIONS@
+ CMD: @frama-c@ -wp -wp-msg-key shell,cluster,print-generated -wp-prover why3 -wp-gen @OPTIONS@ -wp-warn-key "pedantic-assigns=inactive"
OPT:
*/
diff --git a/src/plugins/wp/tests/wp_plugin/model.i b/src/plugins/wp/tests/wp_plugin/model.i
index 6739c61f1e0b01de69af6c172d99740fe8378cfd..3f94f987be8e6f2575257e04bb137253c2c8f24e 100644
--- a/src/plugins/wp/tests/wp_plugin/model.i
+++ b/src/plugins/wp/tests/wp_plugin/model.i
@@ -1,5 +1,5 @@
/* run.config
- CMD: @frama-c@ -wp-msg-key cluster,shell,print-generated -wp-prover why3 @OPTIONS@
+ CMD: @frama-c@ -wp-msg-key cluster,shell,print-generated -wp-prover why3 @OPTIONS@ -wp-warn-key "pedantic-assigns=inactive"
OPT: -wp-model Typed -wp -wp-gen -wp-print -then -wp-model Typed+ref -wp -wp-gen -wp-print
*/
diff --git a/src/plugins/wp/tests/wp_plugin/nosession.i b/src/plugins/wp/tests/wp_plugin/nosession.i
index 655040b2b5690980fc5c7194d57d8ae125df54ab..5f7db991977eb47013617e058af16dc08d8e105e 100644
--- a/src/plugins/wp/tests/wp_plugin/nosession.i
+++ b/src/plugins/wp/tests/wp_plugin/nosession.i
@@ -3,7 +3,7 @@
*/
/* run.config_qualif
- CMD: @frama-c@ -wp-msg-key shell @OPTIONS@
+ CMD: @frama-c@ -wp-msg-key shell @OPTIONS@ -wp-warn-key pedantic-assigns=inactive
OPT: -wp -wp-prover alt-ergo -wp-session shall_not_exists_dir -wp-cache offline -wp-no-cache-env
COMMENT: The session directory shall not be created
*/
diff --git a/src/plugins/wp/tests/wp_plugin/rte.i b/src/plugins/wp/tests/wp_plugin/rte.i
index 48def339a017caf435ecc416bf9c3ce34eb08c9e..b9befd3922c6f1e04b0dc913c51ad2a7fd31eb61 100644
--- a/src/plugins/wp/tests/wp_plugin/rte.i
+++ b/src/plugins/wp/tests/wp_plugin/rte.i
@@ -1,5 +1,5 @@
/* run.config
- CMD: @frama-c@ -wp -wp-prover none -wp-msg-key shell -wp-msg-key rte @OPTIONS@
+ CMD: @frama-c@ -wp -wp-prover none -wp-msg-key shell -wp-msg-key rte @OPTIONS@ -wp-warn-key "pedantic-assigns=inactive"
OPT: -wp-rte -no-warn-invalid-bool -then -print -no-unicode
OPT: -wp-rte -no-warn-signed-overflow -then -print -no-unicode
OPT: -wp-rte -warn-unsigned-overflow -then -print -no-unicode
diff --git a/src/plugins/wp/tests/wp_plugin/stmt.c b/src/plugins/wp/tests/wp_plugin/stmt.c
index 203ee97d9d2975c44ca56d1b2a87699f4c16ae03..b777a13d56ac4df22421b2e74d615e542435fade 100644
--- a/src/plugins/wp/tests/wp_plugin/stmt.c
+++ b/src/plugins/wp/tests/wp_plugin/stmt.c
@@ -5,7 +5,7 @@
/* run.config_qualif
PLUGIN: @PLUGIN@ report
OPT: -then -report
- EXECNOW: LOG stmt.log LOG f.dot LOG f_default_for_stmt_2.dot LOG g.dot LOG g_default_for_stmt_11.dot @frama-c@ -wp-precond-weakening -wp -wp-model Dump -wp-out . -wp-msg-key shell 1> stmt.log
+ EXECNOW: LOG stmt.log LOG f.dot LOG f_default_for_stmt_2.dot LOG g.dot LOG g_default_for_stmt_11.dot @frama-c@ -wp-precond-weakening -wp -wp-warn-key pedantic-assigns=inactive -wp-model Dump -wp-out . -wp-msg-key shell 1> stmt.log
*/
/*@ ensures a > 0 ==> \result == a + b;
@ ensures a <= 0 ==> \result == -1;
diff --git a/src/plugins/wp/tests/wp_region/test_config b/src/plugins/wp/tests/wp_region/test_config
index 10e84152c64cd213fa9612a5c5b359080279eb2e..cc353c1a3769ff673c1dad9a0e92ad473d5e41b5 100644
--- a/src/plugins/wp/tests/wp_region/test_config
+++ b/src/plugins/wp/tests/wp_region/test_config
@@ -1,3 +1,3 @@
CMD: @frama-c@ @OPTIONS@
#LOG: @PTEST_NAME@/region/job.dot
-OPT: -wp-prover none -wp-region -wp-msg-key dot,chunk,roots,garbled -wp-out @PTEST_NAME@ -wp-fct job
+OPT: -wp-prover none -wp-region -wp-msg-key dot,chunk,roots,garbled -wp-warn-key pedantic-assigns=inactive -wp-out @PTEST_NAME@ -wp-fct job
diff --git a/src/plugins/wp/tests/wp_usage/save_load.i b/src/plugins/wp/tests/wp_usage/save_load.i
index 648b4a81871534884125a5a70a97dda657d7861b..8e5b245ddd4a8b4f520dc04b340b2fa169125ba1 100644
--- a/src/plugins/wp/tests/wp_usage/save_load.i
+++ b/src/plugins/wp/tests/wp_usage/save_load.i
@@ -1,6 +1,6 @@
/* run.config
- EXECNOW: LOG save_load.sav.res LOG save_load.sav.err BIN @PTEST_NAME@.sav @frama-c@ -wp -wp-print -wp-prover none -save @PTEST_NAME@.sav > @PTEST_NAME@.sav.res 2> @PTEST_NAME@.sav.err
- CMD: @frama-c@ -load %{dep:@PTEST_NAME@.sav} @OPTIONS@
+ EXECNOW: LOG save_load.sav.res LOG save_load.sav.err BIN @PTEST_NAME@.sav @frama-c@ -wp -wp-warn-key pedantic-assigns=inactive -wp-print -wp-prover none -save @PTEST_NAME@.sav > @PTEST_NAME@.sav.res 2> @PTEST_NAME@.sav.err
+ CMD: @frama-c@ -load %{dep:@PTEST_NAME@.sav} @OPTIONS@ -wp-warn-key pedantic-assigns=inactive
OPT: -print
OPT: -wp -wp-prover none -wp-print
*/