0002332: Information on C type of array is not present (in Coq)

Notes
(0006471) correnson (manager) 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 (manager) 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 (reporter) 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.

Issue History
Date Modified	Username	Field	Change
2017-11-22 08:48	jens	New Issue
2017-11-22 08:48	jens	Status	new => assigned
2017-11-22 08:48	jens	Assigned To	=> correnson
2017-11-22 08:49	jens	File Added: array.c
2017-11-22 08:49	jens	File Added: wp0.script
2017-11-22 09:31	correnson	Note Added: 0006471
2017-11-22 09:32	correnson	Status	assigned => acknowledged
2017-11-22 09:40	correnson	Note Edited: 0006471	View Revisions
2017-11-22 09:40	correnson	Note Edited: 0006471	View Revisions
2017-11-22 09:41	correnson	Note Edited: 0006471	View Revisions
2017-11-22 09:44	correnson	Note Added: 0006472
2017-11-22 09:45	correnson	Note Edited: 0006472	View Revisions
2017-11-22 09:45	correnson	Note Edited: 0006472	View Revisions
2017-11-22 10:28	jens	Note Added: 0006473
2019-10-17 17:23	correnson	Status	acknowledged => resolved
2019-10-17 17:23	correnson	Resolution	open => no change required
2019-10-17 18:02	signoles	Status	resolved => closed

Relationships