|Anonymous | Login | Signup for a new account||2018-12-18 21:30 CET|
|Main | My View | View Issues | Change Log | Roadmap | Repositories|
|View Issue Details|
|ID||Project||Category||View Status||Date Submitted||Last Update|
|0002338||Frama-C||Plug-in > wp||public||2017-12-18 12:43||2017-12-18 16:55|
|Platform||Sulfur-20171101||OS||Ubuntu 17.04||OS Version|
|Target Version||Fixed in Version|
|Summary||0002338: \false provable from recursive logic definition|
|Description||Running "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.
|Tags||No tags attached.|
|Attached Files|| foo.c [^] (220 bytes) 2017-12-18 12:43 [Show Content]
diff.txt [^] (1,575 bytes) 2017-12-18 13:28 [Show Content]
eprover.input [^] (3,591 bytes) 2017-12-18 16:55
|The naming dependance (3) reminds me to the closed issue 0002237, where ordering of goals was involved, too. Maybe both issues are related?|
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/.
|Yes I think the order / dependency problem is harmful here... Thanks for the inputs, it would help to fix the entire problem.|
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.
|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 - 2018 MantisBT Team|