Frama-C Bug Tracking System - Frama-C
View Issue Details
0002427Frama-CPlug-in > wppublic2019-02-16 12:112019-02-18 09:50
jens 
correnson 
normalminoralways
assignedopen 
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.
c foo.c (571) 2019-02-16 12:11
https://bts.frama-c.com/file_download.php?file_id=1302&type=bug
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

Notes
(0006746)
jens   
2019-02-16 16:56   
If one removes the lemma "Accumulate1", then the assertion \false is not proved by eprover anymore.
(0006747)
evdenis   
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 https://bts.frama-c.com/view.php?id=2338
(0006748)
evdenis   
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.
(0006750)
virgile   
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.
(0006751)
jens   
2019-02-18 09:50   
Thanks for the comments!!