@@ -2720,15 +2720,23 @@ void Assume::rauw(const Value &what, Value &with) {
27202720}
27212721
27222722void Assume::print (ostream &os) const {
2723+ const char *str = nullptr ;
27232724 switch (kind) {
2724- case AndNonPoison: os << " assume" ; break ;
2725- case IfNonPoison: os << " assume_non_poison" ; break ;
2726- case WellDefined: os << " assume_welldefined" ; break ;
2727- case Align: os << " assume_align" ; break ;
2728- case NonNull: os << " assume_nonnull" ; break ;
2725+ case AndNonPoison: str = " assume " ; break ;
2726+ case IfNonPoison: str = " assume_non_poison " ; break ;
2727+ case WellDefined: str = " assume_welldefined " ; break ;
2728+ case Align: str = " assume_align " ; break ;
2729+ case NonNull: str = " assume_nonnull " ; break ;
2730+ }
2731+ os << str;
2732+
2733+ bool first = true ;
2734+ for (auto &arg: args) {
2735+ if (!first)
2736+ os << " , " ;
2737+ os << *arg;
2738+ first = false ;
27292739 }
2730- for (auto &arg: args)
2731- os << ' ' << *arg;
27322740}
27332741
27342742StateValue Assume::toSMT (State &s) const {
@@ -2749,10 +2757,13 @@ StateValue Assume::toSMT(State &s) const {
27492757 case Align: {
27502758 // assume(ptr, align)
27512759 const auto &vptr = s.getAndAddPoisonUB (*args[0 ]);
2752- uint64_t align = *dynamic_cast <IntConst *>(args[1 ])->getInt ();
2753-
2754- Pointer ptr (s.getMemory (), vptr.value );
2755- s.addUB (ptr.isAligned (align));
2760+ if (auto align = dynamic_cast <IntConst *>(args[1 ])) {
2761+ Pointer ptr (s.getMemory (), vptr.value );
2762+ s.addUB (ptr.isAligned ((uint64_t )align->getInt ()));
2763+ } else {
2764+ // TODO: add support for non-constant align
2765+ s.addUB (expr ());
2766+ }
27562767 break ;
27572768 }
27582769 case NonNull: {
0 commit comments