Frama-C Bug Tracking System - Frama-C
View Issue Details
0002427Frama-CPlug-in > wppublic2019-02-16 12:112019-10-17 15:36
Frama-C 18-Argon 
0002427: Prove of \false
When 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.
I am using Frama-C 18.0, Why3 0.88.3, alt-ergo 2.2.0, eprover 2.2.
No tags attached.
parent of 0002338closed correnson \false provable from recursive logic definition 
c foo.c (571) 2019-02-16 12:11
Issue History
2019-02-16 12:11jensNew Issue
2019-02-16 12:11jensStatusnew => assigned
2019-02-16 12:11jensAssigned To => correnson
2019-02-16 12:11jensFile Added: foo.c
2019-02-16 16:56jensNote Added: 0006746
2019-02-17 23:26evdenisNote Added: 0006747
2019-02-17 23:40evdenisNote Added: 0006748
2019-02-18 08:58virgileNote Added: 0006750
2019-02-18 09:50jensNote Added: 0006751
2019-10-17 15:29corrensonRelationship addedparent of 0002338
2019-10-17 15:36corrensonStatusassigned => acknowledged

2019-02-16 16:56   
If one removes the lemma "Accumulate1", then the assertion \false is not proved by eprover anymore.
2019-02-17 23:26   
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
2019-02-17 23:40   
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.
2019-02-18 08:58   
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.
2019-02-18 09:50   
Thanks for the comments!!