Use English to report an issue on the BTS. Using French is also acceptable to report a private issue.
Whenever possible, include HOW TO REPRODUCE the issue. StackOverflow's guidelines are helpful. Provide everything necessary for a smart, but not mind-reading, human 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 options from this message.
If possible, attach the automatically-generated journal (by default called
frama_c_journal.ml). Journals are enabled automatically when you use the GUI, or when using option
-journal-enable. Including a journal or a backtrace when available does not exempt you from providing the input files: a backtrace or a journal alone do not contain enough information to reproduce the behavior.
If the source code causing the issue contains confidential data, you can try using our C-Reduce scripts to minimize the code before reporting the issue.
Include the OBTAINED BEHAVIOR in enough detail that someone else can decide if they have reproduced your bug.
Include the CATEGORY, that is, which part of Frama-C is concerned by your bug report or feature request:
- Installation (opam, configure, Makefile)
- Kernel (parsing, command line, libc)
- Graphical interface (GUI)
- A plug-in (use its name)
If the bug report is not for a crash, include the EXPECTED BEHAVIOR that you would have liked to see.