| Anonymous | Login | Signup for a new account | This BTS is being migrated to Gitlab, consider using those issues instead |  |
| Main | My View | View Issues | Change Log | Roadmap | Repositories |
| View Issue Details [ Jump to Notes ] | [ Issue History ] [ Print ] | ||||||||
| ID | Project | Category | View Status | Date Submitted | Last Update | ||||
| 0001092 | Frama-C | Documentation > manuals | public | 2012-02-13 13:12 | 2016-06-21 14:20 | ||||
| Reporter | Jochen | ||||||||
| Assigned To | pascal | ||||||||
| Priority | normal | Severity | text | Reproducibility | N/A | ||||
| Status | closed | Resolution | fixed | ||||||
| Platform | OS | OS Version | |||||||
| Product Version | Frama-C Nitrogen-20111001 | ||||||||
| Target Version | Fixed in Version | Frama-C Oxygen-20120901 | |||||||
| Summary | 0001092: some typos etc. in the value-analysis manual | ||||||||
| Description | During reading the value-analysis manual, I collected some typos and similar issues. They are marked in cyan in the gif images (one per page) in the attached .tar.gz file. Corresponding explanatory text is contained in the file value-analysis-typos.txt. | ||||||||
| Tags | No tags attached. | ||||||||
| Attached Files |  value-analysis.tar.gz [^] (1,449,161 bytes) 2012-02-13 13:12 | ||||||||
 Relationships |
|
 Relationships |
|
Notes |
|
|
(0002923) pascal (reporter) 2012-04-17 14:59 |
Hello, Jochen. Thanks for taking these notes while reading the manual. I should warn you about a couple of suggestions I didn't apply: - differences in log messages: I will have to play the tutorial again and update messages, but in fact, I will have to automate the updating of log messages in the manual when these change in new version. - 55: The program would be analyzed as non-terminating in any case, since an overflow is considered as equivalent to non-termination, too (cf. p.18). Right, but signed integer overflows are only considered as alarms if option -val-signed-overflow-alarms is set. Otherwise, 2's complement behavior is assumed, x eventually comes back to 0, and the loop terminates then. |
|
Notes |
|
Issue History |
|||
| Date Modified | Username | Field | Change |
| 2012-02-13 13:12 | Jochen | New Issue | |
| 2012-02-13 13:12 | Jochen | Status | new => assigned |
| 2012-02-13 13:12 | Jochen | Assigned To | => signoles |
| 2012-02-13 13:12 | Jochen | File Added: value-analysis.tar.gz | |
| 2012-02-13 13:13 | signoles | Assigned To | signoles => pascal |
| 2012-04-17 14:59 | pascal | Note Added: 0002923 | |
| 2012-04-17 15:31 | pascal | Status | assigned => resolved |
| 2012-04-17 15:31 | pascal | Resolution | open => fixed |
| 2012-09-19 17:15 | signoles | Fixed in Version | => Frama-C Oxygen-20120901 |
| 2012-09-19 17:16 | signoles | Status | resolved => closed |
| 2016-06-21 14:11 | signoles | Category | Documentation => Documentation > ACSL |
| 2016-06-21 14:20 | signoles | Category | Documentation > ACSL => Documentation > manuals |
|
Issue History |
| Copyright © 2000 - 2020 MantisBT Team |
|