Generating metrics.html on demand
ID0000784: This issue was created automatically from Mantis Issue 784. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0000784 | Frama-C | Plug-in > metrics | public | 2011-04-11 | 2014-02-12 |
| Reporter | signoles | Assigned To | monate | Resolution | fixed |
| Priority | normal | Severity | minor | Reproducibility | always |
| Platform | - | OS | - | OS Version | - |
| Product Version | Frama-C Carbon-20110201 | Target Version | - | Fixed in Version | Frama-C Nitrogen-20111001 |
Description :
When computing metrics (via a command line option or the GUI), then file metrics.html is created in the current directory (or the plug-in crashes if there is a system error when opening, writing into, closing the file).
It would be nice:
- to generate the file only on demand (through a new command line option taking a filename as argument)
- to prevent crashes by catching exceptions.