Linux Driver Verification

• 6 drivers: bug in envgen #553
• 2 drivers: CIL cannot cast char[] to long/int (drivers/net/myri10ge/myri10ge.ko, drivers/crypto/padlock-sha.ko)

Drivers from the group "Error: Incompatible declaration for"¶

drivers/isdn/hardware/eicon/divas.ko (2 mains)

Structure pc_maint has different number of field in io.c(8) and diva.c(7), but the same SIZE.
So gcc has no problem with allocating memory for it. Cil does not know what to do.

• drivers/isdn/hardware/eicon/io.c:
  

  #define MIPS_SCOM
  #include "pkmaint.h" /* pc_maint.h, packed in os-dependent fashion */
  

• drivers/isdn/hardware/eicon/diva.c:
  

  #include "pc_maint.h" 
  
  

#if !defined(MIPS_SCOM)
struct pc_maint
{
  byte req;
  byte rc;
  POINTER_32BIT mem;
  short length;
  word port;
  byte fill[6];
  BUFFER data;
};
#else
struct pc_maint
{
  byte req;
  byte rc;
  byte reserved[2];     /* R3000 alignment ... */
  POINTER_32BIT mem;
  short length;
  word port;
  byte fill[4];         /* data at offset 16   */
  BUFFER data;
};
#endif

The same for drivers/net/chelsio/cxgb.ko (7 mains)
drivers/net/chelsio/pm3393.c

struct _cmac_instance {
    u8 enabled;
    u8 fc;
    u8 mac_addr[6];
};

drivers/net/chelsio/vsc7326.c

struct _cmac_instance {
    u32 index;
    u32 ticks;
};

drivers/char/ipmi/ipmi_si.ko (4 mains)
different number of fields in si_sm_data: 13 != 11 !=15.
But gcc still has no problems.

drivers/char/ipmi/ipmi_kcs_sm.c

struct si_sm_data {
    enum kcs_states  state;
    struct si_sm_io *io;
    unsigned char    write_data[MAX_KCS_WRITE_SIZE];
    int              write_pos;
    int              write_count;
    int              orig_write_count;
    unsigned char    read_data[MAX_KCS_READ_SIZE];
    int              read_pos;
    int             truncated;

    unsigned int  error_retries;
    long          ibf_timeout;
    long          obf_timeout;
    unsigned long  error0_timeout;
};

drivers/char/ipmi/ipmi_smic_sm.c

struct si_sm_data {
    enum smic_states state;
    struct si_sm_io *io;
    unsigned char     write_data[MAX_SMIC_WRITE_SIZE];
    int         write_pos;
    int         write_count;
    int         orig_write_count;
    unsigned char     read_data[MAX_SMIC_READ_SIZE];
    int         read_pos;
    int         truncated;
    unsigned int     error_retries;
    long         smic_timeout;
};

drivers/char/ipmi/ipmi_bt_sm.c

struct si_sm_data {
    enum bt_states    state;
    unsigned char    seq;        /* BT sequence number */
    struct si_sm_io    *io;
    unsigned char    write_data[IPMI_MAX_MSG_LENGTH];
    int        write_count;
    unsigned char    read_data[IPMI_MAX_MSG_LENGTH];
    int        read_count;
    int        truncated;
    long        timeout;    /* microseconds countdown */
    int        error_retries;    /* end of "common" fields */
    int        nonzero_status;    /* hung BMCs stay all 0 */
    enum bt_states    complete;    /* to divert the state machine */
    int        BT_CAP_outreqs;
    long        BT_CAP_req2rsp;
    int        BT_CAP_retries;    /* Recommended retries */
};

Proper place for CIL related bugs is its bugzilla, since we will unlikely fix them by ourselves. So reopen this issue there and mark this here.