File tree Expand file tree Collapse file tree 3 files changed +6
-3
lines changed Expand file tree Collapse file tree 3 files changed +6
-3
lines changed Original file line number Diff line number Diff line change @@ -3858,7 +3858,7 @@ StateValue GEP::toSMT(State &s) const {
38583858
38593859 // try to simplify the pointer
38603860 if (all_zeros.isFalse ())
3861- ptr.inbounds ();
3861+ ptr.inbounds (true );
38623862 }
38633863
38643864 return { std::move (ptr).release (), non_poison () };
Original file line number Diff line number Diff line change @@ -332,7 +332,10 @@ expr Pointer::isInbounds(bool strict) const {
332332 return (strict ? offset.ult (size) : offset.ule (size)) && !offset.isNegative ();
333333}
334334
335- expr Pointer::inbounds () {
335+ expr Pointer::inbounds (bool simplify_ptr) {
336+ if (!simplify_ptr)
337+ return isInbounds (false );
338+
336339 DisjointExpr<expr> ret (expr (false )), all_ptrs;
337340 for (auto &[ptr_expr, domain] : DisjointExpr<expr>(p, 3 )) {
338341 expr inb = Pointer (m, ptr_expr).isInbounds (false );
Original file line number Diff line number Diff line change @@ -95,7 +95,7 @@ class Pointer {
9595 smt::expr isInboundsOf (const Pointer &block, const smt::expr &bytes) const ;
9696 smt::expr isInboundsOf (const Pointer &block, unsigned bytes) const ;
9797 smt::expr isInbounds (bool strict) const ;
98- smt::expr inbounds ();
98+ smt::expr inbounds (bool simplify_ptr = false );
9999
100100 smt::expr blockAlignment () const ; // log(bits)
101101 smt::expr isBlockAligned (uint64_t align, bool exact = false ) const ;
You can’t perform that action at this time.
0 commit comments