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 */ 57