zetzit / zz

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

implement struct as bitvec #31

Open aep opened 4 years ago

aep commented 4 years ago

currently there's a bunch of edge cases in the prover because it makes assumptions about higher types. It really should tread everything as a memory blob and struct members as slices into the blob