| View Issue Details [ Jump to Notes ] | [ Issue History ] [ Print ] |
| ID | Project | Category | View Status | Date Submitted | Last Update |
| 0000500 | Frama-C | Plug-in > jessie | public | 2010-06-07 12:20 | 2010-12-18 11:19 |
|
| Reporter | Jochen | |
| Assigned To | cmarche | |
| Priority | normal | Severity | text | Reproducibility | always |
| Status | closed | Resolution | fixed | |
| Platform | | OS | | OS Version | |
| Product Version | Frama-C Boron-20100401 | |
| Target Version | | Fixed in Version | Frama-C Carbon-20101202-beta2 | |
|
| Summary | 0000500: Uncaught exception in jc/jc_effect.ml caused by union type |
| Description | The attached program tries to do a dirty conversion from char* to int (just to test the limits of Jessie).
If this is done by a cast, Jessie properly reports <<Jessie plugin can not be used on your code>>.
If this is done by a union type, however, Jessie reports <<Uncaught exception: File "jc/jc_effect.ml", line 1356, characters 22-28: Assertion failed>>. Probably that exception should be caught and <<...cannot be used on your code>> should be reported in this case, too.
See the attached program; comment-out and uncomment the line "#define testUnion" to reproduce both behaviours. |
| Tags | No tags attached. |
|
| Attached Files |  ftest.c [^] (301 bytes) 2010-06-07 12:20 [Show Content] [Hide Content]
// uncomment to show insufficient error message wrt union:
#define testUnion
#define NULL ((void*)0)
/*@
requires s != NULL;
ensures \result != 0;
*/
int conv(char *s)
{
#ifdef testUnion
union _u { char *s; int a; } u;
u.s = s;
return u.a;
#else
return (int)s;
#endif
}
|
|
Relationships 
Relationships