optimize -disable-undef/poison-input expressions
MODIFY
ir/value.cpp
ir/value.cpp
@@ -83,15 +83,22 @@ StateValue Input::toSMT(State &s) const {
expr type = getTyVar();
auto bw = bits();
+ expr val;
+ if (config::disable_undef_input) {
+ val = expr::mkVar(getName().c_str(), bw);
+ } else {
string uname = UndefValue::getFreshName();
expr undef = expr::mkVar(uname.c_str(), bw);
- if (!config::disable_undef_input)
s.addUndefVar(undef);
-
- return { expr::mkIf(type == expr::mkUInt(0, 2),
+ val = expr::mkIf(type == expr::mkUInt(0, 2),
expr::mkVar(getName().c_str(), bw),
- move(undef)),
- type.extract(1,1) == expr::mkUInt(0, 1) };
+ move(undef));
+ }
+
+ return { move(val),
+ config::disable_poison_input
+ ? true
+ : type.extract(1,1) == expr::mkUInt(0, 1) };
}
expr Input::getTyVar() const {

optimize -disable-undef/poison-input expressions