LDV: refine skb allocation stubs

Created by: tautschnig

The original implementation of alloc_skb also initialises several fields of the allocated memory. Not doing so led to spurious results, e.g., CBMC running on ldv-linux-3.16-rc1/205_9a_array_safes_linux-3.16-rc1.tar.xz-205_9a-drivers--net--arcnet--capmode.ko-entry_point.cil.out.i.

The proposed implementation initialises some fields; a further refinement may be necessary.

The changes were done using the following command:

for f in c/ldv-*/*.[ci] c/ldv-*/model/*.[ci]
do
perl -i -e \
  '$s = 0;
   while(<>) {
     if(/^struct sk_buff \*__alloc_skb\(unsigned int arg0, gfp_t arg1, int arg2, int arg3\) \{\s*$/) {
       $s = 1;
     }
     elsif(/^__inline static struct sk_buff \*ldv_alloc_skb_\d+\(unsigned int size , gfp_t priority \)\s*$/) {
       $s = 2;
     }
     elsif($s == 1) {
       if(/^  return ldv_malloc\(sizeof\(struct sk_buff\)\);/) {
         print "  struct sk_buff *skb = ldv_malloc(sizeof(struct sk_buff));\n";
         print "  if(skb) {\n";
         print "    skb->head = ldv_malloc(arg0);\n";
         print "    skb->data = skb->head;\n";
         print "    skb->tail = 0;\n";
         print "  }\n";
         print "  return skb;\n";
         $s = 0;
         next;
       }
       elsif(/^\}/) {
         $s = 0;
       }
     }
     elsif($s == 2) {
       if(/^  tmp = ldv_skb_alloc\(\);/) {
         print;
         print "  if(tmp)\n";
         print "  {\n";
         print "    tmp->head = ldv_malloc(size);\n";
         print "    tmp->data = tmp->head;\n";
         print "  }\n";
         $s = 0;
         next;
       }
       elsif(/^\}/) {
         $s = 0;
       }
     }
     print;
   }' \
  $f
done