Dehydra does a form of basic symbolic execution now. It’s enough to avoid the unfeasable branches. It enabled me to add known_zero() and known_notzero() so dehydra supports all of the functions documented in the UNO paper.

I believe dehydra can now match all of the features of uno’s DSL. Download it here. See malloc.js for an example of how to port UNO scripts. There is no documentation, except for this blog, but the docs on the UNO website should work too.

This is the first release so there are bugs, but the tool should be able to find some API-misuse issues, etc. I need some early adopters to help direct the evolution of this tool.