X-Git-Url: http://andersk.mit.edu/gitweb/splint.git/blobdiff_plain/e6831dcb575eb57980a5e9aba4fa80527c2c4617..2bdabb7a82d577bb4789955f5b18ca29076f9bc4:/test/specclauses.out diff --git a/test/specclauses.out b/test/specclauses.out index 2ada76e..04a3972 100644 --- a/test/specclauses.out +++ b/test/specclauses.out @@ -1,6 +1,4 @@ -Cannot find standard library: ansi.lcd - Check LARCH_PATH environment variable. 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) @@ -8,13 +6,80 @@ 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:32:16: Unrecognized identifier: malloc 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:7: Unrecognized identifier: printf -specclauses.c:40:7: Field r.name used after being released +specclauses.c:40:23: Field r.name used after being released specclauses.c:39:17: Storage r.name released -Finished LCLint checking --- 8 code errors found, expected 6 +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: Undefined storage ->name corresponds to storage + result->name listed in defines clause: NULL +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 --- 6 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:27: Storage r->name becomes observer + +Finished checking --- 3 code warnings, as expected