|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|
|Assigned To||cmarche|| |
|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]