mirror of
https://github.com/ethereum/solidity
synced 2023-10-03 13:03:40 +00:00
[SMTChecker] Fix unsupported type assignment
This commit is contained in:
parent
5fb85a6118
commit
0b046897ae
@ -14,6 +14,7 @@ Bugfixes:
|
|||||||
* SMTChecker: Fix bad cast in base constructor modifier.
|
* SMTChecker: Fix bad cast in base constructor modifier.
|
||||||
* SMTChecker: Fix internal error when visiting state variable inherited from base class.
|
* SMTChecker: Fix internal error when visiting state variable inherited from base class.
|
||||||
* SMTChecker: Fix internal error in fixed point operations.
|
* SMTChecker: Fix internal error in fixed point operations.
|
||||||
|
* SMTChecker: Fix internal error in assignment to unsupported type.
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
@ -377,10 +377,15 @@ void SMTChecker::endVisit(Assignment const& _assignment)
|
|||||||
"Assertion checker does not yet implement this assignment operator."
|
"Assertion checker does not yet implement this assignment operator."
|
||||||
);
|
);
|
||||||
else if (!isSupportedType(_assignment.annotation().type->category()))
|
else if (!isSupportedType(_assignment.annotation().type->category()))
|
||||||
|
{
|
||||||
m_errorReporter.warning(
|
m_errorReporter.warning(
|
||||||
_assignment.location(),
|
_assignment.location(),
|
||||||
"Assertion checker does not yet implement type " + _assignment.annotation().type->toString()
|
"Assertion checker does not yet implement type " + _assignment.annotation().type->toString()
|
||||||
);
|
);
|
||||||
|
// Give it a new index anyway to keep the SSA scheme sound.
|
||||||
|
if (auto varDecl = identifierToVariable(_assignment.leftHandSide()))
|
||||||
|
newValue(*varDecl);
|
||||||
|
}
|
||||||
else
|
else
|
||||||
{
|
{
|
||||||
vector<smt::Expression> rightArguments;
|
vector<smt::Expression> rightArguments;
|
||||||
|
@ -0,0 +1,136 @@
|
|||||||
|
pragma experimental SMTChecker;
|
||||||
|
contract Simple{
|
||||||
|
|
||||||
|
address destination;
|
||||||
|
address source;
|
||||||
|
|
||||||
|
function set(address source_taint) public{
|
||||||
|
destination = source_taint;
|
||||||
|
}
|
||||||
|
|
||||||
|
function set2() public{
|
||||||
|
destination = source;
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
contract Reference{
|
||||||
|
|
||||||
|
struct St{
|
||||||
|
uint val;
|
||||||
|
}
|
||||||
|
|
||||||
|
St destination;
|
||||||
|
St source;
|
||||||
|
St destination_indirect_1;
|
||||||
|
St destination_indirect_2;
|
||||||
|
|
||||||
|
function set(uint source_taint) public{
|
||||||
|
destination.val = source_taint;
|
||||||
|
}
|
||||||
|
|
||||||
|
function set2() public{
|
||||||
|
destination.val = source.val;
|
||||||
|
}
|
||||||
|
|
||||||
|
function set3(uint source_taint) public{
|
||||||
|
St storage ref = destination_indirect_1;
|
||||||
|
if(true){
|
||||||
|
ref = destination_indirect_2;
|
||||||
|
}
|
||||||
|
ref.val = source_taint;
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
contract SolidityVar{
|
||||||
|
|
||||||
|
address addr_1;
|
||||||
|
address addr_2;
|
||||||
|
|
||||||
|
constructor() public{
|
||||||
|
addr_1 = msg.sender;
|
||||||
|
}
|
||||||
|
|
||||||
|
}
|
||||||
|
|
||||||
|
contract Intermediate{
|
||||||
|
|
||||||
|
uint destination;
|
||||||
|
uint source_intermediate;
|
||||||
|
uint source;
|
||||||
|
|
||||||
|
function f() public{
|
||||||
|
destination = source_intermediate;
|
||||||
|
}
|
||||||
|
function f2() public{
|
||||||
|
source_intermediate = source;
|
||||||
|
}
|
||||||
|
|
||||||
|
}
|
||||||
|
|
||||||
|
|
||||||
|
contract Base{
|
||||||
|
|
||||||
|
uint destination;
|
||||||
|
uint source_intermediate;
|
||||||
|
uint source;
|
||||||
|
|
||||||
|
function f() public{
|
||||||
|
destination = source_intermediate;
|
||||||
|
}
|
||||||
|
}
|
||||||
|
contract Derived is Base{
|
||||||
|
|
||||||
|
function f2() public{
|
||||||
|
source_intermediate = source;
|
||||||
|
}
|
||||||
|
|
||||||
|
|
||||||
|
}
|
||||||
|
|
||||||
|
|
||||||
|
contract PropagateThroughArguments {
|
||||||
|
uint var_tainted;
|
||||||
|
uint var_not_tainted;
|
||||||
|
uint var_dependant;
|
||||||
|
|
||||||
|
function f(uint user_input) public {
|
||||||
|
f2(user_input, 4);
|
||||||
|
var_dependant = var_tainted;
|
||||||
|
}
|
||||||
|
|
||||||
|
function f2(uint x, uint y) internal {
|
||||||
|
var_tainted = x;
|
||||||
|
var_not_tainted = y;
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
contract PropagateThroughReturnValue {
|
||||||
|
uint var_dependant;
|
||||||
|
uint var_state;
|
||||||
|
|
||||||
|
function foo() public {
|
||||||
|
var_dependant = bar();
|
||||||
|
}
|
||||||
|
|
||||||
|
function bar() internal returns (uint) {
|
||||||
|
return (var_state);
|
||||||
|
}
|
||||||
|
}
|
||||||
|
// ----
|
||||||
|
// Warning: (1886-1954): Function state mutability can be restricted to view
|
||||||
|
// Warning: (318-332): Assertion checker does not yet support the type of this variable.
|
||||||
|
// Warning: (338-347): Assertion checker does not yet support the type of this variable.
|
||||||
|
// Warning: (353-378): Assertion checker does not yet support the type of this variable.
|
||||||
|
// Warning: (384-409): Assertion checker does not yet support the type of this variable.
|
||||||
|
// Warning: (464-479): Assertion checker does not yet support this expression.
|
||||||
|
// Warning: (464-494): Assertion checker does not yet implement such assignments.
|
||||||
|
// Warning: (539-554): Assertion checker does not yet support this expression.
|
||||||
|
// Warning: (557-567): Assertion checker does not yet support this expression.
|
||||||
|
// Warning: (539-567): Assertion checker does not yet implement such assignments.
|
||||||
|
// Warning: (629-643): Assertion checker does not yet support the type of this variable.
|
||||||
|
// Warning: (646-668): Internal error: Expression undefined for SMT solver.
|
||||||
|
// Warning: (646-668): Assertion checker does not yet implement this type.
|
||||||
|
// Warning: (700-728): Assertion checker does not yet implement type struct Reference.St storage pointer
|
||||||
|
// Warning: (748-755): Assertion checker does not yet support this expression.
|
||||||
|
// Warning: (748-770): Assertion checker does not yet implement such assignments.
|
||||||
|
// Warning: (849-905): Assertion checker does not yet support constructors.
|
Loading…
Reference in New Issue
Block a user