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 204
    • Issues 204
    • 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
  • #34
Closed
Open
Created Oct 15, 2020 by libguestfs@libguestfs

Frama-C should exit with non-zero if proving failed

$ frama-c -wp -wp-rte snippets/range_size.c 
[kernel] Parsing snippets/range_size.c (with preprocessing)
[rte] annotating function range_size
[wp] 4 goals scheduled
[wp] [Alt-Ergo 2.2.0] Goal typed_range_size_ensures : Timeout (Qed:2ms) (10s)
[wp] Proved goals:    3 / 4
  Qed:               1  (0.50ms-0.78ms)
  Alt-Ergo 2.2.0:    2  (13ms-15ms) (80) (interrupted: 1)

Proving failed, but frama-c still exits with a zero exit code:

$ echo $?
0

This problem makes it harder to use frama-c from automated CI systems.

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