X-Git-Url: http://andersk.mit.edu/gitweb/splint.git/blobdiff_plain/885824d34f6f6626fde2fb041801408cbaf1f6f1..f2b6724f9fdd443cbb7cd7db1ddd31c4c54fa5cf:/test/specclauses.expect

diff --git a/test/specclauses.expect b/test/specclauses.expect
index 5165507..04a3972 100644
--- a/test/specclauses.expect
+++ b/test/specclauses.expect
@@ -13,10 +13,10 @@ specclauses.c:34:17: Only storage r.name (type char *) derived from variable
 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
@@ -28,8 +28,8 @@ 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 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
@@ -40,45 +40,46 @@ specclauses2.c: (in function freeName4)
 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: Undefined storage <const ?>->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 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 --- 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
-                         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
 
-Finished LCLint checking --- 3 code errors found, as expected
+Finished checking --- 3 code warnings, as expected