2021-03-03 03:05 CET
  

View Issue Details [ Jump to Notes ] [ Issue History ] [ Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0002332Frama-CPlug-in > wppublic2017-11-22 08:482019-10-17 18:02
Reporterjens 
Assigned Tocorrenson 
PrioritynormalSeveritymajorReproducibilityalways
StatusclosedResolutionno change required 
PlatformLinux, macOSOSOS Version
Product VersionFrama-C 15-Phosphorus 
Target VersionFixed in Version 
Summary0002332: Information on C type of array is not present (in Coq)
DescriptionIn 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 ReproduceRun the command:

  frama-c-gui -no-unicode -wp -wp-prover alt-ergo -wp-prover coq -wp-script 'wp0.script' array.c
Additional InformationThe error also occurs in the beta release of Frama-C 16 (Sulfur).
TagsNo tags attached.
Attached Files
  • c file icon array.c (345 bytes) 2017-11-22 08:48 - 
    /*@
  predicate
    AllEqual{L}(int* a) = a[0] == a[1];

  predicate
    Constant{L}(int* a, int v) = (a[0] == v) && (a[1] == v);

  lemma ConstantImpliesAllEqual{L}:
    \forall int *a, v;
      Constant(a, v) ==> AllEqual(a);

  lemma AllEqualImpliesConstant{L}:
    \forall int *a;
      AllEqual(a) ==> (\exists int v; Constant(a, v));
*/
    c file icon array.c (345 bytes) 2017-11-22 08:48 +
  • ? file icon wp0.script (271 bytes) 2017-11-22 08:49

-Relationships
+Relationships

-Notes

~0006471

correnson (manager)

2017-11-22 09:31

Last edited: 2017-11-22 09:41

View 4 revisions

 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

Last edited: 2017-11-22 09:45

View 3 revisions

 **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.
+Notes

-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
+Issue History