From c882d8584f8bc75733b06659a95b72a136d938fe Mon Sep 17 00:00:00 2001 From: oliver Date: Mon, 22 Jan 2024 15:08:50 +0100 Subject: [PATCH] rename depth to dimension --- src/cdomain/value/cdomains/valueDomain.ml | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) diff --git a/src/cdomain/value/cdomains/valueDomain.ml b/src/cdomain/value/cdomains/valueDomain.ml index 4a5b1edaa0..0ee4f0778b 100644 --- a/src/cdomain/value/cdomains/valueDomain.ml +++ b/src/cdomain/value/cdomains/valueDomain.ml @@ -855,26 +855,26 @@ 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) (depth:int): 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) (dimension:int): 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 let l', o' = shift_one_over l o in - let ev = do_eval_offset ask f (Blobs.value c) ox exp l' o' v t depth in + let ev = do_eval_offset ask f (Blobs.value c) ox exp l' o' v t dimension in zero_init_calloced_memory orig ev t end | Blob((va, _, orig) as c), `Field _ -> begin let l', o' = shift_one_over l o in - let ev = do_eval_offset ask f (Blobs.value c) offs exp l' o' v t depth in + let ev = do_eval_offset ask f (Blobs.value c) offs exp l' o' v t dimension in zero_init_calloced_memory orig ev t end | Blob((va, _, orig) as c), `NoOffset -> begin let l', o' = shift_one_over l o in - let ev = do_eval_offset ask f (Blobs.value c) offs exp l' o' v t depth in + let ev = do_eval_offset ask f (Blobs.value c) offs exp l' o' v t dimension in zero_init_calloced_memory orig ev t end | Bot, _ -> Bot @@ -886,7 +886,7 @@ struct | Struct str -> let x = Structs.get str fld in let l', o' = shift_one_over l o in - do_eval_offset ask f x offs exp l' o' v t depth + do_eval_offset ask f x offs exp l' o' v t dimension | Top -> M.info ~category:Imprecise "Trying to read a field, but the struct is unknown"; top () | _ -> M.warn ~category:Imprecise ~tags:[Category Program] "Trying to read a field, but was not given a struct"; top () end @@ -901,7 +901,7 @@ struct | _ -> let x = cast ~torg:l_fld.ftype fld.ftype value in let l', o' = shift_one_over l o in - do_eval_offset ask f x offs exp l' o' v t depth) + do_eval_offset ask f x offs exp l' o' v t dimension) | Union _ -> top () | Top -> M.info ~category:Imprecise "Trying to read a field, but the union is unknown"; top () | _ -> M.warn ~category:Imprecise ~tags:[Category Program] "Trying to read a field, but was not given a union"; top () @@ -911,10 +911,10 @@ struct match x with | Array x -> let e = determine_offset ask l o exp v in - do_eval_offset ask f (CArrays.get ask x (e, idx) (Some(v,depth))) offs exp l' o' v t (depth+1) + do_eval_offset ask f (CArrays.get ask x (e, idx) (Some(v,dimension))) offs exp l' o' v t (dimension+1) | Address _ -> begin - do_eval_offset ask f x offs exp l' o' v t depth (* this used to be `blob `address -> we ignore the index *) + do_eval_offset ask f x offs exp l' o' v t dimension (* this used to be `blob `address -> we ignore the index *) end | x when GobOption.exists (BI.equal (BI.zero)) (IndexDomain.to_int idx) -> eval_offset ask f x offs exp v t | Top -> M.info ~category:Imprecise "Trying to read an index, but the array is unknown"; top ()