Notes 

(0006471)

correnson

20171122 09:31
(edited on: 20171122 09:41) 

Actually, you are right, the type information in the lemma about `int *` is missing, although it is present
in proof obligations from normal Ccode.
**EDITED** more precisely, such properties are inserted for values actually read by the code, not by the ACSL. Looking into more details, there is no way to guarantee, in the memory model, that all access to an `int *` are actually an `int`, since memory arrays in the WP memory model might be shared among different integer types.
For such a *bug* to be fixed, we need to allocate a separate memory for each integral type in the memory model. This is feasible and it would introduce more separation in WP, but at the cost of adding many stores, hence additional parameters, to ACSL predicates with labels.
However, there is no soundness issue here, since we simply have removed some invariants.



(0006472)

correnson

20171122 09:44
(edited on: 20171122 09:45) 

**Workaround:** turn your second lemma into` \exists integer...` instead of `\exists int`.
Finally, when reaching the point where you use your lemma to introduce a constant `C`, the consequence of the lemma finally allows you to assert that `C = \at( *p , L )` where `*p` is actually read from the Ccode.
And, at this point, the WP would have introduced the fact that `is_int( *p )`, hence you will have a proof for `is_int(C)`.



(0006473)

jens

20171122 10:28


You are right about that there is no soundness issue here but it is definitely a pain in the back.
The problem came recently up in "ACSL by Example" where I wanted to prove a new lemma with a an old lemma. The old lemma is similar to "AllEqual" and thus does not provide the specific type information needed for the newer lemma which is similar to "Constant".
Rewriting "Constant" according to your suggestion would be a major effort for us in "ACSL by Example".
Our approach, so far, has been to preserve the C types of arrays in ACSL.
For indices, however, we have used "integer" instead of "unsigned int" for a long time.
(I am just explaining our current approach.)
I am not sure what other ACSL users would prefer. 
