Skip to content

Commit 7881999

Browse files
committed
Reuse AD.of_int where possible
1 parent a023008 commit 7881999

File tree

2 files changed

+4
-17
lines changed

2 files changed

+4
-17
lines changed

src/analyses/base.ml

Lines changed: 2 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -322,12 +322,7 @@ struct
322322
in
323323
match addr with
324324
| Addr (x, o) -> AD.of_mval (x, addToOffset n (Some x.vtype) o)
325-
| NullPtr ->
326-
begin match ID.equal_to Z.zero n with
327-
| `Eq -> AD.null_ptr
328-
| `Neq -> AD.unknown_ptr
329-
| `Top -> AD.top_ptr
330-
end
325+
| NullPtr -> AD.of_int n
331326
| UnknownPtr
332327
| StrPtr _ ->
333328
begin match ID.equal_to Z.zero n with
@@ -2780,9 +2775,7 @@ struct
27802775
let p_addr =
27812776
match p_rv with
27822777
| Address a -> a
2783-
(* TODO: don't we already have logic for this? *)
2784-
| Int i when ID.equal_to Z.zero i = `Eq -> AD.null_ptr
2785-
| Int i -> AD.top_ptr
2778+
| Int i -> AD.of_int i
27862779
| _ -> AD.top_ptr (* TODO: why does this ever happen? *)
27872780
in
27882781
let p_addr' = AD.remove NullPtr p_addr in (* realloc with NULL is same as malloc, remove to avoid unknown value from NullPtr access *)

src/cdomain/value/cdomains/valueDomain.ml

Lines changed: 2 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -612,10 +612,7 @@ struct
612612
| (Int x, Int y) -> (try Int (ID.join x y) with IntDomain.IncompatibleIKinds m -> Messages.warn ~category:Analyzer ~tags:[Category Imprecise] "%s" m; Top)
613613
| (Float x, Float y) -> Float (FD.join x y)
614614
| (Int x, Address y)
615-
| (Address y, Int x) -> Address (match ID.equal_to Z.zero x with (* TODO: AD.of_int? *)
616-
| `Eq -> AD.join AD.null_ptr y
617-
| `Neq -> AD.(join y not_null)
618-
| `Top -> AD.join y AD.top_ptr)
615+
| (Address y, Int x) -> Address (AD.join y (AD.of_int x))
619616
| (Address x, Address y) -> Address (AD.join x y)
620617
| (Struct x, Struct y) -> Struct (Structs.join x y)
621618
| (Union x, Union y) -> Union (Unions.join x y)
@@ -645,10 +642,7 @@ struct
645642
| (Float x, Float y) -> Float (FD.widen x y)
646643
(* TODO: symmetric widen, wtf? *)
647644
| (Int x, Address y)
648-
| (Address y, Int x) -> Address (match ID.equal_to Z.zero x with (* TODO: AD.of_int? *)
649-
| `Eq -> AD.widen AD.null_ptr (AD.join AD.null_ptr y)
650-
| `Neq -> AD.(widen y (join y not_null))
651-
| `Top -> AD.widen y (AD.join y AD.top_ptr))
645+
| (Address y, Int x) -> Address (AD.widen y (AD.join y (AD.of_int x)))
652646
| (Address x, Address y) -> Address (AD.widen x y)
653647
| (Struct x, Struct y) -> Struct (Structs.widen x y)
654648
| (Union x, Union y) -> Union (Unions.widen x y)

0 commit comments

Comments
 (0)