View Issue Details [ Jump to Notes ] | [ Issue History ] [ Print ] | ||||||||
ID | Project | Category | View Status | Date Submitted | Last Update | ||||
---|---|---|---|---|---|---|---|---|---|
0002332 | Frama-C | Plug-in > wp | public | 2017-11-22 08:48 | 2019-10-17 18:02 | ||||
Reporter | jens | ||||||||
Assigned To | correnson | ||||||||
Priority | normal | Severity | major | Reproducibility | always | ||||
Status | closed | Resolution | no change required | ||||||
Platform | Linux, macOS | OS | OS Version | ||||||
Product Version | Frama-C 15-Phosphorus | ||||||||
Target Version | Fixed in Version | ||||||||
Summary | 0002332: Information on C type of array is not present (in Coq) | ||||||||
Description | 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. | ||||||||
Steps To Reproduce | Run the command: frama-c-gui -no-unicode -wp -wp-prover alt-ergo -wp-prover coq -wp-script 'wp0.script' array.c | ||||||||
Additional Information | The error also occurs in the beta release of Frama-C 16 (Sulfur). | ||||||||
Tags | No tags attached. | ||||||||
Attached Files |
|
![]() |
|
correnson (manager) 2017-11-22 09:31 Last edited: 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. |
correnson (manager) 2017-11-22 09:44 Last edited: 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)`. |
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. |
![]() |
|||
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 |