From 241fad12870c58bd76468267f2816d409dbc7e57 Mon Sep 17 00:00:00 2001
From: jbj <devnull@localhost>
Date: Mon, 8 Jul 2002 14:21:26 +0000
Subject: Propagate splint-3.0.1.7 close(2) internalState annotation
 throughout.

CVS patchset: 5542
CVS date: 2002/07/08 14:21:26
---
 lib/fsm.h | 13 +++++++------
 1 file changed, 7 insertions(+), 6 deletions(-)

(limited to 'lib/fsm.h')

diff --git a/lib/fsm.h b/lib/fsm.h
index d093ca93a..8cd4f0b8c 100644
--- a/lib/fsm.h
+++ b/lib/fsm.h
@@ -244,8 +244,9 @@ int fsmSetup(FSM_t fsm, fileStage goal,
 		FD_t cfd,
 		/*@out@*/ unsigned int * archiveSize,
 		/*@out@*/ const char ** failedFile)
-	/*@globals fileSystem @*/
-	/*@modifies fsm, ts, fi, *archiveSize, *failedFile, fileSystem  @*/;
+	/*@globals fileSystem, internalState @*/
+	/*@modifies fsm, ts, fi, *archiveSize, *failedFile,
+		fileSystem, internalState @*/;
 
 /**
  * Clean file state machine.
@@ -253,8 +254,8 @@ int fsmSetup(FSM_t fsm, fileStage goal,
  * @return		0 on success
  */
 int fsmTeardown(FSM_t fsm)
-	/*@globals fileSystem @*/
-	/*@modifies fsm, fileSystem @*/;
+	/*@globals fileSystem, internalState @*/
+	/*@modifies fsm, fileSystem, internalState @*/;
 
 /*@-exportlocal@*/
 /**
@@ -295,8 +296,8 @@ int fsmMapAttrs(FSM_t fsm)
  * @return		0 on success
  */
 int fsmStage(/*@partial@*/ FSM_t fsm, fileStage stage)
-	/*@globals fileSystem @*/
-	/*@modifies fsm, fileSystem @*/;
+	/*@globals fileSystem, internalState @*/
+	/*@modifies fsm, fileSystem, internalState @*/;
 
 #ifdef __cplusplus
 }
-- 
cgit v1.2.3