everparse icon indicating copy to clipboard operation
everparse copied to clipboard

Published 20 hours ago • verified publisher icon project-everest

Fully specify integer parsers

Open gebner opened this issue 1 year ago • 0 comments

The parsers for little-endian 16- and 32-bit numbers did not have any specification lemmas at all. The others did not have any constraints on the number of consumed bytes. (Although that follows from parser injectivity with a bit of effort.)

I also got rid of one rlimit by locally adding some SMT patterns. The rlimit didn't work at all for me in VS Code.

gebner avatar Feb 16 '24 18:02 gebner