search

runtimeverification / avm-semantics

BSD 3-Clause "New" or "Revised" License
15 stars 4 forks source link

Integrate call counter example #131

Closed nwatson22 closed 1 year ago

nwatson22 commented 2 years ago

I'm worried there may be a subtle bug somewhere with encoded account address strings messing up the K term parser. I encountered this during testing, where sometimes a call to kast would fail, and then when I ran it again, it would succeed. When or before this PR is reviewed this is something that should be looked at.

nwatson22 commented 2 years ago

Since the python test harness inserts addresses as the (intended) TAddressLiteral sort, I had to change parts that were previously written for the older testing harness, which expects these addresses as byte strings. This is convenient because we can give human-readable names to the accounts, but it presents a problem when trying to support both methods. I am currently working on just having it handle Bytes sort addresses by padding them to the appropriate length and encoding them as address literals.