2021-03-02 03:09 CET
  

View Issue Details [ Jump to Notes ] [ Issue History ] [ Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000500Frama-CPlug-in > jessiepublic2010-06-07 12:202010-12-18 11:19
ReporterJochen 
Assigned Tocmarche 
PrioritynormalSeveritytextReproducibilityalways
StatusclosedResolutionfixed 
Product VersionFrama-C Boron-20100401 
Target VersionFixed in VersionFrama-C Carbon-20101202-beta2 
Summary0000500: Uncaught exception in jc/jc_effect.ml caused by union type
DescriptionThe 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.
TagsNo tags attached.
Attached Files
  • c file icon ftest.c (301 bytes) 2010-06-07 12:20 - 
    // 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
}
    c file icon ftest.c (301 bytes) 2010-06-07 12:20 +

-Relationships
+Relationships

-Notes

~0001319

cmarche (developer)

2010-12-16 17:23
A better error message is output by Why 2.28
+Notes

-Issue History
Date Modified Username Field Change
2010-06-07 12:20 Jochen New Issue
2010-06-07 12:20 Jochen Status new => assigned
2010-06-07 12:20 Jochen Assigned To => cmarche
2010-06-07 12:20 Jochen File Added: ftest.c
2010-12-16 17:23 cmarche Note Added: 0001319
2010-12-16 17:23 cmarche Status assigned => resolved
2010-12-16 17:23 cmarche Resolution open => fixed
2010-12-18 11:18 signoles Fixed in Version => Frama-C Carbon-20101202-beta2
2010-12-18 11:19 signoles Status resolved => closed
+Issue History