From 4439652f6a89d8526c712b9e3ab386ab7a1e5402 Mon Sep 17 00:00:00 2001
From: Boris Yakobowski <boris.yakobowski@cea.fr>
Date: Sat, 20 Sep 2014 09:54:45 +0200
Subject: [PATCH] [Value] Optional warnings when the memcpy builtin copies
indeterminate bits
---
src/value/builtins_nonfree.ml | 6 ++++++
tests/misc/oracle/memcpy.res.oracle | 4 ++++
2 files changed, 10 insertions(+)
diff --git a/src/value/builtins_nonfree.ml b/src/value/builtins_nonfree.ml
index d37ad486d55..d8748b113ff 100644
--- a/src/value/builtins_nonfree.ml
+++ b/src/value/builtins_nonfree.ml
@@ -215,6 +215,12 @@ let frama_c_memcpy state actuals =
Valarms.set_syntactic_context (Valarms.SyMemLogic array_src);
Valarms.warn_mem_read with_alarms;
end;
+ begin match v with
+ | V_Or_Uninitialized.C_init_noesc _ -> ()
+ | _ -> Value_parameters.result ~dkey ~current:true ~once:true
+ "@[In memcpy@ builtin:@ imprecise@ copy of@ indeterminate@ values@]%t"
+ Value_util.pp_callstack
+ end;
Valarms.set_syntactic_context (Valarms.SyMemLogic array_dst);
let new_state = Eval_op.add_binding_unspecified ~with_alarms
~remove_invalid:true ~exact:false new_state loc_left v
diff --git a/tests/misc/oracle/memcpy.res.oracle b/tests/misc/oracle/memcpy.res.oracle
index 7bbc6bdf16e..5b8036a6926 100644
--- a/tests/misc/oracle/memcpy.res.oracle
+++ b/tests/misc/oracle/memcpy.res.oracle
@@ -174,6 +174,7 @@ tests/misc/memcpy.c:180:[value] Assertion got status valid.
[value] Done for function make_unknown
tests/misc/memcpy.c:174:[value] Call to builtin memcpy(({{ (char *)&b }},{{ (char const *)&a }},[0..25]))
tests/misc/memcpy.c:174:[value:imprecision] In memcpy builtin: too many sizes to enumerate, possible loss of precision
+tests/misc/memcpy.c:174:[value:imprecision] In memcpy builtin: imprecise copy of indeterminate values
tests/misc/memcpy.c:187:[value] Call to builtin memcpy(({{ (char *)&b }},{{ (char const *)&a }},{10}))
[value] computing for function itv <- main_uninit <- main_all.
Called from tests/misc/memcpy.c:190.
@@ -188,9 +189,11 @@ tests/misc/memcpy.c:175:[value] Assertion got status valid.
tests/misc/memcpy.c:188:[value] Assertion got status valid.
tests/misc/memcpy.c:190:[value] Call to builtin memcpy(({{ (char *)&b }},{{ (char const *)&a }},[0..25]))
tests/misc/memcpy.c:190:[value:imprecision] In memcpy builtin: too many sizes to enumerate, possible loss of precision
+tests/misc/memcpy.c:190:[value:imprecision] In memcpy builtin: imprecise copy of indeterminate values
tests/misc/memcpy.c:198:[value] Call to builtin memcpy(({{ (char *)&b }},{{ (char const *)&a }},{10}))
tests/misc/memcpy.c:181:[value] Call to builtin memcpy(({{ (char *)&b }},{{ (char const *)&a }},[0..25]))
tests/misc/memcpy.c:181:[value:imprecision] In memcpy builtin: too many sizes to enumerate, possible loss of precision
+tests/misc/memcpy.c:181:[value:imprecision] In memcpy builtin: imprecise copy of indeterminate values
tests/misc/memcpy.c:191:[value] Assertion got status valid.
tests/misc/memcpy.c:199:[value] Assertion got status valid.
tests/misc/memcpy.c:182:[kernel] warning: accessing uninitialized left-value: assert \initialized(&b[11]);
@@ -200,6 +203,7 @@ tests/misc/memcpy.c:192:[kernel] warning: accessing uninitialized left-value: as
[value] Done for function itv
tests/misc/memcpy.c:200:[value] Call to builtin memcpy(({{ (char *)&b }},{{ (char const *)&a }},[0..25]))
tests/misc/memcpy.c:200:[value:imprecision] In memcpy builtin: too many sizes to enumerate, possible loss of precision
+tests/misc/memcpy.c:200:[value:imprecision] In memcpy builtin: imprecise copy of indeterminate values
tests/misc/memcpy.c:201:[kernel] warning: accessing uninitialized left-value: assert \initialized(&b[11]);
[value] Recording results for main_uninit
[from] Computing for function main_uninit
--
GitLab