Uninitialized access succeeds

[jacereda]

Shouldn't this fail?

https://github.com/aep/zz/blob/5662bdc311d8dd54585a3f43a580eb6d25d516fc/tests/mustpass/branch_dont_loose_deref/src/main.zz#L19

[aep]

maybe

i'm not sure what a good semantic for uninitialized values is.

should zz simply always emit initialization into the C code? (consistent with rust)
should it make uninitialized access illegal? (consistent with probably all C guidelines)
should only branching on uninitialized be illegal (consistent with valgrind)
should it assert an unknown value? (consistent with actual behavior)

it currently does the last one, so using the value in other assertions will fail, but reading it is fine.

[jacereda]

I guess most C programmers would probably expect the second option. Most C compilers will emit a warning when accessing an unitialized value. I would expect the output to compile without warnings.

[aep]

I would expect the output to compile without warnings.

right, that's a really good basis for these decisions.

[aep]

ok then more decisions to be made.

1. implement as first class some( ) theory
   advantage: can override it with static_attest(some(it))
   advantage: more expressive and people can come up with other insane use cases for it
   advantage: could be merged with safe( ) so that some( ) is valid for any value except 0 if its a pointer
   disadvantage: massive compile time impact of about +50%

2. implement as hard error in the symbolic execution phase
   advantage: basically no performance impact
   advantage: there is actually no use case for uninitialized access anyway, unless its a register.
   disadvantage: cannot be overwritten by the user

[icosahedron]

Sounds like the decision should be a flag. :) I would vote that #2 be the default since it's "safer", with a flag to handle the first case if wanted?