test/specclauses.out

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