llvm2alive: skip atomic load/store
MODIFY
ir/value.cpp
ir/value.cpp
@@ -78,8 +78,8 @@ StateValue NullPointerValue::toSMT(State &s) const {
void GlobalVariable::print(ostream &os) const {
- os << getName() << " = " << (isconst ? "constant " : "global ") << getType()
- << ", align " << align;
+ os << getName() << " = " << (isconst ? "constant " : "global ") << allocsize
+ << " bytes, align " << align;
}
StateValue GlobalVariable::toSMT(State &s) const {

MODIFY
llvm_util/llvm2alive.cpp
llvm_util/llvm2alive.cpp
@@ -386,6 +386,8 @@ public:
RetTy visitLoadInst(llvm::LoadInst &i) {
// TODO: Add support for isVolatile(), getOrdering()
+ if (!i.isSimple())
+ return error(i);
PARSE_UNOP();
RETURN_IDENTIFIER(make_unique<Load>(*ty, value_name(i), *val,
alignment(i, i.getType())));
@@ -393,6 +395,8 @@ public:
RetTy visitStoreInst(llvm::StoreInst &i) {
// TODO: Add support for isVolatile(), getOrdering()
+ if (!i.isSimple())
+ return error(i);
auto val = get_operand(i.getValueOperand());
auto ptr = get_operand(i.getPointerOperand());
if (!val || !ptr)

llvm2alive: skip atomic load/store