Skip to content

Commit 1510a23

Browse files
committed
Revert "128 bit fix"
This reverts commit e16deb7.
1 parent f492437 commit 1510a23

File tree

2 files changed

+0
-22
lines changed

2 files changed

+0
-22
lines changed

lib/smack/Prelude.cpp

-16
Original file line numberDiff line numberDiff line change
@@ -1064,7 +1064,6 @@ void TypeDeclGen::generate(std::stringstream &s) const {
10641064
s << Decl::typee(Naming::FLOAT_TYPE, "float24e8") << "\n";
10651065
s << Decl::typee(Naming::DOUBLE_TYPE, "float53e11") << "\n";
10661066
s << Decl::typee(Naming::LONG_DOUBLE_TYPE, "float65e15") << "\n";
1067-
s << Decl::typee(Naming::UNINTERPRETED_FLOAT_TYPE, "") << "\n";
10681067
} else {
10691068
s << Decl::typee(Naming::UNINTERPRETED_FLOAT_TYPE, "") << "\n";
10701069
}
@@ -1585,21 +1584,6 @@ void FpOpGen::generateConvOps(std::stringstream &s) const {
15851584
desType)
15861585
<< "\n";
15871586
}
1588-
// Conversion between bv-floating types and float
1589-
for (auto bw : FP_BIT_WIDTHS) {
1590-
for (auto name : {"$fpext", "$fptrunc"}) {
1591-
auto exp = FP_LAYOUT.at(bw).first;
1592-
auto sig = FP_LAYOUT.at(bw).second;
1593-
std::string type = getFpTypeName(bw);
1594-
std::list<Binding> bs = makeFpVars(1, srcBw);
1595-
1596-
bs.insert(bs.begin(), {makeRMODEVarName(), getRMODETypeName()});
1597-
s << uninterpretedOp("$fpext", {type, "float"}, bs, "float") << "\n";
1598-
s << uninterpretedOp("$fptrunc", {type, "float"}, bs, "float") << "\n";
1599-
s << uninterpretedOp("$fpext", {"float", type}, bs, type) << "\n";
1600-
s << uninterpretedOp("$fptrunc", {"float", type}, bs, type) << "\n";
1601-
}
1602-
}
16031587
}
16041588

16051589
struct FpOpGen::FpIntConv {

lib/smack/SmackRep.cpp

-6
Original file line numberDiff line numberDiff line change
@@ -226,12 +226,6 @@ std::string SmackRep::type(const llvm::Type *t) {
226226
return Naming::DOUBLE_TYPE;
227227
else if (t->isX86_FP80Ty())
228228
return Naming::LONG_DOUBLE_TYPE;
229-
else if (t->isFP128Ty())
230-
return Naming::UNINTERPRETED_FLOAT_TYPE;
231-
else if (t->isPPC_FP128Ty())
232-
return Naming::UNINTERPRETED_FLOAT_TYPE;
233-
else if (t->isBFloatTy())
234-
return Naming::UNINTERPRETED_FLOAT_TYPE;
235229
else
236230
llvm_unreachable("Unsupported floating-point type.");
237231
}

0 commit comments

Comments
 (0)