Skip to content

Commit 5347c08

Browse files
committed
Add eval_offset tracing
1 parent 810fab5 commit 5347c08

1 file changed

Lines changed: 5 additions & 0 deletions

File tree

src/cdomains/valueDomain.ml

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -824,6 +824,8 @@ struct
824824
(* Funny, this does not compile without the final type annotation! *)
825825
let rec eval_offset (ask: VDQ.t) f (x: t) (offs:offs) (exp:exp option) (v:lval option) (t:typ): t =
826826
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 =
827+
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;
828+
let r =
827829
match x, offs with
828830
| Blob((va, _, orig) as c), `Index (_, ox) ->
829831
begin
@@ -886,6 +888,9 @@ struct
886888
| Top -> M.info ~category:Imprecise "Trying to read an index, but the array is unknown"; top ()
887889
| _ -> M.warn ~category:Imprecise ~tags:[Category Program] "Trying to read an index, but was not given an array (%a)" pretty x; top ()
888890
end
891+
in
892+
if M.tracing then M.traceu "eval_offset" "do_eval_offset -> %a\n" pretty r;
893+
r
889894
in
890895
let l, o = match exp with
891896
| Some(Lval (x,o)) -> Some ((x, NoOffset)), Some(o)

0 commit comments

Comments
 (0)