[cfe-dev] [analyzer] Do we have implicit assumptions on extents of memory regions?

[Balázs Benics via cfe-dev]

Is it reasonable to assume in the analyzer that a symbol representing the
extent
of an analyzed memory region can not be greater then size_t_max/2?

If so, why does the constraint manager not know about this fact?
If not, why does the `ProgramState::assumeInBound` still heavily exploit
this
fact in its implementation?

Without deciding this Z3 refutation will not be able to filter as many false
positives as it potentially could.

Regards,
Balazs
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.llvm.org/pipermail/cfe-dev/attachments/20200706/da2be6cf/attachment.html>