| View Issue Details [ Jump to Notes ] [ Related Changesets ] | [ Issue History ] [ Print ] |
| ID | Project | Category | View Status | Date Submitted | Last Update |
| 0000784 | Frama-C | Plug-in > metrics | public | 2011-04-11 16:01 | 2014-02-12 16:59 |
|
| Reporter | signoles | |
| Assigned To | monate | |
| Priority | normal | Severity | minor | Reproducibility | always |
| Status | closed | Resolution | fixed | |
| Platform | | OS | | OS Version | |
| Product Version | Frama-C Carbon-20110201 | |
| Target Version | | Fixed in Version | Frama-C Nitrogen-20111001 | |
|
| Summary | 0000784: Generating metrics.html on demand |
| 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. |
| Tags | No tags attached. |
|
| Attached Files | |
|
Relationships 
Relationships