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.
issue