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