diff --git a/src/analyses/base.ml b/src/analyses/base.ml index d248fe08b6..1f6e37f1ef 100644 --- a/src/analyses/base.ml +++ b/src/analyses/base.ml @@ -310,7 +310,7 @@ struct let n = ID.neg (ID.cast_to (Cilfacade.ptrdiff_ikind ()) n) in Address (AD.map (addToAddr n) p) | Mod -> Int (ID.top_of (Cilfacade.ptrdiff_ikind ())) (* we assume that address is actually casted to int first*) - | _ -> Address (AD.top_ptr ()) + | _ -> Address (AD.top_ptr Unknown) in (* The main function! *) match a1,a2 with @@ -2300,8 +2300,8 @@ struct | Address a -> a (* TODO: don't we already have logic for this? *) | Int i when ID.to_int i = Some BI.zero -> AD.null_ptr - | Int i -> AD.top_ptr () - | _ -> AD.top_ptr () (* TODO: why does this ever happen? *) + | Int i -> AD.top_ptr Unknown + | _ -> AD.top_ptr Unknown (* TODO: why does this ever happen? *) in let p_addr' = AD.remove NullPtr p_addr in (* realloc with NULL is same as malloc, remove to avoid unknown value from NullPtr access *) let p_addr_get = get ask gs st p_addr' None in (* implicitly includes join of malloc value (VD.bot) *) diff --git a/src/cdomains/addressDomain.ml b/src/cdomains/addressDomain.ml index 9b4237652c..894f9add9a 100644 --- a/src/cdomains/addressDomain.ml +++ b/src/cdomains/addressDomain.ml @@ -271,7 +271,7 @@ struct let null_ptr = singleton Addr.NullPtr let unknown_ptr = singleton (Addr.UnknownPtr {node = None; kind = Unknown}) let not_null = unknown_ptr - let top_ptr () = of_list Addr.[UnknownPtr {node = !Node.current_node; kind = Unknown}; NullPtr] + let top_ptr kind = of_list Addr.[UnknownPtr {node = !Node.current_node; kind = kind}; NullPtr] let is_element a x = cardinal x = 1 && Addr.equal (choose x) a let is_null x = is_element Addr.NullPtr x @@ -289,7 +289,7 @@ struct | x when GobOption.exists BigIntOps.(equal (one)) x -> not_null | _ -> match ID.to_excl_list i with | Some (xs, _) when List.exists BigIntOps.(equal (zero)) xs -> not_null - | _ -> top_ptr () + | _ -> top_ptr Unknown let to_int x = let ik = Cilfacade.ptr_ikind () in @@ -344,7 +344,7 @@ struct (* if any of the input address sets contains an element that isn't a StrPtr, return top *) if List.mem None haystack' || List.mem None needle' then - top_ptr () + top_ptr Unknown else (* else try to find the first occurrence of all strings in needle' in all strings s of haystack', collect s starting from that occurrence or if there is none, collect a NULL pointer, @@ -428,7 +428,7 @@ struct *) let is_top = may_be_unknown - let top () = top_ptr () + let top () = top_ptr Unknown let merge uop cop x y = let no_null x y = diff --git a/src/cdomains/addressDomain_intf.ml b/src/cdomains/addressDomain_intf.ml index 71f5b713c2..8a26c74141 100644 --- a/src/cdomains/addressDomain_intf.ml +++ b/src/cdomains/addressDomain_intf.ml @@ -127,7 +127,7 @@ sig val not_null: t (** Address set containing the unknown pointer, which is non-[NULL]. *) - val top_ptr: unit -> t + val top_ptr: unknownKind -> t (** Address set containing any pointer, [NULL] or not. *) val is_null: t -> bool diff --git a/src/cdomains/valueDomain.ml b/src/cdomains/valueDomain.ml index 1341070ede..a551241214 100644 --- a/src/cdomains/valueDomain.ml +++ b/src/cdomains/valueDomain.ml @@ -175,7 +175,7 @@ struct | t when is_mutexattr_type t -> MutexAttr (MutexAttrDomain.top ()) | TInt (ik,_) -> Int (ID.top_of ik) | TFloat (fkind, _) when not (Cilfacade.isComplexFKind fkind) -> Float (FD.top_of fkind) - | TPtr _ -> Address (AD.top_ptr ()) + | TPtr _ -> Address (AD.top_ptr Unknown) | TComp ({cstruct=true; _} as ci,_) -> Struct (Structs.create (fun fd -> init_value ~varAttr:fd.fattr fd.ftype) ci) | TComp ({cstruct=false; _},_) -> Union (Unions.top ()) | TArray (ai, length, _) -> @@ -194,7 +194,7 @@ struct | t when is_mutexattr_type t -> MutexAttr (MutexAttrDomain.top ()) | TInt (ik,_) -> Int (ID.(cast_to ik (top_of ik))) | TFloat (fkind, _) when not (Cilfacade.isComplexFKind fkind) -> Float (FD.top_of fkind) - | TPtr _ -> Address (AD.top_ptr ()) + | TPtr _ -> Address (AD.top_ptr Unknown) | TComp ({cstruct=true; _} as ci,_) -> Struct (Structs.create (fun fd -> top_value ~varAttr:fd.fattr fd.ftype) ci) | TComp ({cstruct=false; _},_) -> Union (Unions.top ()) | TArray (ai, length, _) -> @@ -454,11 +454,11 @@ struct | TPtr (t,_) -> Address (match v with | Int x when ID.to_int x = Some BI.zero -> AD.null_ptr - | Int x -> AD.top_ptr () + | Int x -> AD.top_ptr Unknown (* we ignore casts to void*! TODO report UB! *) | Address x -> (match t with TVoid _ -> x | _ -> cast_addr t x) (*| Address x -> x*) - | _ -> log_top __POS__; AD.top_ptr () + | _ -> log_top __POS__; AD.top_ptr Unknown ) | TArray (ta, l, _) -> (* TODO, why is the length exp option? *) (* TODO handle casts between different sizes? *) @@ -542,7 +542,7 @@ struct | (Address y, Int x) -> Address (match ID.to_int x with | Some x when BI.equal x BI.zero -> AD.join AD.null_ptr y | Some x -> AD.(join y not_null) - | None -> AD.join y (AD.top_ptr ())) + | None -> AD.join y (AD.top_ptr Unknown)) | (Address x, Address y) -> Address (AD.join x y) | (Struct x, Struct y) -> Struct (Structs.join x y) | (Union x, Union y) -> Union (Unions.join x y) @@ -577,7 +577,7 @@ struct | (Address y, Int x) -> Address (match ID.to_int x with | Some x when BI.equal x BI.zero -> AD.widen AD.null_ptr (AD.join AD.null_ptr y) | Some x -> AD.(widen y (join y not_null)) - | None -> AD.widen y (AD.join y (AD.top_ptr ()))) + | None -> AD.widen y (AD.join y (AD.top_ptr Unknown))) | (Address x, Address y) -> Address (AD.widen x y) | (Struct x, Struct y) -> Struct (Structs.widen x y) | (Union x, Union y) -> Union (Unions.widen x y) @@ -697,7 +697,7 @@ struct in let array_idx_top = (None, ArrIdxDomain.top ()) in match typ, state with - | _ , Address n -> Address (AD.join (AD.top_ptr ()) n) + | _ , Address n -> Address (AD.join (AD.top_ptr Unknown) n) | TComp (ci,_) , Struct n -> Struct (invalid_struct ci n) | _ , Struct n -> Struct (Structs.map (fun x -> invalidate_value ask voidType x) n) | TComp (ci,_) , Union (`Lifted fd,n) -> Union (`Lifted fd, invalidate_value ask fd.ftype n)