]> andersk Git - splint.git/blame - test/sharing5.c
noexpand always false.
[splint.git] / test / sharing5.c
CommitLineData
885824d3 1extern void free (/*@out@*/ /*@only@*/ void *s);
2extern /*@only@*/ char *string_copy (char *s);
3
4void f(/*@only@*/ char *only1, /*@only@*/ char *only2, /*@only@*/ char *only3,
5 /*@shared@*/ char *shared)
6{
7 char *local1, *local2, *local4;
8 char **localp;
9
10 local1 = only1;
11 *only1 = 'c'; /* okay */
12 free (local1); /* okay --- kills only1 */
13 *only1 = 'c'; /* 1. bad --- only1 is dead */
14
15 if (3 > 4)
16 {
17 local2 = only2;
18 }
19 else
20 {
21 local2 = shared;
22 } /* 2. Clauses exit with local2 referencing dependant storage in true */
23
24 free (local2); /* 3. bad --- could free shared2 (may kill only2) */
25
26 localp = malloc(sizeof(char *));
27 *localp = only3; /* 4. possible null deref */
28
29 local4 = only3;
30 local4 = NULL; /* okay */
31
32 localp = &only3; /* 5. new storage not released */
33} /* 6. only3 may not be released [[[ only2 ??? ]]] */
34
35
36
37
38
39
40
41
This page took 0.07257 seconds and 5 git commands to generate.