You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
{{ message }}
This repository was archived by the owner on Jun 17, 2022. It is now read-only.
Repository navigation
This repository was archived by the owner on Jun 17, 2022. It is now read-only.
using <stdio.h>::{printf, scanf};fnfoo(int*p) -> int{// return p[0]; // not okreturn*p;// ok}
export fnmain() -> int{
int mut y = 123;foo(&y);return0;}
that's an unfortunate side effect of the len vs safe theory.
because safe(p) is implicit, the prover knows *p is fine,
but len(p) is undefined, so p + anything is unprovable
a quick fix would be
assert( = (safe(x) (> len(x) 0) )
but this slows down the prover dramatically
i'd prefer to not fix this until deref is correctly implemented. it actually needs to check len() as well because you might cast to a different pointer size and then deref.
that again isn't implemented yet because i haven't found a good way yet to get target pointer sizes. the current prover VM just assumes 64bit.
One leasson learned from rust is that zz will never make assumptions about your target build system, so it cannot possibly know how to call your c compiler with the correct flags for your target.
the options are pretty much
just assume 64bit because the edges cases where 32bit has bugs that 64bit doesnt aren't worth it
add some sort of --architecture build flags
test 64 and 32bit (nope because thats insanely slow)
Activity
aep commentedon Feb 5, 2020
thanks for the report!
that's an unfortunate side effect of the len vs safe theory.
because safe(p) is implicit, the prover knows *p is fine,
but len(p) is undefined, so p + anything is unprovable
a quick fix would be
but this slows down the prover dramatically
i'd prefer to not fix this until deref is correctly implemented. it actually needs to check len() as well because you might cast to a different pointer size and then deref.
that again isn't implemented yet because i haven't found a good way yet to get target pointer sizes. the current prover VM just assumes 64bit.
jacereda commentedon Feb 6, 2020
Does
__SIZEOF_POINTER__preprocessor symbol suffice?aep commentedon Feb 6, 2020
yes, but the prepro is unavailable to zz.
One leasson learned from rust is that zz will never make assumptions about your target build system, so it cannot possibly know how to call your c compiler with the correct flags for your target.
the options are pretty much
jacereda commentedon Feb 6, 2020
Well, you can shell-out to the target compiler (would need to be configured) with
-dM -Eflags to extract things like type sizes and endianness.I guess 2 could also be a good option.
aep commentedon Oct 13, 2020
actually, this is fixed, isnt it?