Linux Driver Verification » BLAST

I reduced the example up to the following (comments show where cil fails):

union ktime
{
};
typedef union ktime ktime_t;
struct hrtimer
{
  ktime_t _expires;
};
static inline ktime_t hrtimer_get_expires(struct hrtimer const *timer)
{
  /* Error: Cannot find matching union field in cast
     Error: cabs2cil/castTo: illegal cast  int  -> union ktime */
  return ( ktime_t ) ( * timer ) . _expires;
}

Gcc parses such the code even with -Wall option and it seems to be the correct one. So I believe that it's some bug in cil.
Even though this doesn't affect on next blast checking (it does it!) sometimes it may corrupt the whole process. Note that the only difference in comparing with the original source code is absence of explicit conversion ('->' is absolutely the same as '(*).'):

static inline ktime_t hrtimer_get_expires(const struct hrtimer *timer)
{
 return timer->_expires;
}

Since ldv gcc pretty printer never skip explicit conversions as well as implicit ones this also must be related with cil.