Skip to content

Commit

Permalink
rename depth to dimension
Browse files Browse the repository at this point in the history
  • Loading branch information
FungOliver committed Jan 24, 2024
1 parent 92cd808 commit c882d85
Showing 1 changed file with 8 additions and 8 deletions.
16 changes: 8 additions & 8 deletions src/cdomain/value/cdomains/valueDomain.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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
Expand All @@ -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 ()
Expand All @@ -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 ()
Expand Down

0 comments on commit c882d85

Please sign in to comment.