zetzit / zz

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

Why is heap allocation discouraged? #51

Closed richardanaya closed 4 years ago

richardanaya commented 4 years ago

Is there some fundamental limitation of zz not being mentioned in the readme?

aep commented 4 years ago

zz is built for non-heap environments. specifically embedded (or wasm, as we just learned) you can call malloc, but none of the tools are built for it, and the prover probably falls on its nose.

the reason this lacks documentation is really that in embedded you don't do malloc anyway, so i assumed most people know

richardanaya commented 4 years ago

I see! I feel like what would be really interesting to see would be an easy way for making global fixed capacity vectors to help play to zz's strengths :)

aep commented 4 years ago

create a string with 200 bytes capacity:

new+200 a = string::empty();

create a generic allocator pool with 200 bytes capacity and slab size of 16 bytes

new+200 a = pool::make(16);
aep commented 4 years ago

happy to answer any questions you have on github issues :)