xref: /illumos-gate/usr/src/tools/smatch/src/validation/sm_skb2.c (revision 1f5207b7604fb44407eb4342aff613f7c4508508)
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