Report an issue with Frama-C

To report an issue, You must either create an account on the GitLab of Frama-C, or use your Github account. The reporting is done through the issue tracking system.

If you are creating your account for your first bug report, consider this trade-off carefully: we will never use your e-mail address to contact you for something other than the bug you reported. But if you provide an invalid e-mail address, your bug may linger for months because the assignee is waiting for more feedback and you didn’t receive the notice.

The menu “Choose a template” provides a template “bug_report” that you just have to fill in.

Some advices to post your issue:

  • Use English to report an issue. Using French is also acceptable to report a private issue.
  • If the bug report is not for a crash, include the EXPECTED BEHAVIOR that you would have liked to see.
  • Include the OBTAINED BEHAVIOR in enough detail that someone else can decide if they have reproduced your bug.
  • Include HOW TO REPRODUCE the issue. Provide everything necessary for someone else to reproduce the bug: input files, command line used, sequence of actions. If your analysis project depends on system headers, please use one of the two following options to be sure that:
    • (Preferred) Use the option -print of Frama-C
      $ frama-c ./your_files*.c -ocode result.c
      
    • Use the preprocessor (Note however that this second option will drop ACSL annotations, using -CC keeps all comments):
      $ gcc -C -E -I . original.c > result.i
      

The status of an issue may be one of the following:

  • new: the issue has not been yet considered by any Frama-C developer.
  • assigned: the issue has been assigned to a Frama-C developer. However the assignee has not yet considered this issue.
  • confirmed: the issue has been confirmed by the assignee (or by any Frama-C developer if there is no assignee). It is really a bug or a wished feature.
  • resolved: the issue has been fixed by the assignee. The Frama-C development version contains the patch which will be part of a future release.
  • closed: the issue is no more relevant. Either it is not really a bug or a wished feature, or it is fixed in a public release available from the download page of Frama-C.