|
|
@ -942,13 +942,19 @@ class Instruction: |
|
|
|
data = symbol_factory.BitVecVal(0, 1) |
|
|
|
data = symbol_factory.BitVecVal(0, 1) |
|
|
|
|
|
|
|
|
|
|
|
if data.symbolic: |
|
|
|
if data.symbolic: |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
annotations = [] |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
for b in state.memory[index : index + length]: |
|
|
|
|
|
|
|
annotations.append(b.annotations) |
|
|
|
|
|
|
|
|
|
|
|
argument_str = str(state.memory[index]).replace(" ", "_") |
|
|
|
argument_str = str(state.memory[index]).replace(" ", "_") |
|
|
|
result = symbol_factory.BitVecFuncSym( |
|
|
|
result = symbol_factory.BitVecFuncSym( |
|
|
|
"KECCAC[{}]".format(argument_str), |
|
|
|
"KECCAC[{}]".format(argument_str), |
|
|
|
"keccak256", |
|
|
|
"keccak256", |
|
|
|
256, |
|
|
|
256, |
|
|
|
input_=data, |
|
|
|
input_=data, |
|
|
|
annotations=state.memory[index].annotations, |
|
|
|
annotations=annotations, |
|
|
|
) |
|
|
|
) |
|
|
|
log.debug("Created BitVecFunc hash.") |
|
|
|
log.debug("Created BitVecFunc hash.") |
|
|
|
|
|
|
|
|
|
|
|