From 5347c087b4eec4c7db77832b2c4f97c7d2841598 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Tue, 26 Sep 2023 11:22:12 +0300 Subject: [PATCH] Add eval_offset tracing --- src/cdomains/valueDomain.ml | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/src/cdomains/valueDomain.ml b/src/cdomains/valueDomain.ml index 9d894b6b34..cba4b04c18 100644 --- a/src/cdomains/valueDomain.ml +++ b/src/cdomains/valueDomain.ml @@ -824,6 +824,8 @@ struct (* Funny, this does not compile without the final type annotation! *) let rec eval_offset (ask: VDQ.t) f (x: t) (offs:offs) (exp:exp option) (v:lval option) (t:typ): t = let rec do_eval_offset (ask:VDQ.t) f (x:t) (offs:offs) (exp:exp option) (l:lval option) (o:offset option) (v:lval option) (t:typ): t = + if M.tracing then M.traceli "eval_offset" "do_eval_offset %a %a (%a)\n" pretty x Offs.pretty offs (Pretty.docOpt (CilType.Exp.pretty ())) exp; + let r = match x, offs with | Blob((va, _, orig) as c), `Index (_, ox) -> begin @@ -886,6 +888,9 @@ struct | Top -> M.info ~category:Imprecise "Trying to read an index, but the array is unknown"; top () | _ -> M.warn ~category:Imprecise ~tags:[Category Program] "Trying to read an index, but was not given an array (%a)" pretty x; top () end + in + if M.tracing then M.traceu "eval_offset" "do_eval_offset -> %a\n" pretty r; + r in let l, o = match exp with | Some(Lval (x,o)) -> Some ((x, NoOffset)), Some(o)