diff --git a/src/value/builtins_nonfree.ml b/src/value/builtins_nonfree.ml index d37ad486d551b60f6f9f653605a31566013fcc11..d8748b113ff2f143dd10ccd1db3829f216d8c318 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 7bbc6bdf16eb46be7db19e80c3b750fc1b0609d5..5b8036a6926c3c5e1ae5232264fef69db0d6e4cb 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