Skip to content

GitLab

  • Menu
Projects Groups Snippets
    • Loading...
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
    • Contribute to GitLab
  • Sign in
  • F frama-c
  • Project information
    • Project information
    • Activity
    • Labels
    • Members
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
  • Issues 209
    • Issues 209
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 0
    • Merge requests 0
  • Deployments
    • Deployments
    • Releases
  • Monitor
    • Monitor
    • Incidents
  • Packages & Registries
    • Packages & Registries
    • Container Registry
  • Analytics
    • Analytics
    • Value stream
    • Repository
  • Wiki
    • Wiki
  • Activity
  • Graph
  • Create a new issue
  • Commits
  • Issue Boards
Collapse sidebar
  • pub
  • frama-c
  • Issues
  • #2596

Closed
Open
Created Mar 15, 2022 by Lélio Brun@Lelio-Brun

[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));
}
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information
Assignee
Assign to
Time tracking