From f8f6243a63370006622229a92fb81499e04aef36 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Tue, 18 Jan 2022 09:11:02 +0100
Subject: [PATCH] [Eva] Always emits undeterminate alarms on arguments of
 functions without body.

Always emits initiatialized/escaping alarms on arguments of call to functions
whose body is not analyzed, as we cannot be sure these arguments will only be
used for copies and not in computations.
---
 src/plugins/value/engine/transfer_stmt.ml      |  6 ++++--
 .../value/oracle/initialized_copy.1.res.oracle | 18 ++++++++++--------
 2 files changed, 14 insertions(+), 10 deletions(-)

diff --git a/src/plugins/value/engine/transfer_stmt.ml b/src/plugins/value/engine/transfer_stmt.ml
index 261bfb1116e..19c6c9973d5 100644
--- a/src/plugins/value/engine/transfer_stmt.ml
+++ b/src/plugins/value/engine/transfer_stmt.ml
@@ -81,10 +81,12 @@ let do_copy_at = function
     with Not_found -> assert false
 
 (* Warn for call arguments that contain uninitialized/escaping except on
-   [Frama_C_show_each] directives or if the user disables these alarms. *)
+   [Frama_C_show_each] directives or if the user disables these alarms
+   on functions whose body is analyzed. *)
 let is_determinate kf =
   let name = Kernel_function.get_name kf in
-  warn_indeterminate kf && not (Ast_info.is_frama_c_builtin name)
+  (warn_indeterminate kf || !Db.Value.use_spec_instead_of_definition kf)
+  && not (Ast_info.is_frama_c_builtin name)
 
 let subdivide_stmt = Value_util.get_subdivision
 
diff --git a/tests/value/oracle/initialized_copy.1.res.oracle b/tests/value/oracle/initialized_copy.1.res.oracle
index 19688c6d03b..99d71e0d2f6 100644
--- a/tests/value/oracle/initialized_copy.1.res.oracle
+++ b/tests/value/oracle/initialized_copy.1.res.oracle
@@ -72,13 +72,8 @@
 [eva] Recording results for f
 [eva] Done for function f
 [eva] initialized_copy.i:130: Frama_C_show_each_unreached:
-[eva] computing for function g <- main.
-  Called from initialized_copy.i:135.
-[kernel:annot:missing-spec] initialized_copy.i:135: Warning: 
-  Neither code nor specification for function g, generating default assigns from the prototype
-[eva] using specification for function g
-[eva] Done for function g
-[eva] initialized_copy.i:136: Frama_C_show_each_unreached:
+[eva:alarm] initialized_copy.i:135: Warning: 
+  accessing uninitialized left-value. assert \initialized(&a_6);
 [eva] computing for function f <- main.
   Called from initialized_copy.i:143.
 [eva] Recording results for f
@@ -91,19 +86,26 @@
   a_7 ∈ {1} or UNINITIALIZED
   __retres ∈ UNINITIALIZED
   ==END OF DUMP==
+[eva:alarm] initialized_copy.i:151: Warning: 
+  accessing uninitialized left-value. assert \initialized(&a_8);
 [eva] computing for function g <- main.
   Called from initialized_copy.i:151.
+[kernel:annot:missing-spec] initialized_copy.i:151: Warning: 
+  Neither code nor specification for function g, generating default assigns from the prototype
+[eva] using specification for function g
 [eva] Done for function g
 [eva] initialized_copy.i:152: 
   Frama_C_dump_each:
   # cvalue:
   w[0..9] ∈ {0; 12} or UNINITIALIZED
   v ∈ [--..--]
-  a_8 ∈ {1} or UNINITIALIZED
+  a_8 ∈ {1}
   __retres ∈ UNINITIALIZED
   ==END OF DUMP==
 [eva] Recording results for main
 [eva] done for function main
+[eva] initialized_copy.i:135: 
+  assertion 'Eva,initialization' got final status invalid.
 [eva] ====== VALUES COMPUTED ======
 [eva:final-states] Values at end of function f:
   
-- 
GitLab