Links between `\initialized{L}(p)` and `\valid_read{L}(p)`.

[pbaudin]

The section about the \initialized{L}(p) needs to be developed.

In ACSL, there is no strong link between \initialized{L}(p) and \valid_read{L}(p) even if from the C side, it seems difficult to have a data initialized at a program state that cannot be read at the same state.

[pbaudin]

In ACSL, the proof of \initialized{L}(p) ensures that the C content *p is initialized iff \valid_read{L}(p) is also proved.

In the same manner the proof of ! \initialized{L}(p) ensures that the C content *p is not initialized iff \valid_read{L}(p) is also proved.

Finally, \initialized{L}(p) is undefined when \valid_read{L}(p)=\false.

The ACSL definition of the initialization property is weaker than it could be in C. That gives some benefits:

Writing requires \initialized(p) && \valid_read{L}(p) allows to explicit the fact that the pointer refers a valid readable memory location. By the way, the specification is more clarified and it will be easier to modify it without forget something.

For example, if the initialization became unnecessary, you can remove \initialized(p) without forget to state on the validity of the pointer.

In the same way, if the location has also to be writable, you can easily replace \valid_read{L}(p) by \valid; and thus without impact on the verification of the \initialized(p) part.

The cut of that link splits the verification of the C initialization in two explicit sub-goals. So, the tools get easier checks to perform.

[claudemarche]

Please see issue #83