From 2c883eb32cc67f17a48bb4ff7aca73f5811a056b Mon Sep 17 00:00:00 2001 From: Stanimir Bozhilov Date: Wed, 4 Oct 2023 21:58:30 +0200 Subject: [PATCH] Warn if lval contains an address with a non-local var --- src/analyses/base.ml | 13 ++++++++++++- 1 file changed, 12 insertions(+), 1 deletion(-) diff --git a/src/analyses/base.ml b/src/analyses/base.ml index a9457ca41b..a323e5f270 100644 --- a/src/analyses/base.ml +++ b/src/analyses/base.ml @@ -1051,7 +1051,18 @@ struct else if AD.may_be_null adr then ( AnalysisStateUtil.set_mem_safety_flag InvalidDeref; M.warn ~category:M.Category.Behavior.Undefined.nullpointer_dereference ~tags:[CWE 476] "May dereference NULL pointer" - ) + ); + (* Warn if any of the addresses contains a non-local variable *) + AD.iter (function + | AD.Addr.Addr (v,o) -> + if not @@ CPA.mem v st.cpa then ( + (* TODO: Not the smartest move to set the global flag within an iter *) + (* TODO: We can resort to using AD.exists instead *) + AnalysisStateUtil.set_mem_safety_flag InvalidDeref; + M.warn "lval %a points to non-local variable %a. Invalid pointer dereference may occur" d_lval lval CilType.Varinfo.pretty v + ) + | _ -> () + ) adr ); AD.map (add_offset_varinfo (convert_offset a gs st ofs)) adr | _ ->