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