Skip to content
GitLab
Projects Groups Topics 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
    • Contributor statistics
    • Graph
    • Compare revisions
  • Issues 171
    • Issues 171
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 0
    • Merge requests 0
  • Deployments
    • Deployments
    • Releases
  • Packages and registries
    • Packages and 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
  • #2050
Closed
Open
Issue created Jul 06, 2011 by Boris Yakobowski@byakoDeveloper

RTE does not generate assertions for non initialized arguments

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


Id Project Category View Due Date Updated
ID0000877 Frama-C Plug-in > RTE public 2011-07-06 2012-05-16
Reporter yakobowski Assigned To pherrmann Resolution fixed
Priority normal Severity major Reproducibility always
Platform - OS - OS Version -
Product Version Frama-C GIT, precise the release id Target Version - Fixed in Version Frama-C Nitrogen-20111001

Description :

Calling the WP (or Jessie for that matter) on the following code results in all goals being proven. Yet, there is a RTE on the call to max, because a is not initialized. I tend to think that -rte-precond should add \initialized(a) and \initialized(b) to the local contract for the call to max, but there is perhaps another better way. Anyway, either RTE or the WP are faulty here.

/*@ ensures \result == (a < b ? a : b); */ int max(int a, int b) { return (a < b ? a : b); }

int main () { int a; int b = 2; return max (a, b); }

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