zchcai
commented
6 years ago update Z3 prover to the latest version: https://github.com/Z3Prover/z3
Closed zchcai closed 6 years ago
zchcai
commented
6 years ago update Z3 prover to the latest version: https://github.com/Z3Prover/z3
[zhicheng@taxi] (26)$ geth version Geth Version: 1.7.2-stable Git Commit: 1db4ecdc0b9e828ff65777fb466fc7c1d04e0de9 Architecture: amd64 Protocol Versions: [63 62] Network Id: 1 Go Version: go1.9 Operating System: linux GOPATH= GOROOT=/usr/lib/go-1.9 [zhicheng@taxi] (27)$ python2 --version Python 2.7.12 [zhicheng@taxi] (28)$ python2 maian.py -s example_contracts/example_suicidal.sol KAI -c 0
==================================================================================================== [ ] Compiling Solidity contract from the file example_contracts/example_suicidal.sol ... Done [ ] Connecting to PRIVATE blockchain emptychain ... ESTABLISHED [ ] Deploying contract ..... confirmed at address: 0x9e536236abf2288a7864c6a1afaa4cb98d464306 [ ] Contract code length on the blockchain : 7750 : 0x606060405236156100ce57600035... [ ] Contract address saved in file: ./out/KAI.address [ ] Check if contract is SUICIDAL
[ ] Contract address : 0x9e536236abf2288a7864c6a1afaa4cb98d464306 [ ] Contract bytecode : 606060405236156100ce576000357c01000000000000000000... [ ] Bytecode length : 7748 [ ] Blockchain contract: True [ ] Debug : False
[ ] Search with call depth: 1 : Traceback (most recent call last): File "maian.py", line 177, in
main(sys.argv[1:])
File "maian.py", line 137, in main
if 0 == MyGlobals.checktype: ret = check_suicide.check_one_contract_on_suicide(code, contract_address, MyGlobals.debug, MyGlobals.read_from_blockchain, True, fhashes)
File "/nobackup/MAIAN/tool/check_suicide.py", line 69, in check_one_contract_on_suicide
run_one_check( i, ops, contract_address, debug, read_from_blockchain )
File "/nobackup/MAIAN/tool/check_suicide.py", line 37, in run_one_check
execute_one_block(ops,stack,0, trace, storage, mmemory, data, configurations, ['SUICIDE'], ether_suicide, 0, 0, debug, read_from_blockchain )
File "/nobackup/MAIAN/tool/execute_block.py", line 88, in execute_one_block
newpos, halt = execute( ops, stack, pos, storage, mmemory, data, trace, calldepth, debug, read_from_blockchain )
File "/nobackup/MAIAN/tool/execute_instruction.py", line 429, in execute
t = copy.deepcopy( args[1] )
File "/usr/lib/python2.7/copy.py", line 163, in deepcopy
y = copier(x, memo)
File "/usr/lib/python2.7/copy.py", line 257, in _deepcopy_dict
y[deepcopy(key, memo)] = deepcopy(value, memo)
File "/usr/lib/python2.7/copy.py", line 163, in deepcopy
y = copier(x, memo)
File "/usr/lib/python2.7/copy.py", line 298, in _deepcopy_inst
state = deepcopy(state, memo)
File "/usr/lib/python2.7/copy.py", line 163, in deepcopy
y = copier(x, memo)
File "/usr/lib/python2.7/copy.py", line 257, in _deepcopy_dict
y[deepcopy(key, memo)] = deepcopy(value, memo)
File "/usr/lib/python2.7/copy.py", line 163, in deepcopy
y = copier(x, memo)
File "/usr/lib/python2.7/copy.py", line 298, in _deepcopy_inst
state = deepcopy(state, memo)
File "/usr/lib/python2.7/copy.py", line 163, in deepcopy
y = copier(x, memo)
File "/usr/lib/python2.7/copy.py", line 257, in _deepcopy_dict
y[deepcopy(key, memo)] = deepcopy(value, memo)
File "/usr/lib/python2.7/copy.py", line 190, in deepcopy
y = _reconstruct(x, rv, 1, memo)
File "/usr/lib/python2.7/copy.py", line 334, in _reconstruct
state = deepcopy(state, memo)
File "/usr/lib/python2.7/copy.py", line 163, in deepcopy
y = copier(x, memo)
File "/usr/lib/python2.7/copy.py", line 257, in _deepcopy_dict
y[deepcopy(key, memo)] = deepcopy(value, memo)
File "/usr/lib/python2.7/copy.py", line 182, in deepcopy
rv = reductor(2)
ValueError: ctypes objects containing pointers cannot be pickled
Exception AttributeError: "BitVecNumRef instance has no attribute 'ctx'" in <object repr() failed> ignored
Exception AttributeError: "Context instance has no attribute 'lib'" in <bound method Context.del of <z3.z3.Context instance at 0x7f72aea32518>> ignored