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 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
  • #1265

Closed
Open
Created Jan 26, 2011 by Julien Signoles@signolesDeveloper

Value may be incorrect in presence of several ensures

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


Id Project Category View Due Date Updated
ID0000689 Frama-C Plug-in > Eva public 2011-01-26 2014-02-12
Reporter signoles Assigned To monate Resolution fixed
Priority normal Severity major Reproducibility always
Platform - OS - OS Version -
Product Version Frama-C Carbon-20101202-beta2 Target Version - Fixed in Version Frama-C Nitrogen-20111001

Description :

If a function has 1 valid ensure and 1 invalid ensure, the GUI says that both ensures are invalid.

Steps To Reproduce :

==== a.c ==== /*@ ensures \result == 0; @ ensures \false; @ */ int f(void) { return 0; }

void main(void) { f(); }

$ frama-c-gui a.c

Then check the property status of both ensures.

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