Frama-C Bug Tracking System - Frama-C
View Issue Details
0002275Frama-CPlug-in > wppublic2017-02-02 16:192017-02-03 14:12
Silicon-20161101xubuntu 16.04.1 LTS
Frama-C 14-Silicon 
0002275: translation to why3 of int* argument to logic function
Running "frama-c -wp -wp-prover eprover foo.c" proves lemma "foo" in line 7, although it essentially says that no objects of type "int*" exist at all. The problem disappears if either (1) the result type "int" of "deref" is changed to "integer" in line 3, (2) "deref" is inlined at line 5, (3) "large" is inlined at line 7, or (4) "large(s) && !large(s)" is simplified to "\false" in line 7. Using option "-wp-out", and comparing the files "Axiomatic.why" before and after change (1), see attached files "Axiomatic_int.why" and "Axiomatic_integer.why", reveals that the former has an "axiom Q_TL_deref" while the latter does not. This axiom essentially says that any value fetched from an integer array (i.e. a "map addr int" in why3 language) is already an int (i.e. satisfies "is_sint32" in why3 language), which imho is wrong. When using "-wp alt-ergo" instead of "-wp eprover", the generated mlw files before and after change (1) literally agree, see attached file "lemma_foo_Alt-Ergo_int.mlw" and "lemma_foo_Alt-Ergo_integer.mlw"; they contain no occurrence of "deref" or "large". The input given to eprover has been intercepted and boiled down as far as possible, resulting in file "foo_eprover_input.p" which is attached for convenience. Its axiom "q_TL_deref" in line 18 is a boiled-down translation of axiom "Q_TL_deref" from the why3 file, and is wrong as argued above.
No tags attached.
c foo.c (152) 2017-02-02 16:19
? Axiomatic_int.why (736) 2017-02-02 16:20
? Axiomatic_integer.why (586) 2017-02-02 16:20
? lemma_foo_Alt-Ergo_int.mlw (16,102) 2017-02-02 16:20
? lemma_foo_Alt-Ergo_integer.mlw (16,102) 2017-02-02 16:21
? foo_eprover_input.p (805) 2017-02-02 16:21
Issue History
2017-02-02 16:19JochenNew Issue
2017-02-02 16:19JochenStatusnew => assigned
2017-02-02 16:19JochenAssigned To => correnson
2017-02-02 16:19JochenFile Added: foo.c
2017-02-02 16:20JochenFile Added: Axiomatic_int.why
2017-02-02 16:20JochenFile Added: Axiomatic_integer.why
2017-02-02 16:20JochenFile Added: lemma_foo_Alt-Ergo_int.mlw
2017-02-02 16:21JochenFile Added: lemma_foo_Alt-Ergo_integer.mlw
2017-02-02 16:21JochenFile Added: foo_eprover_input.p
2017-02-02 16:24JochenNote Added: 0006348
2017-02-03 10:28jensNote Added: 0006349
2017-02-03 13:01corrensonNote Added: 0006350
2017-02-03 13:01corrensonStatusassigned => confirmed
2017-02-03 13:09jensNote Added: 0006351
2017-02-03 14:12jensNote Added: 0006353

2017-02-02 16:24   
To call eprover, we used "eprover -s -R -xAuto -tAuto --cpu-limit=2 --tstp-in foo_eprover_input.p".
2017-02-03 10:28   
We came across this issue in the context of "ACSL by Example" when we observed that Eprover verified a false claim! We first thought that Eprover was the culprit but we now think that is on the WP side of Why3.
2017-02-03 13:01   
Indeed, this is an issue. We clearly miss the materialisation of a meta-hypothesis that memory accesses are well-typed. Such hypotheses are usually inserted as extra-hypotheses during WP calculus, not via axioms. We only use such axioms to assert the type of ACSL logic functions. The problem is that we may need such properties from any instance of logic function calls... Thanks for the report, we will work on a fix. Before a new version is available, please make only use of non-C types as returned values for ACSL logic functions.
2017-02-03 13:09   
Thanks for the quick reply and the pointer to a possible work around. We have currently 14 logic functions in "ACSL by Example" and roughly half of them return C types. I am confident that we can fix the ones which return "int". By we also return something like "int*" ...
2017-02-03 14:12   
As an aside, logic functions with C/C++ types are needed to model iterators.