Skip to content

Commit d3d59ee

Browse files
committed
Use IntDomain equal_to instead of GobOption.exists on to_int result
1 parent 318c25a commit d3d59ee

1 file changed

Lines changed: 2 additions & 2 deletions

File tree

src/cdomain/value/cdomains/valueDomain.ml

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -963,7 +963,7 @@ struct
963963
begin
964964
do_eval_offset x offs l' o' (* this used to be `blob `address -> we ignore the index *)
965965
end
966-
| x when GobOption.exists (Z.equal Z.zero) (IndexDomain.to_int idx) -> eval_offset ask f x offs exp v t (* TODO: why recursive call to outer function? *)
966+
| x when IndexDomain.equal_to Z.zero idx = `Eq -> eval_offset ask f x offs exp v t (* TODO: why recursive call to outer function? *)
967967
| Top -> M.info ~category:Imprecise "Trying to read an index, but the array is unknown"; top ()
968968
| _ -> M.warn ~category:Imprecise ~tags:[Category Program] "Trying to read an index, but was not given an array (%a)" pretty x; top ()
969969
end
@@ -1150,7 +1150,7 @@ struct
11501150
let new_array_value = CArrays.update_length newl new_array_value in
11511151
Array new_array_value
11521152
| Top -> M.warn ~category:Imprecise "Trying to update an index, but the array is unknown"; top ()
1153-
| x when GobOption.exists (Z.equal Z.zero) (IndexDomain.to_int idx) -> do_update_offset x offs l' o'
1153+
| x when IndexDomain.equal_to Z.zero idx = `Eq -> do_update_offset x offs l' o'
11541154
| _ -> M.warn ~category:Imprecise "Trying to update an index, but was not given an array(%a)" pretty x; top ()
11551155
end
11561156
in mu result

0 commit comments

Comments
 (0)