2021-03-01 23:33 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0002427Frama-CPlug-in > wppublic2019-10-17 15:36
Assigned Tocorrenson 
Product VersionFrama-C 18-Argon 
Target VersionFixed in Version 
Summary0002427: Prove of \false
DescriptionWhen the attached program foo.c is analysed with the command line

    frama-c -pp-annot -no-unicode -wp -wp-prover alt-ergo -wp-prover eprover foo.c

then the assertion "\false" is verified with "eprover" (2.2).
To me the axiomatics and the lemma look fine which would mean that it is a problem of "eprover".
However, I would like that an WP expert has a look at it before I contact the developer of "eprover".
Thanks in advance.
Steps To ReproduceI am using Frama-C 18.0, Why3 0.88.3, alt-ergo 2.2.0, eprover 2.2.
TagsNo tags attached.
Attached Files
  • c file icon foo.c (571 bytes) 2019-02-16 12:11 -
      axiomatic AccumulateAxiomatic 
        logic int Accumulate{L}(int* a, integer n, int init) reads a[0..n-1]; 
            \forall int *a, init, integer n;
              n <= 0 ==> Accumulate(a, n, init) == init;
            \forall int *a, init, integer n;
              0 < n ==> Accumulate(a, n, init) == Accumulate(a, n-1, init) + a[n-1];
          \forall int *a, init; Accumulate{L}(a, 1, init) == init + a[0];
    int foo()
      //@ assert danger: \false;
      return 1;
    c file icon foo.c (571 bytes) 2019-02-16 12:11 +

parent of 0002338closedcorrenson \false provable from recursive logic definition 



jens (reporter)

If one removes the lemma "Accumulate1", then the assertion \false is not proved by eprover anymore.


evdenis (reporter)

Interesting enough that you could remove the 2 axioms from the axiomatic block. This will not affect the provability of assert \false. I think that the issue might be related to this one https://bts.frama-c.com/view.php?id=2338


evdenis (reporter)

Please, use integer (Z) as a return value for the Accumulate function. I'm not quite understand for now the output of Eprover but I definetely understand that it tries to instantiate the quantifiers with INT_MIN/INT_MAX values.


virgile (developer)

I agree with evdenis: the statement of the lemma is contradictory in itself, regardless of the definition of Accumulate. Namely, as Accumulate is supposed to return an int, and the addition on the rhs of the equality in Accumulate1 occurs in integer, if you instantiate it with a sufficiently large (or small) value of init and a[0], you'll have issues.


jens (reporter)

Thanks for the comments!!

-Issue History
Date Modified Username Field Change
2019-02-16 12:11 jens New Issue
2019-02-16 12:11 jens Status new => assigned
2019-02-16 12:11 jens Assigned To => correnson
2019-02-16 12:11 jens File Added: foo.c
2019-02-16 16:56 jens Note Added: 0006746
2019-02-17 23:26 evdenis Note Added: 0006747
2019-02-17 23:40 evdenis Note Added: 0006748
2019-02-18 08:58 virgile Note Added: 0006750
2019-02-18 09:50 jens Note Added: 0006751
2019-10-17 15:29 correnson Relationship added parent of 0002338
2019-10-17 15:36 correnson Status assigned => acknowledged
+Issue History