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