1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
|
specclauses.c: (in function f)
specclauses.c:24:28: Only storage r.name (type char *) derived from variable
declared in this scope is not released (memory leak)
specclauses.c:28:24: Undefined storage r.name corresponds to storage listed in
uses clause of called function: r
specclauses.c:28:28: Only storage name not released before return
specclauses.c:17:49: Storage name becomes only
specclauses.c:33:16: Allocated storage r.name corresponds to storage listed in
defines clause of called function: &r
specclauses.c:34:17: Only storage r.name (type char *) derived from variable
declared in this scope is not released (memory leak)
specclauses.c:40:23: Field r.name used after being released
specclauses.c:39:17: Storage r.name released
Finished checking --- 6 code warnings, as expected
specclauses2.c:10:13: Allocates clauses includes r->year of non-dynamically
allocated type int
specclauses2.c: (in function allocYear)
specclauses2.c:14:2: Unallocated storage r->year corresponds to storage listed
in allocates clause
specclauses2.c: (in function setName1)
specclauses2.c:26:2: Undefined storage r->name corresponds to storage listed in
defines clause
specclauses2.c: (in function setName3)
specclauses2.c:37:2: Undefined storage r->name corresponds to storage listed in
sets clause
This sub-reference is undefined: *(r->name)
specclauses2.c: (in function setName4)
specclauses2.c:42:3: Implicitly only storage r->name (type char *) not released
before assignment: r->name = name
specclauses2.c: (in function allocName2)
specclauses2.c:54:2: Unallocated storage r->name corresponds to storage listed
in allocates clause
specclauses2.c: (in function freeName2)
specclauses2.c:65:2: Unreleased storage r.name corresponds to storage listed in
releases clause
specclauses2.c: (in function freeName4)
specclauses2.c:76:2: Unreleased storage r->name corresponds to storage listed
in releases clause
Finished checking --- 8 code warnings, as expected
specclauses3.c:7:6: Special clause accesses field of non-struct or union result
(int): *(result).name
specclauses3.c: (in function badResult)
specclauses3.c:12:10: Null storage returned as non-null: NULL
specclauses3.c: (in function createName2)
specclauses3.c:29:10: Undefined storage res->name corresponds to storage
result->name listed in defines clause: res
specclauses3.c:29:10: Possibly null storage res returned as non-null: res
specclauses3.c:28:16: Storage res may become null
specclauses3.c: (in function createName4)
specclauses3.c:55:10: Unallocated storage res->name corresponds to storage
result->name listed in allocates clause: res
Finished checking --- 5 code warnings, as expected
specclauses4.c: (in function usename)
specclauses4.c:13:4: Dereference of null pointer *name: **name
specclauses4.c:11:8: Storage *name becomes null
specclauses4.c: (in function callname)
specclauses4.c:27:12: Non-null storage *s corresponds to storage listed in
requires isnull clause of called function: s
specclauses4.c: (in function nullname2)
specclauses4.c:42:2: Non-null storage *name corresponds to storage listed in
ensures isnull clause
Finished checking --- 3 code warnings, as expected
specclauses5.c: (in function createrecord2)
specclauses5.c:31:10: Null storage r->name derivable from return value: r
specclauses5.c:30:14: Storage r->name becomes null
specclauses5.c: (in function newrecord2)
specclauses5.c:43:10: Non-observer storage r->name corresponds to storage
result->name listed in ensures observer clause: r
specclauses5.c: (in function createrecordx)
specclauses5.c:49:10: Observer storage r->name reachable from unqualified
return value
specclauses5.c:48:14: Storage r->name becomes observer
Finished checking --- 3 code warnings, as expected
|
