KEVM & eDSL error case studies
1. Halt! Terminating branch
code: errors(bash)
Halt! Terminating branch.
Z3 error: (error "line 32 column 63: Sorts K and InternalOp are incompatible")
Z3 error: (error "line 33 column 80: Sorts K and InternalOp are incompatible")
Z3 error: (error "line 32 column 29: Sorts K and InternalOp are incompatible")
Z3 error: (error "line 32 column 186: Sorts K and InternalOp are incompatible")
...
requireで変数に条件を付けないと探索する範囲が広すぎてエラーになる?
nrryuya.icon > これは、specとマッチしないままhalt(プログラムが停止)した場合に出るもの。
Halt!なしで、こんな感じで出るときもある
code: errors(bash)
z3 error: (error "line 31 column 129: Sorts K and KItem are incompatible")
z3 error: (error "line 28 column 305: Sorts K and KItem are incompatible")
z3 error: (error "line 31 column 715: Sorts K and KItem are incompatible")
z3 error: (error "line 28 column 289: Sorts K and KItem are incompatible")
ストレージ変数への0の代入
code: test(Python)
data: uint256
@public
def setZero():
self.data = 0
0を代入する場合は、refundがあるので、<refund> _ => _ </refund>とする
雑メモ
※あとで整理する
#rangeUIntを#raneUIntにタイポしたらこうなった
Step above: 1, evaluation ended with no successors.
ACCTS: Set とスペースを空けると
code: bash
Error Compiler: Had 1 parsing errors. Error Inner Parser: Parse error: unexpected token ‘:’. だが、ACCTS:SETにしたら治った