search

zetzit / zz

🍺🐙 ZetZ a zymbolic verifier and tranzpiler to bare metal C
MIT License
1.6k stars 52 forks source link

callsite assign #124

Closed aep closed 3 years ago

aep commented 3 years ago

implements callsite assigns that work similar to "default arguments" in C++ except they are full smt expressions

also introduces the tailof() theory which lets you get and finally also set a pointers tail. use in combination with callsite assign to replace tail bindings

jwerle commented 3 years ago

I am very excited for this!

aep commented 3 years ago

specifically see the changes in tests/mustpass/tail/src/main.zz

i'm still unsure if i got all the bugs, more testing tomorrow.