specclauses.c:40:23: Field r.name used after being released
specclauses.c:39:17: Storage r.name released
-Finished LCLint checking --- 6 code errors found, as expected
+Finished checking --- 6 code warnings, as expected
-specclauses2.c:12:2: Special clause allocates includes *<parameter 1>.year of
- non-dynamically allocatated type int
+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
sets clause
This sub-reference is undefined: *(r->name)
specclauses2.c: (in function setName4)
-specclauses2.c:42:3: Implicitly only storage r->name not released before
- assignment: r->name = name
+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:76:2: Unreleased storage r->name corresponds to storage listed
in releases clause
-Finished LCLint checking --- 8 code errors found, as expected
+Finished checking --- 8 code warnings, as expected
-specclauses3.c:7:6: Function result is used in defines clause of badResult but
- not annotated with special: *(result).name
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 listed
- in defines clause: res
+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
- listed in allocates clause: res
+ result->name listed in allocates clause: res
-Finished LCLint checking --- 6 code errors found, as expected
+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
- pre:isnull clause of called function: s
+ 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
- post:isnull clause
+ ensures isnull clause
-Finished LCLint checking --- 3 code errors found, as expected
+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:26: Storage r->name becomes null
+ 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
- listed in post:observer clause: r
+ 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:27: Storage r->name becomes observer
+ specclauses5.c:48:14: Storage r->name becomes observer
-Finished LCLint checking --- 3 code errors found, as expected
+Finished checking --- 3 code warnings, as expected