Function at_least_same_offseting

ir/pointer.cpp:774–796

}

static expr at_least_same_offseting(const Pointer &p1, const Pointer &p2,
                                    bool any_stack) {
  expr size  = p1.blockSizeOffsetT();
  expr off   = p1.getOffsetSizet();
  expr size2 = p2.blockSizeOffsetT();
  expr off2  = p2.getOffsetSizet();
  return
    expr::mkIf(p1.isHeapAllocated(),
               p1.getAllocType() == p2.getAllocType() &&
                 off == off2 && size == size2,

               any_stack
                 ? expr(true)
                 :expr::mkIf(off.sge(0),
                             off2.sge(0) &&
                               expr::mkIf(off.ule(size),
                                          off2.ule(size2) && off2.uge(off) &&
                                            (size2 - off2).uge(size - off),
                                          off2.ugt(size2) && off == off2 &&
                                            size2.uge(size)),
                             // maintains same dereferenceability before/after
                             off == off2 && size2.uge(size)));
}

expr Pointer::refined(const Pointer &other) const {
  bool is_asm = other.m.isAsmMode();