translation to why3 of int* argument to logic function
ID0002275: This issue was created automatically from Mantis Issue 2275. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0002275 | Frama-C | Plug-in > wp | public | 2017-02-02 | 2017-02-03 |
| Reporter | Jochen | Assigned To | correnson | Resolution | open |
| Priority | normal | Severity | minor | Reproducibility | always |
| Platform | Silicon-20161101 | OS | xubuntu 16.04.1 LTS | OS Version | - |
| Product Version | Frama-C 14-Silicon | Target Version | - | Fixed in Version | - |
Description :
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.