GitLab

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));
}