| View Issue Details [ Jump to Notes ] [ Related Changesets ] | [ Issue History ] [ Print ] |
| ID | Project | Category | View Status | Date Submitted | Last Update |
| 0000366 | Frama-C | Plug-in > jessie | public | 2010-01-04 23:24 | 2014-02-12 16:55 |
|
| Reporter | dwheeler | |
| Assigned To | monate | |
| Priority | normal | Severity | minor | Reproducibility | always |
| Status | closed | Resolution | fixed | |
| Platform | | OS | | OS Version | |
| Product Version | Frama-C Beryllium-20090902 | |
| Target Version | | Fixed in Version | Frama-C Boron-20100401 | |
|
| Summary | 0000366: Unicode minus sign (U+2212) not accepted by Jessie, yet used in documentation, causing mysterious failure |
| Description | The Jessie tutorial:
http://frama-c.cea.fr/jessie_tutorial_index.html
includes many examples, but cutting and pasting from them
produces mysterious, hard-to-understand failures.
The problem is that the HTML (and probably PDF) uses Unicode U+2212
("Minus sign") as the subtraction operator;
You can see this by searching for "−" in the HTML.
Frama-C/Jessie does not accept this; they
expect U+002D ("hyphen-minus") instead.
I recommend that Frama-C/Jessie be changed so that U+2122 is
permitted as an alternative to "-", just as many other
Unicode characters are already accepted.
In addition, the documentation should perhaps be changed to use "-"
so that it will work with older systems
that do not cut-and-paste this character correctly.
On my system, the difference is a pixel or two, and is thus
difference is rather hard to detect.
|
| Tags | No tags attached. |
|
| Attached Files | |
|
Relationships 
Relationships