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 1
    • Merge requests 1
  • 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
  • #508

Closed
Open
Created May 31, 2016 by mantis-gitlab-migration@mantis-gitlab-migration

Validation fails when predicate is used with implicit type conversion.

ID0002229: This issue was created automatically from Mantis Issue 2229. Further discussion may take place here.


Id Project Category View Due Date Updated
ID0002229 Frama-C Plug-in > wp public 2016-05-31 2016-05-31
Reporter Ian Assigned To correnson Resolution open
Priority normal Severity minor Reproducibility always
Platform Ubuntu OS - OS Version -
Product Version Frama-C Magnesium Target Version - Fixed in Version -

Description :

When there is an implicit type conversion on a parameter, and the value is checked by a predicate, validation fails when it should succeed.

In the example below, the functions foo and foo_pred have the same precondition, except foo_pred has the statement in a predicate. foo validates while foo_pred does not.

run2 validates the assertion, showing the precondition should be true, but foo_pred still fails.

run3 is similar to run2 except a ghost variable is used. This causes foo_pred to validate.

Steps To Reproduce :

File foo.c (attached): /*@ predicate bar_req(int i) = ((unsigned char) i) == i; */

//@ requires ((unsigned char) i) == i; void foo(int i) { }

//@ requires bar_req(i); void foo_pred(int i) { }

void run(char c) { unsigned char uc = c; foo(uc); // Valid foo_pred(uc); // Fails }

void run2(char c) { unsigned char uc = c; //@ assert ((unsigned char) ((int) uc)) == uc; foo_pred(uc); // Fails }

void run3(char c) { unsigned char uc = c; //@ ghost int ic = uc; //@ assert ((unsigned char) ic) == uc; foo_pred(uc); // Valid }

Run command: frama-c foo.c -wp -wp-prover why3:alt-ergo -wp-model=typed+Cast

[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing) [kernel] Parsing foo.c (with preprocessing) [wp] warning: Missing RTE guards [wp] 6 goals scheduled [wp] [alt-ergo] Goal typed_cast_run2_call_foo_pred_pre : Unknown (158ms) [wp] [alt-ergo] Goal typed_cast_run_call_foo_pred_pre : Unknown (Qed:0.54ms) (157ms) [wp] Proved goals: 4 / 6 Qed: 3 alt-ergo: 1 (10ms) (unknown: 2)

Attachments

  • foo.c
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information
Assignee
Assign to
Time tracking