test/specclauses.expect

   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 checking --- 6 code warnings, as expected
  17
  18 specclauses2.c:10:13: Allocates clauses includes r->year of non-dynamically
  19                          allocated 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 (type char *) not released
  32                         before 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 checking --- 8 code warnings, as expected
  44
  45 specclauses3.c:7:6: Special clause accesses field of non-struct or union result
  46                        (int): *(result).name
  47 specclauses3.c: (in function badResult)
  48 specclauses3.c:12:10: Null storage returned as non-null: NULL
  49 specclauses3.c: (in function createName2)
  50 specclauses3.c:29:10: Undefined storage res->name corresponds to storage
  51                          result->name listed in defines clause: res
  52 specclauses3.c:29:10: Possibly null storage res returned as non-null: res
  53    specclauses3.c:28:16: Storage res may become null
  54 specclauses3.c: (in function createName4)
  55 specclauses3.c:55:10: Unallocated storage res->name corresponds to storage
  56                          result->name listed in allocates clause: res
  57
  58 Finished checking --- 5 code warnings, as expected
  59
  60 specclauses4.c: (in function usename)
  61 specclauses4.c:13:4: Dereference of null pointer *name: **name
  62    specclauses4.c:11:8: Storage *name becomes null
  63 specclauses4.c: (in function callname)
  64 specclauses4.c:27:12: Non-null storage *s corresponds to storage listed in
  65                          requires isnull clause of called function: s
  66 specclauses4.c: (in function nullname2)
  67 specclauses4.c:42:2: Non-null storage *name corresponds to storage listed in
  68                         ensures isnull clause
  69
  70 Finished checking --- 3 code warnings, as expected
  71
  72 specclauses5.c: (in function createrecord2)
  73 specclauses5.c:31:10: Null storage r->name derivable from return value: r
  74    specclauses5.c:30:14: Storage r->name becomes null
  75 specclauses5.c: (in function newrecord2)
  76 specclauses5.c:43:10: Non-observer storage r->name corresponds to storage
  77                          result->name listed in ensures observer clause: r
  78 specclauses5.c: (in function createrecordx)
  79 specclauses5.c:49:10: Observer storage r->name reachable from unqualified
  80                          return value
  81    specclauses5.c:48:14: Storage r->name becomes observer
  82
  83 Finished checking --- 3 code warnings, as expected