Frama-C Bug Tracking System - Frama-C
View Issue Details
0002332Frama-CPlug-in > wppublic2017-11-22 08:482019-10-17 18:02
jens 
correnson 
normalmajoralways
closedno change required 
Linux, macOS
Frama-C 15-Phosphorus 
 
0002332: Information on C type of array is not present (in Coq)
In the attached file 'array.c' there are two simple predicates 'AllEqual' and 'Constant' that involve int arrays. There are also two lemmas that relate both predicate. While it can automatically verified that "Constant" implies "AllEqual" the proof of the "converse" statement fails. When looking at the Coq presentation of "AllEqual" it becomes apparent that Coq only sees an "integer array"; the specific C type (represented by the predicate 'is_sint32') is NOT present at all.
Run the command: frama-c-gui -no-unicode -wp -wp-prover alt-ergo -wp-prover coq -wp-script 'wp0.script' array.c
The error also occurs in the beta release of Frama-C 16 (Sulfur).
No tags attached.
c array.c (345) 2017-11-22 08:48
https://bts.frama-c.com/file_download.php?file_id=1212&type=bug
? wp0.script (271) 2017-11-22 08:49
https://bts.frama-c.com/file_download.php?file_id=1213&type=bug
Issue History
2017-11-22 08:48jensNew Issue
2017-11-22 08:48jensStatusnew => assigned
2017-11-22 08:48jensAssigned To => correnson
2017-11-22 08:49jensFile Added: array.c
2017-11-22 08:49jensFile Added: wp0.script
2017-11-22 09:31corrensonNote Added: 0006471
2017-11-22 09:32corrensonStatusassigned => acknowledged
2017-11-22 09:40corrensonNote Edited: 0006471View Revisions
2017-11-22 09:40corrensonNote Edited: 0006471View Revisions
2017-11-22 09:41corrensonNote Edited: 0006471View Revisions
2017-11-22 09:44corrensonNote Added: 0006472
2017-11-22 09:45corrensonNote Edited: 0006472View Revisions
2017-11-22 09:45corrensonNote Edited: 0006472View Revisions
2017-11-22 10:28jensNote Added: 0006473
2019-10-17 17:23corrensonStatusacknowledged => resolved
2019-10-17 17:23corrensonResolutionopen => no change required
2019-10-17 18:02signolesStatusresolved => closed

Notes
(0006471)
correnson   
2017-11-22 09:31   
(edited on: 2017-11-22 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 C-code. **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   
2017-11-22 09:44   
(edited on: 2017-11-22 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 C-code. 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   
2017-11-22 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.