Comments (4)
@leonardoalt I've added REVERT to the code and your contract should work now. Here is my commit
from oyente.
Update:
For the slightly modified following contract
pragma solidity ^0.4.11;
contract T {
uint sum0;
uint sum1;
function t(bool b, uint x) {
require(x < 1000);
if (b) {
sum1 += x;
}
else {
sum0 += x;
}
}
}
I get the error
Traceback (most recent call last):
File "symExec.py", line 765, in sym_exec_block
sym_exec_block(left_branch, block, visited1, depth, stack1, mem1, global_state1, path_conditions_and_vars1, analysis1)
File "symExec.py", line 740, in sym_exec_block
sym_exec_block(successor, block, visited1, depth, stack1, mem1, global_state1, path_conditions_and_vars1, analysis1)
File "symExec.py", line 740, in sym_exec_block
sym_exec_block(successor, block, visited1, depth, stack1, mem1, global_state1, path_conditions_and_vars1, analysis1)
File "symExec.py", line 693, in sym_exec_block
sym_exec_ins(block, instr, stack, mem, global_state, path_conditions_and_vars, analysis)
File "symExec.py", line 1677, in sym_exec_ins
raise TypeError("Target address must be an integer")
from oyente.
Ok, I figured what the problem was.
This is the piece of the disasm of the second code that I've posted related to the require
command:
000086: PUSH1 0x5e
000088: JUMPI
000089: PUSH1 0x00
000091: PUSH1 0x00
000093: Missing opcode 0xfd (REQUIRE!!)
000094: JUMPDEST
If I change require
to assert
in the same code, it becomes:
000086: PUSH1 0x5a
000088: JUMPI
000089: Missing opcode 0xfe (ASSERT!!)
000090: JUMPDEST
The two extra PUSH
s are what break the stack afterwards, and lead to the TypeError.
My really-not-good-fix just to finish running my tests was to pop twice if INVALID
is followed by 0xfd
. Both examples worked then.
from oyente.
I think we can treat 0xfd as REVERT opcode and pop 2 elements from the stack.
from oyente.
Related Issues (20)
- Solidity 0.6.x
- Option -r has issues
- Having trouble with newest verions solc:0.8.0 as `solc` is now `solcjs`
- Reentrancy detection machanism
- Upcoming changes in CryticCompile
- Nurses
- How to use the oyente to batch test smart contracts? HOT 2
- docker
- First or second argument must be a Z3 bit-vector expression HOT 1
- ModuleNotFoundError: No module named 'crytic_compile' HOT 2
- Any plan to support solc 0.8.x HOT 1
- Bugs HOT 3
- Bad return value HOT 2
- Error: Expected identifier, got 'LParen' HOT 1
- Exception on binary contract
- UNKNOWN INSTRUCTION: SHL HOT 2
- Why does Oyente report different results on virtually identical contracts?
- docker not run HOT 1
- Installation Error
- python3 error in docker
Recommend Projects
-
React
A declarative, efficient, and flexible JavaScript library for building user interfaces.
-
Vue.js
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
-
Typescript
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
-
TensorFlow
An Open Source Machine Learning Framework for Everyone
-
Django
The Web framework for perfectionists with deadlines.
-
Laravel
A PHP framework for web artisans
-
D3
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
-
Recommend Topics
-
javascript
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
-
web
Some thing interesting about web. New door for the world.
-
server
A server is a program made to process requests and deliver data to clients.
-
Machine learning
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
-
Visualization
Some thing interesting about visualization, use data art
-
Game
Some thing interesting about game, make everyone happy.
Recommend Org
-
Facebook
We are working to build community through open source technology. NB: members must have two-factor auth.
-
Microsoft
Open source projects and samples from Microsoft.
-
Google
Google ❤️ Open Source for everyone.
-
Alibaba
Alibaba Open Source for everyone
-
D3
Data-Driven Documents codes.
-
Tencent
China tencent open source team.
from oyente.