mirror of
https://github.com/ethereum/solidity
synced 2023-10-03 13:03:40 +00:00
Merge pull request #9670 from ethereum/smt_struct
[SMTChecker] Support structs
This commit is contained in:
Leonardo
GitHub
commit
f964966090
@ -4,6 +4,7 @@ Language Features:
|
||||
|
||||
|
||||
Compiler Features:
|
||||
* SMTChecker: Support structs.
|
||||
* Yul Optimizer: Prune unused parameters in functions.
|
||||
|
||||
Bugfixes:
|
||||
|
||||
@ -580,7 +580,7 @@ pair<vector<smtutil::Expression>, vector<string>> BMC::modelExpressions()
|
||||
auto const& type = var.second->type();
|
||||
if (
|
||||
type->isValueType() &&
|
||||
smt::smtKind(type->category()) != smtutil::Kind::Function
|
||||
smt::smtKind(*type) != smtutil::Kind::Function
|
||||
)
|
||||
{
|
||||
expressionsToEvaluate.emplace_back(var.second->currentValue());
|
||||
|
||||
@ -378,7 +378,7 @@ void SMTEncoder::endVisit(Assignment const& _assignment)
|
||||
"Assertion checker does not yet implement this assignment operator."
|
||||
);
|
||||
}
|
||||
else if (!smt::isSupportedType(_assignment.annotation().type->category()))
|
||||
else if (!smt::isSupportedType(*_assignment.annotation().type))
|
||||
{
|
||||
// Give it a new index anyway to keep the SSA scheme sound.
|
||||
|
||||
@ -403,8 +403,7 @@ void SMTEncoder::endVisit(Assignment const& _assignment)
|
||||
assignment(
|
||||
_assignment.leftHandSide(),
|
||||
expr(_assignment, type),
|
||||
type,
|
||||
_assignment.location()
|
||||
type
|
||||
);
|
||||
}
|
||||
}
|
||||
@ -463,20 +462,19 @@ void SMTEncoder::endVisit(UnaryOperation const& _op)
|
||||
createExpr(_op);
|
||||
|
||||
auto const* subExpr = innermostTuple(_op.subExpression());
|
||||
|
||||
auto type = _op.annotation().type;
|
||||
switch (_op.getOperator())
|
||||
{
|
||||
case Token::Not: // !
|
||||
{
|
||||
solAssert(smt::isBool(_op.annotation().type->category()), "");
|
||||
solAssert(smt::isBool(*type), "");
|
||||
defineExpr(_op, !expr(*subExpr));
|
||||
break;
|
||||
}
|
||||
case Token::Inc: // ++ (pre- or postfix)
|
||||
case Token::Dec: // -- (pre- or postfix)
|
||||
{
|
||||
auto cat = _op.annotation().type->category();
|
||||
solAssert(smt::isInteger(cat) || smt::isFixedPoint(cat), "");
|
||||
solAssert(smt::isInteger(*type) || smt::isFixedPoint(*type), "");
|
||||
solAssert(subExpr->annotation().willBeWrittenTo, "");
|
||||
if (auto identifier = dynamic_cast<Identifier const*>(subExpr))
|
||||
{
|
||||
@ -487,12 +485,15 @@ void SMTEncoder::endVisit(UnaryOperation const& _op)
|
||||
defineExpr(_op, _op.isPrefixOperation() ? newValue : innerValue);
|
||||
assignment(*decl, newValue);
|
||||
}
|
||||
else if (dynamic_cast<IndexAccess const*>(subExpr))
|
||||
else if (
|
||||
dynamic_cast<IndexAccess const*>(&_op.subExpression()) ||
|
||||
dynamic_cast<MemberAccess const*>(&_op.subExpression())
|
||||
)
|
||||
{
|
||||
auto innerValue = expr(*subExpr);
|
||||
auto newValue = _op.getOperator() == Token::Inc ? innerValue + 1 : innerValue - 1;
|
||||
defineExpr(_op, _op.isPrefixOperation() ? newValue : innerValue);
|
||||
arrayIndexAssignment(*subExpr, newValue);
|
||||
indexOrMemberAssignment(_op.subExpression(), newValue);
|
||||
}
|
||||
else
|
||||
m_errorReporter.warning(
|
||||
@ -521,14 +522,13 @@ void SMTEncoder::endVisit(UnaryOperation const& _op)
|
||||
auto const& symbVar = m_context.expression(*subExpr);
|
||||
symbVar->increaseIndex();
|
||||
m_context.setZeroValue(*symbVar);
|
||||
if (dynamic_cast<IndexAccess const*>(subExpr))
|
||||
arrayIndexAssignment(*subExpr, symbVar->currentValue());
|
||||
if (
|
||||
dynamic_cast<IndexAccess const*>(&_op.subExpression()) ||
|
||||
dynamic_cast<MemberAccess const*>(&_op.subExpression())
|
||||
)
|
||||
indexOrMemberAssignment(_op.subExpression(), symbVar->currentValue());
|
||||
else
|
||||
m_errorReporter.warning(
|
||||
2683_error,
|
||||
_op.location(),
|
||||
"Assertion checker does not yet implement \"delete\" for this expression."
|
||||
);
|
||||
solAssert(false, "");
|
||||
}
|
||||
break;
|
||||
}
|
||||
@ -826,11 +826,11 @@ void SMTEncoder::endVisit(Literal const& _literal)
|
||||
{
|
||||
solAssert(_literal.annotation().type, "Expected type for AST node");
|
||||
Type const& type = *_literal.annotation().type;
|
||||
if (smt::isNumber(type.category()))
|
||||
if (smt::isNumber(type))
|
||||
defineExpr(_literal, smtutil::Expression(type.literalValue(&_literal)));
|
||||
else if (smt::isBool(type.category()))
|
||||
else if (smt::isBool(type))
|
||||
defineExpr(_literal, smtutil::Expression(_literal.token() == Token::TrueLiteral ? true : false));
|
||||
else if (smt::isStringLiteral(type.category()))
|
||||
else if (smt::isStringLiteral(type))
|
||||
createExpr(_literal);
|
||||
else
|
||||
{
|
||||
@ -893,6 +893,13 @@ bool SMTEncoder::visit(MemberAccess const& _memberAccess)
|
||||
defineGlobalVariable(accessedName + "." + _memberAccess.memberName(), _memberAccess);
|
||||
return false;
|
||||
}
|
||||
else if (smt::isNonRecursiveStruct(*exprType))
|
||||
{
|
||||
_memberAccess.expression().accept(*this);
|
||||
auto const& symbStruct = dynamic_pointer_cast<smt::SymbolicStructVariable>(m_context.expression(_memberAccess.expression()));
|
||||
defineExpr(_memberAccess, symbStruct->member(_memberAccess.memberName()));
|
||||
return false;
|
||||
}
|
||||
else if (exprType->category() == Type::Category::TypeType)
|
||||
{
|
||||
if (identifier && dynamic_cast<EnumDefinition const*>(identifier->annotation().referencedDeclaration))
|
||||
@ -964,19 +971,10 @@ void SMTEncoder::endVisit(IndexAccess const& _indexAccess)
|
||||
solAssert(varDecl, "");
|
||||
array = m_context.variable(*varDecl);
|
||||
}
|
||||
else if (auto const* innerAccess = dynamic_cast<IndexAccess const*>(&_indexAccess.baseExpression()))
|
||||
{
|
||||
solAssert(m_context.knownExpression(*innerAccess), "");
|
||||
array = m_context.expression(*innerAccess);
|
||||
}
|
||||
else
|
||||
{
|
||||
m_errorReporter.warning(
|
||||
9118_error,
|
||||
_indexAccess.location(),
|
||||
"Assertion checker does not yet implement this expression."
|
||||
);
|
||||
return;
|
||||
solAssert(m_context.knownExpression(_indexAccess.baseExpression()), "");
|
||||
array = m_context.expression(_indexAccess.baseExpression());
|
||||
}
|
||||
|
||||
auto arrayVar = dynamic_pointer_cast<smt::SymbolicArrayVariable>(array);
|
||||
@ -1008,14 +1006,58 @@ void SMTEncoder::arrayAssignment()
|
||||
m_arrayAssignmentHappened = true;
|
||||
}
|
||||
|
||||
void SMTEncoder::arrayIndexAssignment(Expression const& _expr, smtutil::Expression const& _rightHandSide)
|
||||
void SMTEncoder::indexOrMemberAssignment(Expression const& _expr, smtutil::Expression const& _rightHandSide)
|
||||
{
|
||||
auto toStore = _rightHandSide;
|
||||
auto indexAccess = dynamic_cast<IndexAccess const*>(&_expr);
|
||||
solAssert(indexAccess, "");
|
||||
auto const* lastExpr = &_expr;
|
||||
while (true)
|
||||
{
|
||||
if (auto const& id = dynamic_cast<Identifier const*>(&indexAccess->baseExpression()))
|
||||
if (auto const* indexAccess = dynamic_cast<IndexAccess const*>(lastExpr))
|
||||
{
|
||||
auto const& base = indexAccess->baseExpression();
|
||||
if (dynamic_cast<Identifier const*>(&base))
|
||||
base.accept(*this);
|
||||
auto symbArray = dynamic_pointer_cast<smt::SymbolicArrayVariable>(m_context.expression(base));
|
||||
solAssert(symbArray, "");
|
||||
auto baseType = symbArray->type();
|
||||
toStore = smtutil::Expression::tuple_constructor(
|
||||
smtutil::Expression(make_shared<smtutil::SortSort>(smt::smtSort(*baseType)), baseType->toString(true)),
|
||||
{smtutil::Expression::store(symbArray->elements(), expr(*indexAccess->indexExpression()), toStore), symbArray->length()}
|
||||
);
|
||||
m_context.expression(*indexAccess)->increaseIndex();
|
||||
defineExpr(*indexAccess, smtutil::Expression::select(
|
||||
symbArray->elements(),
|
||||
expr(*indexAccess->indexExpression())
|
||||
));
|
||||
lastExpr = &indexAccess->baseExpression();
|
||||
}
|
||||
else if (auto const* memberAccess = dynamic_cast<MemberAccess const*>(lastExpr))
|
||||
{
|
||||
auto const& base = memberAccess->expression();
|
||||
if (dynamic_cast<Identifier const*>(&base))
|
||||
base.accept(*this);
|
||||
|
||||
if (
|
||||
auto const* structType = dynamic_cast<StructType const*>(base.annotation().type);
|
||||
structType && structType->recursive()
|
||||
)
|
||||
{
|
||||
m_errorReporter.warning(
|
||||
4375_error,
|
||||
memberAccess->location(),
|
||||
"Assertion checker does not support recursive structs."
|
||||
);
|
||||
return;
|
||||
}
|
||||
|
||||
auto symbStruct = dynamic_pointer_cast<smt::SymbolicStructVariable>(m_context.expression(base));
|
||||
solAssert(symbStruct, "");
|
||||
symbStruct->assignMember(memberAccess->memberName(), toStore);
|
||||
toStore = symbStruct->currentValue();
|
||||
defineExpr(*memberAccess, symbStruct->member(memberAccess->memberName()));
|
||||
lastExpr = &memberAccess->expression();
|
||||
}
|
||||
else if (auto const& id = dynamic_cast<Identifier const*>(lastExpr))
|
||||
{
|
||||
auto varDecl = identifierToVariable(*id);
|
||||
solAssert(varDecl, "");
|
||||
@ -1023,43 +1065,22 @@ void SMTEncoder::arrayIndexAssignment(Expression const& _expr, smtutil::Expressi
|
||||
if (varDecl->hasReferenceOrMappingType())
|
||||
resetReferences(*varDecl);
|
||||
|
||||
auto symbArray = dynamic_pointer_cast<smt::SymbolicArrayVariable>(m_context.variable(*varDecl));
|
||||
smtutil::Expression store = smtutil::Expression::store(
|
||||
symbArray->elements(),
|
||||
expr(*indexAccess->indexExpression()),
|
||||
toStore
|
||||
);
|
||||
auto oldLength = symbArray->length();
|
||||
symbArray->increaseIndex();
|
||||
m_context.addAssertion(symbArray->elements() == store);
|
||||
m_context.addAssertion(symbArray->length() == oldLength);
|
||||
// Update the SMT select value after the assignment,
|
||||
// necessary for sound models.
|
||||
defineExpr(*indexAccess, smtutil::Expression::select(
|
||||
symbArray->elements(),
|
||||
expr(*indexAccess->indexExpression())
|
||||
));
|
||||
|
||||
m_context.addAssertion(m_context.newValue(*varDecl) == toStore);
|
||||
m_context.expression(*id)->increaseIndex();
|
||||
defineExpr(*id,currentValue(*varDecl));
|
||||
break;
|
||||
}
|
||||
else if (auto base = dynamic_cast<IndexAccess const*>(&indexAccess->baseExpression()))
|
||||
{
|
||||
auto symbArray = dynamic_pointer_cast<smt::SymbolicArrayVariable>(m_context.expression(*base));
|
||||
solAssert(symbArray, "");
|
||||
auto baseType = base->annotation().type;
|
||||
toStore = smtutil::Expression::tuple_constructor(
|
||||
smtutil::Expression(make_shared<smtutil::SortSort>(smt::smtSort(*baseType)), baseType->toString(true)),
|
||||
{smtutil::Expression::store(symbArray->elements(), expr(*indexAccess->indexExpression()), toStore), symbArray->length()}
|
||||
);
|
||||
indexAccess = base;
|
||||
}
|
||||
else
|
||||
{
|
||||
m_errorReporter.warning(
|
||||
9056_error,
|
||||
_expr.location(),
|
||||
"Assertion checker does not yet implement this expression."
|
||||
);
|
||||
auto type = lastExpr->annotation().type;
|
||||
if (
|
||||
dynamic_cast<ReferenceType const*>(type) ||
|
||||
dynamic_cast<MappingType const*>(type)
|
||||
)
|
||||
resetReferences(type);
|
||||
|
||||
m_context.expression(*lastExpr)->increaseIndex();
|
||||
m_context.addAssertion(expr(*lastExpr) == toStore);
|
||||
break;
|
||||
}
|
||||
}
|
||||
@ -1131,9 +1152,14 @@ void SMTEncoder::arrayPushPopAssign(Expression const& _expr, smtutil::Expression
|
||||
if (varDecl->hasReferenceOrMappingType())
|
||||
resetReferences(*varDecl);
|
||||
m_context.addAssertion(m_context.newValue(*varDecl) == _array);
|
||||
m_context.expression(*id)->increaseIndex();
|
||||
defineExpr(*id,currentValue(*varDecl));
|
||||
}
|
||||
else if (auto const* indexAccess = dynamic_cast<IndexAccess const*>(expr))
|
||||
arrayIndexAssignment(*indexAccess, _array);
|
||||
else if (
|
||||
dynamic_cast<IndexAccess const*>(expr) ||
|
||||
dynamic_cast<MemberAccess const*>(expr)
|
||||
)
|
||||
indexOrMemberAssignment(_expr, _array);
|
||||
else if (auto const* funCall = dynamic_cast<FunctionCall const*>(expr))
|
||||
{
|
||||
FunctionType const& funType = dynamic_cast<FunctionType const&>(*funCall->expression().annotation().type);
|
||||
@ -1156,12 +1182,6 @@ void SMTEncoder::arrayPushPopAssign(Expression const& _expr, smtutil::Expression
|
||||
arrayPushPopAssign(memberAccess->expression(), symbArray->currentValue());
|
||||
}
|
||||
}
|
||||
else if (dynamic_cast<MemberAccess const*>(expr))
|
||||
m_errorReporter.warning(
|
||||
9599_error,
|
||||
_expr.location(),
|
||||
"Assertion checker does not yet implement this expression."
|
||||
);
|
||||
else
|
||||
solAssert(false, "");
|
||||
}
|
||||
@ -1182,7 +1202,7 @@ void SMTEncoder::defineGlobalVariable(string const& _name, Expression const& _ex
|
||||
m_context.globalSymbol(_name)->increaseIndex();
|
||||
// The default behavior is not to increase the index since
|
||||
// most of the global values stay the same throughout a tx.
|
||||
if (smt::isSupportedType(_expr.annotation().type->category()))
|
||||
if (smt::isSupportedType(*_expr.annotation().type))
|
||||
defineExpr(_expr, m_context.globalSymbol(_name)->currentValue());
|
||||
}
|
||||
|
||||
@ -1335,13 +1355,13 @@ void SMTEncoder::compareOperation(BinaryOperation const& _op)
|
||||
{
|
||||
auto const& commonType = _op.annotation().commonType;
|
||||
solAssert(commonType, "");
|
||||
if (smt::isSupportedType(commonType->category()))
|
||||
if (smt::isSupportedType(*commonType))
|
||||
{
|
||||
smtutil::Expression left(expr(_op.leftExpression(), commonType));
|
||||
smtutil::Expression right(expr(_op.rightExpression(), commonType));
|
||||
Token op = _op.getOperator();
|
||||
shared_ptr<smtutil::Expression> value;
|
||||
if (smt::isNumber(commonType->category()))
|
||||
if (smt::isNumber(*commonType))
|
||||
{
|
||||
value = make_shared<smtutil::Expression>(
|
||||
op == Token::Equal ? (left == right) :
|
||||
@ -1354,7 +1374,7 @@ void SMTEncoder::compareOperation(BinaryOperation const& _op)
|
||||
}
|
||||
else // Bool
|
||||
{
|
||||
solUnimplementedAssert(smt::isBool(commonType->category()), "Operation not yet supported");
|
||||
solUnimplementedAssert(smt::isBool(*commonType), "Operation not yet supported");
|
||||
value = make_shared<smtutil::Expression>(
|
||||
op == Token::Equal ? (left == right) :
|
||||
/*op == Token::NotEqual*/ (left != right)
|
||||
@ -1450,8 +1470,7 @@ smtutil::Expression SMTEncoder::division(smtutil::Expression _left, smtutil::Exp
|
||||
void SMTEncoder::assignment(
|
||||
Expression const& _left,
|
||||
smtutil::Expression const& _right,
|
||||
TypePointer const& _type,
|
||||
langutil::SourceLocation const& _location
|
||||
TypePointer const& _type
|
||||
)
|
||||
{
|
||||
solAssert(
|
||||
@ -1461,28 +1480,21 @@ void SMTEncoder::assignment(
|
||||
|
||||
Expression const* left = innermostTuple(_left);
|
||||
|
||||
if (!smt::isSupportedType(_type->category()))
|
||||
if (!smt::isSupportedType(*_type))
|
||||
{
|
||||
// Give it a new index anyway to keep the SSA scheme sound.
|
||||
if (auto varDecl = identifierToVariable(*left))
|
||||
m_context.newValue(*varDecl);
|
||||
|
||||
m_errorReporter.warning(
|
||||
6191_error,
|
||||
_location,
|
||||
"Assertion checker does not yet implement type " + _type->toString()
|
||||
);
|
||||
}
|
||||
else if (auto varDecl = identifierToVariable(*left))
|
||||
assignment(*varDecl, _right);
|
||||
else if (dynamic_cast<IndexAccess const*>(left))
|
||||
arrayIndexAssignment(*left, _right);
|
||||
else if (
|
||||
dynamic_cast<IndexAccess const*>(left) ||
|
||||
dynamic_cast<MemberAccess const*>(left)
|
||||
)
|
||||
indexOrMemberAssignment(*left, _right);
|
||||
else
|
||||
m_errorReporter.warning(
|
||||
8182_error,
|
||||
_location,
|
||||
"Assertion checker does not yet implement such assignments."
|
||||
);
|
||||
solAssert(false, "");
|
||||
}
|
||||
|
||||
void SMTEncoder::tupleAssignment(Expression const& _left, Expression const& _right)
|
||||
@ -1511,7 +1523,7 @@ void SMTEncoder::tupleAssignment(Expression const& _left, Expression const& _rig
|
||||
else
|
||||
{
|
||||
auto type = lExpr.annotation().type;
|
||||
assignment(lExpr, expr(rExpr, type), type, lExpr.location());
|
||||
assignment(lExpr, expr(rExpr, type), type);
|
||||
}
|
||||
}
|
||||
}
|
||||
@ -1528,7 +1540,7 @@ void SMTEncoder::tupleAssignment(Expression const& _left, Expression const& _rig
|
||||
|
||||
for (unsigned i = 0; i < lComponents.size(); ++i)
|
||||
if (auto component = lComponents.at(i); component && rComponents.at(i))
|
||||
assignment(*component, smtutil::Expression::tuple_get(symbRight, i), component->annotation().type, component->location());
|
||||
assignment(*component, smtutil::Expression::tuple_get(symbRight, i), component->annotation().type);
|
||||
}
|
||||
}
|
||||
|
||||
@ -1692,32 +1704,43 @@ void SMTEncoder::resetReferences(VariableDeclaration const& _varDecl)
|
||||
if (_var.isStateVariable() && _varDecl.isStateVariable())
|
||||
return false;
|
||||
|
||||
TypePointer prefix = _var.type();
|
||||
TypePointer originalType = typeWithoutPointer(_varDecl.type());
|
||||
while (
|
||||
prefix->category() == Type::Category::Mapping ||
|
||||
prefix->category() == Type::Category::Array
|
||||
)
|
||||
{
|
||||
if (*originalType == *typeWithoutPointer(prefix))
|
||||
return true;
|
||||
if (prefix->category() == Type::Category::Mapping)
|
||||
{
|
||||
auto mapPrefix = dynamic_cast<MappingType const*>(prefix);
|
||||
solAssert(mapPrefix, "");
|
||||
prefix = mapPrefix->valueType();
|
||||
}
|
||||
else
|
||||
{
|
||||
auto arrayPrefix = dynamic_cast<ArrayType const*>(prefix);
|
||||
solAssert(arrayPrefix, "");
|
||||
prefix = arrayPrefix->baseType();
|
||||
}
|
||||
}
|
||||
return false;
|
||||
return sameTypeOrSubtype(_var.type(), _varDecl.type());
|
||||
});
|
||||
}
|
||||
|
||||
void SMTEncoder::resetReferences(TypePointer _type)
|
||||
{
|
||||
m_context.resetVariables([&](VariableDeclaration const& _var) {
|
||||
return sameTypeOrSubtype(_var.type(), _type);
|
||||
});
|
||||
}
|
||||
|
||||
bool SMTEncoder::sameTypeOrSubtype(TypePointer _a, TypePointer _b)
|
||||
{
|
||||
TypePointer prefix = _a;
|
||||
while (
|
||||
prefix->category() == Type::Category::Mapping ||
|
||||
prefix->category() == Type::Category::Array
|
||||
)
|
||||
{
|
||||
if (*typeWithoutPointer(_b) == *typeWithoutPointer(prefix))
|
||||
return true;
|
||||
if (prefix->category() == Type::Category::Mapping)
|
||||
{
|
||||
auto mapPrefix = dynamic_cast<MappingType const*>(prefix);
|
||||
solAssert(mapPrefix, "");
|
||||
prefix = mapPrefix->valueType();
|
||||
}
|
||||
else
|
||||
{
|
||||
auto arrayPrefix = dynamic_cast<ArrayType const*>(prefix);
|
||||
solAssert(arrayPrefix, "");
|
||||
prefix = arrayPrefix->baseType();
|
||||
}
|
||||
}
|
||||
return false;
|
||||
}
|
||||
|
||||
TypePointer SMTEncoder::typeWithoutPointer(TypePointer const& _type)
|
||||
{
|
||||
if (auto refType = dynamic_cast<ReferenceType const*>(_type))
|
||||
|
||||
@ -146,8 +146,8 @@ protected:
|
||||
/// to variable of some SMT array type
|
||||
/// while aliasing is not supported.
|
||||
void arrayAssignment();
|
||||
/// Handles assignment to SMT array index.
|
||||
void arrayIndexAssignment(Expression const& _expr, smtutil::Expression const& _rightHandSide);
|
||||
/// Handles assignments to index or member access.
|
||||
void indexOrMemberAssignment(Expression const& _expr, smtutil::Expression const& _rightHandSide);
|
||||
|
||||
void arrayPush(FunctionCall const& _funCall);
|
||||
void arrayPop(FunctionCall const& _funCall);
|
||||
@ -168,8 +168,7 @@ protected:
|
||||
void assignment(
|
||||
Expression const& _left,
|
||||
smtutil::Expression const& _right,
|
||||
TypePointer const& _type,
|
||||
langutil::SourceLocation const& _location
|
||||
TypePointer const& _type
|
||||
);
|
||||
/// Handle assignments between tuples.
|
||||
void tupleAssignment(Expression const& _left, Expression const& _right);
|
||||
@ -196,8 +195,12 @@ protected:
|
||||
/// Resets all references/pointers that have the same type or have
|
||||
/// a subexpression of the same type as _varDecl.
|
||||
void resetReferences(VariableDeclaration const& _varDecl);
|
||||
/// Resets all references/pointers that have type _type.
|
||||
void resetReferences(TypePointer _type);
|
||||
/// @returns the type without storage pointer information if it has it.
|
||||
TypePointer typeWithoutPointer(TypePointer const& _type);
|
||||
/// @returns whether _a or a subtype of _a is the same as _b.
|
||||
bool sameTypeOrSubtype(TypePointer _a, TypePointer _b);
|
||||
|
||||
/// Given two different branches and the touched variables,
|
||||
/// merge the touched variables into after-branch ite variables
|
||||
|
||||
@ -25,6 +25,7 @@
|
||||
#include <vector>
|
||||
|
||||
using namespace std;
|
||||
using namespace solidity::util;
|
||||
using namespace solidity::smtutil;
|
||||
|
||||
namespace solidity::frontend::smt
|
||||
@ -32,7 +33,7 @@ namespace solidity::frontend::smt
|
||||
|
||||
SortPointer smtSort(frontend::Type const& _type)
|
||||
{
|
||||
switch (smtKind(_type.category()))
|
||||
switch (smtKind(_type))
|
||||
{
|
||||
case Kind::Int:
|
||||
if (auto const* intType = dynamic_cast<IntegerType const*>(&_type))
|
||||
@ -63,13 +64,13 @@ SortPointer smtSort(frontend::Type const& _type)
|
||||
case Kind::Array:
|
||||
{
|
||||
shared_ptr<ArraySort> array;
|
||||
if (isMapping(_type.category()))
|
||||
if (isMapping(_type))
|
||||
{
|
||||
auto mapType = dynamic_cast<frontend::MappingType const*>(&_type);
|
||||
solAssert(mapType, "");
|
||||
array = make_shared<ArraySort>(smtSortAbstractFunction(*mapType->keyType()), smtSortAbstractFunction(*mapType->valueType()));
|
||||
}
|
||||
else if (isStringLiteral(_type.category()))
|
||||
else if (isStringLiteral(_type))
|
||||
{
|
||||
auto stringLitType = dynamic_cast<frontend::StringLiteralType const*>(&_type);
|
||||
solAssert(stringLitType, "");
|
||||
@ -130,18 +131,32 @@ SortPointer smtSort(frontend::Type const& _type)
|
||||
}
|
||||
case Kind::Tuple:
|
||||
{
|
||||
auto tupleType = dynamic_cast<frontend::TupleType const*>(&_type);
|
||||
solAssert(tupleType, "");
|
||||
vector<string> members;
|
||||
auto const& tupleName = _type.identifier();
|
||||
auto const& components = tupleType->components();
|
||||
for (unsigned i = 0; i < components.size(); ++i)
|
||||
members.emplace_back(tupleName + "_accessor_" + to_string(i));
|
||||
return make_shared<TupleSort>(
|
||||
tupleName,
|
||||
members,
|
||||
smtSortAbstractFunction(tupleType->components())
|
||||
);
|
||||
auto const& tupleName = _type.toString(true);
|
||||
vector<SortPointer> sorts;
|
||||
|
||||
if (auto const* tupleType = dynamic_cast<frontend::TupleType const*>(&_type))
|
||||
{
|
||||
auto const& components = tupleType->components();
|
||||
for (unsigned i = 0; i < components.size(); ++i)
|
||||
members.emplace_back(tupleName + "_accessor_" + to_string(i));
|
||||
sorts = smtSortAbstractFunction(tupleType->components());
|
||||
}
|
||||
else if (auto const* structType = dynamic_cast<frontend::StructType const*>(&_type))
|
||||
{
|
||||
solAssert(!structType->recursive(), "");
|
||||
auto const& structMembers = structType->structDefinition().members();
|
||||
for (auto member: structMembers)
|
||||
members.emplace_back(tupleName + "_accessor_" + member->name());
|
||||
sorts = smtSortAbstractFunction(applyMap(
|
||||
structMembers,
|
||||
[](auto var) { return var->type(); }
|
||||
));
|
||||
}
|
||||
else
|
||||
solAssert(false, "");
|
||||
|
||||
return make_shared<TupleSort>(tupleName, members, sorts);
|
||||
}
|
||||
default:
|
||||
// Abstract case.
|
||||
@ -159,7 +174,7 @@ vector<SortPointer> smtSort(vector<frontend::TypePointer> const& _types)
|
||||
|
||||
SortPointer smtSortAbstractFunction(frontend::Type const& _type)
|
||||
{
|
||||
if (isFunction(_type.category()))
|
||||
if (isFunction(_type))
|
||||
return SortProvider::uintSort;
|
||||
return smtSort(_type);
|
||||
}
|
||||
@ -175,35 +190,36 @@ vector<SortPointer> smtSortAbstractFunction(vector<frontend::TypePointer> const&
|
||||
return sorts;
|
||||
}
|
||||
|
||||
Kind smtKind(frontend::Type::Category _category)
|
||||
Kind smtKind(frontend::Type const& _type)
|
||||
{
|
||||
if (isNumber(_category))
|
||||
if (isNumber(_type))
|
||||
return Kind::Int;
|
||||
else if (isBool(_category))
|
||||
else if (isBool(_type))
|
||||
return Kind::Bool;
|
||||
else if (isFunction(_category))
|
||||
else if (isFunction(_type))
|
||||
return Kind::Function;
|
||||
else if (isMapping(_category) || isArray(_category))
|
||||
else if (isMapping(_type) || isArray(_type))
|
||||
return Kind::Array;
|
||||
else if (isTuple(_category))
|
||||
else if (isTuple(_type) || isNonRecursiveStruct(_type))
|
||||
return Kind::Tuple;
|
||||
// Abstract case.
|
||||
return Kind::Int;
|
||||
}
|
||||
|
||||
bool isSupportedType(frontend::Type::Category _category)
|
||||
bool isSupportedType(frontend::Type const& _type)
|
||||
{
|
||||
return isNumber(_category) ||
|
||||
isBool(_category) ||
|
||||
isMapping(_category) ||
|
||||
isArray(_category) ||
|
||||
isTuple(_category);
|
||||
return isNumber(_type) ||
|
||||
isBool(_type) ||
|
||||
isMapping(_type) ||
|
||||
isArray(_type) ||
|
||||
isTuple(_type) ||
|
||||
isNonRecursiveStruct(_type);
|
||||
}
|
||||
|
||||
bool isSupportedTypeDeclaration(frontend::Type::Category _category)
|
||||
bool isSupportedTypeDeclaration(frontend::Type const& _type)
|
||||
{
|
||||
return isSupportedType(_category) ||
|
||||
isFunction(_category);
|
||||
return isSupportedType(_type) ||
|
||||
isFunction(_type);
|
||||
}
|
||||
|
||||
pair<bool, shared_ptr<SymbolicVariable>> newSymbolicVariable(
|
||||
@ -220,9 +236,9 @@ pair<bool, shared_ptr<SymbolicVariable>> newSymbolicVariable(
|
||||
abstract = true;
|
||||
var = make_shared<SymbolicIntVariable>(frontend::TypeProvider::uint256(), type, _uniqueName, _context);
|
||||
}
|
||||
else if (isBool(_type.category()))
|
||||
else if (isBool(_type))
|
||||
var = make_shared<SymbolicBoolVariable>(type, _uniqueName, _context);
|
||||
else if (isFunction(_type.category()))
|
||||
else if (isFunction(_type))
|
||||
{
|
||||
auto const& fType = dynamic_cast<FunctionType const*>(type);
|
||||
auto const& paramsIn = fType->parameterTypes();
|
||||
@ -245,21 +261,21 @@ pair<bool, shared_ptr<SymbolicVariable>> newSymbolicVariable(
|
||||
else
|
||||
var = make_shared<SymbolicFunctionVariable>(type, _uniqueName, _context);
|
||||
}
|
||||
else if (isInteger(_type.category()))
|
||||
else if (isInteger(_type))
|
||||
var = make_shared<SymbolicIntVariable>(type, type, _uniqueName, _context);
|
||||
else if (isFixedPoint(_type.category()))
|
||||
else if (isFixedPoint(_type))
|
||||
var = make_shared<SymbolicIntVariable>(type, type, _uniqueName, _context);
|
||||
else if (isFixedBytes(_type.category()))
|
||||
else if (isFixedBytes(_type))
|
||||
{
|
||||
auto fixedBytesType = dynamic_cast<frontend::FixedBytesType const*>(type);
|
||||
solAssert(fixedBytesType, "");
|
||||
var = make_shared<SymbolicFixedBytesVariable>(type, fixedBytesType->numBytes(), _uniqueName, _context);
|
||||
}
|
||||
else if (isAddress(_type.category()) || isContract(_type.category()))
|
||||
else if (isAddress(_type) || isContract(_type))
|
||||
var = make_shared<SymbolicAddressVariable>(_uniqueName, _context);
|
||||
else if (isEnum(_type.category()))
|
||||
else if (isEnum(_type))
|
||||
var = make_shared<SymbolicEnumVariable>(type, _uniqueName, _context);
|
||||
else if (isRational(_type.category()))
|
||||
else if (isRational(_type))
|
||||
{
|
||||
auto rational = dynamic_cast<frontend::RationalNumberType const*>(&_type);
|
||||
solAssert(rational, "");
|
||||
@ -268,106 +284,104 @@ pair<bool, shared_ptr<SymbolicVariable>> newSymbolicVariable(
|
||||
else
|
||||
var = make_shared<SymbolicIntVariable>(type, type, _uniqueName, _context);
|
||||
}
|
||||
else if (isMapping(_type.category()) || isArray(_type.category()))
|
||||
else if (isMapping(_type) || isArray(_type))
|
||||
var = make_shared<SymbolicArrayVariable>(type, type, _uniqueName, _context);
|
||||
else if (isTuple(_type.category()))
|
||||
else if (isTuple(_type))
|
||||
var = make_shared<SymbolicTupleVariable>(type, _uniqueName, _context);
|
||||
else if (isStringLiteral(_type.category()))
|
||||
else if (isStringLiteral(_type))
|
||||
{
|
||||
auto stringType = TypeProvider::stringMemory();
|
||||
var = make_shared<SymbolicArrayVariable>(stringType, type, _uniqueName, _context);
|
||||
}
|
||||
else if (isNonRecursiveStruct(_type))
|
||||
var = make_shared<SymbolicStructVariable>(type, _uniqueName, _context);
|
||||
else
|
||||
solAssert(false, "");
|
||||
return make_pair(abstract, var);
|
||||
}
|
||||
|
||||
bool isSupportedType(frontend::Type const& _type)
|
||||
bool isInteger(frontend::Type const& _type)
|
||||
{
|
||||
return isSupportedType(_type.category());
|
||||
return _type.category() == frontend::Type::Category::Integer;
|
||||
}
|
||||
|
||||
bool isSupportedTypeDeclaration(frontend::Type const& _type)
|
||||
bool isFixedPoint(frontend::Type const& _type)
|
||||
{
|
||||
return isSupportedTypeDeclaration(_type.category());
|
||||
return _type.category() == frontend::Type::Category::FixedPoint;
|
||||
}
|
||||
|
||||
bool isInteger(frontend::Type::Category _category)
|
||||
bool isRational(frontend::Type const& _type)
|
||||
{
|
||||
return _category == frontend::Type::Category::Integer;
|
||||
return _type.category() == frontend::Type::Category::RationalNumber;
|
||||
}
|
||||
|
||||
bool isFixedPoint(frontend::Type::Category _category)
|
||||
bool isFixedBytes(frontend::Type const& _type)
|
||||
{
|
||||
return _category == frontend::Type::Category::FixedPoint;
|
||||
return _type.category() == frontend::Type::Category::FixedBytes;
|
||||
}
|
||||
|
||||
bool isRational(frontend::Type::Category _category)
|
||||
bool isAddress(frontend::Type const& _type)
|
||||
{
|
||||
return _category == frontend::Type::Category::RationalNumber;
|
||||
return _type.category() == frontend::Type::Category::Address;
|
||||
}
|
||||
|
||||
bool isFixedBytes(frontend::Type::Category _category)
|
||||
bool isContract(frontend::Type const& _type)
|
||||
{
|
||||
return _category == frontend::Type::Category::FixedBytes;
|
||||
return _type.category() == frontend::Type::Category::Contract;
|
||||
}
|
||||
|
||||
bool isAddress(frontend::Type::Category _category)
|
||||
bool isEnum(frontend::Type const& _type)
|
||||
{
|
||||
return _category == frontend::Type::Category::Address;
|
||||
return _type.category() == frontend::Type::Category::Enum;
|
||||
}
|
||||
|
||||
bool isContract(frontend::Type::Category _category)
|
||||
bool isNumber(frontend::Type const& _type)
|
||||
{
|
||||
return _category == frontend::Type::Category::Contract;
|
||||
return isInteger(_type) ||
|
||||
isFixedPoint(_type) ||
|
||||
isRational(_type) ||
|
||||
isFixedBytes(_type) ||
|
||||
isAddress(_type) ||
|
||||
isContract(_type) ||
|
||||
isEnum(_type);
|
||||
}
|
||||
|
||||
bool isEnum(frontend::Type::Category _category)
|
||||
bool isBool(frontend::Type const& _type)
|
||||
{
|
||||
return _category == frontend::Type::Category::Enum;
|
||||
return _type.category() == frontend::Type::Category::Bool;
|
||||
}
|
||||
|
||||
bool isNumber(frontend::Type::Category _category)
|
||||
bool isFunction(frontend::Type const& _type)
|
||||
{
|
||||
return isInteger(_category) ||
|
||||
isFixedPoint(_category) ||
|
||||
isRational(_category) ||
|
||||
isFixedBytes(_category) ||
|
||||
isAddress(_category) ||
|
||||
isContract(_category) ||
|
||||
isEnum(_category);
|
||||
return _type.category() == frontend::Type::Category::Function;
|
||||
}
|
||||
|
||||
bool isBool(frontend::Type::Category _category)
|
||||
bool isMapping(frontend::Type const& _type)
|
||||
{
|
||||
return _category == frontend::Type::Category::Bool;
|
||||
return _type.category() == frontend::Type::Category::Mapping;
|
||||
}
|
||||
|
||||
bool isFunction(frontend::Type::Category _category)
|
||||
bool isArray(frontend::Type const& _type)
|
||||
{
|
||||
return _category == frontend::Type::Category::Function;
|
||||
return _type.category() == frontend::Type::Category::Array ||
|
||||
_type.category() == frontend::Type::Category::StringLiteral ||
|
||||
_type.category() == frontend::Type::Category::ArraySlice;
|
||||
}
|
||||
|
||||
bool isMapping(frontend::Type::Category _category)
|
||||
bool isTuple(frontend::Type const& _type)
|
||||
{
|
||||
return _category == frontend::Type::Category::Mapping;
|
||||
return _type.category() == frontend::Type::Category::Tuple;
|
||||
}
|
||||
|
||||
bool isArray(frontend::Type::Category _category)
|
||||
bool isStringLiteral(frontend::Type const& _type)
|
||||
{
|
||||
return _category == frontend::Type::Category::Array ||
|
||||
_category == frontend::Type::Category::StringLiteral ||
|
||||
_category == frontend::Type::Category::ArraySlice;
|
||||
return _type.category() == frontend::Type::Category::StringLiteral;
|
||||
}
|
||||
|
||||
bool isTuple(frontend::Type::Category _category)
|
||||
bool isNonRecursiveStruct(frontend::Type const& _type)
|
||||
{
|
||||
return _category == frontend::Type::Category::Tuple;
|
||||
}
|
||||
|
||||
bool isStringLiteral(frontend::Type::Category _category)
|
||||
{
|
||||
return _category == frontend::Type::Category::StringLiteral;
|
||||
auto structType = dynamic_cast<StructType const*>(&_type);
|
||||
return structType && !structType->recursive();
|
||||
}
|
||||
|
||||
smtutil::Expression minValue(frontend::IntegerType const& _type)
|
||||
@ -394,13 +408,13 @@ void setSymbolicZeroValue(smtutil::Expression _expr, frontend::TypePointer const
|
||||
smtutil::Expression zeroValue(frontend::TypePointer const& _type)
|
||||
{
|
||||
solAssert(_type, "");
|
||||
if (isSupportedType(_type->category()))
|
||||
if (isSupportedType(*_type))
|
||||
{
|
||||
if (isNumber(_type->category()))
|
||||
if (isNumber(*_type))
|
||||
return 0;
|
||||
if (isBool(_type->category()))
|
||||
if (isBool(*_type))
|
||||
return smtutil::Expression(false);
|
||||
if (isArray(_type->category()) || isMapping(_type->category()))
|
||||
if (isArray(*_type) || isMapping(*_type))
|
||||
{
|
||||
auto tupleSort = dynamic_pointer_cast<TupleSort>(smtSort(*_type));
|
||||
solAssert(tupleSort, "");
|
||||
@ -421,11 +435,23 @@ smtutil::Expression zeroValue(frontend::TypePointer const& _type)
|
||||
|
||||
solAssert(zeroArray, "");
|
||||
return smtutil::Expression::tuple_constructor(
|
||||
smtutil::Expression(std::make_shared<SortSort>(smtSort(*_type)), _type->toString(true)),
|
||||
smtutil::Expression(std::make_shared<SortSort>(tupleSort), tupleSort->name),
|
||||
vector<smtutil::Expression>{*zeroArray, length}
|
||||
);
|
||||
|
||||
}
|
||||
if (isNonRecursiveStruct(*_type))
|
||||
{
|
||||
auto const* structType = dynamic_cast<StructType const*>(_type);
|
||||
auto structSort = dynamic_pointer_cast<TupleSort>(smtSort(*_type));
|
||||
return smtutil::Expression::tuple_constructor(
|
||||
smtutil::Expression(make_shared<SortSort>(structSort), structSort->name),
|
||||
applyMap(
|
||||
structType->structDefinition().members(),
|
||||
[](auto var) { return zeroValue(var->type()); }
|
||||
)
|
||||
);
|
||||
}
|
||||
solAssert(false, "");
|
||||
}
|
||||
// Unsupported types are abstracted as Int.
|
||||
@ -452,14 +478,14 @@ void setSymbolicUnknownValue(SymbolicVariable const& _variable, EncodingContext&
|
||||
void setSymbolicUnknownValue(smtutil::Expression _expr, frontend::TypePointer const& _type, EncodingContext& _context)
|
||||
{
|
||||
solAssert(_type, "");
|
||||
if (isEnum(_type->category()))
|
||||
if (isEnum(*_type))
|
||||
{
|
||||
auto enumType = dynamic_cast<frontend::EnumType const*>(_type);
|
||||
solAssert(enumType, "");
|
||||
_context.addAssertion(_expr >= 0);
|
||||
_context.addAssertion(_expr < enumType->numberOfMembers());
|
||||
}
|
||||
else if (isInteger(_type->category()))
|
||||
else if (isInteger(*_type))
|
||||
{
|
||||
auto intType = dynamic_cast<frontend::IntegerType const*>(_type);
|
||||
solAssert(intType, "");
|
||||
|
||||
@ -34,29 +34,30 @@ std::vector<smtutil::SortPointer> smtSort(std::vector<frontend::TypePointer> con
|
||||
smtutil::SortPointer smtSortAbstractFunction(frontend::Type const& _type);
|
||||
std::vector<smtutil::SortPointer> smtSortAbstractFunction(std::vector<frontend::TypePointer> const& _types);
|
||||
/// Returns the SMT kind that models the Solidity type type category _category.
|
||||
smtutil::Kind smtKind(frontend::Type::Category _category);
|
||||
smtutil::Kind smtKind(frontend::Type const& _type);
|
||||
|
||||
/// Returns true if type is fully supported (declaration and operations).
|
||||
bool isSupportedType(frontend::Type::Category _category);
|
||||
bool isSupportedType(frontend::Type const& _type);
|
||||
bool isSupportedType(frontend::Type const& _type);
|
||||
/// Returns true if type is partially supported (declaration).
|
||||
bool isSupportedTypeDeclaration(frontend::Type::Category _category);
|
||||
bool isSupportedTypeDeclaration(frontend::Type const& _type);
|
||||
bool isSupportedTypeDeclaration(frontend::Type const& _type);
|
||||
|
||||
bool isInteger(frontend::Type::Category _category);
|
||||
bool isFixedPoint(frontend::Type::Category _category);
|
||||
bool isRational(frontend::Type::Category _category);
|
||||
bool isFixedBytes(frontend::Type::Category _category);
|
||||
bool isAddress(frontend::Type::Category _category);
|
||||
bool isContract(frontend::Type::Category _category);
|
||||
bool isEnum(frontend::Type::Category _category);
|
||||
bool isNumber(frontend::Type::Category _category);
|
||||
bool isBool(frontend::Type::Category _category);
|
||||
bool isFunction(frontend::Type::Category _category);
|
||||
bool isMapping(frontend::Type::Category _category);
|
||||
bool isArray(frontend::Type::Category _category);
|
||||
bool isTuple(frontend::Type::Category _category);
|
||||
bool isStringLiteral(frontend::Type::Category _category);
|
||||
bool isInteger(frontend::Type const& _type);
|
||||
bool isFixedPoint(frontend::Type const& _type);
|
||||
bool isRational(frontend::Type const& _type);
|
||||
bool isFixedBytes(frontend::Type const& _type);
|
||||
bool isAddress(frontend::Type const& _type);
|
||||
bool isContract(frontend::Type const& _type);
|
||||
bool isEnum(frontend::Type const& _type);
|
||||
bool isNumber(frontend::Type const& _type);
|
||||
bool isBool(frontend::Type const& _type);
|
||||
bool isFunction(frontend::Type const& _type);
|
||||
bool isMapping(frontend::Type const& _type);
|
||||
bool isArray(frontend::Type const& _type);
|
||||
bool isTuple(frontend::Type const& _type);
|
||||
bool isStringLiteral(frontend::Type const& _type);
|
||||
bool isNonRecursiveStruct(frontend::Type const& _type);
|
||||
|
||||
/// Returns a new symbolic variable, according to _type.
|
||||
/// Also returns whether the type is abstract or not,
|
||||
|
||||
@ -21,8 +21,11 @@
|
||||
#include <libsolidity/formal/SymbolicTypes.h>
|
||||
#include <libsolidity/ast/AST.h>
|
||||
|
||||
#include <libsolutil/Algorithms.h>
|
||||
|
||||
using namespace std;
|
||||
using namespace solidity;
|
||||
using namespace solidity::util;
|
||||
using namespace solidity::smtutil;
|
||||
using namespace solidity::frontend;
|
||||
using namespace solidity::frontend::smt;
|
||||
@ -118,7 +121,7 @@ SymbolicIntVariable::SymbolicIntVariable(
|
||||
):
|
||||
SymbolicVariable(_type, _originalType, move(_uniqueName), _context)
|
||||
{
|
||||
solAssert(isNumber(m_type->category()), "");
|
||||
solAssert(isNumber(*m_type), "");
|
||||
}
|
||||
|
||||
SymbolicAddressVariable::SymbolicAddressVariable(
|
||||
@ -218,7 +221,7 @@ SymbolicEnumVariable::SymbolicEnumVariable(
|
||||
):
|
||||
SymbolicVariable(_type, _type, move(_uniqueName), _context)
|
||||
{
|
||||
solAssert(isEnum(m_type->category()), "");
|
||||
solAssert(isEnum(*m_type), "");
|
||||
}
|
||||
|
||||
SymbolicTupleVariable::SymbolicTupleVariable(
|
||||
@ -228,7 +231,7 @@ SymbolicTupleVariable::SymbolicTupleVariable(
|
||||
):
|
||||
SymbolicVariable(_type, _type, move(_uniqueName), _context)
|
||||
{
|
||||
solAssert(isTuple(m_type->category()), "");
|
||||
solAssert(isTuple(*m_type), "");
|
||||
}
|
||||
|
||||
SymbolicTupleVariable::SymbolicTupleVariable(
|
||||
@ -274,7 +277,7 @@ SymbolicArrayVariable::SymbolicArrayVariable(
|
||||
m_context
|
||||
)
|
||||
{
|
||||
solAssert(isArray(m_type->category()) || isMapping(m_type->category()), "");
|
||||
solAssert(isArray(*m_type) || isMapping(*m_type), "");
|
||||
}
|
||||
|
||||
SymbolicArrayVariable::SymbolicArrayVariable(
|
||||
@ -319,3 +322,47 @@ smtutil::Expression SymbolicArrayVariable::length()
|
||||
{
|
||||
return m_pair.component(1);
|
||||
}
|
||||
|
||||
SymbolicStructVariable::SymbolicStructVariable(
|
||||
frontend::TypePointer _type,
|
||||
string _uniqueName,
|
||||
EncodingContext& _context
|
||||
):
|
||||
SymbolicVariable(_type, _type, move(_uniqueName), _context)
|
||||
{
|
||||
solAssert(isNonRecursiveStruct(*m_type), "");
|
||||
auto const* structType = dynamic_cast<StructType const*>(_type);
|
||||
solAssert(structType, "");
|
||||
auto const& members = structType->structDefinition().members();
|
||||
for (unsigned i = 0; i < members.size(); ++i)
|
||||
{
|
||||
solAssert(members.at(i), "");
|
||||
m_memberIndices.emplace(members.at(i)->name(), i);
|
||||
}
|
||||
}
|
||||
|
||||
smtutil::Expression SymbolicStructVariable::member(string const& _member)
|
||||
{
|
||||
return smtutil::Expression::tuple_get(currentValue(), m_memberIndices.at(_member));
|
||||
}
|
||||
|
||||
smtutil::Expression SymbolicStructVariable::assignMember(string const& _member, smtutil::Expression const& _memberValue)
|
||||
{
|
||||
auto const* structType = dynamic_cast<StructType const*>(m_type);
|
||||
solAssert(structType, "");
|
||||
auto const& structDef = structType->structDefinition();
|
||||
auto const& structMembers = structDef.members();
|
||||
auto oldMembers = applyMap(
|
||||
structMembers,
|
||||
[&](auto _member) { return member(_member->name()); }
|
||||
);
|
||||
increaseIndex();
|
||||
for (unsigned i = 0; i < structMembers.size(); ++i)
|
||||
{
|
||||
auto const& memberName = structMembers.at(i)->name();
|
||||
auto newMember = memberName == _member ? _memberValue : oldMembers.at(i);
|
||||
m_context.addAssertion(member(memberName) == newMember);
|
||||
}
|
||||
|
||||
return currentValue();
|
||||
}
|
||||
|
||||
@ -23,6 +23,8 @@
|
||||
#include <libsolidity/ast/TypeProvider.h>
|
||||
|
||||
#include <libsmtutil/SolverInterface.h>
|
||||
|
||||
#include <map>
|
||||
#include <memory>
|
||||
|
||||
namespace solidity::frontend::smt
|
||||
@ -265,4 +267,29 @@ private:
|
||||
SymbolicTupleVariable m_pair;
|
||||
};
|
||||
|
||||
/**
|
||||
* Specialization of SymbolicVariable for Struct.
|
||||
*/
|
||||
class SymbolicStructVariable: public SymbolicVariable
|
||||
{
|
||||
public:
|
||||
SymbolicStructVariable(
|
||||
frontend::TypePointer _type,
|
||||
std::string _uniqueName,
|
||||
EncodingContext& _context
|
||||
);
|
||||
|
||||
/// @returns the symbolic expression representing _member.
|
||||
smtutil::Expression member(std::string const& _member);
|
||||
|
||||
/// @returns the symbolic expression representing this struct
|
||||
/// with field _member updated.
|
||||
smtutil::Expression assignMember(std::string const& _member, smtutil::Expression const& _memberValue);
|
||||
|
||||
private:
|
||||
std::map<std::string, unsigned> m_memberIndices;
|
||||
};
|
||||
|
||||
|
||||
|
||||
}
|
||||
|
||||
@ -11,10 +11,3 @@ contract C {
|
||||
}
|
||||
}
|
||||
// ----
|
||||
// Warning 6328: (119-157): Assertion violation happens here
|
||||
// Warning 8115: (76-80): Assertion checker does not yet support the type of this variable.
|
||||
// Warning 8115: (83-87): Assertion checker does not yet support the type of this variable.
|
||||
// Warning 7650: (126-132): Assertion checker does not yet support this expression.
|
||||
// Warning 8364: (126-128): Assertion checker does not yet implement type struct C.S storage ref
|
||||
// Warning 7650: (143-149): Assertion checker does not yet support this expression.
|
||||
// Warning 8364: (143-145): Assertion checker does not yet implement type struct C.S storage ref
|
||||
|
||||
@ -11,12 +11,3 @@ contract C {
|
||||
}
|
||||
}
|
||||
// ----
|
||||
// Warning 6328: (121-165): Assertion violation happens here
|
||||
// Warning 8115: (78-82): Assertion checker does not yet support the type of this variable.
|
||||
// Warning 8115: (85-89): Assertion checker does not yet support the type of this variable.
|
||||
// Warning 7650: (128-134): Assertion checker does not yet support this expression.
|
||||
// Warning 8364: (128-130): Assertion checker does not yet implement type struct C.S storage ref
|
||||
// Warning 9118: (128-137): Assertion checker does not yet implement this expression.
|
||||
// Warning 7650: (148-154): Assertion checker does not yet support this expression.
|
||||
// Warning 8364: (148-150): Assertion checker does not yet implement type struct C.S storage ref
|
||||
// Warning 9118: (148-157): Assertion checker does not yet implement this expression.
|
||||
|
||||
@ -15,13 +15,3 @@ contract C {
|
||||
}
|
||||
|
||||
// ----
|
||||
// Warning 8115: (72-75): Assertion checker does not yet support the type of this variable.
|
||||
// Warning 8115: (100-103): Assertion checker does not yet support the type of this variable.
|
||||
// Warning 7650: (130-133): Assertion checker does not yet support this expression.
|
||||
// Warning 8364: (130-131): Assertion checker does not yet implement type struct C.S storage ref
|
||||
// Warning 9599: (130-133): Assertion checker does not yet implement this expression.
|
||||
// Warning 7650: (144-149): Assertion checker does not yet support this expression.
|
||||
// Warning 8364: (144-147): Assertion checker does not yet implement type struct C.S storage ref
|
||||
// Warning 7650: (144-147): Assertion checker does not yet support this expression.
|
||||
// Warning 8364: (144-145): Assertion checker does not yet implement type struct C.T storage ref
|
||||
// Warning 9599: (144-149): Assertion checker does not yet implement this expression.
|
||||
|
||||
@ -16,18 +16,3 @@ contract C {
|
||||
}
|
||||
|
||||
// ----
|
||||
// Warning 8115: (72-75): Assertion checker does not yet support the type of this variable.
|
||||
// Warning 8115: (102-105): Assertion checker does not yet support the type of this variable.
|
||||
// Warning 7650: (132-135): Assertion checker does not yet support this expression.
|
||||
// Warning 8364: (132-133): Assertion checker does not yet implement type struct C.S storage ref
|
||||
// Warning 9599: (132-135): Assertion checker does not yet implement this expression.
|
||||
// Warning 7650: (146-149): Assertion checker does not yet support this expression.
|
||||
// Warning 8364: (146-147): Assertion checker does not yet implement type struct C.T storage ref
|
||||
// Warning 8364: (146-156): Assertion checker does not yet implement type struct C.S storage ref
|
||||
// Warning 9599: (146-149): Assertion checker does not yet implement this expression.
|
||||
// Warning 7650: (160-168): Assertion checker does not yet support this expression.
|
||||
// Warning 7650: (160-163): Assertion checker does not yet support this expression.
|
||||
// Warning 8364: (160-161): Assertion checker does not yet implement type struct C.T storage ref
|
||||
// Warning 8364: (160-166): Assertion checker does not yet implement type struct C.S storage ref
|
||||
// Warning 9118: (160-166): Assertion checker does not yet implement this expression.
|
||||
// Warning 9599: (160-168): Assertion checker does not yet implement this expression.
|
||||
|
||||
@ -118,23 +118,3 @@ contract PropagateThroughReturnValue {
|
||||
}
|
||||
// ----
|
||||
// Warning 2018: (1879-1947): Function state mutability can be restricted to view
|
||||
// Warning 8115: (318-332): Assertion checker does not yet support the type of this variable.
|
||||
// Warning 8115: (338-347): Assertion checker does not yet support the type of this variable.
|
||||
// Warning 8115: (353-378): Assertion checker does not yet support the type of this variable.
|
||||
// Warning 8115: (384-409): Assertion checker does not yet support the type of this variable.
|
||||
// Warning 7650: (464-479): Assertion checker does not yet support this expression.
|
||||
// Warning 8364: (464-475): Assertion checker does not yet implement type struct Reference.St storage ref
|
||||
// Warning 8182: (464-494): Assertion checker does not yet implement such assignments.
|
||||
// Warning 7650: (539-554): Assertion checker does not yet support this expression.
|
||||
// Warning 8364: (539-550): Assertion checker does not yet implement type struct Reference.St storage ref
|
||||
// Warning 7650: (557-567): Assertion checker does not yet support this expression.
|
||||
// Warning 8364: (557-563): Assertion checker does not yet implement type struct Reference.St storage ref
|
||||
// Warning 8182: (539-567): Assertion checker does not yet implement such assignments.
|
||||
// Warning 8115: (629-643): Assertion checker does not yet support the type of this variable.
|
||||
// Warning 8364: (646-668): Assertion checker does not yet implement type struct Reference.St storage ref
|
||||
// Warning 8364: (700-703): Assertion checker does not yet implement type struct Reference.St storage pointer
|
||||
// Warning 8364: (706-728): Assertion checker does not yet implement type struct Reference.St storage ref
|
||||
// Warning 8364: (700-728): Assertion checker does not yet implement type struct Reference.St storage pointer
|
||||
// Warning 7650: (748-755): Assertion checker does not yet support this expression.
|
||||
// Warning 8364: (748-751): Assertion checker does not yet implement type struct Reference.St storage pointer
|
||||
// Warning 8182: (748-770): Assertion checker does not yet implement such assignments.
|
||||
|
||||
@ -8,7 +8,5 @@ contract C {
|
||||
}
|
||||
// ----
|
||||
// Warning 2072: (133-143): Unused local variable.
|
||||
// Warning 8115: (133-143): Assertion checker does not yet support the type of this variable.
|
||||
// Warning 8364: (146-147): Assertion checker does not yet implement type type(struct C.A storage pointer)
|
||||
// Warning 8364: (146-163): Assertion checker does not yet implement type struct C.A memory
|
||||
// Warning 4639: (146-163): Assertion checker does not yet implement this expression.
|
||||
|
||||
@ -20,3 +20,4 @@ contract LoopFor2 {
|
||||
}
|
||||
// ----
|
||||
// Warning 6328: (363-382): Assertion violation happens here
|
||||
// Warning 4661: (316-336): Assertion violation happens here
|
||||
|
||||
@ -21,3 +21,4 @@ contract LoopFor2 {
|
||||
// ----
|
||||
// Warning 6328: (341-360): Assertion violation happens here
|
||||
// Warning 6328: (364-383): Assertion violation happens here
|
||||
// Warning 4661: (317-337): Assertion violation happens here
|
||||
|
||||
@ -10,7 +10,4 @@ contract C {
|
||||
}
|
||||
}
|
||||
// ----
|
||||
// Warning 8115: (71-74): Assertion checker does not yet support the type of this variable.
|
||||
// Warning 7650: (117-120): Assertion checker does not yet support this expression.
|
||||
// Warning 8364: (117-118): Assertion checker does not yet implement type struct C.S storage ref
|
||||
// Warning 9149: (117-125): Assertion checker does not yet implement this assignment operator.
|
||||
|
||||
@ -10,8 +10,4 @@ contract C {
|
||||
}
|
||||
}
|
||||
// ----
|
||||
// Warning 8115: (73-76): Assertion checker does not yet support the type of this variable.
|
||||
// Warning 7650: (119-122): Assertion checker does not yet support this expression.
|
||||
// Warning 8364: (119-120): Assertion checker does not yet implement type struct C.S storage ref
|
||||
// Warning 9118: (119-125): Assertion checker does not yet implement this expression.
|
||||
// Warning 9149: (119-130): Assertion checker does not yet implement this assignment operator.
|
||||
|
||||
@ -6,7 +6,7 @@ contract C
|
||||
{
|
||||
uint x;
|
||||
}
|
||||
function f(bool b) public {
|
||||
function f(bool b) public pure {
|
||||
S memory s;
|
||||
s.x = 2;
|
||||
if (b)
|
||||
@ -17,15 +17,3 @@ contract C
|
||||
}
|
||||
}
|
||||
// ----
|
||||
// Warning 2018: (73-192): Function state mutability can be restricted to pure
|
||||
// Warning 6328: (172-188): Assertion violation happens here
|
||||
// Warning 8115: (103-113): Assertion checker does not yet support the type of this variable.
|
||||
// Warning 7650: (117-120): Assertion checker does not yet support this expression.
|
||||
// Warning 8364: (117-118): Assertion checker does not yet implement type struct C.S memory
|
||||
// Warning 8182: (117-124): Assertion checker does not yet implement such assignments.
|
||||
// Warning 8364: (145-146): Assertion checker does not yet implement type struct C.S memory
|
||||
// Warning 7650: (165-168): Assertion checker does not yet support this expression.
|
||||
// Warning 8364: (165-166): Assertion checker does not yet implement type struct C.S memory
|
||||
// Warning 2683: (158-168): Assertion checker does not yet implement "delete" for this expression.
|
||||
// Warning 7650: (179-182): Assertion checker does not yet support this expression.
|
||||
// Warning 8364: (179-180): Assertion checker does not yet implement type struct C.S memory
|
||||
|
||||
@ -0,0 +1,16 @@
|
||||
pragma experimental SMTChecker;
|
||||
|
||||
contract C {
|
||||
uint[] a;
|
||||
function h() internal returns (uint[] storage) {
|
||||
if (a[2] == 0)
|
||||
a[2] = 3;
|
||||
return a;
|
||||
}
|
||||
function g() public {
|
||||
h()[2] = 4;
|
||||
assert(h()[2] == 3);
|
||||
}
|
||||
}
|
||||
// ----
|
||||
// Warning 6328: (191-210): Assertion violation happens here
|
||||
@ -8,7 +8,6 @@ contract C {
|
||||
}
|
||||
}
|
||||
// ----
|
||||
// Warning 8115: (151-159): Assertion checker does not yet support the type of this variable.
|
||||
// Warning 8364: (206-209): Assertion checker does not yet implement type abi
|
||||
// Warning 8364: (225-226): Assertion checker does not yet implement type type(struct C.S storage pointer)
|
||||
// Warning 8364: (235-241): Assertion checker does not yet implement type type(uint256[] memory)
|
||||
|
||||
@ -14,19 +14,3 @@ contract C
|
||||
}
|
||||
}
|
||||
// ----
|
||||
// Warning 6328: (202-226): Assertion violation happens here
|
||||
// Warning 7650: (124-130): Assertion checker does not yet support this expression.
|
||||
// Warning 8364: (124-128): Assertion checker does not yet implement type struct C.S memory
|
||||
// Warning 9118: (124-133): Assertion checker does not yet implement this expression.
|
||||
// Warning 9056: (124-136): Assertion checker does not yet implement this expression.
|
||||
// Warning 7650: (154-160): Assertion checker does not yet support this expression.
|
||||
// Warning 8364: (154-158): Assertion checker does not yet implement type struct C.S memory
|
||||
// Warning 9118: (154-163): Assertion checker does not yet implement this expression.
|
||||
// Warning 9056: (154-166): Assertion checker does not yet implement this expression.
|
||||
// Warning 7650: (182-188): Assertion checker does not yet support this expression.
|
||||
// Warning 8364: (182-186): Assertion checker does not yet implement type struct C.S memory
|
||||
// Warning 9118: (182-191): Assertion checker does not yet implement this expression.
|
||||
// Warning 9056: (182-194): Assertion checker does not yet implement this expression.
|
||||
// Warning 7650: (209-215): Assertion checker does not yet support this expression.
|
||||
// Warning 8364: (209-213): Assertion checker does not yet implement type struct C.S memory
|
||||
// Warning 9118: (209-218): Assertion checker does not yet implement this expression.
|
||||
|
||||
@ -11,10 +11,3 @@ contract C
|
||||
}
|
||||
}
|
||||
// ----
|
||||
// Warning 6328: (187-208): Assertion violation happens here
|
||||
// Warning 8115: (143-153): Assertion checker does not yet support the type of this variable.
|
||||
// Warning 7650: (171-174): Assertion checker does not yet support this expression.
|
||||
// Warning 8364: (171-172): Assertion checker does not yet implement type struct C.S memory
|
||||
// Warning 8182: (171-183): Assertion checker does not yet implement such assignments.
|
||||
// Warning 7650: (194-197): Assertion checker does not yet support this expression.
|
||||
// Warning 8364: (194-195): Assertion checker does not yet implement type struct C.S memory
|
||||
|
||||
@ -13,6 +13,5 @@ contract C {
|
||||
}
|
||||
}
|
||||
// ----
|
||||
// Warning 9118: (238-244): Assertion checker does not yet implement this expression.
|
||||
// Warning 7989: (238-247): Assertion checker does not yet support index accessing fixed bytes.
|
||||
// Warning 7989: (251-257): Assertion checker does not yet support index accessing fixed bytes.
|
||||
|
||||
@ -12,8 +12,5 @@ contract C
|
||||
}
|
||||
// ----
|
||||
// Warning 6838: (140-144): Condition is always false.
|
||||
// Warning 8364: (149-156): Assertion checker does not yet implement type struct C.S storage ref
|
||||
// Warning 8364: (159-160): Assertion checker does not yet implement type type(struct C.S storage pointer)
|
||||
// Warning 8364: (159-163): Assertion checker does not yet implement type struct C.S memory
|
||||
// Warning 4639: (159-163): Assertion checker does not yet implement this expression.
|
||||
// Warning 8364: (149-163): Assertion checker does not yet implement type struct C.S storage ref
|
||||
|
||||
@ -17,7 +17,6 @@ contract test {
|
||||
// Warning 6133: (156-163): Statement has no effect.
|
||||
// Warning 8364: (125-126): Assertion checker does not yet implement type type(struct test.s storage pointer)
|
||||
// Warning 8364: (130-131): Assertion checker does not yet implement type type(struct test.s storage pointer)
|
||||
// Warning 8364: (130-136): Assertion checker does not yet implement type struct test.s memory
|
||||
// Warning 4639: (130-136): Assertion checker does not yet implement this expression.
|
||||
// Warning 8364: (140-141): Assertion checker does not yet implement type type(struct test.s storage pointer)
|
||||
// Warning 8364: (140-144): Assertion checker does not yet implement type type(struct test.s memory[7] memory)
|
||||
|
||||
@ -0,0 +1,30 @@
|
||||
pragma experimental SMTChecker;
|
||||
pragma experimental ABIEncoderV2;
|
||||
|
||||
contract C {
|
||||
struct T {
|
||||
uint y;
|
||||
uint[] a;
|
||||
}
|
||||
struct S {
|
||||
uint x;
|
||||
T t;
|
||||
uint[] a;
|
||||
T[] ts;
|
||||
}
|
||||
function f() public pure {
|
||||
S[] memory s1 = new S[](3);
|
||||
s1[0].x = 2;
|
||||
assert(s1[0].x == 2);
|
||||
s1[1].t.y = 3;
|
||||
assert(s1[1].t.y == 3);
|
||||
s1[2].a[2] = 4;
|
||||
assert(s1[2].a[2] == 4);
|
||||
s1[0].ts[3].y = 5;
|
||||
assert(s1[0].ts[3].y == 5);
|
||||
s1[1].ts[4].a[5] = 6;
|
||||
assert(s1[1].ts[4].a[5] == 6);
|
||||
}
|
||||
}
|
||||
// ----
|
||||
// Warning 4588: (217-227): Assertion checker does not yet implement this type of function call.
|
||||
@ -0,0 +1,35 @@
|
||||
pragma experimental SMTChecker;
|
||||
pragma experimental ABIEncoderV2;
|
||||
|
||||
contract C {
|
||||
struct T {
|
||||
uint y;
|
||||
uint[] a;
|
||||
}
|
||||
struct S {
|
||||
uint x;
|
||||
T t;
|
||||
uint[] a;
|
||||
T[] ts;
|
||||
}
|
||||
function f(S memory s2) public pure {
|
||||
S[] memory s1 = new S[](3);
|
||||
s1[0].x = 2;
|
||||
assert(s1[0].x == s2.x);
|
||||
s1[1].t.y = 3;
|
||||
assert(s1[1].t.y == s2.t.y);
|
||||
s1[2].a[2] = 4;
|
||||
assert(s1[2].a[2] == s2.a[2]);
|
||||
s1[0].ts[3].y = 5;
|
||||
assert(s1[0].ts[3].y == s2.ts[3].y);
|
||||
s1[1].ts[4].a[5] = 6;
|
||||
assert(s1[1].ts[4].a[5] == s2.ts[4].a[5]);
|
||||
}
|
||||
}
|
||||
// ----
|
||||
// Warning 6328: (257-280): Assertion violation happens here
|
||||
// Warning 6328: (301-328): Assertion violation happens here
|
||||
// Warning 6328: (350-379): Assertion violation happens here
|
||||
// Warning 6328: (404-439): Assertion violation happens here
|
||||
// Warning 6328: (467-508): Assertion violation happens here
|
||||
// Warning 4588: (228-238): Assertion checker does not yet implement this type of function call.
|
||||
@ -0,0 +1,34 @@
|
||||
pragma experimental SMTChecker;
|
||||
pragma experimental ABIEncoderV2;
|
||||
|
||||
contract C {
|
||||
struct T {
|
||||
uint y;
|
||||
uint[] a;
|
||||
}
|
||||
struct S {
|
||||
uint x;
|
||||
T t;
|
||||
uint[] a;
|
||||
T[] ts;
|
||||
}
|
||||
S[] s1;
|
||||
function f() public {
|
||||
s1.push();
|
||||
s1.push();
|
||||
s1.push();
|
||||
s1[0].x = 2;
|
||||
assert(s1[0].x == 2);
|
||||
s1[1].t.y = 3;
|
||||
assert(s1[1].t.y == 3);
|
||||
s1[2].a[2] = 4;
|
||||
assert(s1[2].a[2] == 4);
|
||||
s1[0].ts[3].y = 5;
|
||||
assert(s1[0].ts[3].y == 5);
|
||||
s1[1].ts[4].a[5] = 6;
|
||||
assert(s1[1].ts[4].a[5] == 6);
|
||||
s1.pop();
|
||||
s1.pop();
|
||||
s1.pop();
|
||||
}
|
||||
}
|
||||
@ -0,0 +1,23 @@
|
||||
pragma experimental SMTChecker;
|
||||
pragma experimental ABIEncoderV2;
|
||||
|
||||
contract C {
|
||||
struct S {
|
||||
uint x;
|
||||
uint[] a;
|
||||
}
|
||||
function f(S memory s1, S memory s2, bool b) public pure {
|
||||
S memory s3 = b ? s1 : s2;
|
||||
assert(s3.x == s1.x);
|
||||
assert(s3.x == s2.x);
|
||||
// This is safe.
|
||||
assert(s3.x == s1.x || s3.x == s2.x);
|
||||
// This fails as false positive because of lack of support to aliasing.
|
||||
s3.x = 42;
|
||||
assert(s3.x == s1.x || s3.x == s2.x);
|
||||
}
|
||||
}
|
||||
// ----
|
||||
// Warning 6328: (208-228): Assertion violation happens here
|
||||
// Warning 6328: (232-252): Assertion violation happens here
|
||||
// Warning 6328: (402-438): Assertion violation happens here
|
||||
@ -0,0 +1,30 @@
|
||||
pragma experimental SMTChecker;
|
||||
|
||||
contract C {
|
||||
struct S {
|
||||
uint x;
|
||||
uint[] a;
|
||||
}
|
||||
S s1;
|
||||
S s2;
|
||||
function f(bool b) public {
|
||||
S storage s3 = b ? s1 : s2;
|
||||
assert(s3.x == s1.x);
|
||||
assert(s3.x == s2.x);
|
||||
// This is safe.
|
||||
assert(s3.x == s1.x || s3.x == s2.x);
|
||||
// This fails as false positive because of lack of support to aliasing.
|
||||
s3.x = 42;
|
||||
assert(s3.x == s1.x || s3.x == s2.x);
|
||||
}
|
||||
function g(bool b, uint _x) public {
|
||||
if (b)
|
||||
s1.x = _x;
|
||||
else
|
||||
s2.x = _x;
|
||||
}
|
||||
}
|
||||
// ----
|
||||
// Warning 6328: (158-178): Assertion violation happens here
|
||||
// Warning 6328: (182-202): Assertion violation happens here
|
||||
// Warning 6328: (352-388): Assertion violation happens here
|
||||
@ -0,0 +1,28 @@
|
||||
pragma experimental SMTChecker;
|
||||
pragma experimental ABIEncoderV2;
|
||||
|
||||
contract C {
|
||||
struct T {
|
||||
uint y;
|
||||
uint[] a;
|
||||
}
|
||||
struct S {
|
||||
uint x;
|
||||
T t;
|
||||
uint[] a;
|
||||
T[] ts;
|
||||
}
|
||||
function f() public pure {
|
||||
S memory s1;
|
||||
s1.x = 2;
|
||||
assert(s1.x == 2);
|
||||
s1.t.y = 3;
|
||||
assert(s1.t.y == 3);
|
||||
s1.a[2] = 4;
|
||||
assert(s1.a[2] == 4);
|
||||
s1.ts[3].y = 5;
|
||||
assert(s1.ts[3].y == 5);
|
||||
s1.ts[4].a[5] = 6;
|
||||
assert(s1.ts[4].a[5] == 6);
|
||||
}
|
||||
}
|
||||
@ -0,0 +1,34 @@
|
||||
pragma experimental SMTChecker;
|
||||
pragma experimental ABIEncoderV2;
|
||||
|
||||
contract C {
|
||||
struct T {
|
||||
uint y;
|
||||
uint[] a;
|
||||
}
|
||||
struct S {
|
||||
uint x;
|
||||
T t;
|
||||
uint[] a;
|
||||
T[] ts;
|
||||
}
|
||||
function f() public pure {
|
||||
S memory s1;
|
||||
s1.x = 2;
|
||||
assert(s1.x != 2);
|
||||
s1.t.y = 3;
|
||||
assert(s1.t.y != 3);
|
||||
s1.a[2] = 4;
|
||||
assert(s1.a[2] != 4);
|
||||
s1.ts[3].y = 5;
|
||||
assert(s1.ts[3].y != 5);
|
||||
s1.ts[4].a[5] = 6;
|
||||
assert(s1.ts[4].a[5] != 6);
|
||||
}
|
||||
}
|
||||
// ----
|
||||
// Warning 6328: (228-245): Assertion violation happens here
|
||||
// Warning 6328: (263-282): Assertion violation happens here
|
||||
// Warning 6328: (301-321): Assertion violation happens here
|
||||
// Warning 6328: (343-366): Assertion violation happens here
|
||||
// Warning 6328: (391-417): Assertion violation happens here
|
||||
@ -0,0 +1,34 @@
|
||||
pragma experimental SMTChecker;
|
||||
pragma experimental ABIEncoderV2;
|
||||
|
||||
contract C {
|
||||
struct T {
|
||||
uint y;
|
||||
uint[] a;
|
||||
}
|
||||
struct S {
|
||||
uint x;
|
||||
T t;
|
||||
uint[] a;
|
||||
T[] ts;
|
||||
}
|
||||
function f(S memory s2) public pure {
|
||||
S memory s1;
|
||||
s1.x = 2;
|
||||
assert(s1.x == s2.x);
|
||||
s1.t.y = 3;
|
||||
assert(s1.t.y == s2.t.y);
|
||||
s1.a[2] = 4;
|
||||
assert(s1.a[2] == s2.a[2]);
|
||||
s1.ts[3].y = 5;
|
||||
assert(s1.ts[3].y == s2.ts[3].y);
|
||||
s1.ts[4].a[5] = 6;
|
||||
assert(s1.ts[4].a[5] == s2.ts[4].a[5]);
|
||||
}
|
||||
}
|
||||
// ----
|
||||
// Warning 6328: (239-259): Assertion violation happens here
|
||||
// Warning 6328: (277-301): Assertion violation happens here
|
||||
// Warning 6328: (320-346): Assertion violation happens here
|
||||
// Warning 6328: (368-400): Assertion violation happens here
|
||||
// Warning 6328: (425-463): Assertion violation happens here
|
||||
@ -0,0 +1,27 @@
|
||||
pragma experimental SMTChecker;
|
||||
|
||||
contract C {
|
||||
struct T {
|
||||
uint y;
|
||||
uint[] a;
|
||||
}
|
||||
struct S {
|
||||
uint x;
|
||||
T t;
|
||||
uint[] a;
|
||||
T[] ts;
|
||||
}
|
||||
S s1;
|
||||
function f() public {
|
||||
s1.x = 2;
|
||||
assert(s1.x == 2);
|
||||
s1.t.y = 3;
|
||||
assert(s1.t.y == 3);
|
||||
s1.a[2] = 4;
|
||||
assert(s1.a[2] == 4);
|
||||
s1.ts[3].y = 5;
|
||||
assert(s1.ts[3].y == 5);
|
||||
s1.ts[4].a[5] = 6;
|
||||
assert(s1.ts[4].a[5] == 6);
|
||||
}
|
||||
}
|
||||
@ -0,0 +1,33 @@
|
||||
pragma experimental SMTChecker;
|
||||
|
||||
contract C {
|
||||
struct T {
|
||||
uint y;
|
||||
uint[] a;
|
||||
}
|
||||
struct S {
|
||||
uint x;
|
||||
T t;
|
||||
uint[] a;
|
||||
T[] ts;
|
||||
}
|
||||
S s1;
|
||||
function f() public {
|
||||
s1.x = 2;
|
||||
assert(s1.x != 2);
|
||||
s1.t.y = 3;
|
||||
assert(s1.t.y != 3);
|
||||
s1.a[2] = 4;
|
||||
assert(s1.a[2] != 4);
|
||||
s1.ts[3].y = 5;
|
||||
assert(s1.ts[3].y != 5);
|
||||
s1.ts[4].a[5] = 6;
|
||||
assert(s1.ts[4].a[5] != 6);
|
||||
}
|
||||
}
|
||||
// ----
|
||||
// Warning 6328: (181-198): Assertion violation happens here
|
||||
// Warning 6328: (216-235): Assertion violation happens here
|
||||
// Warning 6328: (254-274): Assertion violation happens here
|
||||
// Warning 6328: (296-319): Assertion violation happens here
|
||||
// Warning 6328: (344-370): Assertion violation happens here.
|
||||
@ -0,0 +1,18 @@
|
||||
pragma experimental SMTChecker;
|
||||
pragma experimental ABIEncoderV2;
|
||||
|
||||
contract C {
|
||||
struct S {
|
||||
uint x;
|
||||
uint[] a;
|
||||
}
|
||||
function f(S memory s1, S memory s2) public pure {
|
||||
delete s1;
|
||||
assert(s1.x == s2.x);
|
||||
assert(s1.a.length == s2.a.length);
|
||||
assert(s1.a.length == 0);
|
||||
}
|
||||
}
|
||||
// ----
|
||||
// Warning 6328: (184-204): Assertion violation happens here
|
||||
// Warning 6328: (208-242): Assertion violation happens here
|
||||
@ -0,0 +1,23 @@
|
||||
pragma experimental SMTChecker;
|
||||
pragma experimental ABIEncoderV2;
|
||||
|
||||
contract C {
|
||||
struct S {
|
||||
uint x;
|
||||
uint[] a;
|
||||
}
|
||||
S s1;
|
||||
function g(S memory s2) public {
|
||||
s1.x = s2.x;
|
||||
s1.a = s2.a;
|
||||
}
|
||||
function f(S memory s2) public {
|
||||
delete s1;
|
||||
assert(s1.x == s2.x);
|
||||
assert(s1.a.length == s2.a.length);
|
||||
assert(s1.a.length == 0);
|
||||
}
|
||||
}
|
||||
// ----
|
||||
// Warning 6328: (240-260): Assertion violation happens here
|
||||
// Warning 6328: (264-298): Assertion violation happens here
|
||||
@ -0,0 +1,18 @@
|
||||
pragma experimental SMTChecker;
|
||||
|
||||
contract C {
|
||||
struct S {
|
||||
uint x;
|
||||
mapping (uint => uint) m;
|
||||
}
|
||||
S s1;
|
||||
S s2;
|
||||
function f() public view {
|
||||
assert(s1.m[0] == s2.m[0]);
|
||||
}
|
||||
function g(uint a, uint b) public {
|
||||
s1.m[a] = b;
|
||||
}
|
||||
}
|
||||
// ----
|
||||
// Warning 4661: (143-169): Assertion violation happens here
|
||||
@ -0,0 +1,27 @@
|
||||
pragma experimental SMTChecker;
|
||||
|
||||
contract C {
|
||||
struct S {
|
||||
uint x;
|
||||
S[] a;
|
||||
}
|
||||
S s1;
|
||||
S s2;
|
||||
function f() public view {
|
||||
assert(s1.x == s2.x);
|
||||
assert(s1.a.length == s2.a.length);
|
||||
}
|
||||
}
|
||||
// ----
|
||||
// Warning 6328: (124-144): Assertion violation happens here
|
||||
// Warning 6328: (148-182): Assertion violation happens here
|
||||
// Warning 8115: (81-85): Assertion checker does not yet support the type of this variable.
|
||||
// Warning 8115: (88-92): Assertion checker does not yet support the type of this variable.
|
||||
// Warning 7650: (131-135): Assertion checker does not yet support this expression.
|
||||
// Warning 8364: (131-133): Assertion checker does not yet implement type struct C.S storage ref
|
||||
// Warning 7650: (139-143): Assertion checker does not yet support this expression.
|
||||
// Warning 8364: (139-141): Assertion checker does not yet implement type struct C.S storage ref
|
||||
// Warning 7650: (155-159): Assertion checker does not yet support this expression.
|
||||
// Warning 8364: (155-157): Assertion checker does not yet implement type struct C.S storage ref
|
||||
// Warning 7650: (170-174): Assertion checker does not yet support this expression.
|
||||
// Warning 8364: (170-172): Assertion checker does not yet implement type struct C.S storage ref
|
||||
@ -0,0 +1,69 @@
|
||||
pragma experimental SMTChecker;
|
||||
|
||||
contract C {
|
||||
struct S {
|
||||
uint x;
|
||||
S[] a;
|
||||
}
|
||||
S s1;
|
||||
S s2;
|
||||
function f() public view {
|
||||
assert(s1.x == s2.x);
|
||||
assert(s1.a.length == s2.a.length);
|
||||
assert(s1.a[0].x == s2.a[0].x);
|
||||
}
|
||||
function g() public {
|
||||
s1.x = 42;
|
||||
s2.x = 42;
|
||||
s1.a.push();
|
||||
s2.a.push();
|
||||
s1.a[0].x = 43;
|
||||
s2.a[0].x = 43;
|
||||
}
|
||||
}
|
||||
// ----
|
||||
// Warning 6328: (124-144): Assertion violation happens here
|
||||
// Warning 6328: (148-182): Assertion violation happens here
|
||||
// Warning 6328: (186-216): Assertion violation happens here
|
||||
// Warning 8115: (81-85): Assertion checker does not yet support the type of this variable.
|
||||
// Warning 8115: (88-92): Assertion checker does not yet support the type of this variable.
|
||||
// Warning 7650: (131-135): Assertion checker does not yet support this expression.
|
||||
// Warning 8364: (131-133): Assertion checker does not yet implement type struct C.S storage ref
|
||||
// Warning 7650: (139-143): Assertion checker does not yet support this expression.
|
||||
// Warning 8364: (139-141): Assertion checker does not yet implement type struct C.S storage ref
|
||||
// Warning 7650: (155-159): Assertion checker does not yet support this expression.
|
||||
// Warning 8364: (155-157): Assertion checker does not yet implement type struct C.S storage ref
|
||||
// Warning 7650: (170-174): Assertion checker does not yet support this expression.
|
||||
// Warning 8364: (170-172): Assertion checker does not yet implement type struct C.S storage ref
|
||||
// Warning 7650: (193-202): Assertion checker does not yet support this expression.
|
||||
// Warning 7650: (193-197): Assertion checker does not yet support this expression.
|
||||
// Warning 8364: (193-195): Assertion checker does not yet implement type struct C.S storage ref
|
||||
// Warning 8364: (193-200): Assertion checker does not yet implement type struct C.S storage ref
|
||||
// Warning 7650: (206-215): Assertion checker does not yet support this expression.
|
||||
// Warning 7650: (206-210): Assertion checker does not yet support this expression.
|
||||
// Warning 8364: (206-208): Assertion checker does not yet implement type struct C.S storage ref
|
||||
// Warning 8364: (206-213): Assertion checker does not yet implement type struct C.S storage ref
|
||||
// Warning 7650: (246-250): Assertion checker does not yet support this expression.
|
||||
// Warning 8364: (246-248): Assertion checker does not yet implement type struct C.S storage ref
|
||||
// Warning 4375: (246-250): Assertion checker does not support recursive structs.
|
||||
// Warning 7650: (259-263): Assertion checker does not yet support this expression.
|
||||
// Warning 8364: (259-261): Assertion checker does not yet implement type struct C.S storage ref
|
||||
// Warning 4375: (259-263): Assertion checker does not support recursive structs.
|
||||
// Warning 7650: (272-276): Assertion checker does not yet support this expression.
|
||||
// Warning 8364: (272-274): Assertion checker does not yet implement type struct C.S storage ref
|
||||
// Warning 8364: (272-283): Assertion checker does not yet implement type struct C.S storage ref
|
||||
// Warning 4375: (272-276): Assertion checker does not support recursive structs.
|
||||
// Warning 7650: (287-291): Assertion checker does not yet support this expression.
|
||||
// Warning 8364: (287-289): Assertion checker does not yet implement type struct C.S storage ref
|
||||
// Warning 8364: (287-298): Assertion checker does not yet implement type struct C.S storage ref
|
||||
// Warning 4375: (287-291): Assertion checker does not support recursive structs.
|
||||
// Warning 7650: (302-311): Assertion checker does not yet support this expression.
|
||||
// Warning 7650: (302-306): Assertion checker does not yet support this expression.
|
||||
// Warning 8364: (302-304): Assertion checker does not yet implement type struct C.S storage ref
|
||||
// Warning 8364: (302-309): Assertion checker does not yet implement type struct C.S storage ref
|
||||
// Warning 4375: (302-311): Assertion checker does not support recursive structs.
|
||||
// Warning 7650: (320-329): Assertion checker does not yet support this expression.
|
||||
// Warning 7650: (320-324): Assertion checker does not yet support this expression.
|
||||
// Warning 8364: (320-322): Assertion checker does not yet implement type struct C.S storage ref
|
||||
// Warning 8364: (320-327): Assertion checker does not yet implement type struct C.S storage ref
|
||||
// Warning 4375: (320-329): Assertion checker does not support recursive structs.
|
||||
@ -0,0 +1,123 @@
|
||||
pragma experimental SMTChecker;
|
||||
|
||||
contract C {
|
||||
struct S {
|
||||
uint x;
|
||||
S[] a;
|
||||
}
|
||||
S s1;
|
||||
S s2;
|
||||
function f() public view {
|
||||
assert(s1.x == s2.x);
|
||||
assert(s1.a.length == s2.a.length);
|
||||
assert(s1.a[0].x == s2.a[0].x);
|
||||
assert(s1.a[0].a.length == s2.a[0].a.length);
|
||||
assert(s1.a[0].a[0].x == s2.a[0].a[0].x);
|
||||
}
|
||||
function g() public {
|
||||
s1.x = 42;
|
||||
s2.x = 42;
|
||||
s1.a.push();
|
||||
s2.a.push();
|
||||
s1.a[0].x = 43;
|
||||
s2.a[0].x = 43;
|
||||
s1.a[0].a.push();
|
||||
s2.a[0].a.push();
|
||||
s1.a[0].a[0].x = 44;
|
||||
s2.a[0].a[0].x = 44;
|
||||
}
|
||||
}
|
||||
// ----
|
||||
// Warning 6328: (124-144): Assertion violation happens here
|
||||
// Warning 6328: (148-182): Assertion violation happens here
|
||||
// Warning 6328: (186-216): Assertion violation happens here
|
||||
// Warning 6328: (220-264): Assertion violation happens here
|
||||
// Warning 6328: (268-308): Assertion violation happens here
|
||||
// Warning 8115: (81-85): Assertion checker does not yet support the type of this variable.
|
||||
// Warning 8115: (88-92): Assertion checker does not yet support the type of this variable.
|
||||
// Warning 7650: (131-135): Assertion checker does not yet support this expression.
|
||||
// Warning 8364: (131-133): Assertion checker does not yet implement type struct C.S storage ref
|
||||
// Warning 7650: (139-143): Assertion checker does not yet support this expression.
|
||||
// Warning 8364: (139-141): Assertion checker does not yet implement type struct C.S storage ref
|
||||
// Warning 7650: (155-159): Assertion checker does not yet support this expression.
|
||||
// Warning 8364: (155-157): Assertion checker does not yet implement type struct C.S storage ref
|
||||
// Warning 7650: (170-174): Assertion checker does not yet support this expression.
|
||||
// Warning 8364: (170-172): Assertion checker does not yet implement type struct C.S storage ref
|
||||
// Warning 7650: (193-202): Assertion checker does not yet support this expression.
|
||||
// Warning 7650: (193-197): Assertion checker does not yet support this expression.
|
||||
// Warning 8364: (193-195): Assertion checker does not yet implement type struct C.S storage ref
|
||||
// Warning 8364: (193-200): Assertion checker does not yet implement type struct C.S storage ref
|
||||
// Warning 7650: (206-215): Assertion checker does not yet support this expression.
|
||||
// Warning 7650: (206-210): Assertion checker does not yet support this expression.
|
||||
// Warning 8364: (206-208): Assertion checker does not yet implement type struct C.S storage ref
|
||||
// Warning 8364: (206-213): Assertion checker does not yet implement type struct C.S storage ref
|
||||
// Warning 7650: (227-236): Assertion checker does not yet support this expression.
|
||||
// Warning 7650: (227-231): Assertion checker does not yet support this expression.
|
||||
// Warning 8364: (227-229): Assertion checker does not yet implement type struct C.S storage ref
|
||||
// Warning 8364: (227-234): Assertion checker does not yet implement type struct C.S storage ref
|
||||
// Warning 7650: (247-256): Assertion checker does not yet support this expression.
|
||||
// Warning 7650: (247-251): Assertion checker does not yet support this expression.
|
||||
// Warning 8364: (247-249): Assertion checker does not yet implement type struct C.S storage ref
|
||||
// Warning 8364: (247-254): Assertion checker does not yet implement type struct C.S storage ref
|
||||
// Warning 7650: (275-289): Assertion checker does not yet support this expression.
|
||||
// Warning 7650: (275-284): Assertion checker does not yet support this expression.
|
||||
// Warning 7650: (275-279): Assertion checker does not yet support this expression.
|
||||
// Warning 8364: (275-277): Assertion checker does not yet implement type struct C.S storage ref
|
||||
// Warning 8364: (275-282): Assertion checker does not yet implement type struct C.S storage ref
|
||||
// Warning 8364: (275-287): Assertion checker does not yet implement type struct C.S storage ref
|
||||
// Warning 7650: (293-307): Assertion checker does not yet support this expression.
|
||||
// Warning 7650: (293-302): Assertion checker does not yet support this expression.
|
||||
// Warning 7650: (293-297): Assertion checker does not yet support this expression.
|
||||
// Warning 8364: (293-295): Assertion checker does not yet implement type struct C.S storage ref
|
||||
// Warning 8364: (293-300): Assertion checker does not yet implement type struct C.S storage ref
|
||||
// Warning 8364: (293-305): Assertion checker does not yet implement type struct C.S storage ref
|
||||
// Warning 7650: (338-342): Assertion checker does not yet support this expression.
|
||||
// Warning 8364: (338-340): Assertion checker does not yet implement type struct C.S storage ref
|
||||
// Warning 4375: (338-342): Assertion checker does not support recursive structs.
|
||||
// Warning 7650: (351-355): Assertion checker does not yet support this expression.
|
||||
// Warning 8364: (351-353): Assertion checker does not yet implement type struct C.S storage ref
|
||||
// Warning 4375: (351-355): Assertion checker does not support recursive structs.
|
||||
// Warning 7650: (364-368): Assertion checker does not yet support this expression.
|
||||
// Warning 8364: (364-366): Assertion checker does not yet implement type struct C.S storage ref
|
||||
// Warning 8364: (364-375): Assertion checker does not yet implement type struct C.S storage ref
|
||||
// Warning 4375: (364-368): Assertion checker does not support recursive structs.
|
||||
// Warning 7650: (379-383): Assertion checker does not yet support this expression.
|
||||
// Warning 8364: (379-381): Assertion checker does not yet implement type struct C.S storage ref
|
||||
// Warning 8364: (379-390): Assertion checker does not yet implement type struct C.S storage ref
|
||||
// Warning 4375: (379-383): Assertion checker does not support recursive structs.
|
||||
// Warning 7650: (394-403): Assertion checker does not yet support this expression.
|
||||
// Warning 7650: (394-398): Assertion checker does not yet support this expression.
|
||||
// Warning 8364: (394-396): Assertion checker does not yet implement type struct C.S storage ref
|
||||
// Warning 8364: (394-401): Assertion checker does not yet implement type struct C.S storage ref
|
||||
// Warning 4375: (394-403): Assertion checker does not support recursive structs.
|
||||
// Warning 7650: (412-421): Assertion checker does not yet support this expression.
|
||||
// Warning 7650: (412-416): Assertion checker does not yet support this expression.
|
||||
// Warning 8364: (412-414): Assertion checker does not yet implement type struct C.S storage ref
|
||||
// Warning 8364: (412-419): Assertion checker does not yet implement type struct C.S storage ref
|
||||
// Warning 4375: (412-421): Assertion checker does not support recursive structs.
|
||||
// Warning 7650: (430-439): Assertion checker does not yet support this expression.
|
||||
// Warning 7650: (430-434): Assertion checker does not yet support this expression.
|
||||
// Warning 8364: (430-432): Assertion checker does not yet implement type struct C.S storage ref
|
||||
// Warning 8364: (430-437): Assertion checker does not yet implement type struct C.S storage ref
|
||||
// Warning 8364: (430-446): Assertion checker does not yet implement type struct C.S storage ref
|
||||
// Warning 4375: (430-439): Assertion checker does not support recursive structs.
|
||||
// Warning 7650: (450-459): Assertion checker does not yet support this expression.
|
||||
// Warning 7650: (450-454): Assertion checker does not yet support this expression.
|
||||
// Warning 8364: (450-452): Assertion checker does not yet implement type struct C.S storage ref
|
||||
// Warning 8364: (450-457): Assertion checker does not yet implement type struct C.S storage ref
|
||||
// Warning 8364: (450-466): Assertion checker does not yet implement type struct C.S storage ref
|
||||
// Warning 4375: (450-459): Assertion checker does not support recursive structs.
|
||||
// Warning 7650: (470-484): Assertion checker does not yet support this expression.
|
||||
// Warning 7650: (470-479): Assertion checker does not yet support this expression.
|
||||
// Warning 7650: (470-474): Assertion checker does not yet support this expression.
|
||||
// Warning 8364: (470-472): Assertion checker does not yet implement type struct C.S storage ref
|
||||
// Warning 8364: (470-477): Assertion checker does not yet implement type struct C.S storage ref
|
||||
// Warning 8364: (470-482): Assertion checker does not yet implement type struct C.S storage ref
|
||||
// Warning 4375: (470-484): Assertion checker does not support recursive structs.
|
||||
// Warning 7650: (493-507): Assertion checker does not yet support this expression.
|
||||
// Warning 7650: (493-502): Assertion checker does not yet support this expression.
|
||||
// Warning 7650: (493-497): Assertion checker does not yet support this expression.
|
||||
// Warning 8364: (493-495): Assertion checker does not yet implement type struct C.S storage ref
|
||||
// Warning 8364: (493-500): Assertion checker does not yet implement type struct C.S storage ref
|
||||
// Warning 8364: (493-505): Assertion checker does not yet implement type struct C.S storage ref
|
||||
// Warning 4375: (493-507): Assertion checker does not support recursive structs.
|
||||
@ -0,0 +1,56 @@
|
||||
pragma experimental SMTChecker;
|
||||
|
||||
contract C {
|
||||
struct S {
|
||||
uint x;
|
||||
S[] a;
|
||||
}
|
||||
S s1;
|
||||
S s2;
|
||||
function f(bool b1, bool b2) public {
|
||||
S storage s3 = b1 ? s1 : s2;
|
||||
S storage s4 = b2 ? s1 : s2;
|
||||
assert(s3.x == s1.x || s3.x == s2.x);
|
||||
assert(s4.x == s1.x || s4.x == s2.x);
|
||||
s3.x = 44;
|
||||
// Fails as false positive because of lack of support to aliasing.
|
||||
assert(s1.x == 44 || s2.x == 44);
|
||||
}
|
||||
}
|
||||
// ----
|
||||
// Warning 6328: (197-233): Assertion violation happens here
|
||||
// Warning 6328: (237-273): Assertion violation happens here
|
||||
// Warning 6328: (359-391): Assertion violation happens here
|
||||
// Warning 8115: (81-85): Assertion checker does not yet support the type of this variable.
|
||||
// Warning 8115: (88-92): Assertion checker does not yet support the type of this variable.
|
||||
// Warning 8115: (135-147): Assertion checker does not yet support the type of this variable.
|
||||
// Warning 8115: (166-178): Assertion checker does not yet support the type of this variable.
|
||||
// Warning 8364: (155-157): Assertion checker does not yet implement type struct C.S storage ref
|
||||
// Warning 8364: (160-162): Assertion checker does not yet implement type struct C.S storage ref
|
||||
// Warning 8364: (150-162): Assertion checker does not yet implement type struct C.S storage pointer
|
||||
// Warning 8364: (186-188): Assertion checker does not yet implement type struct C.S storage ref
|
||||
// Warning 8364: (191-193): Assertion checker does not yet implement type struct C.S storage ref
|
||||
// Warning 8364: (181-193): Assertion checker does not yet implement type struct C.S storage pointer
|
||||
// Warning 7650: (204-208): Assertion checker does not yet support this expression.
|
||||
// Warning 8364: (204-206): Assertion checker does not yet implement type struct C.S storage pointer
|
||||
// Warning 7650: (212-216): Assertion checker does not yet support this expression.
|
||||
// Warning 8364: (212-214): Assertion checker does not yet implement type struct C.S storage ref
|
||||
// Warning 7650: (220-224): Assertion checker does not yet support this expression.
|
||||
// Warning 8364: (220-222): Assertion checker does not yet implement type struct C.S storage pointer
|
||||
// Warning 7650: (228-232): Assertion checker does not yet support this expression.
|
||||
// Warning 8364: (228-230): Assertion checker does not yet implement type struct C.S storage ref
|
||||
// Warning 7650: (244-248): Assertion checker does not yet support this expression.
|
||||
// Warning 8364: (244-246): Assertion checker does not yet implement type struct C.S storage pointer
|
||||
// Warning 7650: (252-256): Assertion checker does not yet support this expression.
|
||||
// Warning 8364: (252-254): Assertion checker does not yet implement type struct C.S storage ref
|
||||
// Warning 7650: (260-264): Assertion checker does not yet support this expression.
|
||||
// Warning 8364: (260-262): Assertion checker does not yet implement type struct C.S storage pointer
|
||||
// Warning 7650: (268-272): Assertion checker does not yet support this expression.
|
||||
// Warning 8364: (268-270): Assertion checker does not yet implement type struct C.S storage ref
|
||||
// Warning 7650: (277-281): Assertion checker does not yet support this expression.
|
||||
// Warning 8364: (277-279): Assertion checker does not yet implement type struct C.S storage pointer
|
||||
// Warning 4375: (277-281): Assertion checker does not support recursive structs.
|
||||
// Warning 7650: (366-370): Assertion checker does not yet support this expression.
|
||||
// Warning 8364: (366-368): Assertion checker does not yet implement type struct C.S storage ref
|
||||
// Warning 7650: (380-384): Assertion checker does not yet support this expression.
|
||||
// Warning 8364: (380-382): Assertion checker does not yet implement type struct C.S storage ref
|
||||
@ -0,0 +1,29 @@
|
||||
pragma experimental SMTChecker;
|
||||
|
||||
contract C {
|
||||
struct S {
|
||||
uint x;
|
||||
S[] a;
|
||||
}
|
||||
S[] sa;
|
||||
S[][] sa2;
|
||||
function f() public {
|
||||
sa.push();
|
||||
sa2.push();
|
||||
sa2[0].push();
|
||||
sa2[0][0].a.push();
|
||||
assert(sa2[0][0].a.length == sa[0].a.length);
|
||||
}
|
||||
}
|
||||
// ----
|
||||
// Warning 6328: (192-236): Assertion violation happens here
|
||||
// Warning 8364: (126-135): Assertion checker does not yet implement type struct C.S storage ref
|
||||
// Warning 8364: (153-166): Assertion checker does not yet implement type struct C.S storage ref
|
||||
// Warning 7650: (170-181): Assertion checker does not yet support this expression.
|
||||
// Warning 8364: (170-179): Assertion checker does not yet implement type struct C.S storage ref
|
||||
// Warning 8364: (170-188): Assertion checker does not yet implement type struct C.S storage ref
|
||||
// Warning 4375: (170-181): Assertion checker does not support recursive structs.
|
||||
// Warning 7650: (199-210): Assertion checker does not yet support this expression.
|
||||
// Warning 8364: (199-208): Assertion checker does not yet implement type struct C.S storage ref
|
||||
// Warning 7650: (221-228): Assertion checker does not yet support this expression.
|
||||
// Warning 8364: (221-226): Assertion checker does not yet implement type struct C.S storage ref
|
||||
@ -0,0 +1,66 @@
|
||||
pragma experimental SMTChecker;
|
||||
|
||||
contract C {
|
||||
struct S {
|
||||
uint x;
|
||||
S[] a;
|
||||
}
|
||||
S s1;
|
||||
S s2;
|
||||
function f() public {
|
||||
s1.x = 10;
|
||||
++s1.x;
|
||||
s1.x++;
|
||||
s2.x = 20;
|
||||
--s2.x;
|
||||
s2.x--;
|
||||
assert(s1.x == s2.x + 6);
|
||||
assert(s1.a.length == s2.a.length);
|
||||
delete s1;
|
||||
assert(s1.x == 0);
|
||||
}
|
||||
}
|
||||
// ----
|
||||
// Warning 4984: (200-208): Overflow (resulting value larger than 2**256 - 1) happens here
|
||||
// Warning 6328: (185-209): Assertion violation happens here
|
||||
// Warning 6328: (213-247): Assertion violation happens here
|
||||
// Warning 6328: (264-281): Assertion violation happens here
|
||||
// Warning 8115: (81-85): Assertion checker does not yet support the type of this variable.
|
||||
// Warning 8115: (88-92): Assertion checker does not yet support the type of this variable.
|
||||
// Warning 7650: (119-123): Assertion checker does not yet support this expression.
|
||||
// Warning 8364: (119-121): Assertion checker does not yet implement type struct C.S storage ref
|
||||
// Warning 4375: (119-123): Assertion checker does not support recursive structs.
|
||||
// Warning 7650: (134-138): Assertion checker does not yet support this expression.
|
||||
// Warning 8364: (134-136): Assertion checker does not yet implement type struct C.S storage ref
|
||||
// Warning 4375: (134-138): Assertion checker does not support recursive structs.
|
||||
// Warning 7650: (142-146): Assertion checker does not yet support this expression.
|
||||
// Warning 8364: (142-144): Assertion checker does not yet implement type struct C.S storage ref
|
||||
// Warning 4375: (142-146): Assertion checker does not support recursive structs.
|
||||
// Warning 7650: (152-156): Assertion checker does not yet support this expression.
|
||||
// Warning 8364: (152-154): Assertion checker does not yet implement type struct C.S storage ref
|
||||
// Warning 4375: (152-156): Assertion checker does not support recursive structs.
|
||||
// Warning 7650: (167-171): Assertion checker does not yet support this expression.
|
||||
// Warning 8364: (167-169): Assertion checker does not yet implement type struct C.S storage ref
|
||||
// Warning 4375: (167-171): Assertion checker does not support recursive structs.
|
||||
// Warning 7650: (175-179): Assertion checker does not yet support this expression.
|
||||
// Warning 8364: (175-177): Assertion checker does not yet implement type struct C.S storage ref
|
||||
// Warning 4375: (175-179): Assertion checker does not support recursive structs.
|
||||
// Warning 7650: (192-196): Assertion checker does not yet support this expression.
|
||||
// Warning 8364: (192-194): Assertion checker does not yet implement type struct C.S storage ref
|
||||
// Warning 7650: (200-204): Assertion checker does not yet support this expression.
|
||||
// Warning 8364: (200-202): Assertion checker does not yet implement type struct C.S storage ref
|
||||
// Warning 7650: (220-224): Assertion checker does not yet support this expression.
|
||||
// Warning 8364: (220-222): Assertion checker does not yet implement type struct C.S storage ref
|
||||
// Warning 7650: (235-239): Assertion checker does not yet support this expression.
|
||||
// Warning 8364: (235-237): Assertion checker does not yet implement type struct C.S storage ref
|
||||
// Warning 8364: (258-260): Assertion checker does not yet implement type struct C.S storage ref
|
||||
// Warning 7650: (271-275): Assertion checker does not yet support this expression.
|
||||
// Warning 8364: (271-273): Assertion checker does not yet implement type struct C.S storage ref
|
||||
// Warning 4144: (132-138): Underflow (resulting value less than 0) happens here
|
||||
// Warning 2661: (132-138): Overflow (resulting value larger than 2**256 - 1) happens here
|
||||
// Warning 4144: (142-148): Underflow (resulting value less than 0) happens here
|
||||
// Warning 2661: (142-148): Overflow (resulting value larger than 2**256 - 1) happens here
|
||||
// Warning 4144: (165-171): Underflow (resulting value less than 0) happens here
|
||||
// Warning 2661: (165-171): Overflow (resulting value larger than 2**256 - 1) happens here
|
||||
// Warning 4144: (175-181): Underflow (resulting value less than 0) happens here
|
||||
// Warning 2661: (175-181): Overflow (resulting value larger than 2**256 - 1) happens here
|
||||
@ -0,0 +1,31 @@
|
||||
pragma experimental SMTChecker;
|
||||
|
||||
contract C {
|
||||
struct S {
|
||||
uint x;
|
||||
T[] a;
|
||||
}
|
||||
struct T {
|
||||
uint y;
|
||||
S[] a;
|
||||
}
|
||||
S s1;
|
||||
S s2;
|
||||
function f() public view {
|
||||
assert(s1.x == s2.x);
|
||||
assert(s1.a.length == s2.a.length);
|
||||
}
|
||||
}
|
||||
// ----
|
||||
// Warning 6328: (158-178): Assertion violation happens here
|
||||
// Warning 6328: (182-216): Assertion violation happens here
|
||||
// Warning 8115: (115-119): Assertion checker does not yet support the type of this variable.
|
||||
// Warning 8115: (122-126): Assertion checker does not yet support the type of this variable.
|
||||
// Warning 7650: (165-169): Assertion checker does not yet support this expression.
|
||||
// Warning 8364: (165-167): Assertion checker does not yet implement type struct C.S storage ref
|
||||
// Warning 7650: (173-177): Assertion checker does not yet support this expression.
|
||||
// Warning 8364: (173-175): Assertion checker does not yet implement type struct C.S storage ref
|
||||
// Warning 7650: (189-193): Assertion checker does not yet support this expression.
|
||||
// Warning 8364: (189-191): Assertion checker does not yet implement type struct C.S storage ref
|
||||
// Warning 7650: (204-208): Assertion checker does not yet support this expression.
|
||||
// Warning 8364: (204-206): Assertion checker does not yet implement type struct C.S storage ref
|
||||
@ -0,0 +1,57 @@
|
||||
pragma experimental SMTChecker;
|
||||
|
||||
contract C {
|
||||
struct S {
|
||||
uint x;
|
||||
T[] a;
|
||||
}
|
||||
struct T {
|
||||
uint y;
|
||||
S[] a;
|
||||
}
|
||||
S s1;
|
||||
S s2;
|
||||
function f() public {
|
||||
s1.a.push();
|
||||
s2.a.push();
|
||||
s1.a[0].a.push();
|
||||
s2.a[0].a.push();
|
||||
assert(s1.a[0].a[0].x == s2.a[0].a[0].x);
|
||||
}
|
||||
}
|
||||
// ----
|
||||
// Warning 6328: (223-263): Assertion violation happens here
|
||||
// Warning 8115: (115-119): Assertion checker does not yet support the type of this variable.
|
||||
// Warning 8115: (122-126): Assertion checker does not yet support the type of this variable.
|
||||
// Warning 7650: (153-157): Assertion checker does not yet support this expression.
|
||||
// Warning 8364: (153-155): Assertion checker does not yet implement type struct C.S storage ref
|
||||
// Warning 8364: (153-164): Assertion checker does not yet implement type struct C.T storage ref
|
||||
// Warning 4375: (153-157): Assertion checker does not support recursive structs.
|
||||
// Warning 7650: (168-172): Assertion checker does not yet support this expression.
|
||||
// Warning 8364: (168-170): Assertion checker does not yet implement type struct C.S storage ref
|
||||
// Warning 8364: (168-179): Assertion checker does not yet implement type struct C.T storage ref
|
||||
// Warning 4375: (168-172): Assertion checker does not support recursive structs.
|
||||
// Warning 7650: (183-192): Assertion checker does not yet support this expression.
|
||||
// Warning 7650: (183-187): Assertion checker does not yet support this expression.
|
||||
// Warning 8364: (183-185): Assertion checker does not yet implement type struct C.S storage ref
|
||||
// Warning 8364: (183-190): Assertion checker does not yet implement type struct C.T storage ref
|
||||
// Warning 8364: (183-199): Assertion checker does not yet implement type struct C.S storage ref
|
||||
// Warning 4375: (183-192): Assertion checker does not support recursive structs.
|
||||
// Warning 7650: (203-212): Assertion checker does not yet support this expression.
|
||||
// Warning 7650: (203-207): Assertion checker does not yet support this expression.
|
||||
// Warning 8364: (203-205): Assertion checker does not yet implement type struct C.S storage ref
|
||||
// Warning 8364: (203-210): Assertion checker does not yet implement type struct C.T storage ref
|
||||
// Warning 8364: (203-219): Assertion checker does not yet implement type struct C.S storage ref
|
||||
// Warning 4375: (203-212): Assertion checker does not support recursive structs.
|
||||
// Warning 7650: (230-244): Assertion checker does not yet support this expression.
|
||||
// Warning 7650: (230-239): Assertion checker does not yet support this expression.
|
||||
// Warning 7650: (230-234): Assertion checker does not yet support this expression.
|
||||
// Warning 8364: (230-232): Assertion checker does not yet implement type struct C.S storage ref
|
||||
// Warning 8364: (230-237): Assertion checker does not yet implement type struct C.T storage ref
|
||||
// Warning 8364: (230-242): Assertion checker does not yet implement type struct C.S storage ref
|
||||
// Warning 7650: (248-262): Assertion checker does not yet support this expression.
|
||||
// Warning 7650: (248-257): Assertion checker does not yet support this expression.
|
||||
// Warning 7650: (248-252): Assertion checker does not yet support this expression.
|
||||
// Warning 8364: (248-250): Assertion checker does not yet implement type struct C.S storage ref
|
||||
// Warning 8364: (248-255): Assertion checker does not yet implement type struct C.T storage ref
|
||||
// Warning 8364: (248-260): Assertion checker does not yet implement type struct C.S storage ref
|
||||
@ -0,0 +1,20 @@
|
||||
pragma experimental SMTChecker;
|
||||
|
||||
contract C {
|
||||
struct S {
|
||||
uint x;
|
||||
uint[] a;
|
||||
}
|
||||
function s() internal pure returns (S memory s1) {
|
||||
s1.x = 42;
|
||||
s1.a[2] = 43;
|
||||
}
|
||||
function f() public pure {
|
||||
S memory s2 = s();
|
||||
assert(s2.x == 42);
|
||||
assert(s2.a[2] == 43);
|
||||
assert(s2.a[3] == 43);
|
||||
}
|
||||
}
|
||||
// ----
|
||||
// Warning 6328: (265-286): Assertion violation happens here
|
||||
@ -0,0 +1,16 @@
|
||||
pragma experimental SMTChecker;
|
||||
|
||||
contract C {
|
||||
struct S {
|
||||
uint x;
|
||||
uint[] a;
|
||||
}
|
||||
S s;
|
||||
function f(uint _x) public {
|
||||
s.x = _x;
|
||||
s.a[0] = _x;
|
||||
assert(s.a[1] == s.a[0]);
|
||||
}
|
||||
}
|
||||
// ----
|
||||
// Warning 6328: (148-172): Assertion violation happens here.
|
||||
@ -0,0 +1,25 @@
|
||||
pragma experimental SMTChecker;
|
||||
|
||||
contract C {
|
||||
struct S {
|
||||
uint x;
|
||||
uint[] a;
|
||||
}
|
||||
S s;
|
||||
function f(uint _x) public {
|
||||
s.a.pop();
|
||||
s.a.length;
|
||||
s.a.push();
|
||||
s.x = _x;
|
||||
s.a.pop();
|
||||
s.a.push();
|
||||
s.a.push();
|
||||
s.a[0] = _x;
|
||||
assert(s.a[1] == s.a[0]);
|
||||
s.a.pop();
|
||||
s.a.pop();
|
||||
}
|
||||
}
|
||||
// ----
|
||||
// Warning 2529: (121-130): Empty array "pop" detected here
|
||||
// Warning 6328: (230-254): Assertion violation happens here
|
||||
@ -0,0 +1,22 @@
|
||||
pragma experimental SMTChecker;
|
||||
|
||||
contract C {
|
||||
struct S {
|
||||
uint x;
|
||||
uint[] a;
|
||||
}
|
||||
S s;
|
||||
function f(uint _x) public {
|
||||
s.x = _x;
|
||||
s.a.pop();
|
||||
s.a.push();
|
||||
s.a.push();
|
||||
s.a[0] = _x;
|
||||
assert(s.a[1] == s.a[0]);
|
||||
s.a.pop();
|
||||
s.a.pop();
|
||||
}
|
||||
}
|
||||
// ----
|
||||
// Warning 2529: (133-142): Empty array "pop" detected here.
|
||||
// Warning 6328: (189-213): Assertion violation happens here
|
||||
@ -0,0 +1,18 @@
|
||||
pragma experimental SMTChecker;
|
||||
pragma experimental ABIEncoderV2;
|
||||
|
||||
contract C {
|
||||
struct S {
|
||||
uint x;
|
||||
uint[] a;
|
||||
}
|
||||
function f(S memory s1, S memory s2) public pure {
|
||||
delete s1;
|
||||
s1.x++;
|
||||
++s1.x;
|
||||
assert(s1.x == 2);
|
||||
assert(s1.x == s2.x);
|
||||
}
|
||||
}
|
||||
// ----
|
||||
// Warning 6328: (225-245): Assertion violation happens here
|
||||
@ -0,0 +1,19 @@
|
||||
pragma experimental SMTChecker;
|
||||
pragma experimental ABIEncoderV2;
|
||||
|
||||
contract C {
|
||||
struct S {
|
||||
uint x;
|
||||
uint[] a;
|
||||
}
|
||||
function f(S memory s1, S memory s2) public pure {
|
||||
delete s1;
|
||||
s1.x = 100;
|
||||
s1.x--;
|
||||
--s1.x;
|
||||
assert(s1.x == 98);
|
||||
assert(s1.x == s2.x);
|
||||
}
|
||||
}
|
||||
// ----
|
||||
// Warning 6328: (240-260): Assertion violation happens here
|
||||
@ -15,12 +15,7 @@ contract C
|
||||
}
|
||||
// ----
|
||||
// Warning 2072: (157-170): Unused local variable.
|
||||
// Warning 8115: (157-170): Assertion checker does not yet support the type of this variable.
|
||||
// Warning 8364: (139-146): Assertion checker does not yet implement type struct C.S storage ref
|
||||
// Warning 8364: (149-150): Assertion checker does not yet implement type type(struct C.S storage pointer)
|
||||
// Warning 8364: (149-153): Assertion checker does not yet implement type struct C.S memory
|
||||
// Warning 4639: (149-153): Assertion checker does not yet implement this expression.
|
||||
// Warning 8364: (139-153): Assertion checker does not yet implement type struct C.S storage ref
|
||||
// Warning 8364: (173-174): Assertion checker does not yet implement type type(struct C.S storage pointer)
|
||||
// Warning 8364: (173-177): Assertion checker does not yet implement type struct C.S memory
|
||||
// Warning 4639: (173-177): Assertion checker does not yet implement this expression.
|
||||
|
||||
@ -3,7 +3,7 @@ pragma experimental SMTChecker;
|
||||
contract C
|
||||
{
|
||||
struct S { uint[] a; }
|
||||
function f(bool b) public {
|
||||
function f(bool b) public pure {
|
||||
S memory c;
|
||||
c.a[0] = 0;
|
||||
if (b)
|
||||
@ -14,21 +14,3 @@ contract C
|
||||
}
|
||||
}
|
||||
// ----
|
||||
// Warning 2018: (71-197): Function state mutability can be restricted to pure
|
||||
// Warning 6328: (175-193): Assertion violation happens here
|
||||
// Warning 8115: (101-111): Assertion checker does not yet support the type of this variable.
|
||||
// Warning 7650: (115-118): Assertion checker does not yet support this expression.
|
||||
// Warning 8364: (115-116): Assertion checker does not yet implement type struct C.S memory
|
||||
// Warning 9118: (115-121): Assertion checker does not yet implement this expression.
|
||||
// Warning 9056: (115-121): Assertion checker does not yet implement this expression.
|
||||
// Warning 7650: (139-142): Assertion checker does not yet support this expression.
|
||||
// Warning 8364: (139-140): Assertion checker does not yet implement type struct C.S memory
|
||||
// Warning 9118: (139-145): Assertion checker does not yet implement this expression.
|
||||
// Warning 9056: (139-145): Assertion checker does not yet implement this expression.
|
||||
// Warning 7650: (161-164): Assertion checker does not yet support this expression.
|
||||
// Warning 8364: (161-162): Assertion checker does not yet implement type struct C.S memory
|
||||
// Warning 9118: (161-167): Assertion checker does not yet implement this expression.
|
||||
// Warning 9056: (161-167): Assertion checker does not yet implement this expression.
|
||||
// Warning 7650: (182-185): Assertion checker does not yet support this expression.
|
||||
// Warning 8364: (182-183): Assertion checker does not yet implement type struct C.S memory
|
||||
// Warning 9118: (182-188): Assertion checker does not yet implement this expression.
|
||||
|
||||
@ -3,7 +3,7 @@ pragma experimental SMTChecker;
|
||||
contract C
|
||||
{
|
||||
struct S { uint[][] a; }
|
||||
function f(bool b) public {
|
||||
function f(bool b) public pure {
|
||||
S memory c;
|
||||
c.a[0][0] = 0;
|
||||
if (b)
|
||||
@ -14,21 +14,3 @@ contract C
|
||||
}
|
||||
}
|
||||
// ----
|
||||
// Warning 2018: (73-211): Function state mutability can be restricted to pure
|
||||
// Warning 6328: (186-207): Assertion violation happens here
|
||||
// Warning 8115: (103-113): Assertion checker does not yet support the type of this variable.
|
||||
// Warning 7650: (117-120): Assertion checker does not yet support this expression.
|
||||
// Warning 8364: (117-118): Assertion checker does not yet implement type struct C.S memory
|
||||
// Warning 9118: (117-123): Assertion checker does not yet implement this expression.
|
||||
// Warning 9056: (117-126): Assertion checker does not yet implement this expression.
|
||||
// Warning 7650: (144-147): Assertion checker does not yet support this expression.
|
||||
// Warning 8364: (144-145): Assertion checker does not yet implement type struct C.S memory
|
||||
// Warning 9118: (144-150): Assertion checker does not yet implement this expression.
|
||||
// Warning 9056: (144-153): Assertion checker does not yet implement this expression.
|
||||
// Warning 7650: (169-172): Assertion checker does not yet support this expression.
|
||||
// Warning 8364: (169-170): Assertion checker does not yet implement type struct C.S memory
|
||||
// Warning 9118: (169-175): Assertion checker does not yet implement this expression.
|
||||
// Warning 9056: (169-178): Assertion checker does not yet implement this expression.
|
||||
// Warning 7650: (193-196): Assertion checker does not yet support this expression.
|
||||
// Warning 8364: (193-194): Assertion checker does not yet implement type struct C.S memory
|
||||
// Warning 9118: (193-199): Assertion checker does not yet implement this expression.
|
||||
|
||||
@ -14,20 +14,3 @@ contract C
|
||||
}
|
||||
}
|
||||
// ----
|
||||
// Warning 6328: (202-226): Assertion violation happens here
|
||||
// Warning 8115: (110-120): Assertion checker does not yet support the type of this variable.
|
||||
// Warning 7650: (124-127): Assertion checker does not yet support this expression.
|
||||
// Warning 8364: (124-125): Assertion checker does not yet implement type struct C.S memory
|
||||
// Warning 9118: (124-130): Assertion checker does not yet implement this expression.
|
||||
// Warning 9056: (124-136): Assertion checker does not yet implement this expression.
|
||||
// Warning 7650: (154-157): Assertion checker does not yet support this expression.
|
||||
// Warning 8364: (154-155): Assertion checker does not yet implement type struct C.S memory
|
||||
// Warning 9118: (154-160): Assertion checker does not yet implement this expression.
|
||||
// Warning 9056: (154-166): Assertion checker does not yet implement this expression.
|
||||
// Warning 7650: (182-185): Assertion checker does not yet support this expression.
|
||||
// Warning 8364: (182-183): Assertion checker does not yet implement type struct C.S memory
|
||||
// Warning 9118: (182-188): Assertion checker does not yet implement this expression.
|
||||
// Warning 9056: (182-194): Assertion checker does not yet implement this expression.
|
||||
// Warning 7650: (209-212): Assertion checker does not yet support this expression.
|
||||
// Warning 8364: (209-210): Assertion checker does not yet implement type struct C.S memory
|
||||
// Warning 9118: (209-215): Assertion checker does not yet implement this expression.
|
||||
|
||||
@ -14,11 +14,6 @@ contract C {
|
||||
}
|
||||
}
|
||||
// ----
|
||||
// Warning 8115: (112-120): Assertion checker does not yet support the type of this variable.
|
||||
// Warning 8364: (137-138): Assertion checker does not yet implement type type(struct C.S storage pointer)
|
||||
// Warning 8364: (137-141): Assertion checker does not yet implement type struct C.S memory
|
||||
// Warning 4639: (137-141): Assertion checker does not yet implement this expression.
|
||||
// Warning 8115: (193-203): Assertion checker does not yet support the type of this variable.
|
||||
// Warning 8364: (227-228): Assertion checker does not yet implement type struct C.S memory
|
||||
// Warning 4639: (137-141): Assertion checker does not yet implement this expression.
|
||||
// Warning 6191: (227-228): Assertion checker does not yet implement type struct C.S memory
|
||||
|
||||
Loading…
Reference in New Issue
Block a user