Fixing c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-43_2a-drivers--usb--serial--digi_acceleport.ko-entry_point_true-unreach-call.cil.out.c

Author: marek-trtik

c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-43_2a-drivers--usb--serial--digi_acceleport.ko-entry_point_true-unreach-call.cil.out.c

@@ -1,4 +1,13 @@
 extern void __VERIFIER_error() __attribute__ ((__noreturn__));
+
+extern void abort (void) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__));
+void memcpy_guard(void* p1, void* p2, unsigned long int n)
+{
+    if ((char*)p1 + n <= (char*)p2 || (char*)p2 + n <= (char*)p1)
+        return;
+    abort();
+}
+
 /* Generated by CIL v. 1.5.1 */
 /* print_CIL_Input is false */
 
@@ -4595,6 +4604,7 @@ static int digi_write_oob_command(struct usb_serial_port *port , unsigned char *
   } else {
 
   }
+  memcpy_guard((oob_port->write_urb)->transfer_buffer, (void const   *)buf, (size_t )len);
   memcpy((oob_port->write_urb)->transfer_buffer, (void const   *)buf, (size_t )len);
   (oob_port->write_urb)->transfer_buffer_length = (u32 )len;
   ret = ldv_usb_submit_urb_28(oob_port->write_urb, 32U);
@@ -4693,11 +4703,15 @@ static int digi_write_inb_command(struct usb_serial_port *port , unsigned char *
   if (priv->dp_out_buf_len > 0) {
     *data = 18U;
     *(data + 1UL) = (unsigned char )priv->dp_out_buf_len;
+    memcpy_guard((void *)data + 2U, (void const   *)(& priv->dp_out_buf), (size_t )priv->dp_out_buf_len);
     memcpy((void *)data + 2U, (void const   *)(& priv->dp_out_buf), (size_t )priv->dp_out_buf_len);
+    memcpy_guard((void *)(data + ((unsigned long )priv->dp_out_buf_len + 2UL)), (void const   *)buf,
+             (size_t )len);
     memcpy((void *)(data + ((unsigned long )priv->dp_out_buf_len + 2UL)), (void const   *)buf,
              (size_t )len);
     (port->write_urb)->transfer_buffer_length = (u32 )((priv->dp_out_buf_len + 2) + len);
   } else {
+    memcpy_guard((void *)data, (void const   *)buf, (size_t )len);
     memcpy((void *)data, (void const   *)buf, (size_t )len);
     (port->write_urb)->transfer_buffer_length = (u32 )len;
   }
@@ -5443,8 +5457,10 @@ static int digi_write(struct tty_struct *tty , struct usb_serial_port *port , un
   tmp___4 = data;
   data = data + 1;
   *tmp___4 = (unsigned char )data_len;
+  memcpy_guard((void *)data, (void const   *)(& priv->dp_out_buf), (size_t )priv->dp_out_buf_len);
   memcpy((void *)data, (void const   *)(& priv->dp_out_buf), (size_t )priv->dp_out_buf_len);
   data = data + (unsigned long )priv->dp_out_buf_len;
+  memcpy_guard((void *)data, (void const   *)buf, (size_t )new_len);
   memcpy((void *)data, (void const   *)buf, (size_t )new_len);
   ret = ldv_usb_submit_urb_32(port->write_urb, 32U);
   if (ret == 0) {
@@ -5560,6 +5576,8 @@ static void digi_write_bulk_callback(struct urb *urb )
     *((unsigned char *)(port->write_urb)->transfer_buffer) = 18U;
     *((unsigned char *)(port->write_urb)->transfer_buffer + 1UL) = (unsigned char )priv->dp_out_buf_len;
     (port->write_urb)->transfer_buffer_length = (u32 )(priv->dp_out_buf_len + 2);
+    memcpy_guard((port->write_urb)->transfer_buffer + 2UL, (void const   *)(& priv->dp_out_buf),
+             (size_t )priv->dp_out_buf_len);
     memcpy((port->write_urb)->transfer_buffer + 2UL, (void const   *)(& priv->dp_out_buf),
              (size_t )priv->dp_out_buf_len);
     ret = ldv_usb_submit_urb_33(port->write_urb, 32U);