View Issue Details [ Jump to Notes ] | [ Issue History ] [ Print ] | ||||||||||||
ID | Project | Category | View Status | Date Submitted | Last Update | ||||||||
---|---|---|---|---|---|---|---|---|---|---|---|---|---|
0002427 | Frama-C | Plug-in > wp | public | 2019-02-16 12:11 | 2019-10-17 15:36 | ||||||||
Reporter | jens | ||||||||||||
Assigned To | correnson | ||||||||||||
Priority | normal | Severity | minor | Reproducibility | always | ||||||||
Status | acknowledged | Resolution | open | ||||||||||
Product Version | Frama-C 18-Argon | ||||||||||||
Target Version | Fixed in Version | ||||||||||||
Summary | 0002427: Prove of \false | ||||||||||||
Description | 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. | ||||||||||||
Steps To Reproduce | I am using Frama-C 18.0, Why3 0.88.3, alt-ergo 2.2.0, eprover 2.2. | ||||||||||||
Tags | No tags attached. | ||||||||||||
Attached Files |
|
![]() |
|
jens (reporter) 2019-02-16 16:56 |
If one removes the lemma "Accumulate1", then the assertion \false is not proved by eprover anymore. |
evdenis (reporter) 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 |
evdenis (reporter) 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. |
virgile (developer) 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. |
jens (reporter) 2019-02-18 09:50 |
Thanks for the comments!! |
![]() |
|||
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 |