From 026fe73a26459502a454a0a7b1868b565989289b Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Fri, 18 Sep 2020 13:39:06 +0200
Subject: [PATCH] [wp] RefUsage: checks presence of assigns specification for
escaping pointers
---
src/plugins/wp/RefUsage.ml | 22 ++++++++++++++++++++++
1 file changed, 22 insertions(+)
diff --git a/src/plugins/wp/RefUsage.ml b/src/plugins/wp/RefUsage.ml
index df5426a0018..63ce18f7bc1 100644
--- a/src/plugins/wp/RefUsage.ml
+++ b/src/plugins/wp/RefUsage.ml
@@ -668,10 +668,32 @@ let cfun_spec env kf =
let update_spec_env v = env.local.spec <- E.cup env.local.spec v ;
Cil.SkipChildren
in
+ let res_type = Kernel_function.get_return_type kf in
+ let is_from_result ({ it_content=t }, _) = Logic_utils.is_result t in
let visitor = object
inherit Cil.nopCilVisitor
method !vpredicate p = update_spec_env (pred env p)
method !vterm t = update_spec_env (vterm env t)
+
+ method! vassigns = function
+ | WritesAny -> Cil.SkipChildren
+ | Writes l
+ when Cil.isPointerType res_type && not (List.exists is_from_result l) ->
+ Wp_parameters.warning ~once:true
+ "No 'assigns \\result \\from ...' specification for function '%a', \
+ returning pointer type.@ Callers assumptions might be imprecise."
+ Kernel_function.pretty kf ;
+ Cil.DoChildren
+ | _ -> Cil.DoChildren
+
+ method! vfrom = function
+ | it, FromAny when Logic_typing.is_pointer_type it.it_content.term_type ->
+ Wp_parameters.warning ~once:true
+ "No \\from specification for assigned pointer '%a'.@ \
+ Callers assumptions might be imprecise."
+ Cil_printer.pp_identified_term it ;
+ Cil.DoChildren
+ | _ -> Cil.DoChildren
end in
let spec = Annotations.funspec kf in
ignore (Cil.visitCilFunspec (visitor:>Cil.cilVisitor) spec) ;
--
GitLab