validation/sm_skb2.c

   1 #include "check_debug.h"
   2
   3 struct sk_buff {
   4         unsigned char *head, *data;
   5         unsigned short network_header;
   6 };
   7
   8 struct foo {
   9         int a, b, c;
  10 };
  11
  12 static inline unsigned char *skb_network_header(const struct sk_buff *skb)
  13 {
  14         return skb->head + skb->network_header;
  15 }
  16
  17 static inline int skb_network_offset(const struct sk_buff *skb)
  18 {
  19         return skb_network_header(skb) - skb->data;
  20 }
  21
  22 int frob(struct sk_buff *skb)
  23 {
  24         struct foo *p;
  25         int x, y;
  26
  27         __smatch_user_rl(*skb->data);
  28         __smatch_user_rl(skb->data + 1);
  29         __smatch_user_rl(*(int *)skb->data);
  30         __smatch_user_rl(skb->data - skb_network_header(skb));
  31
  32         p = skb->data;
  33         x = *(int *)skb->data;
  34         y = skb->data[1];
  35
  36         __smatch_user_rl(p->a);
  37         __smatch_user_rl(x);
  38         __smatch_user_rl(y);
  39
  40         return 0;
  41 }
  42
  43 /*
  44  * check-name: smatch: userdata from skb
  45  * check-command: smatch -p=kernel -I.. sm_skb2.c
  46  *
  47  * check-output-start
  48 sm_skb2.c:27 frob() user rl: '*skb->data' = '0-255'
  49 sm_skb2.c:28 frob() user rl: 'skb->data + 1' = ''
  50 sm_skb2.c:29 frob() user rl: '*skb->data' = 's32min-s32max'
  51 sm_skb2.c:30 frob() user rl: 'skb->data - skb_network_header(skb)' = ''
  52 sm_skb2.c:36 frob() user rl: 'p->a' = 's32min-s32max'
  53 sm_skb2.c:37 frob() user rl: 'x' = 's32min-s32max'
  54 sm_skb2.c:38 frob() user rl: 'y' = '0-255'
  55  * check-output-end
  56  */