X-Git-Url: http://andersk.mit.edu/gitweb/splint.git/blobdiff_plain/80ee600a548f705b2875267c01bcc63e95203578..16c024b587f5ddc115928d5cca7095508aa208d9:/test/metastate.expect diff --git a/test/metastate.expect b/test/metastate.expect index a7b33c6..e578a34 100644 --- a/test/metastate.expect +++ b/test/metastate.expect @@ -1,16 +1,20 @@ file1.c: (in function main) file1.c:10:14: Invalid transfer from implicitly unopen fle to open (unopen file - passed as open): fle + passed as open): checkOpen(..., fle, ...) + file1.c:6:14: fle becomes implicitly unopen + file1.c:1:53: parameter 1 becomes open file1.c:19:16: Invalid transfer from implicitly open fle to unopen (open file - passed as unopen): fle - file1.c:12:3: Meta state fle becomes implicitly open + passed as unopen): checkClosed(..., fle, ...) + file1.c:12:3: fle becomes implicitly open + file1.c:2:57: parameter 1 becomes unopen file1.c:23:14: Invalid transfer from unopen fle to open (unopen file passed as - open): fle - file1.c:22:10: Meta state fle becomes unopen + open): checkOpen(..., fle, ...) + file1.c:22:10: fle becomes unopen + file1.c:1:53: parameter 1 becomes open file1.c:7:8: Variable s declared but not used -Finished LCLint checking --- 4 code errors found, as expected +Finished checking --- 4 code warnings, as expected file2.c: (in function main) file2.c:11:6: Scope exit loses reference fle2 in invalid state implicitly open @@ -20,63 +24,67 @@ file2.c:13:12: Return loses reference fle1 in invalid state implicitly open (open file not closed) file2.c:5:37: State becomes implicitly open -Finished LCLint checking --- 2 code errors found, as expected +Finished checking --- 2 code warnings, as expected file3.c: (in function main) file3.c:10:22: Possibly null storage fle1 passed as non-null param: fclose (fle1) file3.c:6:16: Storage fle1 may become null file3.c:11:5: Control branches merge with incompatible states for fle1 (unopen - and implicitly open): files merge in inconsistent state - file3.c:6:37: Meta state fle1 becomes implicitly open - file3.c:10:14: Meta state fle1 becomes unopen + and open): files merge in inconsistent state + file3.c:6:37: fle1 becomes implicitly open + file3.c:10:14: fle1 becomes unopen -Finished LCLint checking --- 2 code errors found, as expected +Finished checking --- 2 code warnings, as expected file4.c: (in function main) file4.c:15:14: Invalid transfer from implicitly unopen fle to open (unopen file - passed as open): fle + passed as open): checkOpen(..., fle, ...) + file4.c:11:14: fle becomes implicitly unopen + file4.c:1:53: parameter 1 becomes open -Finished LCLint checking --- 1 code error found, as expected +Finished checking --- 1 code warning, as expected file5.c: (in function passOpen) file5.c:8:2: Ensures clause not satisfied by f (state is open): ensures closed f - file5.c:4:35: Meta state f becomes open + file5.c:4:35: f becomes open file5.c: (in function returnOpen) file5.c:16:10: Result state fle does not satisfy ensures clause: ensures open result (state is unopen, should be open): fle file5.c:13:30: Storage fle becomes dependent -file5.c:16:10: Dependent storage fle returned as implicitly temp: fle - file5.c:13:30: Storage fle becomes dependent file5.c: (in function main) file5.c:25:14: Invalid transfer from implicitly unopen fle to open (unopen file - passed as open): fle + passed as open): checkOpen(..., fle, ...) + file5.c:21:14: fle becomes implicitly unopen + file5.c:1:53: parameter 1 becomes open file5.c:35:18: Invalid transfer from unopen fle to open (unopen file passed as - open): fle - file5.c:34:3: Meta state fle becomes unopen + open): fclose(..., fle, ...) + file5.c:34:3: fle becomes unopen + file.xh:1:44: parameter 1 becomes open -Finished LCLint checking --- 5 code errors found, as expected +Finished checking --- 4 code warnings, as expected file6.c: (in function newOpenBad) file6.c:20:10: Invalid transfer from unopen res to open (unopen file passed as open): return res - file6.c:19:10: Meta state res becomes unopen + file6.c:19:10: res becomes unopen + file6.c:14:2: becomes open file6.c: (in function main) file6.c:30:12: Return loses reference fle in invalid state implicitly open (open file not closed) file6.c:27:3: State becomes implicitly open -Finished LCLint checking --- 2 code errors found, as expected +Finished checking --- 2 code warnings, as expected -filebad.c:1:23: Meta state anntation open used in inconsistent context: +filebad.c:1:23: Attribute annotation open used in inconsistent context: int badOpen(FILE *) -filebad.c:3:12: Meta state anntation open used on inappropriate reference p_x +filebad.c:3:52: Attribute annotation closed used in inconsistent context: + int p_x +filebad.c:3:12: Attribute annotation open used on inappropriate reference p_x in ensures open clause of badEnsures: ensures open p_x -filebad.c:3:12: Meta state anntation closed used on inappropriate reference p_x - in requires closed clause of badEnsures: requires closed p_x -Finished LCLint checking --- 3 code errors found, as expected +Finished checking --- 3 code warnings, as expected sockets.c: (in function test1) sockets.c:13:3: Requires clause of called function useSockets not satisfied @@ -88,28 +96,29 @@ sockets.c: (in function test6) sockets.c:42:3: Requires clause of called function useSockets not satisfied (state is uninitialized): requires sockets_initialized -Finished LCLint checking --- 3 code errors found, as expected +Finished checking --- 3 code warnings, as expected sockets2.c: (in function test1) sockets2.c:15:4: Control branches merge with incompatible global states (initialized and uninitialized): Sockets initialized on true branch, uninitialized on false branch. - sockets2.c:11:24: Meta state becomes uninitialized - sockets2.c:14:5: Meta state becomes initialized + sockets2.c:11:24: becomes uninitialized + sockets2.c:14:5: becomes initialized sockets2.c: (in function test2) sockets2.c:24:3: Control branches merge with incompatible global states (uninitialized and initialized): Sockets uninitialized on false branch, initialized on true branch. - sockets2.c:20:24: Meta state becomes initialized - sockets2.c:23:5: Meta state becomes uninitialized + sockets2.c:20:24: becomes initialized + sockets2.c:23:5: becomes uninitialized -Finished LCLint checking --- 2 code errors found, as expected +Finished checking --- 2 code warnings, as expected struct.c: (in function source_badClose) -struct.c:25:2: Invalid transfer from unopen s->file to open - struct.c:24:10: Meta state s->file becomes unopen +struct.c:10:2: Function returns with parameter s in inconsistent state (s->file + is unopen, should be open): unopen file passed as open + struct.c:9:10: s->file becomes unopen -Finished LCLint checking --- 1 code error found, as expected +Finished checking --- 1 code warning, as expected nullbranch.c: (in function ftest2) nullbranch.c:30:22: Possibly null storage f passed as non-null param: @@ -117,67 +126,12 @@ nullbranch.c:30:22: Possibly null storage f passed as non-null param: nullbranch.c:22:7: Storage f may become null nullbranch.c:32:2: Return loses reference f in invalid state open (open file not closed) - nullbranch.c:31:5: State becomes open - -Finished LCLint checking --- 2 code errors found, as expected - -tainted.c: (in function f) -tainted.c:3:20: Invalid transfer from tainted s to untainted (Possibly tainted - storage used as untainted.): s - tainted.c:1:48: Meta state s becomes tainted -tainted.c: (in function test) -tainted.c:9:18: Invalid transfer from tainted s to untainted (Possibly tainted - storage used as untainted.): s - tainted.c:7:34: Meta state s becomes tainted - -Finished LCLint checking --- 2 code errors found, as expected - -tainted-bad.mts:18:7: Transfer clause uses unrecognized result state peach: - untainted as tainted ==> peach -tainted-bad.mts:14:17: Merge clause uses unrecognized second value junky: - tainted X junky ==> error "Splat!" -tainted-bad.mts:11:7: Annotation declaration uses unrecognized value name blue: - maybetainted reference ==> blue -tainted-bad.mts:5:21: Defaults declaration uses unrecognized value name - stainted: stainted reference -tainted-bad.mts:7:21: Duplicate defaults declaration for context param: - untainted param -tainted.c: (in function f) -tainted.c:3:20: Invalid transfer from tainted s to untainted (Possibly tainted - storage used as untainted.): s - tainted.c:1:48: Meta state s becomes tainted -tainted.c: (in function test) -tainted.c:9:18: Invalid transfer from tainted s to untainted (Possibly tainted - storage used as untainted.): s - tainted.c:7:34: Meta state s becomes tainted - -Finished LCLint checking --- 7 code errors found, as expected - -tainted2.c: (in function test) -tainted2.c:20:10: Invalid transfer from tainted stk to implicitly untainted - (Possibly tainted storage used as untainted.): return stk - tainted2.c:17:14: Meta state stk becomes tainted - -Finished LCLint checking --- 1 code error found, as expected - -tainted3.c: (in function test) -tainted3.c:7:3: Requires clause of called function checkUntainted not satisfied - by def (state is tainted): requires untainted def - -Finished LCLint checking --- 1 code error found, as expected - -tainted4.c: (in function test) -tainted4.c:6:17: Invalid transfer from tainted def to implicitly untainted - tainted4.c:4:36: Meta state def becomes tainted -tainted4.c:7:19: Invalid transfer from tainted def to implicitly untainted - tainted4.c:4:36: Meta state def becomes tainted -tainted4.c:7:3: Requires clause of called function checkUntainted not satisfied - by def (state is tainted): requires untainted *def - -Finished LCLint checking --- 3 code errors found, expected 1 + nullbranch.c:22:3: State becomes open + +Finished checking --- 2 code warnings, as expected osd.c: (in function osd_fileIsReadable) osd.c:9:7: Return value (type int) ignored: fclose(fl) osd.c:10:14: Return value type bool does not match declared type int: (TRUE) -Finished LCLint checking --- 2 code errors found, as expected +Finished checking --- 2 code warnings, as expected