test/metastate.expect

   1
   2 file1.c: (in function main)
   3 file1.c:10:14: Invalid transfer from implicitly unopen fle to open (unopen file
   4                   passed as open): fle
   5 file1.c:19:16: Invalid transfer from implicitly open fle to unopen (open file
   6                   passed as unopen): fle
   7    file1.c:12:3: Meta state fle becomes implicitly open
   8 file1.c:23:14: Invalid transfer from unopen fle to open (unopen file passed as
   9                   open): fle
  10    file1.c:22:10: Meta state fle becomes unopen
  11 file1.c:7:8: Variable s declared but not used
  12
  13 Finished LCLint checking --- 4 code errors found, as expected
  14
  15 file2.c: (in function main)
  16 file2.c:11:6: Scope exit loses reference fle2 in invalid state implicitly open
  17                  (open file not closed)
  18    file2.c:9:41: State becomes implicitly open
  19 file2.c:13:12: Return loses reference fle1 in invalid state implicitly open
  20                   (open file not closed)
  21    file2.c:5:37: State becomes implicitly open
  22
  23 Finished LCLint checking --- 2 code errors found, as expected
  24
  25 file3.c: (in function main)
  26 file3.c:10:22: Possibly null storage fle1 passed as non-null param:
  27                   fclose (fle1)
  28    file3.c:6:16: Storage fle1 may become null
  29 file3.c:11:5: Control branches merge with incompatible states for fle1 (unopen
  30                  and open): files merge in inconsistent state
  31    file3.c:6:37: Meta state fle1 becomes implicitly open
  32    file3.c:10:14: Meta state fle1 becomes unopen
  33
  34 Finished LCLint checking --- 2 code errors found, as expected
  35
  36 file4.c: (in function main)
  37 file4.c:15:14: Invalid transfer from implicitly unopen fle to open (unopen file
  38                   passed as open): fle
  39
  40 Finished LCLint checking --- 1 code error found, as expected
  41
  42 file5.c: (in function passOpen)
  43 file5.c:8:2: Ensures clause not satisfied by f (state is open):
  44                 ensures closed f
  45    file5.c:4:35: Meta state f becomes open
  46 file5.c: (in function returnOpen)
  47 file5.c:16:10: Result state fle does not satisfy ensures clause:
  48                   ensures open result (state is unopen, should be open): fle
  49    file5.c:13:30: Storage fle becomes dependent
  50 file5.c:16:10: Dependent storage fle returned as implicitly temp: fle
  51    file5.c:13:30: Storage fle becomes dependent
  52 file5.c: (in function main)
  53 file5.c:25:14: Invalid transfer from implicitly unopen fle to open (unopen file
  54                   passed as open): fle
  55 file5.c:35:18: Invalid transfer from unopen fle to open (unopen file passed as
  56                   open): fle
  57    file5.c:34:3: Meta state fle becomes unopen
  58
  59 Finished LCLint checking --- 5 code errors found, as expected
  60
  61 file6.c: (in function newOpenBad)
  62 file6.c:20:10: Invalid transfer from unopen res to open (unopen file passed as
  63                   open): return res
  64    file6.c:19:10: Meta state res becomes unopen
  65 file6.c: (in function main)
  66 file6.c:30:12: Return loses reference fle in invalid state implicitly open
  67                   (open file not closed)
  68    file6.c:27:3: State becomes implicitly open
  69
  70 Finished LCLint checking --- 2 code errors found, as expected
  71
  72 filebad.c:1:23: Meta state anntation open used in inconsistent context:
  73                    int badOpen(FILE *)
  74 filebad.c:3:12: Meta state anntation open used on inappropriate reference p_x
  75                    in ensures open clause of badEnsures: ensures open p_x
  76 filebad.c:3:12: Meta state anntation closed used on inappropriate reference p_x
  77                    in requires closed clause of badEnsures: requires closed p_x
  78
  79 Finished LCLint checking --- 3 code errors found, as expected
  80
  81 sockets.c: (in function test1)
  82 sockets.c:13:3: Requires clause of called function useSockets not satisfied
  83                    (state is uninitialized): requires sockets_initialized
  84 sockets.c: (in function test5)
  85 sockets.c:37:3: Requires clause of called function useSockets not satisfied
  86                    (state is uninitialized): requires sockets_initialized
  87 sockets.c: (in function test6)
  88 sockets.c:42:3: Requires clause of called function useSockets not satisfied
  89                    (state is uninitialized): requires sockets_initialized
  90
  91 Finished LCLint checking --- 3 code errors found, as expected
  92
  93 sockets2.c: (in function test1)
  94 sockets2.c:15:4: Control branches merge with incompatible global states
  95     (initialized and uninitialized): Sockets initialized on true branch,
  96     uninitialized on false branch.
  97    sockets2.c:11:24: Meta state <global marker> becomes uninitialized
  98    sockets2.c:14:5: Meta state <global marker> becomes initialized
  99 sockets2.c: (in function test2)
 100 sockets2.c:24:3: Control branches merge with incompatible global states
 101     (uninitialized and initialized): Sockets uninitialized on false branch,
 102     initialized on true branch.
 103    sockets2.c:20:24: Meta state <global marker> becomes initialized
 104    sockets2.c:23:5: Meta state <global marker> becomes uninitialized
 105
 106 Finished LCLint checking --- 2 code errors found, as expected
 107
 108 struct.c: (in function source_badClose)
 109 struct.c:25:2: Invalid transfer from unopen s->file to open
 110    struct.c:24:10: Meta state s->file becomes unopen
 111
 112 Finished LCLint checking --- 1 code error found, as expected
 113
 114 nullbranch.c: (in function ftest2)
 115 nullbranch.c:30:22: Possibly null storage f passed as non-null param:
 116                        fclose (f)
 117    nullbranch.c:22:7: Storage f may become null
 118 nullbranch.c:32:2: Return loses reference f in invalid state open (open file
 119                       not closed)
 120    nullbranch.c:31:5: State becomes open
 121
 122 Finished LCLint checking --- 2 code errors found, as expected
 123
 124 osd.c: (in function osd_fileIsReadable)
 125 osd.c:9:7: Return value (type int) ignored: fclose(fl)
 126 osd.c:10:14: Return value type bool does not match declared type int: (TRUE)
 127
 128 Finished LCLint checking --- 2 code errors found, as expected