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

Closed
Open
Created Jan 29, 2021 by varosi@varosi3 of 3 tasks completed3/3 tasks

An option to return error code if there are any problems with the analysis, so that frama-c is easier to be used in CI/CD workflows

Feature Request

  • the issue has not yet been reported on Gitlab;
  • the issue has not yet been reported on our old BTS (note: the old BTS is deprecated);
  • you installed Frama-C as prescribed in the instructions.

Contextual information

  • Frama-C installation mode: Docker: framac/frama-c:22.0
  • Frama-C version: 22.0
  • Plug-in used: WP and EVA
  • OS name: macOS
  • OS version: 11.1

Steps to reproduce the issue

I put frama-c in a BitBucket CI pipeline. With calling directly frama-c executable. CI pipelines fail when error code returned from executables is different than 0. That way it stops you from pushing erroneous code.

Expected behaviour

It would be great if there is an option so that frama-c executable return non-zero error code if in EVA found any error in my code, or in WP not all conditions are met.

Actual behaviour

frama-c return 0 even if EVA show errors from the analysed code. It returns 0 if WP have found non correct behaviour also.

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