Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0002427Frama-CPlug-in > wppublic2019-02-16 12:112019-10-17 15:36
Reporterjens 
Assigned Tocorrenson 
PrioritynormalSeverityminorReproducibilityalways
StatusacknowledgedResolutionopen 
PlatformOSOS Version
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 Filesc file icon foo.c [^] (571 bytes) 2019-02-16 12:11 [Show Content]

- Relationships
parent of 0002338resolvedcorrenson \false provable from recursive logic definition 

-  Notes
(0006746)
jens (reporter)
2019-02-16 16:56

If one removes the lemma "Accumulate1", then the assertion \false is not proved by eprover anymore.
(0006747)
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
(0006748)
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.
(0006750)
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.
(0006751)
jens (reporter)
2019-02-18 09:50

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


Copyright © 2000 - 2019 MantisBT Team
Powered by Mantis Bugtracker