Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0002338Frama-CPlug-in > wppublic2017-12-18 12:432017-12-18 16:55
Assigned Tocorrenson 
PlatformSulfur-20171101OSUbuntu 17.04OS Version
Product Version 
Target VersionFixed in Version 
Summary0002338: \false provable from recursive logic definition
DescriptionRunning "frama-c -wp foo.c -wp-prover alt-ergo -wp-prover eprover" on the attached file proves all goals, including a lemma "Check" which just says "\false", from nothing but a recursive definition of a logic int function.
The latter is well-founded since its only recursive call uses a parameter value n==0 which immediately employs the base case.

The problem disappears
(1) when "integer" is used as result type and as 3rd parameter type,
(2) when "a[]" is omitted,
(3) when lemma "Alpha" is renamed to a name lexicographically after "Check", or
(4) when "cvc3" or "cvc4-15" is used instead of "eprover".
The problem remains, however, when "z3" is used.
TagsNo tags attached.
Attached Filesc file icon foo.c [^] (220 bytes) 2017-12-18 12:43 [Show Content]
txt file icon diff.txt [^] (1,575 bytes) 2017-12-18 13:28 [Show Content]
? file icon eprover.input [^] (3,591 bytes) 2017-12-18 16:55

- Relationships

-  Notes
Jochen (reporter)
2017-12-18 12:57

The naming dependance (3) reminds me to the closed issue 0002237, where ordering of goals was involved, too. Maybe both issues are related?
Jochen (reporter)
2017-12-18 13:28

Trying to track down the naming dependence (3) somewhat further, I ran the above command with "-wp-out outA" added on the original file "foo.c", and with "-wp-out outD" on a modification of "foo.c" where "AInit" was renamed to "DInit". Then I renamed the files in "outD/typed" appropriately (e.g. "lemma_DInit.ergo" to "lemma_AInit.ergo"), and ran "diff -r outA outD >diff.txt" (attached).

It appears to me the only difference is in file "Axiomatic.why" where the order is "Q_TL_Acc, Q_AInit, Q_Check" in outA/, but "Q_Check, Q_TL_Acc, Q_DInit" in outD/.
correnson (manager)
2017-12-18 14:59

Yes I think the order / dependency problem is harmful here... Thanks for the inputs, it would help to fix the entire problem.
Jochen (reporter)
2017-12-18 16:55

I managed to intercept the input given to eprover, and to boil it down to the version in "eprover.input" (attached).

The call "eprover -s -R -xAuto -tAuto --cpu-limit=10 --tstp-in eprover.input" (options as observed from the call by why3) results in "$false" being proven. None of the axioms can be deleted without losing the provability.

A strange list of predicates is involved in the inconsistency, viz.
    base from_int get included infix_ls infix_lseq infix_pl infix_pl1 is_sint32 is_uint32 l_Acc mk_addr mod offset prefix_mn prefix_mn1 separated shift to_sint32 to_uint32 truncate valid_rd valid_rw
(generated from "eprover.input"). Intersting enough, the translation of the lemma "AInit" doesn't appear in the file. It seems that this lemma is needed in the C source only to ensure inclusion of some axioms that participate in the inconsistency.

- Issue History
Date Modified Username Field Change
2017-12-18 12:43 Jochen New Issue
2017-12-18 12:43 Jochen Status new => assigned
2017-12-18 12:43 Jochen Assigned To => correnson
2017-12-18 12:43 Jochen File Added: foo.c
2017-12-18 12:57 Jochen Note Added: 0006492
2017-12-18 13:28 Jochen Note Added: 0006493
2017-12-18 13:28 Jochen File Added: diff.txt
2017-12-18 14:59 correnson Note Added: 0006495
2017-12-18 16:55 Jochen Note Added: 0006498
2017-12-18 16:55 Jochen File Added: eprover.input

Copyright © 2000 - 2019 MantisBT Team
Powered by Mantis Bugtracker