[WP] Type mismatch with Real model
Steps to reproduce the issue
Here is a minimal example (see foo.c):
//@ predicate Foo(double y) = y == 0.0;
void foo(double x) {
//@ assert Foo((double) (0.0 + 0.0 * x));
}
Launch Frama-C / WP with Real model: frama-c -wp -wp-model real foo.c
Expected behaviour
No error (as for frama-c -wp foo.c
):
[kernel] Parsing foo.c (with preprocessing)
[wp] Warning: Missing RTE guards
[wp] 1 goal scheduled
[wp] [Cache] found:1
[wp] Proved goals: 1 / 1
Qed: 0
Alt-Ergo 2.4.1: 1 (56ms) (400) (cached: 1)
[wp:pedantic-assigns] foo.c:3: Warning:
No 'assigns' specification for function 'foo'.
Callers assumptions might be imprecise.
Actual behaviour
Type mismatch error:
[kernel] Parsing foo.c (with preprocessing)
[wp] Warning: Missing RTE guards
[wp] 1 goal scheduled
[wp] [Alt-Ergo 2.4.1] Goal typed_real_foo_assert : Failed
[Why3 Error] Type mismatch between real and int
[wp] [Cache] not used
[wp] Proved goals: 0 / 1
Alt-Ergo 2.4.1: 0 (failed: 1)
[wp:pedantic-assigns] foo.c:3: Warning:
No 'assigns' specification for function 'foo'.
Callers assumptions might be imprecise.
Indeed, we can see with frama-c-gui
in Script mode that the expression is simplified to 0
, as we are given the following proof context:
Goal Assertion:
Prove: P_Foo(0).
Contextual information
- Frama-C installation mode: Opam
- Frama-C version: 24.0 (Chromium)
- Plug-in used: WP
- OS name: Ubuntu
- OS version: 20.04.4 LTS
Additional information
Removing the addition works:
//@ predicate Foo(double y) = y == 0.0;
void foo(double x) {
//@ assert Foo((double) (0.0 * x));
}