Currently the meet of an unknown string pointer and a known string pointer is the unknown string pointer.
{"string"} \sqcap {(unknown string)} = {(unknown string)}
The problem seems to be in the address domain, as the actual meet in the string domain which is defined to return the known pointer
|
let meet x y = |
|
match x, y with |
|
| None, a |
|
| a, None -> a |
|
| Some a, Some b when a = b -> Some a |
|
| Some a, Some b (* when a <> b *) -> |
|
if get_string_domain () = Disjoint then |
|
raise Lattice.Uncomparable |
|
else |
|
raise Lattice.BotValue |
is never actually called.
Currently the meet of an unknown string pointer and a known string pointer is the unknown string pointer.
The problem seems to be in the address domain, as the actual meet in the string domain which is defined to return the known pointer
analyzer/src/cdomain/value/cdomains/stringDomain.ml
Lines 99 to 108 in bffc5e3
is never actually called.