zetzit / zz

πŸΊπŸ™ ZetZ a zymbolic verifier and tranzpiler to bare metal C
MIT License
1.6k stars 52 forks source link

uninterpreted theories don't check argument types #114

Open aep opened 4 years ago

aep commented 4 years ago

from #111

these are interchangeable

theory isopen(Socket fd) -> bool;
theory isopen(Socket * fd) -> bool;

because unless a theory actually has a body, nothing checks the argument type. Although that's sort of valid, It's rather confusing.