Skip to content

GitLab

  • Menu
Projects Groups Snippets
  • 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 201
    • Issues 201
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 0
    • Merge requests 0
  • Deployments
    • Deployments
    • Releases
  • Packages & Registries
    • Packages & Registries
    • Container Registry
  • Monitor
    • Monitor
    • Incidents
  • Analytics
    • Analytics
    • Value stream
    • Repository
  • Wiki
    • Wiki
  • Activity
  • Graph
  • Create a new issue
  • Commits
  • Issue Boards
Collapse sidebar
  • pub
  • frama-c
  • Issues
  • #617
Closed
Open
Created Jun 29, 2015 by David Cok@cokDeveloper

deficient axioms

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


Id Project Category View Due Date Updated
ID0002138 Frama-C Plug-in > wp public 2015-06-29 2015-06-29
Reporter DavidCok Assigned To correnson Resolution no change required
Priority normal Severity major Reproducibility always
Platform - OS Windows OS Version 7
Product Version Frama-C Neon-20140301 Target Version - Fixed in Version -

Description :

The proof of the following with -WP and alt-ergo fails:

/*@ requires (int)(x+y) == x+y; ensures \result == x+y; */ int f(int x, int y) { return x+y; }

On inspecting the intermediate artifacts, we identified the problem as inadequate axioms. Two solutions requiring changes in axioms worked for us. However, I don't know if either change would have wider ramifications.

axiom is_to_sint32 : (forall x:int [is_sint32(to_sint32(x))]. is_sint32(to_sint32(x)))

The effect of the triggers in this axiom is simply to allow is_sint32(to_sint32(x)) to be reduced to true. In fact the more common need is to know that to_sint32(x) satisfies is_sint32. The proof above goes through if the trigger is changed to

axiom is_to_sint32 : (forall x:int [to_sint32(x)]. is_sint32(to_sint32(x)))

axiom id_sint32 : (forall x:int [to_sint32(x)]. ((((-2147483648) <= x) and (x < 2147483648)) -> (to_sint32(x) = x)))

This axiom is much more useful if it is written as an equivalence instead of an implication. Doing so also enables the proof of the program above to go through.

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