Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0002275Frama-CPlug-in > wppublic2017-02-02 16:192017-02-03 14:12
ReporterJochen 
Assigned Tocorrenson 
PrioritynormalSeverityminorReproducibilityalways
StatusconfirmedResolutionopen 
PlatformSilicon-20161101OSxubuntu 16.04.1 LTS OS Version
Product VersionFrama-C 14-Silicon 
Target VersionFixed in Version 
Summary0002275: translation to why3 of int* argument to logic function
DescriptionRunning "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.
TagsNo tags attached.
Attached Filesc file icon foo.c [^] (152 bytes) 2017-02-02 16:19 [Show Content]
? file icon Axiomatic_int.why [^] (736 bytes) 2017-02-02 16:20
? file icon Axiomatic_integer.why [^] (586 bytes) 2017-02-02 16:20
? file icon lemma_foo_Alt-Ergo_int.mlw [^] (16,102 bytes) 2017-02-02 16:20
? file icon lemma_foo_Alt-Ergo_integer.mlw [^] (16,102 bytes) 2017-02-02 16:21
? file icon foo_eprover_input.p [^] (805 bytes) 2017-02-02 16:21

- Relationships

-  Notes
(0006348)
Jochen (reporter)
2017-02-02 16:24

To call eprover, we used "eprover -s -R -xAuto -tAuto --cpu-limit=2 --tstp-in foo_eprover_input.p".
(0006349)
jens (reporter)
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.
(0006350)
correnson (manager)
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.
(0006351)
jens (reporter)
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*" ...
(0006353)
jens (reporter)
2017-02-03 14:12

As an aside, logic functions with C/C++ types are needed to model iterators.

- Issue History
Date Modified Username Field Change
2017-02-02 16:19 Jochen New Issue
2017-02-02 16:19 Jochen Status new => assigned
2017-02-02 16:19 Jochen Assigned To => correnson
2017-02-02 16:19 Jochen File Added: foo.c
2017-02-02 16:20 Jochen File Added: Axiomatic_int.why
2017-02-02 16:20 Jochen File Added: Axiomatic_integer.why
2017-02-02 16:20 Jochen File Added: lemma_foo_Alt-Ergo_int.mlw
2017-02-02 16:21 Jochen File Added: lemma_foo_Alt-Ergo_integer.mlw
2017-02-02 16:21 Jochen File Added: foo_eprover_input.p
2017-02-02 16:24 Jochen Note Added: 0006348
2017-02-03 10:28 jens Note Added: 0006349
2017-02-03 13:01 correnson Note Added: 0006350
2017-02-03 13:01 correnson Status assigned => confirmed
2017-02-03 13:09 jens Note Added: 0006351
2017-02-03 14:12 jens Note Added: 0006353


Copyright © 2000 - 2019 MantisBT Team
Powered by Mantis Bugtracker