Splint annotations.

CVS patchset: 7182
CVS date: 2004/03/23 05:09:13

54 files changed, 2113 insertions, 618 deletions

diff --git a/lua/.cvsignore b/lua/.cvsignore
new file mode 100644
index 000000000..271f4defd
--- /dev/null
+++ b/lua/.cvsignore
@@ -0,0 +1,7 @@
+.deps
+Makefile
+Makefile.in
+.libs
+*.la
+*.lcd
+*.lo
diff --git a/lua/.splintrc b/lua/.splintrc
new file mode 100644
index 000000000..2983f3816
--- /dev/null
+++ b/lua/.splintrc
@@ -0,0 +1,92 @@
+-I. -I./include -I./local -DHAVE_CONFIG_H -DUSE_DLOPEN -DWITH_POSIX -D_GNU_SOURCE -D_REENTRANT -DUSE_POPEN
+
+#+partial
++forcehints
+
+
+#-warnunixlib
+-warnposix
+
++unixlib
+
+#-unrecogcomments	# XXX ignore doxygen markings
+
++strict			# lclint level
+
+# --- in progress
++enumindex		# 20
+
+-boolops		# 8
+-branchstate		# 54
+-bufferoverflowhigh	# 1
+-castfcnptr		# 1
+-compdef		# 111
+-compdestroy		# 18
+-compmempass		# 137
+-declundef		# 42
+-evalorder		# 60
+-infloops		# 2
+-mayaliasunique		# 4
+-moduncon		# 5 dlopen et al
+-modunconnomods		# 6 ctype.h
+-noeffect		# 169
+-noeffectuncon		# 5
+-nullderef		# 109
+-nullpass		# 28
+-nullptrarith		# 11
+-nullret		# 1
+-nullstate		# 19
+-predboolptr		# 34
+-protoparammatch	# 58
+-realcompare		# 8
+-retalias		# 30
+-retvalint		# 44
+-retvalother		# 42
+-shiftnegative		# 8
+-sizeoftype		# 125
+-stackref		# 5
+-type			# 12
+-uniondef		# 26
+-unrecog
+-usereleased		# 13
+
+-immediatetrans		# 40
+-temptrans		# 27
+-unqualifiedtrans	# 2
+
+-casebreak		# 3
+-looploopbreak		# 1
+-loopswitchbreak	# 89
+-switchswitchbreak	# 9
+
+-exportheader		# 233
+-exportlocal		# 13
+-exporttype
+
+-fielduse		# 24
+-typeuse		# 1 ls_hash
+
+# --- not-yet at strict level
+-bitwisesigned		#
+-elseifcomplete		#
+-forblock		#
+-ifblock		#
+-incondefs		#
+-namechecks		# tedious ANSI compliance checks
+-ptrarith		# tedious
+
+-mustdefine		#
+-shiftimplementation	#
+
+-strictops		#
+-whileblock		#
+
+# --- not-yet at checks level
+-mustfree		#
+-usedef			#
+
+# --- not-yet at standard level
++boolint		#
++charint		#
++ignorequals		#
++matchanyintegral	#
diff --git a/lua/Makefile.am b/lua/Makefile.am
index c33d8d1ed..e2b2f4f80 100644
--- a/lua/Makefile.am
+++ b/lua/Makefile.am
@@ -1,4 +1,6 @@
 
+LINT = splint
+
 noinst_LTLIBRARIES = liblua.la
 noinst_PROGRAMS = lua/lua luac/luac
 
@@ -75,3 +77,73 @@ liblua_la_SOURCES = \
 
 local/linit.lch: local/linit.lua
 	bin2c local/linit.lua > local/linit.lch
+
+# XXX to avoid local/linit.lch syntax problem.
+#
+#		local/linit.c \
+#		lib/lstrlib.c \
+#
+LUA_SPLINT_SOURCES = \
+		lua/lua.c \
+		include/lauxlib.h \
+		include/lua.h \
+		include/lualib.h \
+		lib/lauxlib.c \
+		lib/lbaselib.c \
+		lib/ldblib.c \
+		lib/liolib.c \
+		lib/loadlib.c \
+		lib/lmathlib.c \
+		lib/ltablib.c \
+		local/lposix.h \
+		local/lposix.c \
+		local/lrexlib.h \
+		local/lrexlib.c \
+		lapi.c \
+		lapi.h \
+		lcode.c \
+		lcode.h \
+		ldebug.c \
+		ldebug.h \
+		ldo.c \
+		ldo.h \
+		ldump.c \
+		lfunc.c \
+		lfunc.h \
+		lgc.c \
+		lgc.h \
+		llex.c \
+		llex.h \
+		llimits.h \
+		lmem.c \
+		lmem.h \
+		lobject.c \
+		lobject.h \
+		lopcodes.c \
+		lopcodes.h \
+		lparser.c \
+		lparser.h \
+		lstate.c \
+		lstate.h \
+		lstring.c \
+		lstring.h \
+		ltable.c \
+		ltable.h \
+		ltests.c \
+		ltm.c \
+		ltm.h \
+		lundump.c \
+		lundump.h \
+		lvm.c \
+		lvm.h \
+		lzio.c \
+		lzio.h
+
+.PHONY:	sources
+sources:
+	@echo $(LUA_SPLINT_SOURCES:%=lua/%)
+
+.PHONY:	lint
+lint:
+	$(LINT) $(DEFS) $(INCLUDES) $(LUA_SPLINT_SOURCES)
+
diff --git a/lua/include/lauxlib.h b/lua/include/lauxlib.h
index 1b595503f..a06d816c5 100644
--- a/lua/include/lauxlib.h
+++ b/lua/include/lauxlib.h
@@ -1,5 +1,5 @@
 /*
-** $Id: lauxlib.h,v 1.2 2004/03/23 02:27:55 jbj Exp $
+** $Id: lauxlib.h,v 1.3 2004/03/23 05:09:14 jbj Exp $
 ** Auxiliary functions for building Lua libraries
 ** See Copyright Notice in lua.h
 */
@@ -31,62 +31,65 @@ typedef struct luaL_reg {
 
 LUALIB_API void luaL_openlib (lua_State *L, const char *libname,
                                const luaL_reg *l, int nup)
-	/*@*/;
+	/*@modifies L @*/;
 LUALIB_API int luaL_getmetafield (lua_State *L, int obj, const char *e)
-	/*@*/;
+	/*@modifies L @*/;
 LUALIB_API int luaL_callmeta (lua_State *L, int obj, const char *e)
-	/*@*/;
+	/*@modifies L @*/;
 LUALIB_API int luaL_typerror (lua_State *L, int narg, const char *tname)
-	/*@*/;
+	/*@modifies L @*/;
 LUALIB_API int luaL_argerror (lua_State *L, int numarg, const char *extramsg)
-	/*@*/;
+	/*@modifies L @*/;
+/*@observer@*/
 LUALIB_API const char *luaL_checklstring (lua_State *L, int numArg, size_t *l)
-	/*@*/;
+	/*@modifies L, *l @*/;
+/*@observer@*/
 LUALIB_API const char *luaL_optlstring (lua_State *L, int numArg,
                                            const char *def, size_t *l)
-	/*@*/;
+	/*@modifies L, *l @*/;
 LUALIB_API lua_Number luaL_checknumber (lua_State *L, int numArg)
-	/*@*/;
+	/*@modifies L @*/;
 LUALIB_API lua_Number luaL_optnumber (lua_State *L, int nArg, lua_Number def)
-	/*@*/;
+	/*@modifies L @*/;
 
 LUALIB_API void luaL_checkstack (lua_State *L, int sz, const char *msg)
-	/*@*/;
+	/*@modifies L @*/;
 LUALIB_API void luaL_checktype (lua_State *L, int narg, int t)
-	/*@*/;
+	/*@modifies L @*/;
 LUALIB_API void luaL_checkany (lua_State *L, int narg)
-	/*@*/;
+	/*@modifies L @*/;
 
 LUALIB_API int   luaL_newmetatable (lua_State *L, const char *tname)
-	/*@*/;
+	/*@modifies L @*/;
 LUALIB_API void  luaL_getmetatable (lua_State *L, const char *tname)
-	/*@*/;
+	/*@modifies L @*/;
 LUALIB_API void *luaL_checkudata (lua_State *L, int ud, const char *tname)
-	/*@*/;
+	/*@modifies L @*/;
 
 LUALIB_API void luaL_where (lua_State *L, int lvl)
-	/*@*/;
+	/*@modifies L @*/;
 LUALIB_API int luaL_error (lua_State *L, const char *fmt, ...)
-	/*@*/;
+	/*@modifies L @*/;
 
 LUALIB_API int luaL_findstring (const char *st, const char *const lst[])
 	/*@*/;
 
 LUALIB_API int luaL_ref (lua_State *L, int t)
-	/*@*/;
+	/*@modifies L @*/;
 LUALIB_API void luaL_unref (lua_State *L, int t, int ref)
-	/*@*/;
+	/*@modifies L @*/;
 
 LUALIB_API int luaL_getn (lua_State *L, int t)
-	/*@*/;
+	/*@modifies L @*/;
 LUALIB_API void luaL_setn (lua_State *L, int t, int n)
-	/*@*/;
+	/*@modifies L @*/;
 
 LUALIB_API int luaL_loadfile (lua_State *L, const char *filename)
-	/*@*/;
+	/*@globals fileSystem @*/
+	/*@modifies L, fileSystem @*/;
 LUALIB_API int luaL_loadbuffer (lua_State *L, const char *buff, size_t sz,
                                 const char *name)
-	/*@*/;
+	/*@modifies L @*/;
 
 
 
@@ -119,6 +122,7 @@ LUALIB_API int luaL_loadbuffer (lua_State *L, const char *buff, size_t sz,
 
 
 typedef struct luaL_Buffer {
+/*@dependent@*/
   char *p;			/* current position in buffer */
   int lvl;  /* number of strings in the stack (level) */
   lua_State *L;
@@ -132,17 +136,18 @@ typedef struct luaL_Buffer {
 #define luaL_addsize(B,n)	((B)->p += (n))
 
 LUALIB_API void luaL_buffinit (lua_State *L, luaL_Buffer *B)
-	/*@*/;
+	/*@modifies L, B @*/;
+/*@dependent@*/
 LUALIB_API char *luaL_prepbuffer (luaL_Buffer *B)
-	/*@*/;
+	/*@modifies B @*/;
 LUALIB_API void luaL_addlstring (luaL_Buffer *B, const char *s, size_t l)
-	/*@*/;
+	/*@modifies B @*/;
 LUALIB_API void luaL_addstring (luaL_Buffer *B, const char *s)
-	/*@*/;
+	/*@modifies B @*/;
 LUALIB_API void luaL_addvalue (luaL_Buffer *B)
-	/*@*/;
+	/*@modifies B @*/;
 LUALIB_API void luaL_pushresult (luaL_Buffer *B)
-	/*@*/;
+	/*@modifies B @*/;
 
 
 /* }====================================================== */
@@ -154,12 +159,15 @@ LUALIB_API void luaL_pushresult (luaL_Buffer *B)
 */
 
 LUALIB_API int   lua_dofile (lua_State *L, const char *filename)
-	/*@*/;
+	/*@globals fileSystem @*/
+	/*@modifies L, fileSystem @*/;
 LUALIB_API int   lua_dostring (lua_State *L, const char *str)
-	/*@*/;
+	/*@globals fileSystem @*/
+	/*@modifies L, fileSystem @*/;
 LUALIB_API int   lua_dobuffer (lua_State *L, const char *buff, size_t sz,
                                const char *n)
-	/*@*/;
+	/*@globals fileSystem @*/
+	/*@modifies L, fileSystem @*/;
 
 
 #define luaL_check_lstr 	luaL_checklstring
diff --git a/lua/include/lualib.h b/lua/include/lualib.h
index 29f037e82..bdbb51447 100644
--- a/lua/include/lualib.h
+++ b/lua/include/lualib.h
@@ -1,5 +1,5 @@
 /*
-** $Id: lualib.h,v 1.2 2004/03/23 02:27:55 jbj Exp $
+** $Id: lualib.h,v 1.3 2004/03/23 05:09:14 jbj Exp $
 ** Lua standard libraries
 ** See Copyright Notice in lua.h
 */
@@ -18,32 +18,32 @@
 
 #define LUA_COLIBNAME	"coroutine"
 LUALIB_API int luaopen_base (lua_State *L)
-	/*@*/;
+	/*@modifies L @*/;
 
 #define LUA_TABLIBNAME	"table"
 LUALIB_API int luaopen_table (lua_State *L)
-	/*@*/;
+	/*@modifies L @*/;
 
 #define LUA_IOLIBNAME	"io"
 #define LUA_OSLIBNAME	"os"
 LUALIB_API int luaopen_io (lua_State *L)
-	/*@*/;
+	/*@modifies L @*/;
 
 #define LUA_STRLIBNAME	"string"
 LUALIB_API int luaopen_string (lua_State *L)
-	/*@*/;
+	/*@modifies L @*/;
 
 #define LUA_MATHLIBNAME	"math"
 LUALIB_API int luaopen_math (lua_State *L)
-	/*@*/;
+	/*@modifies L @*/;
 
 #define LUA_DBLIBNAME	"debug"
 LUALIB_API int luaopen_debug (lua_State *L)
-	/*@*/;
+	/*@modifies L @*/;
 
 
 LUALIB_API int luaopen_loadlib (lua_State *L)
-	/*@*/;
+	/*@modifies L @*/;
 
 
 /* to help testing the libraries */
diff --git a/lua/lapi.c b/lua/lapi.c
index 32dcdd911..06419b7b6 100644
--- a/lua/lapi.c
+++ b/lua/lapi.c
@@ -1,5 +1,5 @@
 /*
-** $Id: lapi.c,v 1.1 2004/03/16 21:58:30 niemeyer Exp $
+** $Id: lapi.c,v 1.2 2004/03/23 05:09:14 jbj Exp $
 ** Lua API
 ** See Copyright Notice in lua.h
 */
@@ -27,6 +27,7 @@
 #include "lvm.h"
 
 
+/*@unused@*/
 const char lua_ident[] =
   "$Lua: " LUA_VERSION " " LUA_COPYRIGHT " $\n"
   "$Authors: " LUA_AUTHORS " $\n"
@@ -45,7 +46,10 @@ const char lua_ident[] =
 
 
 
-static TObject *negindex (lua_State *L, int idx) {
+/*@dependent@*/ /*@null@*/
+static TObject *negindex (lua_State *L, int idx)
+	/*@*/
+{
   if (idx > LUA_REGISTRYINDEX) {
     api_check(L, idx != 0 && -idx <= L->top - L->base);
     return L->top+idx;
@@ -65,7 +69,10 @@ static TObject *negindex (lua_State *L, int idx) {
 }
 
 
-static TObject *luaA_index (lua_State *L, int idx) {
+/*@dependent@*/ /*@relnull@*/
+static TObject *luaA_index (lua_State *L, int idx)
+	/*@*/
+{
   if (idx > 0) {
     api_check(L, idx <= L->top - L->base);
     return L->base + idx - 1;
@@ -78,7 +85,10 @@ static TObject *luaA_index (lua_State *L, int idx) {
 }
 
 
-static TObject *luaA_indexAcceptable (lua_State *L, int idx) {
+/*@dependent@*/ /*@null@*/
+static TObject *luaA_indexAcceptable (lua_State *L, int idx)
+	/*@*/
+{
   if (idx > 0) {
     TObject *o = L->base+(idx-1);
     api_check(L, idx <= L->stack_last - L->base);
@@ -144,7 +154,9 @@ LUA_API lua_State *lua_newthread (lua_State *L) {
   api_incr_top(L);
   lua_unlock(L);
   lua_userstateopen(L1);
+/*@-kepttrans@*/
   return L1;
+/*@=kepttrans@*/
 }
 
 
@@ -662,12 +674,15 @@ LUA_API void lua_call (lua_State *L, int nargs, int nresults) {
 ** Execute a protected call.
 */
 struct CallS {  /* data to `f_call' */
+/*@dependent@*/
   StkId func;
   int nresults;
 };
 
 
-static void f_call (lua_State *L, void *ud) {
+static void f_call (lua_State *L, void *ud)
+	/*@modifies L @*/
+{
   struct CallS *c = cast(struct CallS *, ud);
   luaD_call(L, c->func, c->nresults);
 }
@@ -697,7 +712,9 @@ struct CCallS {  /* data to `f_Ccall' */
 };
 
 
-static void f_Ccall (lua_State *L, void *ud) {
+static void f_Ccall (lua_State *L, void *ud)
+	/*@modifies L @*/
+{
   struct CCallS *c = cast(struct CCallS *, ud);
   Closure *cl;
   cl = luaF_newCclosure(L, 0);
@@ -851,7 +868,9 @@ LUA_API void *lua_newuserdata (lua_State *L, size_t size) {
   setuvalue(L->top, u);
   api_incr_top(L);
   lua_unlock(L);
+/*@-kepttrans@*/
   return u + 1;
+/*@=kepttrans@*/
 }
 
 
@@ -872,8 +891,11 @@ LUA_API int lua_pushupvalues (lua_State *L) {
 }
 
 
+/*@observer@*/ /*@null@*/
 static const char *aux_upvalue (lua_State *L, int funcindex, int n,
-                                TObject **val) {
+                                TObject **val)
+	/*@modifies *val @*/
+{
   Closure *f;
   StkId fi = luaA_index(L, funcindex);
   if (!ttisfunction(fi)) return NULL;
@@ -886,7 +908,9 @@ static const char *aux_upvalue (lua_State *L, int funcindex, int n,
   else {
     Proto *p = f->l.p;
     if (n > p->sizeupvalues) return NULL;
+/*@-onlytrans@*/
     *val = f->l.upvals[n-1]->v;
+/*@=onlytrans@*/
     return getstr(p->upvalues[n-1]);
   }
 }
diff --git a/lua/lapi.h b/lua/lapi.h
index 835c03534..a271f0b2f 100644
--- a/lua/lapi.h
+++ b/lua/lapi.h
@@ -1,5 +1,5 @@
 /*
-** $Id: lapi.h,v 1.1 2004/03/16 21:58:30 niemeyer Exp $
+** $Id: lapi.h,v 1.2 2004/03/23 05:09:14 jbj Exp $
 ** Auxiliary functions from Lua API
 ** See Copyright Notice in lua.h
 */
@@ -11,6 +11,7 @@
 #include "lobject.h"
 
 
-void luaA_pushobject (lua_State *L, const TObject *o);
+void luaA_pushobject (lua_State *L, const TObject *o)
+	/*@modifies L @*/;
 
 #endif
diff --git a/lua/lcode.c b/lua/lcode.c
index 033e8ecf3..7047adf36 100644
--- a/lua/lcode.c
+++ b/lua/lcode.c
@@ -1,5 +1,5 @@
 /*
-** $Id: lcode.c,v 1.1 2004/03/16 21:58:30 niemeyer Exp $
+** $Id: lcode.c,v 1.2 2004/03/23 05:09:14 jbj Exp $
 ** Code generator for Lua
 ** See Copyright Notice in lua.h
 */
@@ -51,13 +51,17 @@ int luaK_jump (FuncState *fs) {
 }
 
 
-static int luaK_condjump (FuncState *fs, OpCode op, int A, int B, int C) {
+static int luaK_condjump (FuncState *fs, OpCode op, int A, int B, int C)
+	/*@modifies fs @*/
+{
   luaK_codeABC(fs, op, A, B, C);
   return luaK_jump(fs);
 }
 
 
-static void luaK_fixjump (FuncState *fs, int pc, int dest) {
+static void luaK_fixjump (FuncState *fs, int pc, int dest)
+	/*@modifies fs @*/
+{
   Instruction *jmp = &fs->f->code[pc];
   int offset = dest-(pc+1);
   lua_assert(dest != NO_JUMP);
@@ -77,7 +81,9 @@ int luaK_getlabel (FuncState *fs) {
 }
 
 
-static int luaK_getjump (FuncState *fs, int pc) {
+static int luaK_getjump (FuncState *fs, int pc)
+	/*@*/
+{
   int offset = GETARG_sBx(fs->f->code[pc]);
   if (offset == NO_JUMP)  /* point to itself represents end of list */
     return NO_JUMP;  /* end of list */
@@ -86,7 +92,9 @@ static int luaK_getjump (FuncState *fs, int pc) {
 }
 
 
-static Instruction *getjumpcontrol (FuncState *fs, int pc) {
+static Instruction *getjumpcontrol (FuncState *fs, int pc)
+	/*@*/
+{
   Instruction *pi = &fs->f->code[pc];
   if (pc >= 1 && testOpMode(GET_OPCODE(*(pi-1)), OpModeT))
     return pi-1;
@@ -99,7 +107,9 @@ static Instruction *getjumpcontrol (FuncState *fs, int pc) {
 ** check whether list has any jump that do not produce a value
 ** (or produce an inverted value)
 */
-static int need_value (FuncState *fs, int list, int cond) {
+static int need_value (FuncState *fs, int list, int cond)
+	/*@*/
+{
   for (; list != NO_JUMP; list = luaK_getjump(fs, list)) {
     Instruction i = *getjumpcontrol(fs, list);
     if (GET_OPCODE(i) != OP_TEST || GETARG_C(i) != cond) return 1;
@@ -108,14 +118,18 @@ static int need_value (FuncState *fs, int list, int cond) {
 }
 
 
-static void patchtestreg (Instruction *i, int reg) {
+static void patchtestreg (Instruction *i, int reg)
+	/*@modifies *i @*/
+{
   if (reg == NO_REG) reg = GETARG_B(*i);
   SETARG_A(*i, reg);
 }
 
 
 static void luaK_patchlistaux (FuncState *fs, int list,
-          int ttarget, int treg, int ftarget, int freg, int dtarget) {
+          int ttarget, int treg, int ftarget, int freg, int dtarget)
+	/*@modifies fs @*/
+{
   while (list != NO_JUMP) {
     int next = luaK_getjump(fs, list);
     Instruction *i = getjumpcontrol(fs, list);
@@ -140,7 +154,9 @@ static void luaK_patchlistaux (FuncState *fs, int list,
 }
 
 
-static void luaK_dischargejpc (FuncState *fs) {
+static void luaK_dischargejpc (FuncState *fs)
+	/*@modifies fs @*/
+{
   luaK_patchlistaux(fs, fs->jpc, fs->pc, NO_REG, fs->pc, NO_REG, fs->pc);
   fs->jpc = NO_JUMP;
 }
@@ -192,7 +208,9 @@ void luaK_reserveregs (FuncState *fs, int n) {
 }
 
 
-static void freereg (FuncState *fs, int reg) {
+static void freereg (FuncState *fs, int reg)
+	/*@modifies fs @*/
+{
   if (reg >= fs->nactvar && reg < MAXSTACK) {
     fs->freereg--;
     lua_assert(reg == fs->freereg);
@@ -200,13 +218,17 @@ static void freereg (FuncState *fs, int reg) {
 }
 
 
-static void freeexp (FuncState *fs, expdesc *e) {
+static void freeexp (FuncState *fs, expdesc *e)
+	/*@modifies fs @*/
+{
   if (e->k == VNONRELOC)
     freereg(fs, e->info);
 }
 
 
-static int addk (FuncState *fs, TObject *k, TObject *v) {
+static int addk (FuncState *fs, TObject *k, TObject *v)
+	/*@modifies fs @*/
+{
   const TObject *idx = luaH_get(fs->h, k);
   if (ttisnumber(idx)) {
     lua_assert(luaO_rawequalObj(&fs->f->k[cast(int, nvalue(idx))], v));
@@ -237,7 +259,9 @@ int luaK_numberK (FuncState *fs, lua_Number r) {
 }
 
 
-static int nil_constant (FuncState *fs) {
+static int nil_constant (FuncState *fs)
+	/*@modifies fs @*/
+{
   TObject k, v;
   setnilvalue(&v);
   sethvalue(&k, fs->h);  /* cannot use nil as key; instead use table itself */
@@ -288,13 +312,17 @@ void luaK_dischargevars (FuncState *fs, expdesc *e) {
 }
 
 
-static int code_label (FuncState *fs, int A, int b, int jump) {
+static int code_label (FuncState *fs, int A, int b, int jump)
+	/*@modifies fs @*/
+{
   luaK_getlabel(fs);  /* those instructions may be jump targets */
   return luaK_codeABC(fs, OP_LOADBOOL, A, b, jump);
 }
 
 
-static void discharge2reg (FuncState *fs, expdesc *e, int reg) {
+static void discharge2reg (FuncState *fs, expdesc *e, int reg)
+	/*@modifies fs, e @*/
+{
   luaK_dischargevars(fs, e);
   switch (e->k) {
     case VNIL: {
@@ -329,7 +357,9 @@ static void discharge2reg (FuncState *fs, expdesc *e, int reg) {
 }
 
 
-static void discharge2anyreg (FuncState *fs, expdesc *e) {
+static void discharge2anyreg (FuncState *fs, expdesc *e)
+	/*@modifies fs, e @*/
+{
   if (e->k != VNONRELOC) {
     luaK_reserveregs(fs, 1);
     discharge2reg(fs, e, fs->freereg-1);
@@ -337,7 +367,9 @@ static void discharge2anyreg (FuncState *fs, expdesc *e) {
 }
 
 
-static void luaK_exp2reg (FuncState *fs, expdesc *e, int reg) {
+static void luaK_exp2reg (FuncState *fs, expdesc *e, int reg)
+	/*@modifies fs, e @*/
+{
   discharge2reg(fs, e, reg);
   if (e->k == VJMP)
     luaK_concat(fs, &e->t, e->info);  /* put this jump in `t' list */
@@ -460,7 +492,9 @@ void luaK_self (FuncState *fs, expdesc *e, expdesc *key) {
 }
 
 
-static void invertjump (FuncState *fs, expdesc *e) {
+static void invertjump (FuncState *fs, expdesc *e)
+	/*@*/
+{
   Instruction *pc = getjumpcontrol(fs, e->info);
   lua_assert(testOpMode(GET_OPCODE(*pc), OpModeT) &&
              GET_OPCODE(*pc) != OP_TEST);
@@ -468,7 +502,9 @@ static void invertjump (FuncState *fs, expdesc *e) {
 }
 
 
-static int jumponcond (FuncState *fs, expdesc *e, int cond) {
+static int jumponcond (FuncState *fs, expdesc *e, int cond)
+	/*@modifies fs, e @*/
+{
   if (e->k == VRELOCABLE) {
     Instruction ie = getcode(fs, e);
     if (GET_OPCODE(ie) == OP_NOT) {
@@ -534,7 +570,9 @@ void luaK_goiffalse (FuncState *fs, expdesc *e) {
 }
 
 
-static void codenot (FuncState *fs, expdesc *e) {
+static void codenot (FuncState *fs, expdesc *e)
+	/*@modifies fs, e @*/
+{
   luaK_dischargevars(fs, e);
   switch (e->k) {
     case VNIL: case VFALSE: {
@@ -617,7 +655,9 @@ void luaK_infix (FuncState *fs, BinOpr op, expdesc *v) {
 
 
 static void codebinop (FuncState *fs, expdesc *res, BinOpr op,
-                       int o1, int o2) {
+                       int o1, int o2)
+	/*@modifies fs, res @*/
+{
   if (op <= OPR_POW) {  /* arithmetic operator? */
     OpCode opc = cast(OpCode, (op - OPR_ADD) + OP_ADD);  /* ORDER OP */
     res->info = luaK_codeABC(fs, opc, 0, o1, o2);
diff --git a/lua/lcode.h b/lua/lcode.h
index ad7ad8ce5..5209be78c 100644
--- a/lua/lcode.h
+++ b/lua/lcode.h
@@ -1,5 +1,5 @@
 /*
-** $Id: lcode.h,v 1.1 2004/03/16 21:58:30 niemeyer Exp $
+** $Id: lcode.h,v 1.2 2004/03/23 05:09:14 jbj Exp $
 ** Code generator for Lua
 ** See Copyright Notice in lua.h
 */
@@ -41,34 +41,62 @@ typedef enum UnOpr { OPR_MINUS, OPR_NOT, OPR_NOUNOPR } UnOpr;
 
 #define luaK_codeAsBx(fs,o,A,sBx)	luaK_codeABx(fs,o,A,(sBx)+MAXARG_sBx)
 
-int luaK_code (FuncState *fs, Instruction i, int line);
-int luaK_codeABx (FuncState *fs, OpCode o, int A, unsigned int Bx);
-int luaK_codeABC (FuncState *fs, OpCode o, int A, int B, int C);
-void luaK_fixline (FuncState *fs, int line);
-void luaK_nil (FuncState *fs, int from, int n);
-void luaK_reserveregs (FuncState *fs, int n);
-void luaK_checkstack (FuncState *fs, int n);
-int luaK_stringK (FuncState *fs, TString *s);
-int luaK_numberK (FuncState *fs, lua_Number r);
-void luaK_dischargevars (FuncState *fs, expdesc *e);
-int luaK_exp2anyreg (FuncState *fs, expdesc *e);
-void luaK_exp2nextreg (FuncState *fs, expdesc *e);
-void luaK_exp2val (FuncState *fs, expdesc *e);
-int luaK_exp2RK (FuncState *fs, expdesc *e);
-void luaK_self (FuncState *fs, expdesc *e, expdesc *key);
-void luaK_indexed (FuncState *fs, expdesc *t, expdesc *k);
-void luaK_goiftrue (FuncState *fs, expdesc *e);
-void luaK_goiffalse (FuncState *fs, expdesc *e);
-void luaK_storevar (FuncState *fs, expdesc *var, expdesc *e);
-void luaK_setcallreturns (FuncState *fs, expdesc *var, int nresults);
-int luaK_jump (FuncState *fs);
-void luaK_patchlist (FuncState *fs, int list, int target);
-void luaK_patchtohere (FuncState *fs, int list);
-void luaK_concat (FuncState *fs, int *l1, int l2);
-int luaK_getlabel (FuncState *fs);
-void luaK_prefix (FuncState *fs, UnOpr op, expdesc *v);
-void luaK_infix (FuncState *fs, BinOpr op, expdesc *v);
-void luaK_posfix (FuncState *fs, BinOpr op, expdesc *v1, expdesc *v2);
+int luaK_code (FuncState *fs, Instruction i, int line)
+	/*@modifies fs @*/;
+int luaK_codeABx (FuncState *fs, OpCode o, int A, unsigned int Bx)
+	/*@modifies fs @*/;
+int luaK_codeABC (FuncState *fs, OpCode o, int A, int B, int C)
+	/*@modifies fs @*/;
+void luaK_fixline (FuncState *fs, int line)
+	/*@modifies fs @*/;
+void luaK_nil (FuncState *fs, int from, int n)
+	/*@modifies fs @*/;
+void luaK_reserveregs (FuncState *fs, int n)
+	/*@modifies fs @*/;
+void luaK_checkstack (FuncState *fs, int n)
+	/*@modifies fs @*/;
+int luaK_stringK (FuncState *fs, TString *s)
+	/*@modifies fs @*/;
+int luaK_numberK (FuncState *fs, lua_Number r)
+	/*@modifies fs @*/;
+void luaK_dischargevars (FuncState *fs, expdesc *e)
+	/*@modifies fs, e @*/;
+int luaK_exp2anyreg (FuncState *fs, expdesc *e)
+	/*@modifies fs, e @*/;
+void luaK_exp2nextreg (FuncState *fs, expdesc *e)
+	/*@modifies fs, e @*/;
+void luaK_exp2val (FuncState *fs, expdesc *e)
+	/*@modifies fs, e @*/;
+int luaK_exp2RK (FuncState *fs, expdesc *e)
+	/*@modifies fs, e @*/;
+void luaK_self (FuncState *fs, expdesc *e, expdesc *key)
+	/*@modifies fs, e, key @*/;
+void luaK_indexed (FuncState *fs, expdesc *t, expdesc *k)
+	/*@modifies fs, t, k @*/;
+void luaK_goiftrue (FuncState *fs, expdesc *e)
+	/*@modifies fs, e @*/;
+void luaK_goiffalse (FuncState *fs, expdesc *e)
+	/*@modifies fs, e @*/;
+void luaK_storevar (FuncState *fs, expdesc *var, expdesc *e)
+	/*@modifies fs, e @*/;
+void luaK_setcallreturns (FuncState *fs, expdesc *var, int nresults)
+	/*@modifies fs, var @*/;
+int luaK_jump (FuncState *fs)
+	/*@modifies fs @*/;
+void luaK_patchlist (FuncState *fs, int list, int target)
+	/*@modifies fs @*/;
+void luaK_patchtohere (FuncState *fs, int list)
+	/*@modifies fs @*/;
+void luaK_concat (FuncState *fs, int *l1, int l2)
+	/*@modifies fs, *l1 @*/;
+int luaK_getlabel (FuncState *fs)
+	/*@modifies fs @*/;
+void luaK_prefix (FuncState *fs, UnOpr op, expdesc *v)
+	/*@modifies fs, v @*/;
+void luaK_infix (FuncState *fs, BinOpr op, expdesc *v)
+	/*@modifies fs, v @*/;
+void luaK_posfix (FuncState *fs, BinOpr op, expdesc *v1, expdesc *v2)
+	/*@modifies fs, v1, v2 @*/;
 
 
 #endif
diff --git a/lua/ldebug.c b/lua/ldebug.c
index aaff167cc..5701bdf53 100644
--- a/lua/ldebug.c
+++ b/lua/ldebug.c
@@ -1,5 +1,5 @@
 /*
-** $Id: ldebug.c,v 1.1 2004/03/16 21:58:30 niemeyer Exp $
+** $Id: ldebug.c,v 1.2 2004/03/23 05:09:14 jbj Exp $
 ** Debug Interface
 ** See Copyright Notice in lua.h
 */
@@ -27,13 +27,17 @@
 
 
 
-static const char *getfuncname (CallInfo *ci, const char **name);
+/*@null@*/
+static const char *getfuncname (CallInfo *ci, const char **name)
+	/*@modifies ci, *name @*/;
 
 
 #define isLua(ci)	(!((ci)->state & CI_C))
 
 
-static int currentpc (CallInfo *ci) {
+static int currentpc (CallInfo *ci)
+	/*@modifies ci @*/
+{
   if (!isLua(ci)) return -1;  /* function is not a Lua function? */
   if (ci->state & CI_HASFRAME)  /* function has a frame? */
     ci->u.l.savedpc = *ci->u.l.pc;  /* use `pc' from there */
@@ -42,7 +46,9 @@ static int currentpc (CallInfo *ci) {
 }
 
 
-static int currentline (CallInfo *ci) {
+static int currentline (CallInfo *ci)
+	/*@modifies ci @*/
+{
   int pc = currentpc(ci);
   if (pc < 0)
     return -1;  /* only active lua functions have current-line information */
@@ -114,7 +120,10 @@ LUA_API int lua_getstack (lua_State *L, int level, lua_Debug *ar) {
 }
 
 
-static Proto *getluaproto (CallInfo *ci) {
+/*@null@*/
+static Proto *getluaproto (CallInfo *ci)
+	/*@*/
+{
   return (isLua(ci) ? ci_func(ci)->l.p : NULL);
 }
 
@@ -158,7 +167,9 @@ LUA_API const char *lua_setlocal (lua_State *L, const lua_Debug *ar, int n) {
 }
 
 
-static void funcinfo (lua_Debug *ar, StkId func) {
+static void funcinfo (lua_Debug *ar, StkId func)
+	/*@modifies ar @*/
+{
   Closure *cl = clvalue(func);
   if (cl->c.isC) {
     ar->source = "=[C]";
@@ -174,7 +185,10 @@ static void funcinfo (lua_Debug *ar, StkId func) {
 }
 
 
-static const char *travglobals (lua_State *L, const TObject *o) {
+/*@null@*/
+static const char *travglobals (lua_State *L, const TObject *o)
+	/*@*/
+{
   Table *g = hvalue(gt(L));
   int i = sizenode(g);
   while (i--) {
@@ -186,7 +200,9 @@ static const char *travglobals (lua_State *L, const TObject *o) {
 }
 
 
-static void info_tailcall (lua_State *L, lua_Debug *ar) {
+static void info_tailcall (lua_State *L, lua_Debug *ar)
+	/*@modifies L, ar @*/
+{
   ar->name = ar->namewhat = "";
   ar->what = "tail";
   ar->linedefined = ar->currentline = -1;
@@ -198,7 +214,9 @@ static void info_tailcall (lua_State *L, lua_Debug *ar) {
 
 
 static int auxgetinfo (lua_State *L, const char *what, lua_Debug *ar,
-                    StkId f, CallInfo *ci) {
+                    StkId f, /*@null@*/ CallInfo *ci)
+	/*@modifies L, ar, ci @*/
+{
   int status = 1;
   for (; *what; what++) {
     switch (*what) {
@@ -215,7 +233,9 @@ static int auxgetinfo (lua_State *L, const char *what, lua_Debug *ar,
         break;
       }
       case 'n': {
+/*@-modobserver@*/
         ar->namewhat = (ci) ? getfuncname(ci, &ar->name) : NULL;
+/*@=modobserver@*/
         if (ar->namewhat == NULL) {
           /* try to find a global name */
           if ((ar->name = travglobals(L, f)) != NULL)
@@ -272,7 +292,9 @@ LUA_API int lua_getinfo (lua_State *L, const char *what, lua_Debug *ar) {
 
 
 
-static int precheck (const Proto *pt) {
+static int precheck (const Proto *pt)
+	/*@*/
+{
   check(pt->maxstacksize <= MAXSTACK);
   check(pt->sizelineinfo == pt->sizecode || pt->sizelineinfo == 0);
   lua_assert(pt->numparams+pt->is_vararg <= pt->maxstacksize);
@@ -281,7 +303,9 @@ static int precheck (const Proto *pt) {
 }
 
 
-static int checkopenop (const Proto *pt, int pc) {
+static int checkopenop (const Proto *pt, int pc)
+	/*@*/
+{
   Instruction i = pt->code[pc+1];
   switch (GET_OPCODE(i)) {
     case OP_CALL:
@@ -296,12 +320,16 @@ static int checkopenop (const Proto *pt, int pc) {
 }
 
 
-static int checkRK (const Proto *pt, int r) {
+static int checkRK (const Proto *pt, int r)
+	/*@*/
+{
   return (r < pt->maxstacksize || (r >= MAXSTACK && r-MAXSTACK < pt->sizek));
 }
 
 
-static Instruction luaG_symbexec (const Proto *pt, int lastpc, int reg) {
+static Instruction luaG_symbexec (const Proto *pt, int lastpc, int reg)
+	/*@*/
+{
   int pc;
   int last;  /* stores position of last instruction that changed `reg' */
   last = pt->sizecode-1;  /* points to final return (a `neutral' instruction) */
@@ -440,7 +468,10 @@ int luaG_checkcode (const Proto *pt) {
 }
 
 
-static const char *kname (Proto *p, int c) {
+/*@observer@*/
+static const char *kname (Proto *p, int c)
+	/*@*/
+{
   c = c - MAXSTACK;
   if (c >= 0 && ttisstring(&p->k[c]))
     return svalue(&p->k[c]);
@@ -449,12 +480,17 @@ static const char *kname (Proto *p, int c) {
 }
 
 
-static const char *getobjname (CallInfo *ci, int stackpos, const char **name) {
+/*@observer@*/ /*@null@*/
+static const char *getobjname (CallInfo *ci, int stackpos, const char **name)
+	/*@modifies ci, *name @*/
+{
   if (isLua(ci)) {  /* a Lua function? */
     Proto *p = ci_func(ci)->l.p;
     int pc = currentpc(ci);
     Instruction i;
+/*@-observertrans -dependenttrans @*/
     *name = luaF_getlocalname(p, stackpos+1, pc);
+/*@=observertrans =dependenttrans @*/
     if (*name)  /* is a local? */
       return "local";
     i = luaG_symbexec(p, pc, stackpos);  /* try symbolic execution */
@@ -475,12 +511,16 @@ static const char *getobjname (CallInfo *ci, int stackpos, const char **name) {
       }
       case OP_GETTABLE: {
         int k = GETARG_C(i);  /* key index */
+/*@-observertrans -dependenttrans @*/
         *name = kname(p, k);
+/*@=observertrans =dependenttrans @*/
         return "field";
       }
       case OP_SELF: {
         int k = GETARG_C(i);  /* key index */
+/*@-observertrans -dependenttrans @*/
         *name = kname(p, k);
+/*@=observertrans =dependenttrans @*/
         return "method";
       }
       default: break;
@@ -490,7 +530,10 @@ static const char *getobjname (CallInfo *ci, int stackpos, const char **name) {
 }
 
 
-static const char *getfuncname (CallInfo *ci, const char **name) {
+/*@observer@*/ /*@null@*/
+static const char *getfuncname (CallInfo *ci, const char **name)
+	/*@modifies ci, *name @*/
+{
   Instruction i;
   if ((isLua(ci) && ci->u.l.tailcalls > 0) || !isLua(ci - 1))
     return NULL;  /* calling function is not Lua (or is unknown) */
@@ -504,7 +547,9 @@ static const char *getfuncname (CallInfo *ci, const char **name) {
 
 
 /* only ANSI way to check whether a pointer points to an array */
-static int isinstack (CallInfo *ci, const TObject *o) {
+static int isinstack (CallInfo *ci, const TObject *o)
+	/*@*/
+{
   StkId p;
   for (p = ci->base; p < ci->top; p++)
     if (o == p) return 1;
@@ -512,7 +557,9 @@ static int isinstack (CallInfo *ci, const TObject *o) {
 }
 
 
-void luaG_typeerror (lua_State *L, const TObject *o, const char *op) {
+void luaG_typeerror (lua_State *L, const TObject *o, const char *op)
+	/*@*/
+{
   const char *name = NULL;
   const char *t = luaT_typenames[ttype(o)];
   const char *kind = (isinstack(L->ci, o)) ?
@@ -551,7 +598,9 @@ int luaG_ordererror (lua_State *L, const TObject *p1, const TObject *p2) {
 }
 
 
-static void addinfo (lua_State *L, const char *msg) {
+static void addinfo (lua_State *L, const char *msg)
+	/*@modifies L @*/
+{
   CallInfo *ci = L->ci;
   if (isLua(ci)) {  /* is Lua code? */
     char buff[LUA_IDSIZE];  /* add file:line information */
diff --git a/lua/ldebug.h b/lua/ldebug.h
index 1412b32d4..edf258ed5 100644
--- a/lua/ldebug.h
+++ b/lua/ldebug.h
@@ -1,5 +1,5 @@
 /*
-** $Id: ldebug.h,v 1.1 2004/03/16 21:58:30 niemeyer Exp $
+** $Id: ldebug.h,v 1.2 2004/03/23 05:09:14 jbj Exp $
 ** Auxiliary functions from Debug Interface module
 ** See Copyright Notice in lua.h
 */
@@ -18,14 +18,22 @@
 #define resethookcount(L)	(L->hookcount = L->basehookcount)
 
 
-void luaG_inithooks (lua_State *L);
-void luaG_typeerror (lua_State *L, const TObject *o, const char *opname);
-void luaG_concaterror (lua_State *L, StkId p1, StkId p2);
-void luaG_aritherror (lua_State *L, const TObject *p1, const TObject *p2);
-int luaG_ordererror (lua_State *L, const TObject *p1, const TObject *p2);
-void luaG_runerror (lua_State *L, const char *fmt, ...);
-void luaG_errormsg (lua_State *L);
-int luaG_checkcode (const Proto *pt);
+void luaG_inithooks (lua_State *L)
+	/*@modifies L @*/;
+void luaG_typeerror (lua_State *L, const TObject *o, const char *opname)
+	/*@modifies L @*/;
+void luaG_concaterror (lua_State *L, StkId p1, StkId p2)
+	/*@modifies L @*/;
+void luaG_aritherror (lua_State *L, const TObject *p1, const TObject *p2)
+	/*@modifies L @*/;
+int luaG_ordererror (lua_State *L, const TObject *p1, const TObject *p2)
+	/*@modifies L @*/;
+void luaG_runerror (lua_State *L, const char *fmt, ...)
+	/*@modifies L @*/;
+void luaG_errormsg (lua_State *L)
+	/*@modifies L @*/;
+int luaG_checkcode (const Proto *pt)
+	/*@*/;
 
 
 #endif
diff --git a/lua/ldo.c b/lua/ldo.c
index 19f9069fd..6ba71ca08 100644
--- a/lua/ldo.c
+++ b/lua/ldo.c
@@ -1,5 +1,5 @@
 /*
-** $Id: ldo.c,v 1.2 2004/03/19 21:14:32 niemeyer Exp $
+** $Id: ldo.c,v 1.3 2004/03/23 05:09:14 jbj Exp $
 ** Stack and Call structure of Lua
 ** See Copyright Notice in lua.h
 */
@@ -47,7 +47,9 @@ struct lua_longjmp {
 };
 
 
-static void seterrorobj (lua_State *L, int errcode, StkId oldtop) {
+static void seterrorobj (lua_State *L, int errcode, StkId oldtop)
+	/*@modifies L, oldtop @*/
+{
   switch (errcode) {
     case LUA_ERRMEM: {
       setsvalue2s(oldtop, luaS_new(L, MEMERRMSG));
@@ -91,7 +93,9 @@ int luaD_rawrunprotected (lua_State *L, Pfunc f, void *ud) {
 }
 
 
-static void restore_stack_limit (lua_State *L) {
+static void restore_stack_limit (lua_State *L)
+	/*@modifies L @*/
+{
   L->stack_last = L->stack+L->stacksize-1;
   if (L->size_ci > LUA_MAXCALLS) {  /* there was an overflow? */
     int inuse = (L->ci - L->base_ci);
@@ -103,7 +107,9 @@ static void restore_stack_limit (lua_State *L) {
 /* }====================================================== */
 
 
-static void correctstack (lua_State *L, TObject *oldstack) {
+static void correctstack (lua_State *L, TObject *oldstack)
+	/*@modifies L @*/
+{
   CallInfo *ci;
   GCObject *up;
   L->top = (L->top - oldstack) + L->stack;
@@ -143,7 +149,9 @@ void luaD_growstack (lua_State *L, int n) {
 }
 
 
-static void luaD_growCI (lua_State *L) {
+static void luaD_growCI (lua_State *L)
+	/*@modifies L @*/
+{
   if (L->size_ci > LUA_MAXCALLS)  /* overflow while handling overflow? */
     luaD_throw(L, LUA_ERRERR);
   else {
@@ -180,7 +188,9 @@ void luaD_callhook (lua_State *L, int event, int line) {
 }
 
 
-static void adjust_varargs (lua_State *L, int nfixargs, StkId base) {
+static void adjust_varargs (lua_State *L, int nfixargs, StkId base)
+	/*@modifies L @*/
+{
   int i;
   Table *htab;
   TObject nname;
@@ -203,7 +213,10 @@ static void adjust_varargs (lua_State *L, int nfixargs, StkId base) {
 }
 
 
-static StkId tryfuncTM (lua_State *L, StkId func) {
+/*@dependent@*/
+static StkId tryfuncTM (lua_State *L, StkId func)
+	/*@modifies L @*/
+{
   const TObject *tm = luaT_gettmbyobj(L, func, TM_CALL);
   StkId p;
   ptrdiff_t funcr = savestack(L, func);
@@ -264,7 +277,10 @@ StkId luaD_precall (lua_State *L, StkId func) {
 }
 
 
-static StkId callrethooks (lua_State *L, StkId firstResult) {
+/*@dependent@*/
+static StkId callrethooks (lua_State *L, StkId firstResult)
+	/*@modifies L @*/
+{
   ptrdiff_t fr = savestack(L, firstResult);  /* next call may change stack */
   luaD_callhook(L, LUA_HOOKRET, -1);
   if (!(L->ci->state & CI_C)) {  /* Lua function? */
@@ -317,7 +333,9 @@ void luaD_call (lua_State *L, StkId func, int nResults) {
 }
 
 
-static void resume (lua_State *L, void *ud) {
+static void resume (lua_State *L, void *ud)
+	/*@modifies L @*/
+{
   StkId firstResult;
   int nargs = *cast(int *, ud);
   CallInfo *ci = L->ci;
@@ -347,7 +365,9 @@ static void resume (lua_State *L, void *ud) {
 }
 
 
-static int resume_error (lua_State *L, const char *msg) {
+static int resume_error (lua_State *L, const char *msg)
+	/*@modifies L @*/
+{
   L->top = L->ci->base;
   setsvalue2s(L->top, luaS_new(L, msg));
   incr_top(L);
@@ -356,7 +376,9 @@ static int resume_error (lua_State *L, const char *msg) {
 }
 
 
-LUA_API int lua_resume (lua_State *L, int nargs) {
+LUA_API int lua_resume (lua_State *L, int nargs)
+	/*@modifies L @*/
+{
   int status;
   lu_byte old_allowhooks;
   lua_lock(L);
@@ -383,7 +405,9 @@ LUA_API int lua_resume (lua_State *L, int nargs) {
 }
 
 
-LUA_API int lua_yield (lua_State *L, int nresults) {
+LUA_API int lua_yield (lua_State *L, int nresults)
+	/*@modifies L @*/
+{
   CallInfo *ci;
   lua_lock(L);
   ci = L->ci;
@@ -439,7 +463,9 @@ struct SParser {  /* data to `f_parser' */
   int bin;
 };
 
-static void f_parser (lua_State *L, void *ud) {
+static void f_parser (lua_State *L, void *ud)
+	/*@modifies L @*/
+{
   struct SParser *p;
   Proto *tf;
   Closure *cl;
diff --git a/lua/ldo.h b/lua/ldo.h
index 25903ad4d..76e7b873a 100644
--- a/lua/ldo.h
+++ b/lua/ldo.h
@@ -1,5 +1,5 @@
 /*
-** $Id: ldo.h,v 1.1 2004/03/16 21:58:30 niemeyer Exp $
+** $Id: ldo.h,v 1.2 2004/03/23 05:09:14 jbj Exp $
 ** Stack and Call structure of Lua
 ** See Copyright Notice in lua.h
 */
@@ -41,20 +41,34 @@
 /* type of protected functions, to be ran by `runprotected' */
 typedef void (*Pfunc) (lua_State *L, void *ud);
 
-void luaD_resetprotection (lua_State *L);
-int luaD_protectedparser (lua_State *L, ZIO *z, int bin);
-void luaD_callhook (lua_State *L, int event, int line);
-StkId luaD_precall (lua_State *L, StkId func);
-void luaD_call (lua_State *L, StkId func, int nResults);
+/*@unused@*/
+void luaD_resetprotection (lua_State *L)
+	/*@modifies L @*/;
+int luaD_protectedparser (lua_State *L, ZIO *z, int bin)
+	/*@modifies L, z @*/;
+void luaD_callhook (lua_State *L, int event, int line)
+	/*@modifies L @*/;
+/*@null@*/
+StkId luaD_precall (lua_State *L, StkId func)
+	/*@modifies L @*/;
+void luaD_call (lua_State *L, StkId func, int nResults)
+	/*@modifies L @*/;
 int luaD_pcall (lua_State *L, Pfunc func, void *u,
-                ptrdiff_t oldtop, ptrdiff_t ef);
-void luaD_poscall (lua_State *L, int wanted, StkId firstResult);
-void luaD_reallocCI (lua_State *L, int newsize);
-void luaD_reallocstack (lua_State *L, int newsize);
-void luaD_growstack (lua_State *L, int n);
-
-void luaD_throw (lua_State *L, int errcode);
-int luaD_rawrunprotected (lua_State *L, Pfunc f, void *ud);
+                ptrdiff_t oldtop, ptrdiff_t ef)
+	/*@modifies L @*/;
+void luaD_poscall (lua_State *L, int wanted, StkId firstResult)
+	/*@modifies L @*/;
+void luaD_reallocCI (lua_State *L, int newsize)
+	/*@modifies L @*/;
+void luaD_reallocstack (lua_State *L, int newsize)
+	/*@modifies L @*/;
+void luaD_growstack (lua_State *L, int n)
+	/*@modifies L @*/;
+
+void luaD_throw (lua_State *L, int errcode)
+	/*@modifies L @*/;
+int luaD_rawrunprotected (lua_State *L, Pfunc f, /*@null@*/ void *ud)
+	/*@modifies L @*/;
 
 
 #endif
diff --git a/lua/ldump.c b/lua/ldump.c
index 00732acaa..bf80d73c9 100644
--- a/lua/ldump.c
+++ b/lua/ldump.c
@@ -1,5 +1,5 @@
 /*
-** $Id: ldump.c,v 1.1 2004/03/16 21:58:30 niemeyer Exp $
+** $Id: ldump.c,v 1.2 2004/03/23 05:09:14 jbj Exp $
 ** save bytecodes
 ** See Copyright Notice in lua.h
 */
@@ -25,6 +25,7 @@ typedef struct {
 } DumpState;
 
 static void DumpBlock(const void* b, size_t size, DumpState* D)
+	/*@*/
 {
  lua_unlock(D->L);
  (*D->write)(D->L,b,size,D->data);
@@ -32,27 +33,32 @@ static void DumpBlock(const void* b, size_t size, DumpState* D)
 }
 
 static void DumpByte(int y, DumpState* D)
+	/*@*/
 {
  char x=(char)y;
  DumpBlock(&x,sizeof(x),D);
 }
 
 static void DumpInt(int x, DumpState* D)
+	/*@*/
 {
  DumpBlock(&x,sizeof(x),D);
 }
 
 static void DumpSize(size_t x, DumpState* D)
+	/*@*/
 {
  DumpBlock(&x,sizeof(x),D);
 }
 
 static void DumpNumber(lua_Number x, DumpState* D)
+	/*@*/
 {
  DumpBlock(&x,sizeof(x),D);
 }
 
-static void DumpString(TString* s, DumpState* D)
+static void DumpString(/*@null@*/ TString* s, DumpState* D)
+	/*@*/
 {
  if (s==NULL || getstr(s)==NULL)
   DumpSize(0,D);
@@ -65,12 +71,14 @@ static void DumpString(TString* s, DumpState* D)
 }
 
 static void DumpCode(const Proto* f, DumpState* D)
+	/*@*/
 {
  DumpInt(f->sizecode,D);
  DumpVector(f->code,f->sizecode,sizeof(*f->code),D);
 }
 
 static void DumpLocals(const Proto* f, DumpState* D)
+	/*@*/
 {
  int i,n=f->sizelocvars;
  DumpInt(n,D);
@@ -83,21 +91,24 @@ static void DumpLocals(const Proto* f, DumpState* D)
 }
 
 static void DumpLines(const Proto* f, DumpState* D)
+	/*@*/
 {
  DumpInt(f->sizelineinfo,D);
  DumpVector(f->lineinfo,f->sizelineinfo,sizeof(*f->lineinfo),D);
 }
 
 static void DumpUpvalues(const Proto* f, DumpState* D)
+	/*@*/
 {
  int i,n=f->sizeupvalues;
  DumpInt(n,D);
  for (i=0; i<n; i++) DumpString(f->upvalues[i],D);
 }
 
-static void DumpFunction(const Proto* f, const TString* p, DumpState* D);
+static void DumpFunction(const Proto* f, /*@null@*/ const TString* p, DumpState* D)		/*@*/;
 
 static void DumpConstants(const Proto* f, DumpState* D)
+	/*@*/
 {
  int i,n;
  DumpInt(n=f->sizek,D);
@@ -125,6 +136,7 @@ static void DumpConstants(const Proto* f, DumpState* D)
 }
 
 static void DumpFunction(const Proto* f, const TString* p, DumpState* D)
+	/*@*/
 {
  DumpString((f->source==p) ? NULL : f->source,D);
  DumpInt(f->lineDefined,D);
@@ -140,6 +152,7 @@ static void DumpFunction(const Proto* f, const TString* p, DumpState* D)
 }
 
 static void DumpHeader(DumpState* D)
+	/*@*/
 {
  DumpLiteral(LUA_SIGNATURE,D);
  DumpByte(VERSION,D);
diff --git a/lua/lfunc.h b/lua/lfunc.h
index 90b959f64..8378deaba 100644
--- a/lua/lfunc.h
+++ b/lua/lfunc.h
@@ -1,5 +1,5 @@
 /*
-** $Id: lfunc.h,v 1.1 2004/03/16 21:58:30 niemeyer Exp $
+** $Id: lfunc.h,v 1.2 2004/03/23 05:09:14 jbj Exp $
 ** Auxiliary functions to manipulate prototypes and closures
 ** See Copyright Notice in lua.h
 */
@@ -11,15 +11,28 @@
 #include "lobject.h"
 
 
-Proto *luaF_newproto (lua_State *L);
-Closure *luaF_newCclosure (lua_State *L, int nelems);
-Closure *luaF_newLclosure (lua_State *L, int nelems, TObject *e);
-UpVal *luaF_findupval (lua_State *L, StkId level);
-void luaF_close (lua_State *L, StkId level);
-void luaF_freeproto (lua_State *L, Proto *f);
-void luaF_freeclosure (lua_State *L, Closure *c);
-
-const char *luaF_getlocalname (const Proto *func, int local_number, int pc);
+/*@null@*/
+Proto *luaF_newproto (lua_State *L)
+	/*@modifies L @*/;
+/*@null@*/
+Closure *luaF_newCclosure (lua_State *L, int nelems)
+	/*@modifies L @*/;
+/*@null@*/
+Closure *luaF_newLclosure (lua_State *L, int nelems, TObject *e)
+	/*@modifies L @*/;
+/*@null@*/
+UpVal *luaF_findupval (lua_State *L, StkId level)
+	/*@modifies L @*/;
+void luaF_close (lua_State *L, StkId level)
+	/*@modifies L @*/;
+void luaF_freeproto (lua_State *L, Proto *f)
+	/*@modifies L, f @*/;
+void luaF_freeclosure (lua_State *L, Closure *c)
+	/*@modifies L, c @*/;
+
+/*@observer@*/ /*@null@*/
+const char *luaF_getlocalname (const Proto *func, int local_number, int pc)
+	/*@*/;
 
 
 #endif
diff --git a/lua/lgc.c b/lua/lgc.c
index dab85e058..f2c60936a 100644
--- a/lua/lgc.c
+++ b/lua/lgc.c
@@ -1,5 +1,5 @@
 /*
-** $Id: lgc.c,v 1.2 2004/03/19 21:14:32 niemeyer Exp $
+** $Id: lgc.c,v 1.3 2004/03/23 05:09:14 jbj Exp $
 ** Garbage Collector
 ** See Copyright Notice in lua.h
 */
@@ -23,10 +23,15 @@
 
 
 typedef struct GCState {
+/*@null@*/
   GCObject *tmark;  /* list of marked objects to be traversed */
+/*@null@*/
   GCObject *wk;  /* list of traversed key-weak tables (to be cleared) */
+/*@null@*/
   GCObject *wv;  /* list of traversed value-weak tables */
+/*@null@*/
   GCObject *wkv;  /* list of traversed key-value weak tables */
+/*@null@*/
   global_State *g;
 } GCState;
 
@@ -67,7 +72,9 @@ typedef struct GCState {
 
 
 
-static void reallymarkobject (GCState *st, GCObject *o) {
+static void reallymarkobject (GCState *st, GCObject *o)
+	/*@modifies st, o @*/
+{
   lua_assert(!ismarked(o));
   setbit(o->gch.marked, 0);  /* mark object */
   switch (o->gch.tt) {
@@ -86,7 +93,9 @@ static void reallymarkobject (GCState *st, GCObject *o) {
       break;
     }
     case LUA_TTHREAD: {
+/*@-onlytrans@*/
       gcototh(o)->gclist = st->tmark;
+/*@=onlytrans@*/
       st->tmark = o;
       break;
     }
@@ -100,7 +109,9 @@ static void reallymarkobject (GCState *st, GCObject *o) {
 }
 
 
-static void marktmu (GCState *st) {
+static void marktmu (GCState *st)
+	/*@modifies st @*/
+{
   GCObject *u;
   for (u = st->g->tmudata; u; u = u->gch.next) {
     unmark(u);  /* may be marked, if left from previous GC */
@@ -134,20 +145,26 @@ size_t luaC_separateudata (lua_State *L) {
     }
   }
   /* insert collected udata with gc event into `tmudata' list */
+/*@-dependenttrans@*/
   *lastcollected = G(L)->tmudata;
+/*@=dependenttrans@*/
   G(L)->tmudata = collected;
   return deadmem;
 }
 
 
-static void removekey (Node *n) {
+static void removekey (Node *n)
+	/*@modifies n @*/
+{
   setnilvalue(gval(n));  /* remove corresponding value ... */
   if (iscollectable(gkey(n)))
     setttype(gkey(n), LUA_TNONE);  /* dead key; remove it */
 }
 
 
-static void traversetable (GCState *st, Table *h) {
+static void traversetable (GCState *st, Table *h)
+	/*@modifies st, h @*/
+{
   int i;
   int weakkey = 0;
   int weakvalue = 0;
@@ -187,7 +204,9 @@ static void traversetable (GCState *st, Table *h) {
 }
 
 
-static void traverseproto (GCState *st, Proto *f) {
+static void traverseproto (GCState *st, Proto *f)
+	/*@modifies st, f @*/
+{
   int i;
   stringmark(f->source);
   for (i=0; i<f->sizek; i++) {  /* mark literal strings */
@@ -205,7 +224,9 @@ static void traverseproto (GCState *st, Proto *f) {
 
 
 
-static void traverseclosure (GCState *st, Closure *cl) {
+static void traverseclosure (GCState *st, Closure *cl)
+	/*@modifies st, cl @*/
+{
   if (cl->c.isC) {
     int i;
     for (i=0; i<cl->c.nupvalues; i++)  /* mark its upvalues */
@@ -227,7 +248,9 @@ static void traverseclosure (GCState *st, Closure *cl) {
 }
 
 
-static void checkstacksizes (lua_State *L, StkId max) {
+static void checkstacksizes (lua_State *L, StkId max)
+	/*@modifies L @*/
+{
   int used = L->ci - L->base_ci;  /* number of `ci' in use */
   if (4*used < L->size_ci && 2*BASIC_CI_SIZE < L->size_ci)
     luaD_reallocCI(L, L->size_ci/2);  /* still big enough... */
@@ -239,7 +262,9 @@ static void checkstacksizes (lua_State *L, StkId max) {
 }
 
 
-static void traversestack (GCState *st, lua_State *L1) {
+static void traversestack (GCState *st, lua_State *L1)
+	/*@modifies st, L1 @*/
+{
   StkId o, lim;
   CallInfo *ci;
   markobject(st, gt(L1));
@@ -258,7 +283,9 @@ static void traversestack (GCState *st, lua_State *L1) {
 }
 
 
-static void propagatemarks (GCState *st) {
+static void propagatemarks (GCState *st)
+	/*@modifies st @*/
+{
   while (st->tmark) {  /* traverse marked objects */
     switch (st->tmark->gch.tt) {
       case LUA_TTABLE: {
@@ -275,7 +302,9 @@ static void propagatemarks (GCState *st) {
       }
       case LUA_TTHREAD: {
         lua_State *th = gcototh(st->tmark);
+/*@-dependenttrans@*/
         st->tmark = th->gclist;
+/*@=dependenttrans@*/
         traversestack(st, th);
         break;
       }
@@ -291,7 +320,9 @@ static void propagatemarks (GCState *st) {
 }
 
 
-static int valismarked (const TObject *o) {
+static int valismarked (const TObject *o)
+	/*@modifies o @*/
+{
   if (ttisstring(o))
     stringmark(tsvalue(o));  /* strings are `values', so are never weak */
   return !iscollectable(o) || testbit(o->value.gc->gch.marked, 0);
@@ -301,7 +332,9 @@ static int valismarked (const TObject *o) {
 /*
 ** clear collected keys from weaktables
 */
-static void cleartablekeys (GCObject *l) {
+static void cleartablekeys (/*@null@*/ GCObject *l)
+	/*@modifies l @*/
+{
   while (l) {
     Table *h = gcotoh(l);
     int i = sizenode(h);
@@ -319,7 +352,9 @@ static void cleartablekeys (GCObject *l) {
 /*
 ** clear collected values from weaktables
 */
-static void cleartablevalues (GCObject *l) {
+static void cleartablevalues (/*@null@*/ GCObject *l)
+	/*@modifies l @*/
+{
   while (l) {
     Table *h = gcotoh(l);
     int i = h->sizearray;
@@ -340,7 +375,9 @@ static void cleartablevalues (GCObject *l) {
 }
 
 
-static void freeobj (lua_State *L, GCObject *o) {
+static void freeobj (lua_State *L, GCObject *o)
+	/*@modifies L, o @*/
+{
   switch (o->gch.tt) {
     case LUA_TPROTO: luaF_freeproto(L, gcotop(o)); break;
     case LUA_TFUNCTION: luaF_freeclosure(L, gcotocl(o)); break;
@@ -364,7 +401,9 @@ static void freeobj (lua_State *L, GCObject *o) {
 }
 
 
-static int sweeplist (lua_State *L, GCObject **p, int limit) {
+static int sweeplist (lua_State *L, GCObject **p, int limit)
+	/*@modifies L, *p @*/
+{
   GCObject *curr;
   int count = 0;  /* number of collected items */
   while ((curr = *p) != NULL) {
@@ -374,7 +413,9 @@ static int sweeplist (lua_State *L, GCObject **p, int limit) {
     }
     else {
       count++;
+/*@-dependenttrans@*/
       *p = curr->gch.next;
+/*@=dependenttrans@*/
       freeobj(L, curr);
     }
   }
@@ -382,7 +423,9 @@ static int sweeplist (lua_State *L, GCObject **p, int limit) {
 }
 
 
-static void sweepstrings (lua_State *L, int all) {
+static void sweepstrings (lua_State *L, int all)
+	/*@modifies L @*/
+{
   int i;
   for (i=0; i<G(L)->strt.size; i++) {  /* for each list */
     G(L)->strt.nuse -= sweeplist(L, &G(L)->strt.hash[i], all);
@@ -390,7 +433,9 @@ static void sweepstrings (lua_State *L, int all) {
 }
 
 
-static void checkSizes (lua_State *L, size_t deadmem) {
+static void checkSizes (lua_State *L, size_t deadmem)
+	/*@modifies L @*/
+{
   /* check size of string hash */
   if (G(L)->strt.nuse < cast(ls_nstr, G(L)->strt.size/4) &&
       G(L)->strt.size > MINSTRTABSIZE*2)
@@ -404,7 +449,9 @@ static void checkSizes (lua_State *L, size_t deadmem) {
 }
 
 
-static void do1gcTM (lua_State *L, Udata *udata) {
+static void do1gcTM (lua_State *L, Udata *udata)
+	/*@modifies L, udata @*/
+{
   const TObject *tm = fasttm(L, udata->uv.metatable, TM_GC);
   if (tm != NULL) {
     setobj2s(L->top, tm);
@@ -444,7 +491,9 @@ void luaC_sweep (lua_State *L, int all) {
 
 
 /* mark root set */
-static void markroot (GCState *st, lua_State *L) {
+static void markroot (GCState *st, lua_State *L)
+	/*@modifies st, L @*/
+{
   global_State *g = st->g;
   markobject(st, defaultmeta(L));
   markobject(st, registry(L));
@@ -454,7 +503,9 @@ static void markroot (GCState *st, lua_State *L) {
 }
 
 
-static size_t mark (lua_State *L) {
+static size_t mark (lua_State *L)
+	/*@modifies L @*/
+{
   size_t deadmem;
   GCState st;
   GCObject *wkv;
diff --git a/lua/lgc.h b/lua/lgc.h
index 36fd877cb..d6542797e 100644
--- a/lua/lgc.h
+++ b/lua/lgc.h
@@ -1,5 +1,5 @@
 /*
-** $Id: lgc.h,v 1.2 2004/03/19 21:14:32 niemeyer Exp $
+** $Id: lgc.h,v 1.3 2004/03/23 05:09:14 jbj Exp $
 ** Garbage Collector
 ** See Copyright Notice in lua.h
 */
@@ -15,11 +15,16 @@
 	if (G(L)->nblocks >= G(L)->GCthreshold) luaC_collectgarbage(L); }
 
 
-size_t luaC_separateudata (lua_State *L);
-void luaC_callGCTM (lua_State *L);
-void luaC_sweep (lua_State *L, int all);
-void luaC_collectgarbage (lua_State *L);
-void luaC_link (lua_State *L, GCObject *o, lu_byte tt);
+size_t luaC_separateudata (lua_State *L)
+	/*@modifies L @*/;
+void luaC_callGCTM (lua_State *L)
+	/*@modifies L @*/;
+void luaC_sweep (lua_State *L, int all)
+	/*@modifies L @*/;
+void luaC_collectgarbage (lua_State *L)
+	/*@modifies L @*/;
+void luaC_link (lua_State *L, GCObject *o, lu_byte tt)
+	/*@modifies L, o @*/;
 
 
 #endif
diff --git a/lua/lib/lauxlib.c b/lua/lib/lauxlib.c
index 2655c3310..47e7b91bf 100644
--- a/lua/lib/lauxlib.c
+++ b/lua/lib/lauxlib.c
@@ -1,5 +1,5 @@
 /*
-** $Id: lauxlib.c,v 1.1 2004/03/16 21:58:30 niemeyer Exp $
+** $Id: lauxlib.c,v 1.2 2004/03/23 05:09:14 jbj Exp $
 ** Auxiliary functions for building Lua libraries
 ** See Copyright Notice in lua.h
 */
@@ -66,7 +66,9 @@ LUALIB_API int luaL_typerror (lua_State *L, int narg, const char *tname) {
 }
 
 
-static void tag_error (lua_State *L, int narg, int tag) {
+static void tag_error (lua_State *L, int narg, int tag)
+	/*@modifies L @*/
+{
   luaL_typerror(L, narg, lua_typename(L, tag)); 
 }
 
@@ -255,7 +257,9 @@ LUALIB_API void luaL_openlib (lua_State *L, const char *libname,
 ** =======================================================
 */
 
-static int checkint (lua_State *L, int topop) {
+static int checkint (lua_State *L, int topop)
+	/*@modifies L @*/
+{
   int n = (int)lua_tonumber(L, -1);
   if (n == 0 && !lua_isnumber(L, -1)) n = -1;
   lua_pop(L, topop);
@@ -263,7 +267,9 @@ static int checkint (lua_State *L, int topop) {
 }
 
 
-static void getsizes (lua_State *L) {
+static void getsizes (lua_State *L)
+	/*@modifies L @*/
+{
   lua_rawgeti(L, LUA_REGISTRYINDEX, ARRAYSIZE_REF);
   if (lua_isnil(L, -1)) {  /* no `size' table? */
     lua_pop(L, 1);  /* remove nil */
@@ -334,7 +340,9 @@ int luaL_getn (lua_State *L, int t) {
 #define LIMIT	(LUA_MINSTACK/2)
 
 
-static int emptybuffer (luaL_Buffer *B) {
+static int emptybuffer (luaL_Buffer *B)
+	/*@modifies B @*/
+{
   size_t l = bufflen(B);
   if (l == 0) return 0;  /* put nothing on stack */
   else {
@@ -346,7 +354,9 @@ static int emptybuffer (luaL_Buffer *B) {
 }
 
 
-static void adjuststack (luaL_Buffer *B) {
+static void adjuststack (luaL_Buffer *B)
+	/*@modifies B @*/
+{
   if (B->lvl > 1) {
     lua_State *L = B->L;
     int toget = 1;  /* number of levels to concat */
@@ -461,12 +471,17 @@ LUALIB_API void luaL_unref (lua_State *L, int t, int ref) {
 */
 
 typedef struct LoadF {
+/*@dependent@*/
   FILE *f;
   char buff[LUAL_BUFFERSIZE];
 } LoadF;
 
 
-static const char *getF (lua_State *L, void *ud, size_t *size) {
+/*@observer@*/ /*@null@*/
+static const char *getF (lua_State *L, void *ud, size_t *size)
+	/*@globals fileSystem @*/
+	/*@modifies *size, fileSystem @*/
+{
   LoadF *lf = (LoadF *)ud;
   (void)L;
   if (feof(lf->f)) return NULL;
@@ -475,7 +490,9 @@ static const char *getF (lua_State *L, void *ud, size_t *size) {
 }
 
 
-static int errfile (lua_State *L, int fnameindex) {
+static int errfile (lua_State *L, int fnameindex)
+	/*@modifies L @*/
+{
   const char *filename = lua_tostring(L, fnameindex) + 1;
   lua_pushfstring(L, "cannot read %s: %s", filename, strerror(errno));
   lua_remove(L, fnameindex);
@@ -521,7 +538,9 @@ typedef struct LoadS {
 } LoadS;
 
 
-static const char *getS (lua_State *L, void *ud, size_t *size) {
+static const char *getS (lua_State *L, void *ud, size_t *size)
+	/*@modifies *size @*/
+{
   LoadS *ls = (LoadS *)ud;
   (void)L;
   if (ls->size == 0) return NULL;
@@ -549,7 +568,10 @@ LUALIB_API int luaL_loadbuffer (lua_State *L, const char *buff, size_t size,
 */
 
 
-static void callalert (lua_State *L, int status) {
+static void callalert (lua_State *L, int status)
+	/*@globals fileSystem @*/
+	/*@modifies L, fileSystem @*/
+{
   if (status != 0) {
     lua_getglobal(L, "_ALERT");
     if (lua_isfunction(L, -1)) {
@@ -564,7 +586,10 @@ static void callalert (lua_State *L, int status) {
 }
 
 
-static int aux_do (lua_State *L, int status) {
+static int aux_do (lua_State *L, int status)
+	/*@globals fileSystem @*/
+	/*@modifies L, fileSystem @*/
+{
   if (status == 0) {  /* parse OK? */
     status = lua_pcall(L, 0, LUA_MULTRET, 0);  /* call main */
   }
diff --git a/lua/lib/lbaselib.c b/lua/lib/lbaselib.c
index e7b0fe33b..55568bdde 100644
--- a/lua/lib/lbaselib.c
+++ b/lua/lib/lbaselib.c
@@ -1,5 +1,5 @@
 /*
-** $Id: lbaselib.c,v 1.2 2004/03/19 21:14:32 niemeyer Exp $
+** $Id: lbaselib.c,v 1.3 2004/03/23 05:09:14 jbj Exp $
 ** Basic library
 ** See Copyright Notice in lua.h
 */
@@ -27,7 +27,10 @@
 ** model but changing `fputs' to put the strings at a proper place
 ** (a console window or a log file, for instance).
 */
-static int luaB_print (lua_State *L) {
+static int luaB_print (lua_State *L)
+	/*@globals fileSystem @*/
+	/*@modifies L, fileSystem @*/
+{
   int n = lua_gettop(L);  /* number of arguments */
   int i;
   lua_getglobal(L, "tostring");
@@ -48,7 +51,9 @@ static int luaB_print (lua_State *L) {
 }
 
 
-static int luaB_tonumber (lua_State *L) {
+static int luaB_tonumber (lua_State *L)
+	/*@modifies L @*/
+{
   int base = luaL_optint(L, 2, 10);
   if (base == 10) {  /* standard conversion */
     luaL_checkany(L, 1);
@@ -76,7 +81,9 @@ static int luaB_tonumber (lua_State *L) {
 }
 
 
-static int luaB_error (lua_State *L) {
+static int luaB_error (lua_State *L)
+	/*@modifies L @*/
+{
   int level = luaL_optint(L, 2, 1);
   luaL_checkany(L, 1);
   if (!lua_isstring(L, 1) || level == 0)
@@ -90,7 +97,9 @@ static int luaB_error (lua_State *L) {
 }
 
 
-static int luaB_getmetatable (lua_State *L) {
+static int luaB_getmetatable (lua_State *L)
+	/*@modifies L @*/
+{
   luaL_checkany(L, 1);
   if (!lua_getmetatable(L, 1)) {
     lua_pushnil(L);
@@ -101,7 +110,9 @@ static int luaB_getmetatable (lua_State *L) {
 }
 
 
-static int luaB_setmetatable (lua_State *L) {
+static int luaB_setmetatable (lua_State *L)
+	/*@modifies L @*/
+{
   int t = lua_type(L, 2);
   luaL_checktype(L, 1, LUA_TTABLE);
   luaL_argcheck(L, t == LUA_TNIL || t == LUA_TTABLE, 2,
@@ -114,7 +125,9 @@ static int luaB_setmetatable (lua_State *L) {
 }
 
 
-static void getfunc (lua_State *L) {
+static void getfunc (lua_State *L)
+	/*@modifies L @*/
+{
   if (lua_isfunction(L, 1)) lua_pushvalue(L, 1);
   else {
     lua_Debug ar;
@@ -130,7 +143,9 @@ static void getfunc (lua_State *L) {
 }
 
 
-static int aux_getfenv (lua_State *L) {
+static int aux_getfenv (lua_State *L)
+	/*@modifies L @*/
+{
   lua_getfenv(L, -1);
   lua_pushliteral(L, "__fenv");
   lua_rawget(L, -2);
@@ -138,7 +153,9 @@ static int aux_getfenv (lua_State *L) {
 }
 
 
-static int luaB_getfenv (lua_State *L) {
+static int luaB_getfenv (lua_State *L)
+	/*@modifies L @*/
+{
   getfunc(L);
   if (!aux_getfenv(L))  /* __fenv not defined? */
     lua_pop(L, 1);  /* remove it, to return real environment */
@@ -146,7 +163,9 @@ static int luaB_getfenv (lua_State *L) {
 }
 
 
-static int luaB_setfenv (lua_State *L) {
+static int luaB_setfenv (lua_State *L)
+	/*@modifies L @*/
+{
   luaL_checktype(L, 2, LUA_TTABLE);
   getfunc(L);
   if (aux_getfenv(L))  /* __fenv defined? */
@@ -162,7 +181,9 @@ static int luaB_setfenv (lua_State *L) {
 }
 
 
-static int luaB_rawequal (lua_State *L) {
+static int luaB_rawequal (lua_State *L)
+	/*@modifies L @*/
+{
   luaL_checkany(L, 1);
   luaL_checkany(L, 2);
   lua_pushboolean(L, lua_rawequal(L, 1, 2));
@@ -170,14 +191,18 @@ static int luaB_rawequal (lua_State *L) {
 }
 
 
-static int luaB_rawget (lua_State *L) {
+static int luaB_rawget (lua_State *L)
+	/*@modifies L @*/
+{
   luaL_checktype(L, 1, LUA_TTABLE);
   luaL_checkany(L, 2);
   lua_rawget(L, 1);
   return 1;
 }
 
-static int luaB_rawset (lua_State *L) {
+static int luaB_rawset (lua_State *L)
+	/*@modifies L @*/
+{
   luaL_checktype(L, 1, LUA_TTABLE);
   luaL_checkany(L, 2);
   luaL_checkany(L, 3);
@@ -186,27 +211,35 @@ static int luaB_rawset (lua_State *L) {
 }
 
 
-static int luaB_gcinfo (lua_State *L) {
+static int luaB_gcinfo (lua_State *L)
+	/*@modifies L @*/
+{
   lua_pushnumber(L, (lua_Number)lua_getgccount(L));
   lua_pushnumber(L, (lua_Number)lua_getgcthreshold(L));
   return 2;
 }
 
 
-static int luaB_collectgarbage (lua_State *L) {
+static int luaB_collectgarbage (lua_State *L)
+	/*@modifies L @*/
+{
   lua_setgcthreshold(L, luaL_optint(L, 1, 0));
   return 0;
 }
 
 
-static int luaB_type (lua_State *L) {
+static int luaB_type (lua_State *L)
+	/*@modifies L @*/
+{
   luaL_checkany(L, 1);
   lua_pushstring(L, lua_typename(L, lua_type(L, 1)));
   return 1;
 }
 
 
-static int luaB_next (lua_State *L) {
+static int luaB_next (lua_State *L)
+	/*@modifies L @*/
+{
   luaL_checktype(L, 1, LUA_TTABLE);
   lua_settop(L, 2);  /* create a 2nd argument if there isn't one */
   if (lua_next(L, 1))
@@ -218,7 +251,9 @@ static int luaB_next (lua_State *L) {
 }
 
 
-static int luaB_pairs (lua_State *L) {
+static int luaB_pairs (lua_State *L)
+	/*@modifies L @*/
+{
   luaL_checktype(L, 1, LUA_TTABLE);
   lua_pushliteral(L, "next");
   lua_rawget(L, LUA_GLOBALSINDEX);  /* return generator, */
@@ -228,7 +263,9 @@ static int luaB_pairs (lua_State *L) {
 }
 
 
-static int luaB_ipairs (lua_State *L) {
+static int luaB_ipairs (lua_State *L)
+	/*@modifies L @*/
+{
   lua_Number i = lua_tonumber(L, 2);
   luaL_checktype(L, 1, LUA_TTABLE);
   if (i == 0 && lua_isnone(L, 2)) {  /* `for' start? */
@@ -247,7 +284,9 @@ static int luaB_ipairs (lua_State *L) {
 }
 
 
-static int load_aux (lua_State *L, int status) {
+static int load_aux (lua_State *L, int status)
+	/*@modifies L @*/
+{
   if (status == 0)  /* OK? */
     return 1;
   else {
@@ -258,7 +297,9 @@ static int load_aux (lua_State *L, int status) {
 }
 
 
-static int luaB_loadstring (lua_State *L) {
+static int luaB_loadstring (lua_State *L)
+	/*@modifies L @*/
+{
   size_t l;
   const char *s = luaL_checklstring(L, 1, &l);
   const char *chunkname = luaL_optstring(L, 2, s);
@@ -266,13 +307,19 @@ static int luaB_loadstring (lua_State *L) {
 }
 
 
-static int luaB_loadfile (lua_State *L) {
+static int luaB_loadfile (lua_State *L)
+	/*@globals fileSystem @*/
+	/*@modifies L, fileSystem @*/
+{
   const char *fname = luaL_optstring(L, 1, NULL);
   return load_aux(L, luaL_loadfile(L, fname));
 }
 
 
-static int luaB_dofile (lua_State *L) {
+static int luaB_dofile (lua_State *L)
+	/*@globals fileSystem @*/
+	/*@modifies L, fileSystem @*/
+{
   const char *fname = luaL_optstring(L, 1, NULL);
   int n = lua_gettop(L);
   int status = luaL_loadfile(L, fname);
@@ -282,7 +329,9 @@ static int luaB_dofile (lua_State *L) {
 }
 
 
-static int luaB_assert (lua_State *L) {
+static int luaB_assert (lua_State *L)
+	/*@modifies L @*/
+{
   luaL_checkany(L, 1);
   if (!lua_toboolean(L, 1))
     return luaL_error(L, "%s", luaL_optstring(L, 2, "assertion failed!"));
@@ -291,7 +340,9 @@ static int luaB_assert (lua_State *L) {
 }
 
 
-static int luaB_unpack (lua_State *L) {
+static int luaB_unpack (lua_State *L)
+	/*@modifies L @*/
+{
   int n, i;
   luaL_checktype(L, 1, LUA_TTABLE);
   n = luaL_getn(L, 1);
@@ -302,7 +353,9 @@ static int luaB_unpack (lua_State *L) {
 }
 
 
-static int luaB_pcall (lua_State *L) {
+static int luaB_pcall (lua_State *L)
+	/*@modifies L @*/
+{
   int status;
   luaL_checkany(L, 1);
   status = lua_pcall(L, lua_gettop(L) - 1, LUA_MULTRET, 0);
@@ -312,7 +365,9 @@ static int luaB_pcall (lua_State *L) {
 }
 
 
-static int luaB_xpcall (lua_State *L) {
+static int luaB_xpcall (lua_State *L)
+	/*@modifies L @*/
+{
   int status;
   luaL_checkany(L, 2);
   lua_settop(L, 2);
@@ -324,7 +379,9 @@ static int luaB_xpcall (lua_State *L) {
 }
 
 
-static int luaB_tostring (lua_State *L) {
+static int luaB_tostring (lua_State *L)
+	/*@modifies L @*/
+{
   char buff[128];
   luaL_checkany(L, 1);
   if (luaL_callmeta(L, 1, "__tostring"))  /* is there a metafield? */
@@ -361,7 +418,9 @@ static int luaB_tostring (lua_State *L) {
 }
 
 
-static int luaB_newproxy (lua_State *L) {
+static int luaB_newproxy (lua_State *L)
+	/*@modifies L @*/
+{
   lua_settop(L, 1);
   lua_newuserdata(L, 0);  /* create proxy */
   if (lua_toboolean(L, 1) == 0)
@@ -413,7 +472,10 @@ static int luaB_newproxy (lua_State *L) {
 #endif
 
 
-static const char *getpath (lua_State *L) {
+/*@observer@*/
+static const char *getpath (lua_State *L)
+	/*@modifies L @*/
+{
   const char *path;
   lua_getglobal(L, LUA_PATH);  /* try global variable */
   path = lua_tostring(L, -1);
@@ -425,7 +487,9 @@ static const char *getpath (lua_State *L) {
 }
 
 
-static const char *pushnextpath (lua_State *L, const char *path) {
+static const char *pushnextpath (lua_State *L, const char *path)
+	/*@modifies L @*/
+{
   const char *l;
   if (*path == '\0') return NULL;  /* no more paths */
   if (*path == LUA_PATH_SEP) path++;  /* skip separator */
@@ -436,7 +500,9 @@ static const char *pushnextpath (lua_State *L, const char *path) {
 }
 
 
-static void pushcomposename (lua_State *L) {
+static void pushcomposename (lua_State *L)
+	/*@modifies L @*/
+{
   const char *path = lua_tostring(L, -1);
   const char *wild;
   int n = 1;
@@ -453,7 +519,10 @@ static void pushcomposename (lua_State *L) {
 }
 
 
-static int luaB_require (lua_State *L) {
+static int luaB_require (lua_State *L)
+	/*@globals fileSystem @*/
+	/*@modifies L, fileSystem @*/
+{
   const char *path;
   int status = LUA_ERRFILE;  /* not found (yet) */
   luaL_checkstring(L, 1);
@@ -505,6 +574,8 @@ static int luaB_require (lua_State *L) {
 /* }====================================================== */
 
 
+/*@-readonlytrans@*/
+/*@unchecked@*/
 static const luaL_reg base_funcs[] = {
   {"error", luaB_error},
   {"getmetatable", luaB_getmetatable},
@@ -533,6 +604,7 @@ static const luaL_reg base_funcs[] = {
   {"require", luaB_require},
   {NULL, NULL}
 };
+/*@=readonlytrans@*/
 
 
 /*
@@ -541,7 +613,9 @@ static const luaL_reg base_funcs[] = {
 ** =======================================================
 */
 
-static int auxresume (lua_State *L, lua_State *co, int narg) {
+static int auxresume (lua_State *L, lua_State *co, int narg)
+	/*@modifies L, co @*/
+{
   int status;
   if (!lua_checkstack(co, narg))
     luaL_error(L, "too many arguments to resume");
@@ -561,7 +635,9 @@ static int auxresume (lua_State *L, lua_State *co, int narg) {
 }
 
 
-static int luaB_coresume (lua_State *L) {
+static int luaB_coresume (lua_State *L)
+	/*@modifies L @*/
+{
   lua_State *co = lua_tothread(L, 1);
   int r;
   luaL_argcheck(L, co, 1, "coroutine expected");
@@ -579,7 +655,9 @@ static int luaB_coresume (lua_State *L) {
 }
 
 
-static int luaB_auxwrap (lua_State *L) {
+static int luaB_auxwrap (lua_State *L)
+	/*@modifies L @*/
+{
   lua_State *co = lua_tothread(L, lua_upvalueindex(1));
   int r = auxresume(L, co, lua_gettop(L));
   if (r < 0) {
@@ -594,7 +672,9 @@ static int luaB_auxwrap (lua_State *L) {
 }
 
 
-static int luaB_cocreate (lua_State *L) {
+static int luaB_cocreate (lua_State *L)
+	/*@modifies L @*/
+{
   lua_State *NL = lua_newthread(L);
   luaL_argcheck(L, lua_isfunction(L, 1) && !lua_iscfunction(L, 1), 1,
     "Lua function expected");
@@ -604,19 +684,25 @@ static int luaB_cocreate (lua_State *L) {
 }
 
 
-static int luaB_cowrap (lua_State *L) {
+static int luaB_cowrap (lua_State *L)
+	/*@modifies L @*/
+{
   luaB_cocreate(L);
   lua_pushcclosure(L, luaB_auxwrap, 1);
   return 1;
 }
 
 
-static int luaB_yield (lua_State *L) {
+static int luaB_yield (lua_State *L)
+	/*@modifies L @*/
+{
   return lua_yield(L, lua_gettop(L));
 }
 
 
-static int luaB_costatus (lua_State *L) {
+static int luaB_costatus (lua_State *L)
+	/*@modifies L @*/
+{
   lua_State *co = lua_tothread(L, 1);
   luaL_argcheck(L, co, 1, "coroutine expected");
   if (L == co) lua_pushliteral(L, "running");
@@ -631,6 +717,8 @@ static int luaB_costatus (lua_State *L) {
 }
 
 
+/*@-readonlytrans@*/
+/*@unchecked@*/
 static const luaL_reg co_funcs[] = {
   {"create", luaB_cocreate},
   {"wrap", luaB_cowrap},
@@ -639,12 +727,15 @@ static const luaL_reg co_funcs[] = {
   {"status", luaB_costatus},
   {NULL, NULL}
 };
+/*@=readonlytrans@*/
 
 /* }====================================================== */
 
 
 
-static void base_open (lua_State *L) {
+static void base_open (lua_State *L)
+	/*@modifies L @*/
+{
   lua_pushliteral(L, "_G");
   lua_pushvalue(L, LUA_GLOBALSINDEX);
   luaL_openlib(L, NULL, base_funcs, 0);  /* open lib into global table */
diff --git a/lua/lib/ldblib.c b/lua/lib/ldblib.c
index ca1ddfcad..3f5a1a3c2 100644
--- a/lua/lib/ldblib.c
+++ b/lua/lib/ldblib.c
@@ -1,5 +1,5 @@
 /*
-** $Id: ldblib.c,v 1.1 2004/03/16 21:58:30 niemeyer Exp $
+** $Id: ldblib.c,v 1.2 2004/03/23 05:09:14 jbj Exp $
 ** Interface from Lua to its debug API
 ** See Copyright Notice in lua.h
 */
@@ -18,21 +18,27 @@
 
 
 
-static void settabss (lua_State *L, const char *i, const char *v) {
+static void settabss (lua_State *L, const char *i, const char *v)
+	/*@modifies L @*/
+{
   lua_pushstring(L, i);
   lua_pushstring(L, v);
   lua_rawset(L, -3);
 }
 
 
-static void settabsi (lua_State *L, const char *i, int v) {
+static void settabsi (lua_State *L, const char *i, int v)
+	/*@modifies L @*/
+{
   lua_pushstring(L, i);
   lua_pushnumber(L, (lua_Number)v);
   lua_rawset(L, -3);
 }
 
 
-static int getinfo (lua_State *L) {
+static int getinfo (lua_State *L)
+	/*@modifies L @*/
+{
   lua_Debug ar;
   const char *options = luaL_optstring(L, 2, "flnSu");
   if (lua_isnumber(L, 1)) {
@@ -80,7 +86,9 @@ static int getinfo (lua_State *L) {
 }
     
 
-static int getlocal (lua_State *L) {
+static int getlocal (lua_State *L)
+	/*@modifies L @*/
+{
   lua_Debug ar;
   const char *name;
   if (!lua_getstack(L, luaL_checkint(L, 1), &ar))  /* level out of range? */
@@ -98,7 +106,9 @@ static int getlocal (lua_State *L) {
 }
 
 
-static int setlocal (lua_State *L) {
+static int setlocal (lua_State *L)
+	/*@modifies L @*/
+{
   lua_Debug ar;
   if (!lua_getstack(L, luaL_checkint(L, 1), &ar))  /* level out of range? */
     return luaL_argerror(L, 1, "level out of range");
@@ -108,7 +118,9 @@ static int setlocal (lua_State *L) {
 }
 
 
-static int auxupvalue (lua_State *L, int get) {
+static int auxupvalue (lua_State *L, int get)
+	/*@modifies L @*/
+{
   const char *name;
   int n = luaL_checkint(L, 2);
   luaL_checktype(L, 1, LUA_TFUNCTION);
@@ -121,22 +133,30 @@ static int auxupvalue (lua_State *L, int get) {
 }
 
 
-static int getupvalue (lua_State *L) {
+static int getupvalue (lua_State *L)
+	/*@modifies L @*/
+{
   return auxupvalue(L, 1);
 }
 
 
-static int setupvalue (lua_State *L) {
+static int setupvalue (lua_State *L)
+	/*@modifies L @*/
+{
   luaL_checkany(L, 3);
   return auxupvalue(L, 0);
 }
 
 
 
+/*@unchecked@*/
 static const char KEY_HOOK = 'h';
 
 
-static void hookf (lua_State *L, lua_Debug *ar) {
+static void hookf (lua_State *L, lua_Debug *ar)
+	/*@modifies L @*/
+{
+  /*@observer@*/
   static const char *const hooknames[] =
     {"call", "return", "line", "count", "tail return"};
   lua_pushlightuserdata(L, (void *)&KEY_HOOK);
@@ -154,7 +174,9 @@ static void hookf (lua_State *L, lua_Debug *ar) {
 }
 
 
-static int makemask (const char *smask, int count) {
+static int makemask (const char *smask, int count)
+	/*@*/
+{
   int mask = 0;
   if (strchr(smask, 'c')) mask |= LUA_MASKCALL;
   if (strchr(smask, 'r')) mask |= LUA_MASKRET;
@@ -164,7 +186,9 @@ static int makemask (const char *smask, int count) {
 }
 
 
-static char *unmakemask (int mask, char *smask) {
+static char *unmakemask (int mask, char *smask)
+	/*@modifies *smask @*/
+{
   int i = 0;
   if (mask & LUA_MASKCALL) smask[i++] = 'c';
   if (mask & LUA_MASKRET) smask[i++] = 'r';
@@ -174,7 +198,9 @@ static char *unmakemask (int mask, char *smask) {
 }
 
 
-static int sethook (lua_State *L) {
+static int sethook (lua_State *L)
+	/*@modifies L @*/
+{
   if (lua_isnoneornil(L, 1)) {
     lua_settop(L, 1);
     lua_sethook(L, NULL, 0, 0);  /* turn off hooks */
@@ -192,7 +218,9 @@ static int sethook (lua_State *L) {
 }
 
 
-static int gethook (lua_State *L) {
+static int gethook (lua_State *L)
+	/*@modifies L @*/
+{
   char buff[5];
   int mask = lua_gethookmask(L);
   lua_Hook hook = lua_gethook(L);
@@ -208,7 +236,10 @@ static int gethook (lua_State *L) {
 }
 
 
-static int debug (lua_State *L) {
+static int debug (lua_State *L)
+	/*@globals fileSystem @*/
+	/*@modifies L, fileSystem @*/
+{
   for (;;) {
     char buffer[250];
     fputs("lua_debug> ", stderr);
@@ -224,7 +255,9 @@ static int debug (lua_State *L) {
 #define LEVELS1	12	/* size of the first part of the stack */
 #define LEVELS2	10	/* size of the second part of the stack */
 
-static int errorfb (lua_State *L) {
+static int errorfb (lua_State *L)
+	/*@modifies L @*/
+{
   int level = 1;  /* skip level 0 (it's this function) */
   int firstpart = 1;  /* still before eventual `...' */
   lua_Debug ar;
@@ -275,6 +308,8 @@ static int errorfb (lua_State *L) {
 }
 
 
+/*@-readonlytrans@*/
+/*@unchecked@*/
 static const luaL_reg dblib[] = {
   {"getlocal", getlocal},
   {"getinfo", getinfo},
@@ -287,6 +322,7 @@ static const luaL_reg dblib[] = {
   {"traceback", errorfb},
   {NULL, NULL}
 };
+/*@=readonlytrans@*/
 
 
 LUALIB_API int luaopen_debug (lua_State *L) {
diff --git a/lua/lib/liolib.c b/lua/lib/liolib.c
index 3e3963644..49cbd5271 100644
--- a/lua/lib/liolib.c
+++ b/lua/lib/liolib.c
@@ -1,5 +1,5 @@
 /*
-** $Id: liolib.c,v 1.2 2004/03/19 21:14:32 niemeyer Exp $
+** $Id: liolib.c,v 1.3 2004/03/23 05:09:14 jbj Exp $
 ** Standard I/O (and system) library
 ** See Copyright Notice in lua.h
 */
@@ -19,6 +19,7 @@
 #include "lauxlib.h"
 #include "lualib.h"
 
+/*@access FILE @*/
 
 
 /*
@@ -69,7 +70,9 @@
 #define IO_OUTPUT		"_output"
 
 
-static int pushresult (lua_State *L, int i, const char *filename) {
+static int pushresult (lua_State *L, int i, const char *filename)
+	/*@modifies L @*/
+{
   if (i) {
     lua_pushboolean(L, 1);
     return 1;
@@ -86,14 +89,18 @@ static int pushresult (lua_State *L, int i, const char *filename) {
 }
 
 
-static FILE **topfile (lua_State *L, int findex) {
+static FILE **topfile (lua_State *L, int findex)
+	/*@modifies L @*/
+{
   FILE **f = (FILE **)luaL_checkudata(L, findex, FILEHANDLE);
   if (f == NULL) luaL_argerror(L, findex, "bad file");
   return f;
 }
 
 
-static int io_type (lua_State *L) {
+static int io_type (lua_State *L)
+	/*@modifies L @*/
+{
   FILE **f = (FILE **)luaL_checkudata(L, 1, FILEHANDLE);
   if (f == NULL) lua_pushnil(L);
   else if (*f == NULL)
@@ -104,7 +111,9 @@ static int io_type (lua_State *L) {
 }
 
 
-static FILE *tofile (lua_State *L, int findex) {
+static FILE *tofile (lua_State *L, int findex)
+	/*@modifies L @*/
+{
   FILE **f = topfile(L, findex);
   if (*f == NULL)
     luaL_error(L, "attempt to use a closed file");
@@ -118,7 +127,9 @@ static FILE *tofile (lua_State *L, int findex) {
 ** before opening the actual file; so, if there is a memory error, the
 ** file is not left opened.
 */
-static FILE **newfile (lua_State *L) {
+static FILE **newfile (lua_State *L)
+	/*@modifies L @*/
+{
   FILE **pf = (FILE **)lua_newuserdata(L, sizeof(FILE *));
   *pf = NULL;  /* file handle is currently `closed' */
   luaL_getmetatable(L, FILEHANDLE);
@@ -132,7 +143,9 @@ static FILE **newfile (lua_State *L) {
 ** the `io' metatable
 */
 static void registerfile (lua_State *L, FILE *f, const char *name,
-                                                 const char *impname) {
+                                                 const char *impname)
+	/*@modifies L @*/
+{
   lua_pushstring(L, name);
   *newfile(L) = f;
   if (impname) {
@@ -144,7 +157,10 @@ static void registerfile (lua_State *L, FILE *f, const char *name,
 }
 
 
-static int aux_close (lua_State *L) {
+static int aux_close (lua_State *L)
+	/*@globals fileSystem @*/
+	/*@modifies L, fileSystem @*/
+{
   FILE *f = tofile(L, 1);
   if (f == stdin || f == stdout || f == stderr)
     return 0;  /* file cannot be closed */
@@ -157,7 +173,10 @@ static int aux_close (lua_State *L) {
 }
 
 
-static int io_close (lua_State *L) {
+static int io_close (lua_State *L)
+	/*@globals fileSystem @*/
+	/*@modifies L, fileSystem @*/
+{
   if (lua_isnone(L, 1) && lua_type(L, lua_upvalueindex(1)) == LUA_TTABLE) {
     lua_pushstring(L, IO_OUTPUT);
     lua_rawget(L, lua_upvalueindex(1));
@@ -166,7 +185,10 @@ static int io_close (lua_State *L) {
 }
 
 
-static int io_gc (lua_State *L) {
+static int io_gc (lua_State *L)
+	/*@globals fileSystem @*/
+	/*@modifies L, fileSystem @*/
+{
   FILE **f = topfile(L, 1);
   if (*f != NULL)  /* ignore closed files */
     aux_close(L);
@@ -174,7 +196,9 @@ static int io_gc (lua_State *L) {
 }
 
 
-static int io_tostring (lua_State *L) {
+static int io_tostring (lua_State *L)
+	/*@modifies L @*/
+{
   char buff[128];
   FILE **f = topfile(L, 1);
   if (*f == NULL)
@@ -186,7 +210,10 @@ static int io_tostring (lua_State *L) {
 }
 
 
-static int io_open (lua_State *L) {
+static int io_open (lua_State *L)
+	/*@globals fileSystem @*/
+	/*@modifies L, fileSystem @*/
+{
   const char *filename = luaL_checkstring(L, 1);
   const char *mode = luaL_optstring(L, 2, "r");
   FILE **pf = newfile(L);
@@ -195,7 +222,10 @@ static int io_open (lua_State *L) {
 }
 
 
-static int io_popen (lua_State *L) {
+static int io_popen (lua_State *L)
+	/*@globals fileSystem @*/
+	/*@modifies L, fileSystem @*/
+{
 #if !USE_POPEN
   luaL_error(L, "`popen' not supported");
   return 0;
@@ -209,21 +239,29 @@ static int io_popen (lua_State *L) {
 }
 
 
-static int io_tmpfile (lua_State *L) {
+static int io_tmpfile (lua_State *L)
+	/*@globals fileSystem @*/
+	/*@modifies L, fileSystem @*/
+{
   FILE **pf = newfile(L);
   *pf = tmpfile();
   return (*pf == NULL) ? pushresult(L, 0, NULL) : 1;
 }
 
 
-static FILE *getiofile (lua_State *L, const char *name) {
+static FILE *getiofile (lua_State *L, const char *name)
+	/*@modifies L @*/
+{
   lua_pushstring(L, name);
   lua_rawget(L, lua_upvalueindex(1));
   return tofile(L, -1);
 }
 
 
-static int g_iofile (lua_State *L, const char *name, const char *mode) {
+static int g_iofile (lua_State *L, const char *name, const char *mode)
+	/*@globals fileSystem @*/
+	/*@modifies L, fileSystem @*/
+{
   if (!lua_isnoneornil(L, 1)) {
     const char *filename = lua_tostring(L, 1);
     lua_pushstring(L, name);
@@ -248,20 +286,30 @@ static int g_iofile (lua_State *L, const char *name, const char *mode) {
 }
 
 
-static int io_input (lua_State *L) {
+static int io_input (lua_State *L)
+	/*@globals fileSystem @*/
+	/*@modifies L, fileSystem @*/
+{
   return g_iofile(L, IO_INPUT, "r");
 }
 
 
-static int io_output (lua_State *L) {
+static int io_output (lua_State *L)
+	/*@globals fileSystem @*/
+	/*@modifies L, fileSystem @*/
+{
   return g_iofile(L, IO_OUTPUT, "w");
 }
 
 
-static int io_readline (lua_State *L);
+static int io_readline (lua_State *L)
+	/*@globals fileSystem @*/
+	/*@modifies L, fileSystem @*/;
 
 
-static void aux_lines (lua_State *L, int idx, int close) {
+static void aux_lines (lua_State *L, int idx, int close)
+	/*@modifies L @*/
+{
   lua_pushliteral(L, FILEHANDLE);
   lua_rawget(L, LUA_REGISTRYINDEX);
   lua_pushvalue(L, idx);
@@ -270,14 +318,19 @@ static void aux_lines (lua_State *L, int idx, int close) {
 }
 
 
-static int f_lines (lua_State *L) {
+static int f_lines (lua_State *L)
+	/*@modifies L @*/
+{
   tofile(L, 1);  /* check that it's a valid file handle */
   aux_lines(L, 1, 0);
   return 1;
 }
 
 
-static int io_lines (lua_State *L) {
+static int io_lines (lua_State *L)
+	/*@globals fileSystem @*/
+	/*@modifies L, fileSystem @*/
+{
   if (lua_isnoneornil(L, 1)) {  /* no arguments? */
     lua_pushstring(L, IO_INPUT);
     lua_rawget(L, lua_upvalueindex(1));  /* will iterate over default input */
@@ -301,7 +354,10 @@ static int io_lines (lua_State *L) {
 */
 
 
-static int read_number (lua_State *L, FILE *f) {
+static int read_number (lua_State *L, FILE *f)
+	/*@globals fileSystem @*/
+	/*@modifies L, f, fileSystem @*/
+{
   lua_Number d;
   if (fscanf(f, LUA_NUMBER_SCAN, &d) == 1) {
     lua_pushnumber(L, d);
@@ -311,7 +367,10 @@ static int read_number (lua_State *L, FILE *f) {
 }
 
 
-static int test_eof (lua_State *L, FILE *f) {
+static int test_eof (lua_State *L, FILE *f)
+	/*@globals fileSystem @*/
+	/*@modifies L, f, fileSystem @*/
+{
   int c = getc(f);
   ungetc(c, f);
   lua_pushlstring(L, NULL, 0);
@@ -319,7 +378,10 @@ static int test_eof (lua_State *L, FILE *f) {
 }
 
 
-static int read_line (lua_State *L, FILE *f) {
+static int read_line (lua_State *L, FILE *f)
+	/*@globals fileSystem @*/
+	/*@modifies L, f, fileSystem @*/
+{
   luaL_Buffer b;
   luaL_buffinit(L, &b);
   for (;;) {
@@ -341,7 +403,10 @@ static int read_line (lua_State *L, FILE *f) {
 }
 
 
-static int read_chars (lua_State *L, FILE *f, size_t n) {
+static int read_chars (lua_State *L, FILE *f, size_t n)
+	/*@globals fileSystem @*/
+	/*@modifies L, f, fileSystem @*/
+{
   size_t rlen;  /* how much to read */
   size_t nr;  /* number of chars actually read */
   luaL_Buffer b;
@@ -359,7 +424,10 @@ static int read_chars (lua_State *L, FILE *f, size_t n) {
 }
 
 
-static int g_read (lua_State *L, FILE *f, int first) {
+static int g_read (lua_State *L, FILE *f, int first)
+	/*@globals fileSystem @*/
+	/*@modifies L, f, fileSystem @*/
+{
   int nargs = lua_gettop(L) - 1;
   int success;
   int n;
@@ -405,17 +473,26 @@ static int g_read (lua_State *L, FILE *f, int first) {
 }
 
 
-static int io_read (lua_State *L) {
+static int io_read (lua_State *L)
+	/*@globals fileSystem @*/
+	/*@modifies L, fileSystem @*/
+{
   return g_read(L, getiofile(L, IO_INPUT), 1);
 }
 
 
-static int f_read (lua_State *L) {
+static int f_read (lua_State *L)
+	/*@globals fileSystem @*/
+	/*@modifies L, fileSystem @*/
+{
   return g_read(L, tofile(L, 1), 2);
 }
 
 
-static int io_readline (lua_State *L) {
+static int io_readline (lua_State *L)
+	/*@globals fileSystem @*/
+	/*@modifies L, fileSystem @*/
+{
   FILE *f = *(FILE **)lua_touserdata(L, lua_upvalueindex(2));
   if (f == NULL)  /* file is already closed? */
     luaL_error(L, "file is already closed");
@@ -433,7 +510,10 @@ static int io_readline (lua_State *L) {
 /* }====================================================== */
 
 
-static int g_write (lua_State *L, FILE *f, int arg) {
+static int g_write (lua_State *L, FILE *f, int arg)
+	/*@globals fileSystem @*/
+	/*@modifies L, f, fileSystem @*/
+{
   int nargs = lua_gettop(L) - 1;
   int status = 1;
   for (; nargs--; arg++) {
@@ -452,19 +532,32 @@ static int g_write (lua_State *L, FILE *f, int arg) {
 }
 
 
-static int io_write (lua_State *L) {
+static int io_write (lua_State *L)
+	/*@globals fileSystem @*/
+	/*@modifies L, fileSystem @*/
+{
   return g_write(L, getiofile(L, IO_OUTPUT), 1);
 }
 
 
-static int f_write (lua_State *L) {
+static int f_write (lua_State *L)
+	/*@globals fileSystem @*/
+	/*@modifies L, fileSystem @*/
+{
   return g_write(L, tofile(L, 1), 2);
 }
 
 
-static int f_seek (lua_State *L) {
+static int f_seek (lua_State *L)
+	/*@globals fileSystem @*/
+	/*@modifies L, fileSystem @*/
+{
+  /*@observer@*/
   static const int mode[] = {SEEK_SET, SEEK_CUR, SEEK_END};
+/*@-nullassign@*/
+  /*@observer@*/
   static const char *const modenames[] = {"set", "cur", "end", NULL};
+/*@=nullassign@*/
   FILE *f = tofile(L, 1);
   int op = luaL_findstring(luaL_optstring(L, 2, "cur"), modenames);
   long offset = luaL_optlong(L, 3, 0);
@@ -479,16 +572,24 @@ static int f_seek (lua_State *L) {
 }
 
 
-static int io_flush (lua_State *L) {
+static int io_flush (lua_State *L)
+	/*@globals fileSystem @*/
+	/*@modifies L, fileSystem @*/
+{
   return pushresult(L, fflush(getiofile(L, IO_OUTPUT)) == 0, NULL);
 }
 
 
-static int f_flush (lua_State *L) {
+static int f_flush (lua_State *L)
+	/*@globals fileSystem @*/
+	/*@modifies L, fileSystem @*/
+{
   return pushresult(L, fflush(tofile(L, 1)) == 0, NULL);
 }
 
 
+/*@-readonlytrans@*/
+/*@unchecked@*/
 static const luaL_reg iolib[] = {
   {"input", io_input},
   {"output", io_output},
@@ -505,6 +606,7 @@ static const luaL_reg iolib[] = {
 };
 
 
+/*@unchecked@*/
 static const luaL_reg flib[] = {
   {"flush", f_flush},
   {"read", f_read},
@@ -516,9 +618,12 @@ static const luaL_reg flib[] = {
   {"__tostring", io_tostring},
   {NULL, NULL}
 };
+/*@=readonlytrans@*/
 
 
-static void createmeta (lua_State *L) {
+static void createmeta (lua_State *L)
+	/*@modifies L @*/
+{
   luaL_newmetatable(L, FILEHANDLE);  /* create new metatable for file handles */
   /* file methods */
   lua_pushliteral(L, "__index");
@@ -536,26 +641,38 @@ static void createmeta (lua_State *L) {
 ** =======================================================
 */
 
-static int io_execute (lua_State *L) {
+static int io_execute (lua_State *L)
+	/*@globals fileSystem @*/
+	/*@modifies L, fileSystem @*/
+{
   lua_pushnumber(L, system(luaL_checkstring(L, 1)));
   return 1;
 }
 
 
-static int io_remove (lua_State *L) {
+static int io_remove (lua_State *L)
+	/*@globals fileSystem @*/
+	/*@modifies L, fileSystem @*/
+{
   const char *filename = luaL_checkstring(L, 1);
   return pushresult(L, remove(filename) == 0, filename);
 }
 
 
-static int io_rename (lua_State *L) {
+static int io_rename (lua_State *L)
+	/*@globals fileSystem @*/
+	/*@modifies L, fileSystem @*/
+{
   const char *fromname = luaL_checkstring(L, 1);
   const char *toname = luaL_checkstring(L, 2);
   return pushresult(L, rename(fromname, toname) == 0, fromname);
 }
 
 
-static int io_tmpname (lua_State *L) {
+static int io_tmpname (lua_State *L)
+	/*@globals internalState @*/
+	/*@modifies L, internalState @*/
+{
 #if !USE_TMPNAME
   luaL_error(L, "`tmpname' not supported");
   return 0;
@@ -569,13 +686,18 @@ static int io_tmpname (lua_State *L) {
 }
 
 
-static int io_getenv (lua_State *L) {
+static int io_getenv (lua_State *L)
+	/*@modifies L @*/
+{
   lua_pushstring(L, getenv(luaL_checkstring(L, 1)));  /* if NULL push nil */
   return 1;
 }
 
 
-static int io_clock (lua_State *L) {
+static int io_clock (lua_State *L)
+	/*@globals internalState @*/
+	/*@modifies L, internalState @*/
+{
   lua_pushnumber(L, ((lua_Number)clock())/(lua_Number)CLOCKS_PER_SEC);
   return 1;
 }
@@ -589,19 +711,25 @@ static int io_clock (lua_State *L) {
 ** =======================================================
 */
 
-static void setfield (lua_State *L, const char *key, int value) {
+static void setfield (lua_State *L, const char *key, int value)
+	/*@modifies L @*/
+{
   lua_pushstring(L, key);
   lua_pushnumber(L, value);
   lua_rawset(L, -3);
 }
 
-static void setboolfield (lua_State *L, const char *key, int value) {
+static void setboolfield (lua_State *L, const char *key, int value)
+	/*@modifies L @*/
+{
   lua_pushstring(L, key);
   lua_pushboolean(L, value);
   lua_rawset(L, -3);
 }
 
-static int getboolfield (lua_State *L, const char *key) {
+static int getboolfield (lua_State *L, const char *key)
+	/*@modifies L @*/
+{
   int res;
   lua_pushstring(L, key);
   lua_gettable(L, -2);
@@ -611,7 +739,9 @@ static int getboolfield (lua_State *L, const char *key) {
 }
 
 
-static int getfield (lua_State *L, const char *key, int d) {
+static int getfield (lua_State *L, const char *key, int d)
+	/*@modifies L @*/
+{
   int res;
   lua_pushstring(L, key);
   lua_gettable(L, -2);
@@ -627,7 +757,9 @@ static int getfield (lua_State *L, const char *key, int d) {
 }
 
 
-static int io_date (lua_State *L) {
+static int io_date (lua_State *L)
+	/*@modifies L @*/
+{
   const char *s = luaL_optstring(L, 1, "%c");
   time_t t = (time_t)(luaL_optnumber(L, 2, -1));
   struct tm *stm;
@@ -664,7 +796,9 @@ static int io_date (lua_State *L) {
 }
 
 
-static int io_time (lua_State *L) {
+static int io_time (lua_State *L)
+	/*@modifies L @*/
+{
   if (lua_isnoneornil(L, 1))  /* called without args? */
     lua_pushnumber(L, time(NULL));  /* return current time */
   else {
@@ -689,7 +823,9 @@ static int io_time (lua_State *L) {
 }
 
 
-static int io_difftime (lua_State *L) {
+static int io_difftime (lua_State *L)
+	/*@modifies L @*/
+{
   lua_pushnumber(L, difftime((time_t)(luaL_checknumber(L, 1)),
                              (time_t)(luaL_optnumber(L, 2, 0))));
   return 1;
@@ -698,9 +834,14 @@ static int io_difftime (lua_State *L) {
 /* }====================================================== */
 
 
-static int io_setloc (lua_State *L) {
+static int io_setloc (lua_State *L)
+	/*@globals internalState @*/
+	/*@modifies L, internalState @*/
+{
+  /*@observer@*/
   static const int cat[] = {LC_ALL, LC_COLLATE, LC_CTYPE, LC_MONETARY,
                       LC_NUMERIC, LC_TIME};
+  /*@observer@*/
   static const char *const catnames[] = {"all", "collate", "ctype", "monetary",
      "numeric", "time", NULL};
   const char *l = lua_tostring(L, 1);
@@ -712,11 +853,17 @@ static int io_setloc (lua_State *L) {
 }
 
 
-static int io_exit (lua_State *L) {
+/*@exits@*/
+static int io_exit (lua_State *L)
+	/*@modifies L @*/
+{
   exit(luaL_optint(L, 1, EXIT_SUCCESS));
+  /*@notreached@*/
   return 0;  /* to avoid warnings */
 }
 
+/*@-readonlytrans@*/
+/*@unchecked@*/
 static const luaL_reg syslib[] = {
   {"clock",     io_clock},
   {"date",      io_date},
@@ -731,6 +878,7 @@ static const luaL_reg syslib[] = {
   {"tmpname",   io_tmpname},
   {NULL, NULL}
 };
+/*@=readonlytrans@*/
 
 /* }====================================================== */
 
diff --git a/lua/lib/lmathlib.c b/lua/lib/lmathlib.c
index c5a6b14ee..3a05f6da0 100644
--- a/lua/lib/lmathlib.c
+++ b/lua/lib/lmathlib.c
@@ -1,5 +1,5 @@
 /*
-** $Id: lmathlib.c,v 1.1 2004/03/16 21:58:30 niemeyer Exp $
+** $Id: lmathlib.c,v 1.2 2004/03/23 05:09:14 jbj Exp $
 ** Standard mathematical library
 ** See Copyright Notice in lua.h
 */
@@ -35,111 +35,153 @@
 #endif
 
 
-static int math_abs (lua_State *L) {
+static int math_abs (lua_State *L)
+	/*@modifies L @*/
+{
   lua_pushnumber(L, fabs(luaL_checknumber(L, 1)));
   return 1;
 }
 
-static int math_sin (lua_State *L) {
+static int math_sin (lua_State *L)
+	/*@modifies L @*/
+{
   lua_pushnumber(L, sin(TORAD(luaL_checknumber(L, 1))));
   return 1;
 }
 
-static int math_cos (lua_State *L) {
+static int math_cos (lua_State *L)
+	/*@modifies L @*/
+{
   lua_pushnumber(L, cos(TORAD(luaL_checknumber(L, 1))));
   return 1;
 }
 
-static int math_tan (lua_State *L) {
+static int math_tan (lua_State *L)
+	/*@modifies L @*/
+{
   lua_pushnumber(L, tan(TORAD(luaL_checknumber(L, 1))));
   return 1;
 }
 
-static int math_asin (lua_State *L) {
+static int math_asin (lua_State *L)
+	/*@modifies L @*/
+{
   lua_pushnumber(L, FROMRAD(asin(luaL_checknumber(L, 1))));
   return 1;
 }
 
-static int math_acos (lua_State *L) {
+static int math_acos (lua_State *L)
+	/*@modifies L @*/
+{
   lua_pushnumber(L, FROMRAD(acos(luaL_checknumber(L, 1))));
   return 1;
 }
 
-static int math_atan (lua_State *L) {
+static int math_atan (lua_State *L)
+	/*@modifies L @*/
+{
   lua_pushnumber(L, FROMRAD(atan(luaL_checknumber(L, 1))));
   return 1;
 }
 
-static int math_atan2 (lua_State *L) {
+static int math_atan2 (lua_State *L)
+	/*@modifies L @*/
+{
   lua_pushnumber(L, FROMRAD(atan2(luaL_checknumber(L, 1), luaL_checknumber(L, 2))));
   return 1;
 }
 
-static int math_ceil (lua_State *L) {
+static int math_ceil (lua_State *L)
+	/*@modifies L @*/
+{
   lua_pushnumber(L, ceil(luaL_checknumber(L, 1)));
   return 1;
 }
 
-static int math_floor (lua_State *L) {
+static int math_floor (lua_State *L)
+	/*@modifies L @*/
+{
   lua_pushnumber(L, floor(luaL_checknumber(L, 1)));
   return 1;
 }
 
-static int math_mod (lua_State *L) {
+static int math_mod (lua_State *L)
+	/*@modifies L @*/
+{
   lua_pushnumber(L, fmod(luaL_checknumber(L, 1), luaL_checknumber(L, 2)));
   return 1;
 }
 
-static int math_sqrt (lua_State *L) {
+static int math_sqrt (lua_State *L)
+	/*@modifies L @*/
+{
   lua_pushnumber(L, sqrt(luaL_checknumber(L, 1)));
   return 1;
 }
 
-static int math_pow (lua_State *L) {
+static int math_pow (lua_State *L)
+	/*@modifies L @*/
+{
   lua_pushnumber(L, pow(luaL_checknumber(L, 1), luaL_checknumber(L, 2)));
   return 1;
 }
 
-static int math_log (lua_State *L) {
+static int math_log (lua_State *L)
+	/*@modifies L @*/
+{
   lua_pushnumber(L, log(luaL_checknumber(L, 1)));
   return 1;
 }
 
-static int math_log10 (lua_State *L) {
+static int math_log10 (lua_State *L)
+	/*@modifies L @*/
+{
   lua_pushnumber(L, log10(luaL_checknumber(L, 1)));
   return 1;
 }
 
-static int math_exp (lua_State *L) {
+static int math_exp (lua_State *L)
+	/*@modifies L @*/
+{
   lua_pushnumber(L, exp(luaL_checknumber(L, 1)));
   return 1;
 }
 
-static int math_deg (lua_State *L) {
+static int math_deg (lua_State *L)
+	/*@modifies L @*/
+{
   lua_pushnumber(L, luaL_checknumber(L, 1)/RADIANS_PER_DEGREE);
   return 1;
 }
 
-static int math_rad (lua_State *L) {
+static int math_rad (lua_State *L)
+	/*@modifies L @*/
+{
   lua_pushnumber(L, luaL_checknumber(L, 1)*RADIANS_PER_DEGREE);
   return 1;
 }
 
-static int math_frexp (lua_State *L) {
+static int math_frexp (lua_State *L)
+	/*@modifies L @*/
+{
   int e;
   lua_pushnumber(L, frexp(luaL_checknumber(L, 1), &e));
   lua_pushnumber(L, e);
   return 2;
 }
 
-static int math_ldexp (lua_State *L) {
+static int math_ldexp (lua_State *L)
+	/*@modifies L @*/
+{
   lua_pushnumber(L, ldexp(luaL_checknumber(L, 1), luaL_checkint(L, 2)));
   return 1;
 }
 
 
 
-static int math_min (lua_State *L) {
+static int math_min (lua_State *L)
+	/*@modifies L @*/
+{
   int n = lua_gettop(L);  /* number of arguments */
   lua_Number dmin = luaL_checknumber(L, 1);
   int i;
@@ -153,7 +195,9 @@ static int math_min (lua_State *L) {
 }
 
 
-static int math_max (lua_State *L) {
+static int math_max (lua_State *L)
+	/*@modifies L @*/
+{
   int n = lua_gettop(L);  /* number of arguments */
   lua_Number dmax = luaL_checknumber(L, 1);
   int i;
@@ -167,7 +211,10 @@ static int math_max (lua_State *L) {
 }
 
 
-static int math_random (lua_State *L) {
+static int math_random (lua_State *L)
+	/*@globals internalState @*/
+	/*@modifies L, internalState @*/
+{
   /* the `%' avoids the (rare) case of r==1, and is needed also because on
      some systems (SunOS!) `rand()' may return a value larger than RAND_MAX */
   lua_Number r = (lua_Number)(rand()%RAND_MAX) / (lua_Number)RAND_MAX;
@@ -195,12 +242,17 @@ static int math_random (lua_State *L) {
 }
 
 
-static int math_randomseed (lua_State *L) {
+static int math_randomseed (lua_State *L)
+	/*@globals internalState @*/
+	/*@modifies L, internalState @*/
+{
   srand(luaL_checkint(L, 1));
   return 0;
 }
 
 
+/*@-readonlytrans@*/
+/*@unchecked@*/
 static const luaL_reg mathlib[] = {
   {"abs",   math_abs},
   {"sin",   math_sin},
@@ -228,6 +280,7 @@ static const luaL_reg mathlib[] = {
   {"randomseed", math_randomseed},
   {NULL, NULL}
 };
+/*@=readonlytrans@*/
 
 
 /*
diff --git a/lua/lib/loadlib.c b/lua/lib/loadlib.c
index 267cbecad..15d82669a 100644
--- a/lua/lib/loadlib.c
+++ b/lua/lib/loadlib.c
@@ -1,5 +1,5 @@
 /*
-** $Id: loadlib.c,v 1.1 2004/03/16 21:58:30 niemeyer Exp $
+** $Id: loadlib.c,v 1.2 2004/03/23 05:09:14 jbj Exp $
 ** Dynamic library loader for Lua
 ** See Copyright Notice in lua.h
 *
@@ -46,6 +46,7 @@
 #include <dlfcn.h>
 
 static int loadlib(lua_State *L)
+	/*@modifies L @*/
 {
  const char *path=luaL_checkstring(L,1);
  const char *init=luaL_checkstring(L,2);
@@ -93,6 +94,7 @@ static int loadlib(lua_State *L)
 #include <windows.h>
 
 static void pusherror(lua_State *L)
+	/*@modifies L @*/
 {
  int error=GetLastError();
  char buffer[128];
@@ -104,6 +106,7 @@ static void pusherror(lua_State *L)
 }
 
 static int loadlib(lua_State *L)
+	/*@modifies L @*/
 {
  const char *path=luaL_checkstring(L,1);
  const char *init=luaL_checkstring(L,2);
@@ -164,6 +167,7 @@ static int loadlib(lua_State *L)
 #endif
 
 static int loadlib(lua_State *L)
+	/*@modifies L @*/
 {
  lua_pushnil(L);
  lua_pushliteral(L,LOADLIB);
diff --git a/lua/lib/ltablib.c b/lua/lib/ltablib.c
index 1ea1d6943..6e1713155 100644
--- a/lua/lib/ltablib.c
+++ b/lua/lib/ltablib.c
@@ -1,5 +1,5 @@
 /*
-** $Id: ltablib.c,v 1.1 2004/03/16 21:58:30 niemeyer Exp $
+** $Id: ltablib.c,v 1.2 2004/03/23 05:09:14 jbj Exp $
 ** Library for Table Manipulation
 ** See Copyright Notice in lua.h
 */
@@ -18,7 +18,9 @@
 #define aux_getn(L,n)	(luaL_checktype(L, n, LUA_TTABLE), luaL_getn(L, n))
 
 
-static int luaB_foreachi (lua_State *L) {
+static int luaB_foreachi (lua_State *L)
+	/*@modifies L @*/
+{
   int i;
   int n = aux_getn(L, 1);
   luaL_checktype(L, 2, LUA_TFUNCTION);
@@ -35,7 +37,9 @@ static int luaB_foreachi (lua_State *L) {
 }
 
 
-static int luaB_foreach (lua_State *L) {
+static int luaB_foreach (lua_State *L)
+	/*@modifies L @*/
+{
   luaL_checktype(L, 1, LUA_TTABLE);
   luaL_checktype(L, 2, LUA_TFUNCTION);
   lua_pushnil(L);  /* first key */
@@ -53,20 +57,26 @@ static int luaB_foreach (lua_State *L) {
 }
 
 
-static int luaB_getn (lua_State *L) {
+static int luaB_getn (lua_State *L)
+	/*@modifies L @*/
+{
   lua_pushnumber(L, (lua_Number)aux_getn(L, 1));
   return 1;
 }
 
 
-static int luaB_setn (lua_State *L) {
+static int luaB_setn (lua_State *L)
+	/*@modifies L @*/
+{
   luaL_checktype(L, 1, LUA_TTABLE);
   luaL_setn(L, 1, luaL_checkint(L, 2));
   return 0;
 }
 
 
-static int luaB_tinsert (lua_State *L) {
+static int luaB_tinsert (lua_State *L)
+	/*@modifies L @*/
+{
   int v = lua_gettop(L);  /* number of arguments */
   int n = aux_getn(L, 1) + 1;
   int pos;  /* where to insert new element */
@@ -88,7 +98,9 @@ static int luaB_tinsert (lua_State *L) {
 }
 
 
-static int luaB_tremove (lua_State *L) {
+static int luaB_tremove (lua_State *L)
+	/*@modifies L @*/
+{
   int n = aux_getn(L, 1);
   int pos = luaL_optint(L, 2, n);
   if (n <= 0) return 0;  /* table is `empty' */
@@ -104,7 +116,9 @@ static int luaB_tremove (lua_State *L) {
 }
 
 
-static int str_concat (lua_State *L) {
+static int str_concat (lua_State *L)
+	/*@modifies L @*/
+{
   luaL_Buffer b;
   size_t lsep;
   const char *sep = luaL_optlstring(L, 2, "", &lsep);
@@ -134,12 +148,16 @@ static int str_concat (lua_State *L) {
 */
 
 
-static void set2 (lua_State *L, int i, int j) {
+static void set2 (lua_State *L, int i, int j)
+	/*@modifies L @*/
+{
   lua_rawseti(L, 1, i);
   lua_rawseti(L, 1, j);
 }
 
-static int sort_comp (lua_State *L, int a, int b) {
+static int sort_comp (lua_State *L, int a, int b)
+	/*@modifies L @*/
+{
   if (!lua_isnil(L, 2)) {  /* function? */
     int res;
     lua_pushvalue(L, 2);
@@ -154,7 +172,9 @@ static int sort_comp (lua_State *L, int a, int b) {
     return lua_lessthan(L, a, b);
 }
 
-static void auxsort (lua_State *L, int l, int u) {
+static void auxsort (lua_State *L, int l, int u)
+	/*@modifies L @*/
+{
   while (l < u) {  /* for tail recursion */
     int i, j;
     /* sort elements a[l], a[(l+u)/2] and a[u] */
@@ -217,7 +237,9 @@ static void auxsort (lua_State *L, int l, int u) {
   }  /* repeat the routine for the larger one */
 }
 
-static int luaB_sort (lua_State *L) {
+static int luaB_sort (lua_State *L)
+	/*@modifies L @*/
+{
   int n = aux_getn(L, 1);
   luaL_checkstack(L, 40, "");  /* assume array is smaller than 2^40 */
   if (!lua_isnoneornil(L, 2))  /* is there a 2nd argument? */
@@ -230,6 +252,8 @@ static int luaB_sort (lua_State *L) {
 /* }====================================================== */
 
 
+/*@-readonlytrans@*/
+/*@unchecked@*/
 static const luaL_reg tab_funcs[] = {
   {"concat", str_concat},
   {"foreach", luaB_foreach},
@@ -241,6 +265,7 @@ static const luaL_reg tab_funcs[] = {
   {"remove", luaB_tremove},
   {NULL, NULL}
 };
+/*@=readonlytrans@*/
 
 
 LUALIB_API int luaopen_table (lua_State *L) {
diff --git a/lua/llex.c b/lua/llex.c
index 87ca2aed0..5a69c6665 100644
--- a/lua/llex.c
+++ b/lua/llex.c
@@ -1,5 +1,5 @@
 /*
-** $Id: llex.c,v 1.1 2004/03/16 21:58:30 niemeyer Exp $
+** $Id: llex.c,v 1.2 2004/03/23 05:09:14 jbj Exp $
 ** Lexical Analyzer
 ** See Copyright Notice in lua.h
 */
@@ -27,6 +27,7 @@
 
 
 /* ORDER RESERVED */
+/*@observer@*/ /*@unchecked@*/
 static const char *const token2string [] = {
     "and", "break", "do", "else", "elseif",
     "end", "false", "for", "function", "if",
@@ -68,7 +69,9 @@ void luaX_errorline (LexState *ls, const char *s, const char *token, int line) {
 }
 
 
-static void luaX_error (LexState *ls, const char *s, const char *token) {
+static void luaX_error (LexState *ls, const char *s, const char *token)
+	/*@modifies ls @*/
+{
   luaX_errorline(ls, s, token, ls->linenumber);
 }
 
@@ -101,7 +104,9 @@ const char *luaX_token2str (LexState *ls, int token) {
 }
 
 
-static void luaX_lexerror (LexState *ls, const char *s, int token) {
+static void luaX_lexerror (LexState *ls, const char *s, int token)
+	/*@modifies ls @*/
+{
   if (token == TK_EOS)
     luaX_error(ls, s, luaX_token2str(ls, token));
   else
@@ -109,7 +114,9 @@ static void luaX_lexerror (LexState *ls, const char *s, int token) {
 }
 
 
-static void inclinenumber (LexState *LS) {
+static void inclinenumber (LexState *LS)
+	/*@modifies LS @*/
+{
   next(LS);  /* skip `\n' */
   ++LS->linenumber;
   luaX_checklimit(LS, LS->linenumber, MAX_INT, "lines in a chunk");
@@ -158,7 +165,9 @@ void luaX_setinput (lua_State *L, LexState *LS, ZIO *z, TString *source) {
 #define save_and_next(LS, l)  (save(LS, LS->current, l), next(LS))
 
 
-static size_t readname (LexState *LS) {
+static size_t readname (LexState *LS)
+	/*@modifies LS @*/
+{
   size_t l = 0;
   checkbuffer(LS, l);
   do {
@@ -171,7 +180,9 @@ static size_t readname (LexState *LS) {
 
 
 /* LUA_NUMBER */
-static void read_numeral (LexState *LS, int comma, SemInfo *seminfo) {
+static void read_numeral (LexState *LS, int comma, SemInfo *seminfo)
+	/*@modifies LS, seminfo @*/
+{
   size_t l = 0;
   checkbuffer(LS, l);
   if (comma) save(LS, '.', l);
@@ -208,7 +219,9 @@ static void read_numeral (LexState *LS, int comma, SemInfo *seminfo) {
 }
 
 
-static void read_long_string (LexState *LS, SemInfo *seminfo) {
+static void read_long_string (LexState *LS, /*@null@*/ SemInfo *seminfo)
+	/*@modifies LS, seminfo @*/
+{
   int cont = 0;
   size_t l = 0;
   checkbuffer(LS, l);
@@ -255,7 +268,9 @@ static void read_long_string (LexState *LS, SemInfo *seminfo) {
 }
 
 
-static void read_string (LexState *LS, int del, SemInfo *seminfo) {
+static void read_string (LexState *LS, int del, SemInfo *seminfo)
+	/*@modifies LS, seminfo @*/
+{
   size_t l = 0;
   checkbuffer(LS, l);
   save_and_next(LS, l);
diff --git a/lua/llex.h b/lua/llex.h
index 37a6bc588..68d615aed 100644
--- a/lua/llex.h
+++ b/lua/llex.h
@@ -1,5 +1,5 @@
 /*
-** $Id: llex.h,v 1.1 2004/03/16 21:58:30 niemeyer Exp $
+** $Id: llex.h,v 1.2 2004/03/23 05:09:14 jbj Exp $
 ** Lexical Analyzer
 ** See Copyright Notice in lua.h
 */
@@ -38,6 +38,7 @@ enum RESERVED {
 
 typedef union {
   lua_Number r;
+/*@null@*/
   TString *ts;
 } SemInfo;  /* semantics information */
 
@@ -63,13 +64,21 @@ typedef struct LexState {
 } LexState;
 
 
-void luaX_init (lua_State *L);
-void luaX_setinput (lua_State *L, LexState *LS, ZIO *z, TString *source);
-int luaX_lex (LexState *LS, SemInfo *seminfo);
-void luaX_checklimit (LexState *ls, int val, int limit, const char *msg);
-void luaX_syntaxerror (LexState *ls, const char *s);
-void luaX_errorline (LexState *ls, const char *s, const char *token, int line);
-const char *luaX_token2str (LexState *ls, int token);
+void luaX_init (lua_State *L)
+	/*@modifies L @*/;
+void luaX_setinput (lua_State *L, LexState *LS, ZIO *z, TString *source)
+	/*@modifies LS, z @*/;
+int luaX_lex (LexState *LS, SemInfo *seminfo)
+	/*@modifies LS, seminfo @*/;
+void luaX_checklimit (LexState *ls, int val, int limit, const char *msg)
+	/*@modifies ls @*/;
+void luaX_syntaxerror (LexState *ls, const char *s)
+	/*@modifies ls @*/;
+void luaX_errorline (LexState *ls, const char *s, const char *token, int line)
+	/*@modifies ls @*/;
+/*@observer@*/
+const char *luaX_token2str (LexState *ls, int token)
+	/*@modifies ls @*/;
 
 
 #endif
diff --git a/lua/lmem.h b/lua/lmem.h
index 101e61a05..0388185d7 100644
--- a/lua/lmem.h
+++ b/lua/lmem.h
@@ -1,5 +1,5 @@
 /*
-** $Id: lmem.h,v 1.1 2004/03/16 21:58:30 niemeyer Exp $
+** $Id: lmem.h,v 1.2 2004/03/23 05:09:14 jbj Exp $
 ** Interface to Memory Manager
 ** See Copyright Notice in lua.h
 */
@@ -16,10 +16,14 @@
 #define MEMERRMSG	"not enough memory"
 
 
-void *luaM_realloc (lua_State *L, void *oldblock, lu_mem oldsize, lu_mem size);
+/*@null@*/
+void *luaM_realloc (/*@null@*/ lua_State *L, /*@null@*/ void *oldblock, lu_mem oldsize, lu_mem size)
+	/*@modifies L, oldblock @*/;
 
+/*@null@*/
 void *luaM_growaux (lua_State *L, void *block, int *size, int size_elem,
-                    int limit, const char *errormsg);
+                    int limit, const char *errormsg)
+	/*@modifies L, block, *size @*/;
 
 #define luaM_free(L, b, s)	luaM_realloc(L, (b), (s), 0)
 #define luaM_freelem(L, b)	luaM_realloc(L, (b), sizeof(*(b)), 0)
diff --git a/lua/lobject.c b/lua/lobject.c
index dabc6db91..dd088de71 100644
--- a/lua/lobject.c
+++ b/lua/lobject.c
@@ -1,5 +1,5 @@
 /*
-** $Id: lobject.c,v 1.1 2004/03/16 21:58:30 niemeyer Exp $
+** $Id: lobject.c,v 1.2 2004/03/23 05:09:14 jbj Exp $
 ** Some generic functions over Lua objects
 ** See Copyright Notice in lua.h
 */
@@ -101,7 +101,9 @@ int luaO_str2d (const char *s, lua_Number *result) {
 
 
 
-static void pushstr (lua_State *L, const char *str) {
+static void pushstr (lua_State *L, const char *str)
+	/*@modifies L @*/
+{
   setsvalue2s(L->top, luaS_new(L, str));
   incr_top(L);
 }
diff --git a/lua/lobject.h b/lua/lobject.h
index c0792e508..72eaf6df6 100644
--- a/lua/lobject.h
+++ b/lua/lobject.h
@@ -1,5 +1,5 @@
 /*
-** $Id: lobject.h,v 1.1 2004/03/16 21:58:30 niemeyer Exp $
+** $Id: lobject.h,v 1.2 2004/03/23 05:09:14 jbj Exp $
 ** Type definitions for Lua objects
 ** See Copyright Notice in lua.h
 */
@@ -33,7 +33,7 @@ typedef union GCObject GCObject;
 ** Common Header for all collectable objects (in macro form, to be
 ** included in other objects)
 */
-#define CommonHeader	GCObject *next; lu_byte tt; lu_byte marked
+#define CommonHeader	/*@dependent@*/ /*@null@*/ GCObject *next; lu_byte tt; lu_byte marked
 
 
 /*
@@ -50,6 +50,7 @@ typedef struct GCheader {
 ** Union of all Lua values
 */
 typedef union {
+/*@relnull@*/
   GCObject *gc;
   void *p;
   lua_Number n;
@@ -209,12 +210,19 @@ typedef union Udata {
 */
 typedef struct Proto {
   CommonHeader;
+/*@relnull@*/
   TObject *k;  /* constants used by the function */
+/*@relnull@*/
   Instruction *code;
+/*@relnull@*/
   struct Proto **p;  /* functions defined inside the function */
+/*@relnull@*/
   int *lineinfo;  /* map from opcodes to source lines */
+/*@relnull@*/
   struct LocVar *locvars;  /* information about local variables */
+/*@relnull@*/
   TString **upvalues;  /* upvalue names */
+/*@relnull@*/
   TString  *source;
   int sizeupvalues;
   int sizek;  /* size of `k' */
@@ -223,6 +231,7 @@ typedef struct Proto {
   int sizep;  /* size of `p' */
   int sizelocvars;
   int lineDefined;
+/*@relnull@*/
   GCObject *gclist;
   lu_byte nups;  /* number of upvalues */
   lu_byte numparams;
@@ -232,6 +241,7 @@ typedef struct Proto {
 
 
 typedef struct LocVar {
+/*@relnull@*/
   TString *varname;
   int startpc;  /* first point where variable is active */
   int endpc;    /* first point where variable is dead */
@@ -245,6 +255,7 @@ typedef struct LocVar {
 
 typedef struct UpVal {
   CommonHeader;
+/*@null@*/
   TObject *v;  /* points to stack or to its own value */
   TObject value;  /* the value (when closed) */
 } UpVal;
@@ -255,7 +266,7 @@ typedef struct UpVal {
 */
 
 #define ClosureHeader \
-	CommonHeader; lu_byte isC; lu_byte nupvalues; GCObject *gclist
+	CommonHeader; lu_byte isC; lu_byte nupvalues; /*@null@*/ GCObject *gclist
 
 typedef struct CClosure {
   ClosureHeader;
@@ -298,7 +309,9 @@ typedef struct Table {
   lu_byte flags;  /* 1<<p means tagmethod(p) is not present */ 
   lu_byte lsizenode;  /* log2 of size of `node' array */
   struct Table *metatable;
+/*@null@*/
   TObject *array;  /* array part */
+/*@owned@*/ /*@null@*/
   Node *node;
   Node *firstfree;  /* this position is free; all positions after it are full */
   GCObject *gclist;
@@ -319,18 +332,28 @@ typedef struct Table {
 
 
 
+/*@unchecked@*/
 extern const TObject luaO_nilobject;
 
-int luaO_log2 (unsigned int x);
-int luaO_int2fb (unsigned int x);
+int luaO_log2 (unsigned int x)
+	/*@*/;
+int luaO_int2fb (unsigned int x)
+	/*@*/;
 #define fb2int(x)	(((x) & 7) << ((x) >> 3))
 
-int luaO_rawequalObj (const TObject *t1, const TObject *t2);
-int luaO_str2d (const char *s, lua_Number *result);
-
-const char *luaO_pushvfstring (lua_State *L, const char *fmt, va_list argp);
-const char *luaO_pushfstring (lua_State *L, const char *fmt, ...);
-void luaO_chunkid (char *out, const char *source, int len);
+int luaO_rawequalObj (const TObject *t1, const TObject *t2)
+	/*@*/;
+int luaO_str2d (const char *s, lua_Number *result)
+	/*@modifies *result @*/;
+
+/*@observer@*/
+const char *luaO_pushvfstring (lua_State *L, const char *fmt, va_list argp)
+	/*@modifies L @*/;
+/*@observer@*/
+const char *luaO_pushfstring (lua_State *L, const char *fmt, ...)
+	/*@modifies L @*/;
+void luaO_chunkid (char *out, const char *source, int len)
+	/*@modifies *out @*/;
 
 
 #endif
diff --git a/lua/local/lposix.c b/lua/local/lposix.c
index a54d20559..64b0301a3 100644
--- a/lua/local/lposix.c
+++ b/lua/local/lposix.c
@@ -29,13 +29,17 @@
 #include "lua.h"
 #include "lauxlib.h"
 
+/*@access DIR @*/
+
 #ifndef MYBUFSIZ
 #define MYBUFSIZ 512
 #endif
 
 #include "modemuncher.c"
 
+/*@observer@*/
 static const char *filetype(mode_t m)
+	/*@*/
 {
 	if (S_ISREG(m))		return "regular";
 	else if (S_ISLNK(m))	return "link";
@@ -50,6 +54,7 @@ static const char *filetype(mode_t m)
 typedef int (*Selector)(lua_State *L, int i, const void *data);
 
 static int doselection(lua_State *L, int i, const char *const S[], Selector F, const void *data)
+	/*@modifies L @*/
 {
 	if (lua_isnone(L, i))
 	{
@@ -71,12 +76,14 @@ static int doselection(lua_State *L, int i, const char *const S[], Selector F, c
 }
 
 static void storeindex(lua_State *L, int i, const char *value)
+	/*@modifies L @*/
 {
 	lua_pushstring(L, value);
 	lua_rawseti(L, -2, i);
 }
 
 static void storestring(lua_State *L, const char *name, const char *value)
+	/*@modifies L @*/
 {
 	lua_pushstring(L, name);
 	lua_pushstring(L, value);
@@ -84,6 +91,7 @@ static void storestring(lua_State *L, const char *name, const char *value)
 }
 
 static void storenumber(lua_State *L, const char *name, lua_Number value)
+	/*@modifies L @*/
 {
 	lua_pushstring(L, name);
 	lua_pushnumber(L, value);
@@ -91,6 +99,7 @@ static void storenumber(lua_State *L, const char *name, lua_Number value)
 }
 
 static int pusherror(lua_State *L, const char *info)
+	/*@modifies L @*/
 {
 	lua_pushnil(L);
 	if (info==NULL)
@@ -102,6 +111,7 @@ static int pusherror(lua_State *L, const char *info)
 }
 
 static int pushresult(lua_State *L, int i, const char *info)
+	/*@modifies L @*/
 {
 	if (i != -1)
 	{
@@ -112,13 +122,15 @@ static int pushresult(lua_State *L, int i, const char *info)
 		return pusherror(L, info);
 }
 
-static void badoption(lua_State *L, int i, const char *what, int option)
+static void badoption(lua_State *L, /*@unused@*/ int i, const char *what, int option)
+	/*@modifies L @*/
 {
 	luaL_argerror(L, 2,
 		lua_pushfstring(L, "unknown %s option `%c'", what, option));
 }
 
 static uid_t mygetuid(lua_State *L, int i)
+	/*@modifies L @*/
 {
 	if (lua_isnone(L, i))
 		return -1;
@@ -134,6 +146,7 @@ static uid_t mygetuid(lua_State *L, int i)
 }
 
 static gid_t mygetgid(lua_State *L, int i)
+	/*@modifies L @*/
 {
 	if (lua_isnone(L, i))
 		return -1;
@@ -151,6 +164,7 @@ static gid_t mygetgid(lua_State *L, int i)
 
 
 static int Perrno(lua_State *L)			/** errno() */
+	/*@modifies L @*/
 {
 	lua_pushstring(L, strerror(errno));
 	lua_pushnumber(L, errno);
@@ -159,6 +173,8 @@ static int Perrno(lua_State *L)			/** errno() */
 
 
 static int Pdir(lua_State *L)			/** dir([path]) */
+	/*@globals fileSystem @*/
+	/*@modifies L, fileSystem @*/
 {
 	const char *path = luaL_optstring(L, 1, ".");
 	DIR *d = opendir(path);
@@ -178,6 +194,7 @@ static int Pdir(lua_State *L)			/** dir([path]) */
 
 
 static int aux_files(lua_State *L)
+	/*@modifies L @*/
 {
 	DIR *d = lua_touserdata(L, lua_upvalueindex(1));
 	struct dirent *entry;
@@ -204,6 +221,8 @@ static int aux_files(lua_State *L)
 }
 
 static int Pfiles(lua_State *L)			/** files([path]) */
+	/*@globals fileSystem @*/
+	/*@modifies L, fileSystem @*/
 {
 	const char *path = luaL_optstring(L, 1, ".");
 	DIR *d = opendir(path);
@@ -219,6 +238,7 @@ static int Pfiles(lua_State *L)			/** files([path]) */
 
 
 static int Pgetcwd(lua_State *L)		/** getcwd() */
+	/*@modifies L @*/
 {
 	char buf[MYBUFSIZ];
 	if (getcwd(buf, sizeof(buf)) == NULL)
@@ -232,6 +252,8 @@ static int Pgetcwd(lua_State *L)		/** getcwd() */
 
 
 static int Pmkdir(lua_State *L)			/** mkdir(path) */
+	/*@globals fileSystem @*/
+	/*@modifies L, fileSystem @*/
 {
 	const char *path = luaL_checkstring(L, 1);
 	return pushresult(L, mkdir(path, 0777), path);
@@ -239,6 +261,8 @@ static int Pmkdir(lua_State *L)			/** mkdir(path) */
 
 
 static int Pchdir(lua_State *L)			/** chdir(path) */
+	/*@globals internalState @*/
+	/*@modifies L, internalState @*/
 {
 	const char *path = luaL_checkstring(L, 1);
 	return pushresult(L, chdir(path), path);
@@ -246,6 +270,8 @@ static int Pchdir(lua_State *L)			/** chdir(path) */
 
 
 static int Prmdir(lua_State *L)			/** rmdir(path) */
+	/*@globals fileSystem @*/
+	/*@modifies L, fileSystem @*/
 {
 	const char *path = luaL_checkstring(L, 1);
 	return pushresult(L, rmdir(path), path);
@@ -253,6 +279,8 @@ static int Prmdir(lua_State *L)			/** rmdir(path) */
 
 
 static int Punlink(lua_State *L)		/** unlink(path) */
+	/*@globals fileSystem @*/
+	/*@modifies L, fileSystem @*/
 {
 	const char *path = luaL_checkstring(L, 1);
 	return pushresult(L, unlink(path), path);
@@ -260,6 +288,8 @@ static int Punlink(lua_State *L)		/** unlink(path) */
 
 
 static int Plink(lua_State *L)			/** link(oldpath,newpath) */
+	/*@globals fileSystem @*/
+	/*@modifies L, fileSystem @*/
 {
 	const char *oldpath = luaL_checkstring(L, 1);
 	const char *newpath = luaL_checkstring(L, 2);
@@ -268,6 +298,8 @@ static int Plink(lua_State *L)			/** link(oldpath,newpath) */
 
 
 static int Psymlink(lua_State *L)		/** symlink(oldpath,newpath) */
+	/*@globals fileSystem @*/
+	/*@modifies L, fileSystem @*/
 {
 	const char *oldpath = luaL_checkstring(L, 1);
 	const char *newpath = luaL_checkstring(L, 2);
@@ -276,6 +308,8 @@ static int Psymlink(lua_State *L)		/** symlink(oldpath,newpath) */
 
 
 static int Preadlink(lua_State *L)		/** readlink(path) */
+	/*@globals fileSystem @*/
+	/*@modifies L, fileSystem @*/
 {
 	char buf[MYBUFSIZ];
 	const char *path = luaL_checkstring(L, 1);
@@ -287,6 +321,7 @@ static int Preadlink(lua_State *L)		/** readlink(path) */
 
 
 static int Paccess(lua_State *L)		/** access(path,[mode]) */
+	/*@modifies L @*/
 {
 	int mode=F_OK;
 	const char *path=luaL_checkstring(L, 1);
@@ -306,6 +341,8 @@ static int Paccess(lua_State *L)		/** access(path,[mode]) */
 
 
 static int Pmkfifo(lua_State *L)		/** mkfifo(path) */
+	/*@globals fileSystem @*/
+	/*@modifies L, fileSystem @*/
 {
 	const char *path = luaL_checkstring(L, 1);
 	return pushresult(L, mkfifo(path, 0777), path);
@@ -313,6 +350,8 @@ static int Pmkfifo(lua_State *L)		/** mkfifo(path) */
 
 
 static int Pexec(lua_State *L)			/** exec(path,[args]) */
+	/*@globals internalState @*/
+	/*@modifies L, internalState @*/
 {
 	const char *path = luaL_checkstring(L, 1);
 	int i,n=lua_gettop(L);
@@ -327,12 +366,16 @@ static int Pexec(lua_State *L)			/** exec(path,[args]) */
 
 
 static int Pfork(lua_State *L)			/** fork() */
+	/*@globals fileSystem, internalState @*/
+	/*@modifies L, fileSystem, internalState @*/
 {
 	return pushresult(L, fork(), NULL);
 }
 
 
 static int Pwait(lua_State *L)			/** wait([pid]) */
+	/*@globals fileSystem @*/
+	/*@modifies L, fileSystem @*/
 {
 	pid_t pid = luaL_optint(L, 1, -1);
 	return pushresult(L, waitpid(pid, NULL, 0), NULL);
@@ -340,6 +383,7 @@ static int Pwait(lua_State *L)			/** wait([pid]) */
 
 
 static int Pkill(lua_State *L)			/** kill(pid,[sig]) */
+	/*@modifies L @*/
 {
 	pid_t pid = luaL_checkint(L, 1);
 	int sig = luaL_optint(L, 2, SIGTERM);
@@ -348,6 +392,8 @@ static int Pkill(lua_State *L)			/** kill(pid,[sig]) */
 
 
 static int Psleep(lua_State *L)			/** sleep(seconds) */
+	/*@globals fileSystem @*/
+	/*@modifies L, fileSystem @*/
 {
 	unsigned int seconds = luaL_checkint(L, 1);
 	lua_pushnumber(L, sleep(seconds));
@@ -356,6 +402,7 @@ static int Psleep(lua_State *L)			/** sleep(seconds) */
 
 
 static int Pputenv(lua_State *L)		/** putenv(string) */
+	/*@modifies L @*/
 {
 	size_t l;
 	const char *s=luaL_checklstring(L, 1, &l);
@@ -366,6 +413,7 @@ static int Pputenv(lua_State *L)		/** putenv(string) */
 
 #ifdef linux
 static int Psetenv(lua_State *L)		/** setenv(name,value,[over]) */
+	/*@modifies L @*/
 {
 	const char *name=luaL_checkstring(L, 1);
 	const char *value=luaL_checkstring(L, 2);
@@ -375,6 +423,7 @@ static int Psetenv(lua_State *L)		/** setenv(name,value,[over]) */
 
 
 static int Punsetenv(lua_State *L)		/** unsetenv(name) */
+	/*@modifies L @*/
 {
 	const char *name=luaL_checkstring(L, 1);
 	unsetenv(name);
@@ -384,10 +433,13 @@ static int Punsetenv(lua_State *L)		/** unsetenv(name) */
 
 
 static int Pgetenv(lua_State *L)		/** getenv([name]) */
+	/*@modifies L @*/
 {
 	if (lua_isnone(L, 1))
 	{
+/*@-nestedextern -shadow@*/
 		extern char **environ;
+/*@=nestedextern =shadow@*/
 		char **e;
 		if (*environ==NULL) lua_pushnil(L); else lua_newtable(L);
 		for (e=environ; *e!=NULL; e++)
@@ -414,6 +466,8 @@ static int Pgetenv(lua_State *L)		/** getenv([name]) */
 
 
 static int Pumask(lua_State *L)			/** umask([mode]) */
+	/*@globals fileSystem @*/
+	/*@modifies L, fileSystem @*/
 {
 	char m[10];
 	mode_t mode;
@@ -436,6 +490,8 @@ static int Pumask(lua_State *L)			/** umask([mode]) */
 
 
 static int Pchmod(lua_State *L)			/** chmod(path,mode) */
+	/*@globals fileSystem @*/
+	/*@modifies L, fileSystem @*/
 {
 	mode_t mode;
 	struct stat s;
@@ -449,6 +505,8 @@ static int Pchmod(lua_State *L)			/** chmod(path,mode) */
 
 
 static int Pchown(lua_State *L)			/** chown(path,uid,gid) */
+	/*@globals fileSystem, internalState @*/
+	/*@modifies L, fileSystem, internalState @*/
 {
 	const char *path = luaL_checkstring(L, 1);
 	uid_t uid = mygetuid(L, 2);
@@ -458,6 +516,8 @@ static int Pchown(lua_State *L)			/** chown(path,uid,gid) */
 
 
 static int Putime(lua_State *L)			/** utime(path,[mtime,atime]) */
+	/*@globals fileSystem @*/
+	/*@modifies L, fileSystem @*/
 {
 	struct utimbuf times;
 	time_t currtime = time(NULL);
@@ -468,7 +528,8 @@ static int Putime(lua_State *L)			/** utime(path,[mtime,atime]) */
 }
 
 
-static int FgetID(lua_State *L, int i, const void *data)
+static int FgetID(lua_State *L, int i, /*@unused@*/ const void *data)
+	/*@modifies L @*/
 {
 	switch (i)
 	{
@@ -483,18 +544,21 @@ static int FgetID(lua_State *L, int i, const void *data)
 	return 1;
 }
 
+/*@observer@*/ /*@unchecked@*/
 static const char *const SgetID[] =
 {
 	"egid", "euid", "gid", "uid", "pgrp", "pid", "ppid", NULL
 };
 
 static int Pgetprocessid(lua_State *L)		/** getprocessid([selector]) */
+	/*@modifies L @*/
 {
 	return doselection(L, 1, SgetID, FgetID, NULL);
 }
 
 
 static int Pttyname(lua_State *L)		/** ttyname(fd) */
+	/*@modifies L @*/
 {
 	int fd=luaL_optint(L, 1, 0);
 	lua_pushstring(L, ttyname(fd));
@@ -502,6 +566,8 @@ static int Pttyname(lua_State *L)		/** ttyname(fd) */
 }
 
 static int Pctermid(lua_State *L)		/** ctermid() */
+	/*@globals fileSystem @*/
+	/*@modifies L, fileSystem @*/
 {
 	char b[L_ctermid];
 	lua_pushstring(L, ctermid(b));
@@ -510,6 +576,7 @@ static int Pctermid(lua_State *L)		/** ctermid() */
 
 
 static int Pgetlogin(lua_State *L)		/** getlogin() */
+	/*@modifies L @*/
 {
 	lua_pushstring(L, getlogin());
 	return 1;
@@ -517,6 +584,7 @@ static int Pgetlogin(lua_State *L)		/** getlogin() */
 
 
 static int Fgetpasswd(lua_State *L, int i, const void *data)
+	/*@modifies L @*/
 {
 	const struct passwd *p=data;
 	switch (i)
@@ -533,6 +601,7 @@ static int Fgetpasswd(lua_State *L, int i, const void *data)
 	return 1;
 }
 
+/*@observer@*/ /*@unchecked@*/
 static const char *const Sgetpasswd[] =
 {
 	"name", "uid", "gid", "dir", "shell", "gecos", "passwd", NULL
@@ -540,6 +609,7 @@ static const char *const Sgetpasswd[] =
 
 
 static int Pgetpasswd(lua_State *L)		/** getpasswd(name or id) */
+	/*@modifies L @*/
 {
 	struct passwd *p=NULL;
 	if (lua_isnoneornil(L, 1))
@@ -559,6 +629,7 @@ static int Pgetpasswd(lua_State *L)		/** getpasswd(name or id) */
 
 
 static int Pgetgroup(lua_State *L)		/** getgroup(name or id) */
+	/*@modifies L @*/
 {
 	struct group *g=NULL;
 	if (lua_isnumber(L, 1))
@@ -583,12 +654,16 @@ static int Pgetgroup(lua_State *L)		/** getgroup(name or id) */
 
 
 static int Psetuid(lua_State *L)		/** setuid(name or id) */
+	/*@globals fileSystem, internalState @*/
+	/*@modifies L, fileSystem, internalState @*/
 {
 	return pushresult(L, setuid(mygetuid(L, 1)), NULL);
 }
 
 
 static int Psetgid(lua_State *L)		/** setgid(name or id) */
+	/*@globals fileSystem @*/
+	/*@modifies L, fileSystem @*/
 {
 	return pushresult(L, setgid(mygetgid(L, 1)), NULL);
 }
@@ -602,6 +677,7 @@ struct mytimes
 #define pushtime(L,x)		lua_pushnumber(L,((lua_Number)x)/CLOCKS_PER_SEC)
 
 static int Ftimes(lua_State *L, int i, const void *data)
+	/*@modifies L @*/
 {
 	const struct mytimes *t=data;
 	switch (i)
@@ -615,6 +691,7 @@ static int Ftimes(lua_State *L, int i, const void *data)
 	return 1;
 }
 
+/*@observer@*/ /*@unchecked@*/
 static const char *const Stimes[] =
 {
 	"utime", "stime", "cutime", "cstime", "elapsed", NULL
@@ -623,6 +700,7 @@ static const char *const Stimes[] =
 #define storetime(L,name,x)	storenumber(L,name,(lua_Number)x/CLOCKS_PER_SEC)
 
 static int Ptimes(lua_State *L)			/** times() */
+	/*@modifies L @*/
 {
 	struct mytimes t;
 	t.elapsed = times(&t.t);
@@ -634,10 +712,12 @@ struct mystat
 {
 	struct stat s;
 	char mode[10];
+/*@observer@*/
 	const char *type;
 };
 
 static int Fstat(lua_State *L, int i, const void *data)
+	/*@modifies L @*/
 {
 	const struct mystat *s=data;
 	switch (i)
@@ -658,6 +738,7 @@ static int Fstat(lua_State *L, int i, const void *data)
 	return 1;
 }
 
+/*@observer@*/ /*@unchecked@*/
 static const char *const Sstat[] =
 {
 	"mode", "ino", "dev", "nlink", "uid", "gid",
@@ -666,6 +747,7 @@ static const char *const Sstat[] =
 };
 
 static int Pstat(lua_State *L)			/** stat(path,[selector]) */
+	/*@modifies L @*/
 {
 	struct mystat s;
 	const char *path=luaL_checkstring(L, 1);
@@ -677,6 +759,7 @@ static int Pstat(lua_State *L)			/** stat(path,[selector]) */
 
 
 static int Puname(lua_State *L)			/** uname([string]) */
+	/*@modifies L @*/
 {
 	struct utsname u;
 	luaL_Buffer b;
@@ -701,6 +784,7 @@ static int Puname(lua_State *L)			/** uname([string]) */
 }
 
 
+/*@observer@*/ /*@unchecked@*/
 static const int Kpathconf[] =
 {
 	_PC_LINK_MAX, _PC_MAX_CANON, _PC_MAX_INPUT, _PC_NAME_MAX, _PC_PATH_MAX,
@@ -709,12 +793,15 @@ static const int Kpathconf[] =
 };
 
 static int Fpathconf(lua_State *L, int i, const void *data)
+	/*@globals internalState @*/
+	/*@modifies L, internalState @*/
 {
 	const char *path=data;
 	lua_pushnumber(L, pathconf(path, Kpathconf[i]));
 	return 1;
 }
 
+/*@observer@*/ /*@unchecked@*/
 static const char *const Spathconf[] =
 {
 	"link_max", "max_canon", "max_input", "name_max", "path_max",
@@ -723,12 +810,14 @@ static const char *const Spathconf[] =
 };
 
 static int Ppathconf(lua_State *L)		/** pathconf(path,[selector]) */
+	/*@modifies L @*/
 {
 	const char *path=luaL_checkstring(L, 1);
 	return doselection(L, 2, Spathconf, Fpathconf, path);
 }
 
 
+/*@observer@*/ /*@unchecked@*/
 static const int Ksysconf[] =
 {
 	_SC_ARG_MAX, _SC_CHILD_MAX, _SC_CLK_TCK, _SC_NGROUPS_MAX, _SC_STREAM_MAX,
@@ -736,12 +825,14 @@ static const int Ksysconf[] =
 	-1
 };
 
-static int Fsysconf(lua_State *L, int i, const void *data)
+static int Fsysconf(lua_State *L, int i, /*@unused@*/ const void *data)
+	/*@modifies L @*/
 {
 	lua_pushnumber(L, sysconf(Ksysconf[i]));
 	return 1;
 }
 
+/*@observer@*/ /*@unchecked@*/
 static const char *const Ssysconf[] =
 {
 	"arg_max", "child_max", "clk_tck", "ngroups_max", "stream_max",
@@ -750,11 +841,14 @@ static const char *const Ssysconf[] =
 };
 
 static int Psysconf(lua_State *L)		/** sysconf([selector]) */
+	/*@modifies L @*/
 {
 	return doselection(L, 1, Ssysconf, Fsysconf, NULL);
 }
 
 
+/*@-readonlytrans@*/
+/*@observer@*/ /*@unchecked@*/
 static const luaL_reg R[] =
 {
 	{"access",		Paccess},
@@ -801,6 +895,7 @@ static const luaL_reg R[] =
 #endif
 	{NULL,			NULL}
 };
+/*@=readonlytrans@*/
 
 LUALIB_API int luaopen_posix (lua_State *L)
 {
diff --git a/lua/local/lposix.h b/lua/local/lposix.h
index e1e819cb3..9f42414eb 100644
--- a/lua/local/lposix.h
+++ b/lua/local/lposix.h
@@ -1,6 +1,7 @@
 #ifndef LPOSIX_H
 #define LPOSIX_H
 
-int luaopen_posix (lua_State *L);
+int luaopen_posix (lua_State *L)
+	/*@modifies L @*/;
 
 #endif
diff --git a/lua/local/lrexlib.c b/lua/local/lrexlib.c
index fe9a73576..8486330c8 100644
--- a/lua/local/lrexlib.c
+++ b/lua/local/lrexlib.c
@@ -10,6 +10,8 @@
 #include "lua.h"
 #include "lauxlib.h"
 
+/*@access regex_t @*/
+
 /* Sanity check */
 #if !defined(WITH_POSIX) && !defined(WITH_PCRE)
 #error Define WITH_POSIX or WITH_PCRE, otherwise this library is useless!
@@ -22,7 +24,9 @@
 
 #include <regex.h>
 
-static int rex_comp(lua_State *L) {
+static int rex_comp(lua_State *L)
+	/*@modifies L @*/
+{
   size_t l;
   const char *pattern;
   int res;
@@ -46,22 +50,28 @@ static int rex_comp(lua_State *L) {
   return 1;
 }
 
-static void rex_getargs(lua_State *L, size_t *len, size_t *ncapt,
-                        const char **text, regex_t **pr, regmatch_t **match) {
+static void rex_getargs(lua_State *L, /*@unused@*/ size_t *len, size_t *ncapt,
+                        const char **text, regex_t **pr, regmatch_t **match)
+	/*@modifies L, *ncapt, *text, *pr, *match @*/
+{
   luaL_checkany(L, 1);
   *pr = (regex_t *)lua_touserdata(L, 1);
+/*@-observertrans -dependenttrans @*/
 #ifdef REG_BASIC
   *text = luaL_checklstring(L, 2, len);
 #else
   *text = luaL_checklstring(L, 2, NULL);
 #endif
+/*@=observertrans =dependenttrans @*/
   *ncapt = (*pr)->re_nsub;
   luaL_checkstack(L, *ncapt + 2, "too many captures");
   *match = malloc((*ncapt + 1) * sizeof(regmatch_t));
 }
 
 static void rex_push_matches(lua_State *L, const char *text, regmatch_t *match,
-                             size_t ncapt) {
+                             size_t ncapt)
+	/*@modifies L @*/
+{
   size_t i;
   lua_newtable(L);
   for (i = 1; i <= ncapt; i++) {
@@ -73,7 +83,9 @@ static void rex_push_matches(lua_State *L, const char *text, regmatch_t *match,
   }
 }
 
-static int rex_match(lua_State *L) {
+static int rex_match(lua_State *L)
+	/*@modifies L @*/
+{
   int res;
 #ifdef REG_BASIC
   size_t len;
@@ -108,7 +120,9 @@ static int rex_match(lua_State *L) {
     return 0;
 }
 
-static int rex_gmatch(lua_State *L) {
+static int rex_gmatch(lua_State *L)
+	/*@modifies L @*/
+{
   int res;
 #ifdef REG_BASIC
   size_t len;
@@ -154,19 +168,24 @@ static int rex_gmatch(lua_State *L) {
   return 1;
 }
 
-static int rex_gc (lua_State *L) {
+static int rex_gc (lua_State *L)
+	/*@modifies L @*/
+{
   regex_t *r = (regex_t *)luaL_checkudata(L, 1, "regex_t");
   if (r)
     regfree(r);
   return 0;
 }
 
+/*@-readonlytrans@*/
+/*@unchecked@*/
 static const luaL_reg rexmeta[] = {
   {"match",   rex_match},
   {"gmatch",  rex_gmatch},
   {"__gc",    rex_gc},
   {NULL, NULL}
 };
+/*@=readonlytrans@*/
 
 #endif /* WITH_POSIX */
 
@@ -297,6 +316,8 @@ static const luaL_reg pcremeta[] = {
 
 /* Open the library */
 
+/*@-readonlytrans@*/
+/*@unchecked@*/
 static const luaL_reg rexlib[] = {
 #ifdef WITH_POSIX
   {"newPOSIX", rex_comp},
@@ -306,8 +327,10 @@ static const luaL_reg rexlib[] = {
 #endif
   {NULL, NULL}
 };
+/*@=readonlytrans@*/
 
 static void createmeta(lua_State *L, const char *name)
+	/*@modifies L @*/
 {
   luaL_newmetatable(L, name);   /* create new metatable */
   lua_pushliteral(L, "__index");
diff --git a/lua/local/lrexlib.h b/lua/local/lrexlib.h
index 663c635ef..e6df8e560 100644
--- a/lua/local/lrexlib.h
+++ b/lua/local/lrexlib.h
@@ -1,6 +1,7 @@
 #ifndef LREXLIB_H
 #define LREXLIB_H
 
-int luaopen_rex(lua_State *L);
+int luaopen_rex(lua_State *L)
+	/*@modifies L @*/;
 
 #endif
diff --git a/lua/local/modemuncher.c b/lua/local/modemuncher.c
index b1e966c9b..10264c3dc 100644
--- a/lua/local/modemuncher.c
+++ b/lua/local/modemuncher.c
@@ -21,6 +21,7 @@ struct modeLookup
 
 typedef struct modeLookup modeLookup;
 
+/*@observer@*/ /*@unchecked@*/
 static modeLookup modesel[] =
 {
 	/* RWX char				Posix Constant */
@@ -41,6 +42,7 @@ static modeLookup modesel[] =
 
 
 static int rwxrwxrwx(mode_t *mode, const char *p)
+	/*@modifies *mode @*/
 {
 	int count;
 	mode_t tmp_mode = *mode;
@@ -62,6 +64,7 @@ static int rwxrwxrwx(mode_t *mode, const char *p)
 
 			default:
 			return -4; /* failed! -- bad rwxrwxrwx mode change */
+			/*@notreached@*/
 			break;
 		}
 		p++;
@@ -71,6 +74,7 @@ static int rwxrwxrwx(mode_t *mode, const char *p)
 }
 
 static void modechopper(mode_t mode, char *p)
+	/*@modifies *p @*/
 {
 	/* requires char p[10] */
 	int count;
@@ -94,6 +98,7 @@ static void modechopper(mode_t mode, char *p)
 }
 
 static int mode_munch(mode_t *mode, const char* p)
+	/*@modifies *mode @*/
 {
 
 	char op=0;
diff --git a/lua/lopcodes.h b/lua/lopcodes.h
index 3718cea30..d93ee0dcb 100644
--- a/lua/lopcodes.h
+++ b/lua/lopcodes.h
@@ -1,5 +1,5 @@
 /*
-** $Id: lopcodes.h,v 1.1 2004/03/16 21:58:30 niemeyer Exp $
+** $Id: lopcodes.h,v 1.2 2004/03/23 05:09:14 jbj Exp $
 ** Opcodes for Lua virtual machine
 ** See Copyright Notice in lua.h
 */
@@ -218,6 +218,7 @@ enum OpModeMask {
 };
 
 
+/*@unchecked@*/
 extern const lu_byte luaP_opmodes[NUM_OPCODES];
 
 #define getOpMode(m)            (cast(enum OpMode, luaP_opmodes[m] & 3))
diff --git a/lua/lparser.c b/lua/lparser.c
index 81341bf92..be4a5dd43 100644
--- a/lua/lparser.c
+++ b/lua/lparser.c
@@ -1,5 +1,5 @@
 /*
-** $Id: lparser.c,v 1.2 2004/03/19 21:14:32 niemeyer Exp $
+** $Id: lparser.c,v 1.3 2004/03/23 05:09:14 jbj Exp $
 ** Lua Parser
 ** See Copyright Notice in lua.h
 */
@@ -37,6 +37,7 @@
 ** nodes for block list (list of active blocks)
 */
 typedef struct BlockCnt {
+/*@null@*/
   struct BlockCnt *previous;  /* chain */
   int breaklist;  /* list of jumps out of this loop */
   int nactvar;  /* # active local variables outside the breakable structure */
@@ -49,12 +50,16 @@ typedef struct BlockCnt {
 /*
 ** prototypes for recursive non-terminal functions
 */
-static void chunk (LexState *ls);
-static void expr (LexState *ls, expdesc *v);
+static void chunk (LexState *ls)
+	/*@modifies ls @*/;
+static void expr (LexState *ls, expdesc *v)
+	/*@modifies ls, v @*/;
 
 
 
-static void next (LexState *ls) {
+static void next (LexState *ls)
+	/*@modifies ls @*/
+{
   ls->lastline = ls->linenumber;
   if (ls->lookahead.token != TK_EOS) {  /* is there a look-ahead token? */
     ls->t = ls->lookahead;  /* use this one */
@@ -65,19 +70,25 @@ static void next (LexState *ls) {
 }
 
 
-static void lookahead (LexState *ls) {
+static void lookahead (LexState *ls)
+	/*@modifies ls @*/
+{
   lua_assert(ls->lookahead.token == TK_EOS);
   ls->lookahead.token = luaX_lex(ls, &ls->lookahead.seminfo);
 }
 
 
-static void error_expected (LexState *ls, int token) {
+static void error_expected (LexState *ls, int token)
+	/*@modifies ls @*/
+{
   luaX_syntaxerror(ls,
          luaO_pushfstring(ls->L, "`%s' expected", luaX_token2str(ls, token)));
 }
 
 
-static int testnext (LexState *ls, int c) {
+static int testnext (LexState *ls, int c)
+	/*@modifies ls @*/
+{
   if (ls->t.token == c) {
     next(ls);
     return 1;
@@ -86,7 +97,9 @@ static int testnext (LexState *ls, int c) {
 }
 
 
-static void check (LexState *ls, int c) {
+static void check (LexState *ls, int c)
+	/*@modifies ls @*/
+{
   if (!testnext(ls, c))
     error_expected(ls, c);
 }
@@ -96,7 +109,9 @@ static void check (LexState *ls, int c) {
 
 
 
-static void check_match (LexState *ls, int what, int who, int where) {
+static void check_match (LexState *ls, int what, int who, int where)
+	/*@modifies ls @*/
+{
   if (!testnext(ls, what)) {
     if (where == ls->linenumber)
       error_expected(ls, what);
@@ -109,7 +124,9 @@ static void check_match (LexState *ls, int what, int who, int where) {
 }
 
 
-static TString *str_checkname (LexState *ls) {
+static TString *str_checkname (LexState *ls)
+	/*@modifies ls @*/
+{
   TString *ts;
   check_condition(ls, (ls->t.token == TK_NAME), "<name> expected");
   ts = ls->t.seminfo.ts;
@@ -118,24 +135,32 @@ static TString *str_checkname (LexState *ls) {
 }
 
 
-static void init_exp (expdesc *e, expkind k, int i) {
+static void init_exp (expdesc *e, expkind k, int i)
+	/*@modifies e @*/
+{
   e->f = e->t = NO_JUMP;
   e->k = k;
   e->info = i;
 }
 
 
-static void codestring (LexState *ls, expdesc *e, TString *s) {
+static void codestring (LexState *ls, expdesc *e, TString *s)
+	/*@modifies ls, e @*/
+{
   init_exp(e, VK, luaK_stringK(ls->fs, s));
 }
 
 
-static void checkname(LexState *ls, expdesc *e) {
+static void checkname(LexState *ls, expdesc *e)
+	/*@modifies ls, e @*/
+{
   codestring(ls, e, str_checkname(ls));
 }
 
 
-static int luaI_registerlocalvar (LexState *ls, TString *varname) {
+static int luaI_registerlocalvar (LexState *ls, TString *varname)
+	/*@modifies ls @*/
+{
   FuncState *fs = ls->fs;
   Proto *f = fs->f;
   luaM_growvector(ls->L, f->locvars, fs->nlocvars, f->sizelocvars,
@@ -145,14 +170,18 @@ static int luaI_registerlocalvar (LexState *ls, TString *varname) {
 }
 
 
-static void new_localvar (LexState *ls, TString *name, int n) {
+static void new_localvar (LexState *ls, TString *name, int n)
+	/*@modifies ls @*/
+{
   FuncState *fs = ls->fs;
   luaX_checklimit(ls, fs->nactvar+n+1, MAXVARS, "local variables");
   fs->actvar[fs->nactvar+n] = luaI_registerlocalvar(ls, name);
 }
 
 
-static void adjustlocalvars (LexState *ls, int nvars) {
+static void adjustlocalvars (LexState *ls, int nvars)
+	/*@modifies ls @*/
+{
   FuncState *fs = ls->fs;
   fs->nactvar += nvars;
   for (; nvars; nvars--) {
@@ -161,25 +190,33 @@ static void adjustlocalvars (LexState *ls, int nvars) {
 }
 
 
-static void removevars (LexState *ls, int tolevel) {
+static void removevars (LexState *ls, int tolevel)
+	/*@modifies ls @*/
+{
   FuncState *fs = ls->fs;
   while (fs->nactvar > tolevel)
     getlocvar(fs, --fs->nactvar).endpc = fs->pc;
 }
 
 
-static void new_localvarstr (LexState *ls, const char *name, int n) {
+static void new_localvarstr (LexState *ls, const char *name, int n)
+	/*@modifies ls @*/
+{
   new_localvar(ls, luaS_new(ls->L, name), n);
 }
 
 
-static void create_local (LexState *ls, const char *name) {
+static void create_local (LexState *ls, const char *name)
+	/*@modifies ls @*/
+{
   new_localvarstr(ls, name, 0);
   adjustlocalvars(ls, 1);
 }
 
 
-static int indexupvalue (FuncState *fs, TString *name, expdesc *v) {
+static int indexupvalue (FuncState *fs, TString *name, expdesc *v)
+	/*@modifies fs @*/
+{
   int i;
   Proto *f = fs->f;
   for (i=0; i<f->nups; i++) {
@@ -198,7 +235,9 @@ static int indexupvalue (FuncState *fs, TString *name, expdesc *v) {
 }
 
 
-static int searchvar (FuncState *fs, TString *n) {
+static int searchvar (FuncState *fs, TString *n)
+	/*@*/
+{
   int i;
   for (i=fs->nactvar-1; i >= 0; i--) {
     if (n == getlocvar(fs, i).varname)
@@ -208,14 +247,18 @@ static int searchvar (FuncState *fs, TString *n) {
 }
 
 
-static void markupval (FuncState *fs, int level) {
+static void markupval (FuncState *fs, int level)
+	/*@modifies fs @*/
+{
   BlockCnt *bl = fs->bl;
   while (bl && bl->nactvar > level) bl = bl->previous;
   if (bl) bl->upval = 1;
 }
 
 
-static void singlevaraux (FuncState *fs, TString *n, expdesc *var, int base) {
+static void singlevaraux (FuncState *fs, TString *n, expdesc *var, int base)
+	/*@modifies fs, var @*/
+{
   if (fs == NULL)  /* no more levels? */
     init_exp(var, VGLOBAL, NO_REG);  /* default is global variable */
   else {
@@ -240,14 +283,18 @@ static void singlevaraux (FuncState *fs, TString *n, expdesc *var, int base) {
 }
 
 
-static TString *singlevar (LexState *ls, expdesc *var, int base) {
+static TString *singlevar (LexState *ls, expdesc *var, int base)
+	/*@modifies ls, var @*/
+{
   TString *varname = str_checkname(ls);
   singlevaraux(ls->fs, varname, var, base);
   return varname;
 }
 
 
-static void adjust_assign (LexState *ls, int nvars, int nexps, expdesc *e) {
+static void adjust_assign (LexState *ls, int nvars, int nexps, expdesc *e)
+	/*@modifies ls, e @*/
+{
   FuncState *fs = ls->fs;
   int extra = nvars - nexps;
   if (e->k == VCALL) {
@@ -267,7 +314,9 @@ static void adjust_assign (LexState *ls, int nvars, int nexps, expdesc *e) {
 }
 
 
-static void code_params (LexState *ls, int nparams, int dots) {
+static void code_params (LexState *ls, int nparams, int dots)
+	/*@modifies ls @*/
+{
   FuncState *fs = ls->fs;
   adjustlocalvars(ls, nparams);
   luaX_checklimit(ls, fs->nactvar, MAXPARAMS, "parameters");
@@ -279,7 +328,9 @@ static void code_params (LexState *ls, int nparams, int dots) {
 }
 
 
-static void enterblock (FuncState *fs, BlockCnt *bl, int isbreakable) {
+static void enterblock (FuncState *fs, BlockCnt *bl, int isbreakable)
+	/*@modifies fs, bl @*/
+{
   bl->breaklist = NO_JUMP;
   bl->isbreakable = isbreakable;
   bl->nactvar = fs->nactvar;
@@ -290,7 +341,9 @@ static void enterblock (FuncState *fs, BlockCnt *bl, int isbreakable) {
 }
 
 
-static void leaveblock (FuncState *fs) {
+static void leaveblock (FuncState *fs)
+	/*@modifies fs @*/
+{
   BlockCnt *bl = fs->bl;
   fs->bl = bl->previous;
   removevars(fs->ls, bl->nactvar);
@@ -302,13 +355,17 @@ static void leaveblock (FuncState *fs) {
 }
 
 
-static void pushclosure (LexState *ls, FuncState *func, expdesc *v) {
+static void pushclosure (LexState *ls, FuncState *func, expdesc *v)
+	/*@modifies ls, v @*/
+{
   FuncState *fs = ls->fs;
   Proto *f = fs->f;
   int i;
   luaM_growvector(ls->L, f->p, fs->np, f->sizep, Proto *,
                   MAXARG_Bx, "constant table overflow");
+/*@-onlytrans@*/
   f->p[fs->np++] = func->f;
+/*@=onlytrans@*/
   init_exp(v, VRELOCABLE, luaK_codeABx(fs, OP_CLOSURE, 0, fs->np-1));
   for (i=0; i<func->f->nups; i++) {
     OpCode o = (func->upvalues[i].k == VLOCAL) ? OP_MOVE : OP_GETUPVAL;
@@ -317,7 +374,9 @@ static void pushclosure (LexState *ls, FuncState *func, expdesc *v) {
 }
 
 
-static void open_func (LexState *ls, FuncState *fs) {
+static void open_func (LexState *ls, FuncState *fs)
+	/*@modifies ls, fs @*/
+{
   Proto *f = luaF_newproto(ls->L);
   fs->f = f;
   fs->prev = ls->fs;  /* linked list of funcstates */
@@ -339,7 +398,9 @@ static void open_func (LexState *ls, FuncState *fs) {
 }
 
 
-static void close_func (LexState *ls) {
+static void close_func (LexState *ls)
+	/*@modifies ls @*/
+{
   lua_State *L = ls->L;
   FuncState *fs = ls->fs;
   Proto *f = fs->f;
@@ -387,7 +448,9 @@ Proto *luaY_parser (lua_State *L, ZIO *z, Mbuffer *buff) {
 /*============================================================*/
 
 
-static void luaY_field (LexState *ls, expdesc *v) {
+static void luaY_field (LexState *ls, expdesc *v)
+	/*@modifies ls, v @*/
+{
   /* field -> ['.' | ':'] NAME */
   FuncState *fs = ls->fs;
   expdesc key;
@@ -398,7 +461,9 @@ static void luaY_field (LexState *ls, expdesc *v) {
 }
 
 
-static void luaY_index (LexState *ls, expdesc *v) {
+static void luaY_index (LexState *ls, expdesc *v)
+	/*@modifies ls, v @*/
+{
   /* index -> '[' expr ']' */
   next(ls);  /* skip the '[' */
   expr(ls, v);
@@ -423,7 +488,9 @@ struct ConsControl {
 };
 
 
-static void recfield (LexState *ls, struct ConsControl *cc) {
+static void recfield (LexState *ls, struct ConsControl *cc)
+	/*@modifies ls, cc @*/
+{
   /* recfield -> (NAME | `['exp1`]') = exp1 */
   FuncState *fs = ls->fs;
   int reg = ls->fs->freereg;
@@ -444,7 +511,9 @@ static void recfield (LexState *ls, struct ConsControl *cc) {
 }
 
 
-static void closelistfield (FuncState *fs, struct ConsControl *cc) {
+static void closelistfield (FuncState *fs, struct ConsControl *cc)
+	/*@modifies fs, cc @*/
+{
   if (cc->v.k == VVOID) return;  /* there is no list item */
   luaK_exp2nextreg(fs, &cc->v);
   cc->v.k = VVOID;
@@ -456,7 +525,9 @@ static void closelistfield (FuncState *fs, struct ConsControl *cc) {
 }
 
 
-static void lastlistfield (FuncState *fs, struct ConsControl *cc) {
+static void lastlistfield (FuncState *fs, struct ConsControl *cc)
+	/*@modifies fs, cc @*/
+{
   if (cc->tostore == 0) return;
   if (cc->v.k == VCALL) {
     luaK_setcallreturns(fs, &cc->v, LUA_MULTRET);
@@ -471,7 +542,9 @@ static void lastlistfield (FuncState *fs, struct ConsControl *cc) {
 }
 
 
-static void listfield (LexState *ls, struct ConsControl *cc) {
+static void listfield (LexState *ls, struct ConsControl *cc)
+	/*@modifies ls, cc @*/
+{
   expr(ls, &cc->v);
   luaX_checklimit(ls, cc->na, MAXARG_Bx, "items in a constructor");
   cc->na++;
@@ -479,7 +552,9 @@ static void listfield (LexState *ls, struct ConsControl *cc) {
 }
 
 
-static void constructor (LexState *ls, expdesc *t) {
+static void constructor (LexState *ls, expdesc *t)
+	/*@modifies ls, t @*/
+{
   /* constructor -> ?? */
   FuncState *fs = ls->fs;
   int line = ls->linenumber;
@@ -525,7 +600,9 @@ static void constructor (LexState *ls, expdesc *t) {
 
 
 
-static void parlist (LexState *ls) {
+static void parlist (LexState *ls)
+	/*@modifies ls @*/
+{
   /* parlist -> [ param { `,' param } ] */
   int nparams = 0;
   int dots = 0;
@@ -542,7 +619,9 @@ static void parlist (LexState *ls) {
 }
 
 
-static void body (LexState *ls, expdesc *e, int needself, int line) {
+static void body (LexState *ls, expdesc *e, int needself, int line)
+	/*@modifies ls, e @*/
+{
   /* body ->  `(' parlist `)' chunk END */
   FuncState new_fs;
   open_func(ls, &new_fs);
@@ -559,7 +638,9 @@ static void body (LexState *ls, expdesc *e, int needself, int line) {
 }
 
 
-static int explist1 (LexState *ls, expdesc *v) {
+static int explist1 (LexState *ls, expdesc *v)
+	/*@modifies ls, v @*/
+{
   /* explist1 -> expr { `,' expr } */
   int n = 1;  /* at least one expression */
   expr(ls, v);
@@ -572,7 +653,9 @@ static int explist1 (LexState *ls, expdesc *v) {
 }
 
 
-static void funcargs (LexState *ls, expdesc *f) {
+static void funcargs (LexState *ls, expdesc *f)
+	/*@modifies ls, f @*/
+{
   FuncState *fs = ls->fs;
   expdesc args;
   int base, nparams;
@@ -630,7 +713,9 @@ static void funcargs (LexState *ls, expdesc *f) {
 */
 
 
-static void prefixexp (LexState *ls, expdesc *v) {
+static void prefixexp (LexState *ls, expdesc *v)
+	/*@modifies ls, v @*/
+{
   /* prefixexp -> NAME | '(' expr ')' */
   switch (ls->t.token) {
     case '(': {
@@ -665,7 +750,9 @@ static void prefixexp (LexState *ls, expdesc *v) {
 }
 
 
-static void primaryexp (LexState *ls, expdesc *v) {
+static void primaryexp (LexState *ls, expdesc *v)
+	/*@modifies ls, v @*/
+{
   /* primaryexp ->
         prefixexp { `.' NAME | `[' exp `]' | `:' NAME funcargs | funcargs } */
   FuncState *fs = ls->fs;
@@ -702,7 +789,9 @@ static void primaryexp (LexState *ls, expdesc *v) {
 }
 
 
-static void simpleexp (LexState *ls, expdesc *v) {
+static void simpleexp (LexState *ls, expdesc *v)
+	/*@modifies ls, v @*/
+{
   /* simpleexp -> NUMBER | STRING | NIL | constructor | FUNCTION body
                | primaryexp */
   switch (ls->t.token) {
@@ -748,7 +837,9 @@ static void simpleexp (LexState *ls, expdesc *v) {
 }
 
 
-static UnOpr getunopr (int op) {
+static UnOpr getunopr (int op)
+	/*@*/
+{
   switch (op) {
     case TK_NOT: return OPR_NOT;
     case '-': return OPR_MINUS;
@@ -757,7 +848,9 @@ static UnOpr getunopr (int op) {
 }
 
 
-static BinOpr getbinopr (int op) {
+static BinOpr getbinopr (int op)
+	/*@*/
+{
   switch (op) {
     case '+': return OPR_ADD;
     case '-': return OPR_SUB;
@@ -778,6 +871,7 @@ static BinOpr getbinopr (int op) {
 }
 
 
+/*@unchecked@*/
 static const struct {
   lu_byte left;  /* left priority for each binary operator */
   lu_byte right; /* right priority */
@@ -796,7 +890,9 @@ static const struct {
 ** subexpr -> (simplexep | unop subexpr) { binop subexpr }
 ** where `binop' is any binary operator with a priority higher than `limit'
 */
-static BinOpr subexpr (LexState *ls, expdesc *v, int limit) {
+static BinOpr subexpr (LexState *ls, expdesc *v, int limit)
+	/*@modifies ls, v @*/
+{
   BinOpr op;
   UnOpr uop;
   enterlevel(ls);
@@ -824,7 +920,9 @@ static BinOpr subexpr (LexState *ls, expdesc *v, int limit) {
 }
 
 
-static void expr (LexState *ls, expdesc *v) {
+static void expr (LexState *ls, expdesc *v)
+	/*@modifies ls @*/
+{
   subexpr(ls, v, -1);
 }
 
@@ -839,7 +937,9 @@ static void expr (LexState *ls, expdesc *v) {
 */
 
 
-static int block_follow (int token) {
+static int block_follow (int token)
+	/*@*/
+{
   switch (token) {
     case TK_ELSE: case TK_ELSEIF: case TK_END:
     case TK_UNTIL: case TK_EOS:
@@ -849,7 +949,9 @@ static int block_follow (int token) {
 }
 
 
-static void block (LexState *ls) {
+static void block (LexState *ls)
+	/*@modifies ls @*/
+{
   /* block -> chunk */
   FuncState *fs = ls->fs;
   BlockCnt bl;
@@ -876,7 +978,9 @@ struct LHS_assign {
 ** local value in a safe place and use this safe copy in the previous
 ** assignment.
 */
-static void check_conflict (LexState *ls, struct LHS_assign *lh, expdesc *v) {
+static void check_conflict (LexState *ls, struct LHS_assign *lh, expdesc *v)
+	/*@modifies ls, lh @*/
+{
   FuncState *fs = ls->fs;
   int extra = fs->freereg;  /* eventual position to save local variable */
   int conflict = 0;
@@ -899,7 +1003,9 @@ static void check_conflict (LexState *ls, struct LHS_assign *lh, expdesc *v) {
 }
 
 
-static void assignment (LexState *ls, struct LHS_assign *lh, int nvars) {
+static void assignment (LexState *ls, struct LHS_assign *lh, int nvars)
+	/*@modifies ls, lh @*/
+{
   expdesc e;
   check_condition(ls, VLOCAL <= lh->v.k && lh->v.k <= VINDEXED,
                       "syntax error");
@@ -931,7 +1037,9 @@ static void assignment (LexState *ls, struct LHS_assign *lh, int nvars) {
 }
 
 
-static void cond (LexState *ls, expdesc *v) {
+static void cond (LexState *ls, expdesc *v)
+	/*@modifies ls, v @*/
+{
   /* cond -> exp */
   expr(ls, v);  /* read condition */
   if (v->k == VNIL) v->k = VFALSE;  /* `falses' are all equal here */
@@ -958,7 +1066,9 @@ static void cond (LexState *ls, expdesc *v) {
 */
 #define EXTRAEXP	5
 
-static void whilestat (LexState *ls, int line) {
+static void whilestat (LexState *ls, int line)
+	/*@modifies ls @*/
+{
   /* whilestat -> WHILE cond DO block END */
   Instruction codeexp[MAXEXPWHILE + EXTRAEXP];
   int lineexp;
@@ -1000,7 +1110,9 @@ static void whilestat (LexState *ls, int line) {
 }
 
 
-static void repeatstat (LexState *ls, int line) {
+static void repeatstat (LexState *ls, int line)
+	/*@modifies ls @*/
+{
   /* repeatstat -> REPEAT block UNTIL cond */
   FuncState *fs = ls->fs;
   int repeat_init = luaK_getlabel(fs);
@@ -1016,7 +1128,9 @@ static void repeatstat (LexState *ls, int line) {
 }
 
 
-static int exp1 (LexState *ls) {
+static int exp1 (LexState *ls)
+	/*@modifies ls @*/
+{
   expdesc e;
   int k;
   expr(ls, &e);
@@ -1026,7 +1140,9 @@ static int exp1 (LexState *ls) {
 }
 
 
-static void forbody (LexState *ls, int base, int line, int nvars, int isnum) {
+static void forbody (LexState *ls, int base, int line, int nvars, int isnum)
+	/*@modifies ls @*/
+{
   BlockCnt bl;
   FuncState *fs = ls->fs;
   int prep, endfor;
@@ -1044,7 +1160,9 @@ static void forbody (LexState *ls, int base, int line, int nvars, int isnum) {
 }
 
 
-static void fornum (LexState *ls, TString *varname, int line) {
+static void fornum (LexState *ls, TString *varname, int line)
+	/*@modifies ls @*/
+{
   /* fornum -> NAME = exp1,exp1[,exp1] DO body */
   FuncState *fs = ls->fs;
   int base = fs->freereg;
@@ -1067,7 +1185,9 @@ static void fornum (LexState *ls, TString *varname, int line) {
 }
 
 
-static void forlist (LexState *ls, TString *indexname) {
+static void forlist (LexState *ls, TString *indexname)
+	/*@modifies ls @*/
+{
   /* forlist -> NAME {,NAME} IN explist1 DO body */
   FuncState *fs = ls->fs;
   expdesc e;
@@ -1088,7 +1208,9 @@ static void forlist (LexState *ls, TString *indexname) {
 }
 
 
-static void forstat (LexState *ls, int line) {
+static void forstat (LexState *ls, int line)
+	/*@modifies ls @*/
+{
   /* forstat -> fornum | forlist */
   FuncState *fs = ls->fs;
   TString *varname;
@@ -1106,7 +1228,9 @@ static void forstat (LexState *ls, int line) {
 }
 
 
-static void test_then_block (LexState *ls, expdesc *v) {
+static void test_then_block (LexState *ls, expdesc *v)
+	/*@modifies ls, v @*/
+{
   /* test_then_block -> [IF | ELSEIF] cond THEN block */
   next(ls);  /* skip IF or ELSEIF */
   cond(ls, v);
@@ -1115,7 +1239,9 @@ static void test_then_block (LexState *ls, expdesc *v) {
 }
 
 
-static void ifstat (LexState *ls, int line) {
+static void ifstat (LexState *ls, int line)
+	/*@modifies ls @*/
+{
   /* ifstat -> IF cond THEN block {ELSEIF cond THEN block} [ELSE block] END */
   FuncState *fs = ls->fs;
   expdesc v;
@@ -1139,7 +1265,9 @@ static void ifstat (LexState *ls, int line) {
 }
 
 
-static void localfunc (LexState *ls) {
+static void localfunc (LexState *ls)
+	/*@modifies ls @*/
+{
   expdesc v, b;
   FuncState *fs = ls->fs;
   new_localvar(ls, str_checkname(ls), 0);
@@ -1153,7 +1281,9 @@ static void localfunc (LexState *ls) {
 }
 
 
-static void localstat (LexState *ls) {
+static void localstat (LexState *ls)
+	/*@modifies ls @*/
+{
   /* stat -> LOCAL NAME {`,' NAME} [`=' explist1] */
   int nvars = 0;
   int nexps;
@@ -1172,7 +1302,9 @@ static void localstat (LexState *ls) {
 }
 
 
-static int funcname (LexState *ls, expdesc *v) {
+static int funcname (LexState *ls, expdesc *v)
+	/*@modifies ls, v @*/
+{
   /* funcname -> NAME {field} [`:' NAME] */
   int needself = 0;
   singlevar(ls, v, 1);
@@ -1186,7 +1318,9 @@ static int funcname (LexState *ls, expdesc *v) {
 }
 
 
-static void funcstat (LexState *ls, int line) {
+static void funcstat (LexState *ls, int line)
+	/*@modifies ls @*/
+{
   /* funcstat -> FUNCTION funcname body */
   int needself;
   expdesc v, b;
@@ -1198,7 +1332,9 @@ static void funcstat (LexState *ls, int line) {
 }
 
 
-static void exprstat (LexState *ls) {
+static void exprstat (LexState *ls)
+	/*@modifies ls @*/
+{
   /* stat -> func | assignment */
   FuncState *fs = ls->fs;
   struct LHS_assign v;
@@ -1213,7 +1349,9 @@ static void exprstat (LexState *ls) {
 }
 
 
-static void retstat (LexState *ls) {
+static void retstat (LexState *ls)
+	/*@modifies ls @*/
+{
   /* stat -> RETURN explist */
   FuncState *fs = ls->fs;
   expdesc e;
@@ -1246,7 +1384,9 @@ static void retstat (LexState *ls) {
 }
 
 
-static void breakstat (LexState *ls) {
+static void breakstat (LexState *ls)
+	/*@modifies ls @*/
+{
   /* stat -> BREAK [NAME] */
   FuncState *fs = ls->fs;
   BlockCnt *bl = fs->bl;
@@ -1264,7 +1404,9 @@ static void breakstat (LexState *ls) {
 }
 
 
-static int statement (LexState *ls) {
+static int statement (LexState *ls)
+	/*@modifies ls @*/
+{
   int line = ls->linenumber;  /* may be needed for error messages */
   switch (ls->t.token) {
     case TK_IF: {  /* stat -> ifstat */
@@ -1317,7 +1459,9 @@ static int statement (LexState *ls) {
 }
 
 
-static void chunk (LexState *ls) {
+static void chunk (LexState *ls)
+	/*@modifies ls @*/
+{
   /* chunk -> { stat [`;'] } */
   int islast = 0;
   enterlevel(ls);
diff --git a/lua/lparser.h b/lua/lparser.h
index d744da33f..ce88a5389 100644
--- a/lua/lparser.h
+++ b/lua/lparser.h
@@ -1,5 +1,5 @@
 /*
-** $Id: lparser.h,v 1.1 2004/03/16 21:58:30 niemeyer Exp $
+** $Id: lparser.h,v 1.2 2004/03/23 05:09:14 jbj Exp $
 ** Lua Parser
 ** See Copyright Notice in lua.h
 */
@@ -46,11 +46,15 @@ struct BlockCnt;  /* defined in lparser.c */
 
 /* state needed to generate code for a given function */
 typedef struct FuncState {
+/*@null@*/
   Proto *f;  /* current function header */
+/*@null@*/
   Table *h;  /* table to find (and reuse) elements in `k' */
+/*@null@*/
   struct FuncState *prev;  /* enclosing function */
   struct LexState *ls;  /* lexical state */
   struct lua_State *L;  /* copy of the Lua state */
+/*@null@*/
   struct BlockCnt *bl;  /* chain of current blocks */
   int pc;  /* next position to code (equivalent to `ncode') */
   int lasttarget;   /* `pc' of last `jump target' */
@@ -65,7 +69,8 @@ typedef struct FuncState {
 } FuncState;
 
 
-Proto *luaY_parser (lua_State *L, ZIO *z, Mbuffer *buff);
+Proto *luaY_parser (lua_State *L, ZIO *z, Mbuffer *buff)
+	/*@modifies L, z @*/;
 
 
 #endif
diff --git a/lua/lstate.c b/lua/lstate.c
index 2165bd0aa..03ca2b1f4 100644
--- a/lua/lstate.c
+++ b/lua/lstate.c
@@ -1,5 +1,5 @@
 /*
-** $Id: lstate.c,v 1.1 2004/03/16 21:58:30 niemeyer Exp $
+** $Id: lstate.c,v 1.2 2004/03/23 05:09:14 jbj Exp $
 ** Global State
 ** See Copyright Notice in lua.h
 */
@@ -39,13 +39,18 @@ union UEXTRASPACE {L_Umaxalign a; LUA_USERSTATE b;};
 ** you can change this function through the official API:
 ** call `lua_setpanicf'
 */
-static int default_panic (lua_State *L) {
+static int default_panic (lua_State *L)
+	/*@*/
+{
   UNUSED(L);
   return 0;
 }
 
 
-static lua_State *mallocstate (lua_State *L) {
+/*@null@*/
+static lua_State *mallocstate (/*@null@*/ lua_State *L)
+	/*@modifies L @*/
+{
   lu_byte *block = (lu_byte *)luaM_malloc(L, sizeof(lua_State) + EXTRASPACE);
   if (block == NULL) return NULL;
   else {
@@ -55,13 +60,17 @@ static lua_State *mallocstate (lua_State *L) {
 }
 
 
-static void freestate (lua_State *L, lua_State *L1) {
+static void freestate (/*@null@*/ lua_State *L, lua_State *L1)
+	/*@modifies L @*/
+{
   luaM_free(L, cast(lu_byte *, L1) - EXTRASPACE,
                sizeof(lua_State) + EXTRASPACE);
 }
 
 
-static void stack_init (lua_State *L1, lua_State *L) {
+static void stack_init (lua_State *L1, lua_State *L)
+	/*@modifies L1, L @*/
+{
   L1->stack = luaM_newvector(L, BASIC_STACK_SIZE + EXTRA_STACK, TObject);
   L1->stacksize = BASIC_STACK_SIZE + EXTRA_STACK;
   L1->top = L1->stack;
@@ -77,7 +86,9 @@ static void stack_init (lua_State *L1, lua_State *L) {
 }
 
 
-static void freestack (lua_State *L, lua_State *L1) {
+static void freestack (lua_State *L, lua_State *L1)
+	/*@modifies L, L1 @*/
+{
   luaM_freearray(L, L1->base_ci, L1->size_ci, CallInfo);
   luaM_freearray(L, L1->stack, L1->stacksize, TObject);
 }
@@ -86,7 +97,9 @@ static void freestack (lua_State *L, lua_State *L1) {
 /*
 ** open parts that may cause memory-allocation errors
 */
-static void f_luaopen (lua_State *L, void *ud) {
+static void f_luaopen (lua_State *L, void *ud)
+	/*@modifies L @*/
+{
   /* create a new global state */
   global_State *g = luaM_new(NULL, global_State);
   UNUSED(ud);
@@ -123,7 +136,9 @@ static void f_luaopen (lua_State *L, void *ud) {
 }
 
 
-static void preinit_state (lua_State *L) {
+static void preinit_state (lua_State *L)
+	/*@modifies L @*/
+{
   L->stack = NULL;
   L->stacksize = 0;
   L->errorJmp = NULL;
@@ -135,13 +150,15 @@ static void preinit_state (lua_State *L) {
   L->openupval = NULL;
   L->size_ci = 0;
   L->nCcalls = 0;
-  L->base_ci = L->ci = NULL;
+  L->ci = L->base_ci = NULL;
   L->errfunc = 0;
   setnilvalue(gt(L));
 }
 
 
-static void close_state (lua_State *L) {
+static void close_state (lua_State *L)
+	/*@modifies L @*/
+{
   luaF_close(L, L->stack);  /* close all upvalues for this thread */
   if (G(L)) {  /* close global state */
     luaC_sweep(L, 1);  /* collect all elements */
@@ -178,6 +195,7 @@ void luaE_freethread (lua_State *L, lua_State *L1) {
 }
 
 
+/*@null@*/
 LUA_API lua_State *lua_open (void) {
   lua_State *L = mallocstate(NULL);
   if (L) {  /* allocation OK? */
@@ -197,7 +215,9 @@ LUA_API lua_State *lua_open (void) {
 }
 
 
-static void callallgcTM (lua_State *L, void *ud) {
+static void callallgcTM (lua_State *L, void *ud)
+	/*@modifies L @*/
+{
   UNUSED(ud);
   luaC_callGCTM(L);  /* call GC metamethods for all udata */
 }
diff --git a/lua/lstate.h b/lua/lstate.h
index 40fd160af..de79fe866 100644
--- a/lua/lstate.h
+++ b/lua/lstate.h
@@ -1,5 +1,5 @@
 /*
-** $Id: lstate.h,v 1.1 2004/03/16 21:58:30 niemeyer Exp $
+** $Id: lstate.h,v 1.2 2004/03/23 05:09:14 jbj Exp $
 ** Global State
 ** See Copyright Notice in lua.h
 */
@@ -63,6 +63,7 @@ struct lua_longjmp;  /* defined in ldo.c */
 
 
 typedef struct stringtable {
+/*@null@*/
   GCObject **hash;
   ls_nstr nuse;  /* number of elements */
   int size;
@@ -73,12 +74,16 @@ typedef struct stringtable {
 ** informations about a call
 */
 typedef struct CallInfo {
+/*@dependent@*/ /*@relnull@*/
   StkId base;  /* base for called function */
+/*@dependent@*/ /*@relnull@*/
   StkId	top;  /* top for this function */
   int state;  /* bit fields; see below */
   union {
     struct {  /* for Lua functions */
+/*@observer@*/
       const Instruction *savedpc;
+/*@observer@*/
       const Instruction **pc;  /* points to `pc' variable in `luaV_execute' */
       int tailcalls;  /* number of tail calls lost under this entry */
     } l;
@@ -110,8 +115,11 @@ typedef struct CallInfo {
 */
 typedef struct global_State {
   stringtable strt;  /* hash table for strings */
+/*@owned@*/
   GCObject *rootgc;  /* list of (almost) all collectable objects */
+/*@dependent@*/ /*@null@*/
   GCObject *rootudata;   /* (separated) list of all userdata */
+/*@dependent@*/ /*@null@*/
   GCObject *tmudata;  /* list of userdata to be GC */
   Mbuffer buff;  /* temporary buffer for string concatentation */
   lu_mem GCthreshold;
@@ -130,14 +138,22 @@ typedef struct global_State {
 */
 struct lua_State {
   CommonHeader;
+/*@dependent@*/ /*@relnull@*/
   StkId top;  /* first free slot in the stack */
+/*@dependent@*/ /*@relnull@*/
   StkId base;  /* base of current function */
+/*@relnull@*/
   global_State *l_G;
+/*@dependent@*/ /*@relnull@*/
   CallInfo *ci;  /* call info for current function */
+/*@dependent@*/
   StkId stack_last;  /* last free slot in the stack */
+/*@owned@*/ /*@relnull@*/
   StkId stack;  /* stack base */
   int stacksize;
+/*@dependent@*/ /*@relnull@*/
   CallInfo *end_ci;  /* points after end of ci array*/
+/*@owned@*/ /*@relnull@*/
   CallInfo *base_ci;  /* array of CallInfo's */
   unsigned short size_ci;  /* size of array `base_ci' */
   unsigned short nCcalls;  /* number of nested C calls */
@@ -146,10 +162,14 @@ struct lua_State {
   lu_byte hookinit;
   int basehookcount;
   int hookcount;
+/*@relnull@*/
   lua_Hook hook;
   TObject _gt;  /* table of globals */
+/*@dependent@*/ /*@relnull@*/
   GCObject *openupval;  /* list of open upvalues in this stack */
+/*@dependent@*/ /*@relnull@*/
   GCObject *gclist;
+/*@relnull@*/
   struct lua_longjmp *errorJmp;  /* current error recover point */
   ptrdiff_t errfunc;  /* current error handling function (stack index) */
 };
@@ -188,8 +208,11 @@ union GCObject {
 #define valtogco(v)	(cast(GCObject *, (v)))
 
 
-lua_State *luaE_newthread (lua_State *L);
-void luaE_freethread (lua_State *L, lua_State *L1);
+/*@null@*/
+lua_State *luaE_newthread (lua_State *L)
+	/*@modifies L @*/;
+void luaE_freethread (lua_State *L, lua_State *L1)
+	/*@modifies L, L1 @*/;
 
 #endif
 
diff --git a/lua/lstring.c b/lua/lstring.c
index 8f194ec8a..3ef0c9c10 100644
--- a/lua/lstring.c
+++ b/lua/lstring.c
@@ -1,5 +1,5 @@
 /*
-** $Id: lstring.c,v 1.1 2004/03/16 21:58:30 niemeyer Exp $
+** $Id: lstring.c,v 1.2 2004/03/23 05:09:14 jbj Exp $
 ** String table (keeps all strings handled by Lua)
 ** See Copyright Notice in lua.h
 */
@@ -48,7 +48,10 @@ void luaS_resize (lua_State *L, int newsize) {
 }
 
 
-static TString *newlstr (lua_State *L, const char *str, size_t l, lu_hash h) {
+/*@null@*/
+static TString *newlstr (lua_State *L, const char *str, size_t l, lu_hash h)
+	/*@modifies L @*/
+{
   TString *ts = cast(TString *, luaM_malloc(L, sizestring(l)));
   stringtable *tb;
   ts->tsv.len = l;
diff --git a/lua/lstring.h b/lua/lstring.h
index 099524c1c..90e88264e 100644
--- a/lua/lstring.h
+++ b/lua/lstring.h
@@ -1,5 +1,5 @@
 /*
-** $Id: lstring.h,v 1.1 2004/03/16 21:58:30 niemeyer Exp $
+** $Id: lstring.h,v 1.2 2004/03/23 05:09:14 jbj Exp $
 ** String table (keep all strings handled by Lua)
 ** See Copyright Notice in lua.h
 */
@@ -24,10 +24,16 @@
 
 #define luaS_fix(s)	((s)->tsv.marked |= (1<<4))
 
-void luaS_resize (lua_State *L, int newsize);
-Udata *luaS_newudata (lua_State *L, size_t s);
-void luaS_freeall (lua_State *L);
-TString *luaS_newlstr (lua_State *L, const char *str, size_t l);
+void luaS_resize (lua_State *L, int newsize)
+	/*@modifies L @*/;
+/*@null@*/
+Udata *luaS_newudata (lua_State *L, size_t s)
+	/*@modifies L @*/;
+void luaS_freeall (lua_State *L)
+	/*@modifies L @*/;
+/*@null@*/
+TString *luaS_newlstr (lua_State *L, /*@null@*/ const char *str, size_t l)
+	/*@modifies L @*/;
 
 
 #endif
diff --git a/lua/ltable.c b/lua/ltable.c
index 70aef3894..bda8865bb 100644
--- a/lua/ltable.c
+++ b/lua/ltable.c
@@ -1,5 +1,5 @@
 /*
-** $Id: ltable.c,v 1.1 2004/03/16 21:58:30 niemeyer Exp $
+** $Id: ltable.c,v 1.2 2004/03/23 05:09:14 jbj Exp $
 ** Lua tables (hash)
 ** See Copyright Notice in lua.h
 */
@@ -80,7 +80,9 @@
 /*
 ** hash for lua_Numbers
 */
-static Node *hashnum (const Table *t, lua_Number n) {
+static Node *hashnum (const Table *t, lua_Number n)
+	/*@*/
+{
   unsigned int a[numints];
   int i;
   n += 1;  /* normalize number (avoid -0) */
@@ -116,7 +118,9 @@ Node *luaH_mainposition (const Table *t, const TObject *key) {
 ** returns the index for `key' if `key' is an appropriate key to live in
 ** the array part of the table, -1 otherwise.
 */
-static int arrayindex (const TObject *key) {
+static int arrayindex (const TObject *key)
+	/*@*/
+{
   if (ttisnumber(key)) {
     int k;
     lua_number2int(k, (nvalue(key)));
@@ -132,7 +136,9 @@ static int arrayindex (const TObject *key) {
 ** elements in the array part, then elements in the hash part. The
 ** beginning and end of a traversal are signalled by -1.
 */
-static int luaH_index (lua_State *L, Table *t, StkId key) {
+static int luaH_index (lua_State *L, Table *t, StkId key)
+	/*@modifies L @*/
+{
   int i;
   if (ttisnil(key)) return -1;  /* first iteration */
   i = arrayindex(key);
@@ -177,7 +183,9 @@ int luaH_next (lua_State *L, Table *t, StkId key) {
 */
 
 
-static void computesizes  (int nums[], int ntotal, int *narray, int *nhash) {
+static void computesizes  (int nums[], int ntotal, int *narray, int *nhash)
+	/*@modifies *narray, *nhash @*/
+{
   int i;
   int a = nums[0];  /* number of elements smaller than 2^i */
   int na = a;  /* number of elements to go to array part */
@@ -198,7 +206,9 @@ static void computesizes  (int nums[], int ntotal, int *narray, int *nhash) {
 }
 
 
-static void numuse (const Table *t, int *narray, int *nhash) {
+static void numuse (const Table *t, int *narray, int *nhash)
+	/*@modifies *narray, *nhash @*/
+{
   int nums[MAXBITS+1];
   int i, lg;
   int totaluse = 0;
@@ -236,7 +246,9 @@ static void numuse (const Table *t, int *narray, int *nhash) {
 }
 
 
-static void setarrayvector (lua_State *L, Table *t, int size) {
+static void setarrayvector (lua_State *L, Table *t, int size)
+	/*@modifies L, t @*/
+{
   int i;
   luaM_reallocvector(L, t->array, t->sizearray, size, TObject);
   for (i=t->sizearray; i<size; i++)
@@ -245,7 +257,9 @@ static void setarrayvector (lua_State *L, Table *t, int size) {
 }
 
 
-static void setnodevector (lua_State *L, Table *t, int lsize) {
+static void setnodevector (lua_State *L, Table *t, int lsize)
+	/*@modifies L, t @*/
+{
   int i;
   int size = twoto(lsize);
   if (lsize > MAXBITS)
@@ -269,7 +283,9 @@ static void setnodevector (lua_State *L, Table *t, int lsize) {
 }
 
 
-static void resize (lua_State *L, Table *t, int nasize, int nhsize) {
+static void resize (lua_State *L, Table *t, int nasize, int nhsize)
+	/*@modifies L, t @*/
+{
   int i;
   int oldasize = t->sizearray;
   int oldhsize = t->lsizenode;
@@ -311,7 +327,9 @@ static void resize (lua_State *L, Table *t, int nasize, int nhsize) {
 }
 
 
-static void rehash (lua_State *L, Table *t) {
+static void rehash (lua_State *L, Table *t)
+	/*@modifies L, t @*/
+{
   int nasize, nhsize;
   numuse(t, &nasize, &nhsize);  /* compute new sizes for array and hash parts */
   resize(L, t, nasize, luaO_log2(nhsize)+1);
@@ -376,7 +394,9 @@ void luaH_remove (Table *t, Node *e) {
 ** put new key in its main position; otherwise (colliding node is in its main 
 ** position), new key goes to an empty position. 
 */
-static TObject *newkey (lua_State *L, Table *t, const TObject *key) {
+static TObject *newkey (lua_State *L, Table *t, const TObject *key)
+	/*@modifies L, t @*/
+{
   TObject *val;
   Node *mp = luaH_mainposition(t, key);
   if (!ttisnil(gval(mp))) {  /* main position is not free? */
@@ -411,14 +431,19 @@ static TObject *newkey (lua_State *L, Table *t, const TObject *key) {
   val = cast(TObject *, luaH_get(t, key));  /* get new position */
   lua_assert(ttisboolean(val));
   setnilvalue(val);
+/*@-observertrans -dependenttrans @*/
   return val;
+/*@=observertrans =dependenttrans @*/
 }
 
 
 /*
 ** generic search function
 */
-static const TObject *luaH_getany (Table *t, const TObject *key) {
+/*@observer@*/
+static const TObject *luaH_getany (Table *t, const TObject *key)
+	/*@*/
+{
   if (ttisnil(key)) return &luaO_nilobject;
   else {
     Node *n = luaH_mainposition(t, key);
@@ -486,7 +511,9 @@ TObject *luaH_set (lua_State *L, Table *t, const TObject *key) {
   const TObject *p = luaH_get(t, key);
   t->flags = 0;
   if (p != &luaO_nilobject)
+/*@-observertrans -dependenttrans @*/
     return cast(TObject *, p);
+/*@=observertrans =dependenttrans @*/
   else {
     if (ttisnil(key)) luaG_runerror(L, "table index is nil");
     else if (ttisnumber(key) && nvalue(key) != nvalue(key))
@@ -499,7 +526,9 @@ TObject *luaH_set (lua_State *L, Table *t, const TObject *key) {
 TObject *luaH_setnum (lua_State *L, Table *t, int key) {
   const TObject *p = luaH_getnum(t, key);
   if (p != &luaO_nilobject)
+/*@-observertrans -dependenttrans @*/
     return cast(TObject *, p);
+/*@=observertrans =dependenttrans @*/
   else {
     TObject k;
     setnvalue(&k, cast(lua_Number, key));
diff --git a/lua/ltable.h b/lua/ltable.h
index 10f412a2f..563c19f79 100644
--- a/lua/ltable.h
+++ b/lua/ltable.h
@@ -1,5 +1,5 @@
 /*
-** $Id: ltable.h,v 1.1 2004/03/16 21:58:30 niemeyer Exp $
+** $Id: ltable.h,v 1.2 2004/03/23 05:09:14 jbj Exp $
 ** Lua tables (hash)
 ** See Copyright Notice in lua.h
 */
@@ -15,17 +15,30 @@
 #define gval(n)		(&(n)->i_val)
 
 
-const TObject *luaH_getnum (Table *t, int key);
-TObject *luaH_setnum (lua_State *L, Table *t, int key);
-const TObject *luaH_getstr (Table *t, TString *key);
-const TObject *luaH_get (Table *t, const TObject *key);
-TObject *luaH_set (lua_State *L, Table *t, const TObject *key);
-Table *luaH_new (lua_State *L, int narray, int lnhash);
-void luaH_free (lua_State *L, Table *t);
-int luaH_next (lua_State *L, Table *t, StkId key);
+/*@observer@*/
+const TObject *luaH_getnum (Table *t, int key)
+	/*@*/;
+TObject *luaH_setnum (lua_State *L, Table *t, int key)
+	/*@modifies L, t @*/;
+/*@observer@*/
+const TObject *luaH_getstr (Table *t, TString *key)
+	/*@*/;
+/*@observer@*/
+const TObject *luaH_get (Table *t, const TObject *key)
+	/*@*/;
+TObject *luaH_set (lua_State *L, Table *t, const TObject *key)
+	/*@modifies L, t @*/;
+/*@null@*/
+Table *luaH_new (lua_State *L, int narray, int lnhash)
+	/*@modifies L @*/;
+void luaH_free (lua_State *L, Table *t)
+	/*@modifies L, t @*/;
+int luaH_next (lua_State *L, Table *t, StkId key)
+	/*@modifies L, key @*/;
 
 /* exported only for debugging */
-Node *luaH_mainposition (const Table *t, const TObject *key);
+Node *luaH_mainposition (const Table *t, const TObject *key)
+	/*@*/;
 
 
 #endif
diff --git a/lua/ltests.c b/lua/ltests.c
index f2cab4d36..317da2df0 100644
--- a/lua/ltests.c
+++ b/lua/ltests.c
@@ -1,5 +1,5 @@
 /*
-** $Id: ltests.c,v 1.1 2004/03/16 21:58:30 niemeyer Exp $
+** $Id: ltests.c,v 1.2 2004/03/23 05:09:14 jbj Exp $
 ** Internal Module for Debugging of the Lua Implementation
 ** See Copyright Notice in lua.h
 */
@@ -47,7 +47,9 @@ int islocked = 0;
 #define func_at(L,k)	(L->ci->base+(k) - 1)
 
 
-static void setnameval (lua_State *L, const char *name, int val) {
+static void setnameval (lua_State *L, const char *name, int val)
+	/*@*/
+{
   lua_pushstring(L, name);
   lua_pushintegral(L, val);
   lua_settable(L, -3);
@@ -86,7 +88,9 @@ unsigned long memdebug_maxmem = 0;
 unsigned long memdebug_memlimit = ULONG_MAX;
 
 
-static void *checkblock (void *block, size_t size) {
+static void *checkblock (void *block, size_t size)
+	/*@*/
+{
   void *b = blockhead(block);
   int i;
   for (i=0;i<MARKSIZE;i++)
@@ -95,7 +99,9 @@ static void *checkblock (void *block, size_t size) {
 }
 
 
-static void freeblock (void *block, size_t size) {
+static void freeblock (void *block, size_t size)
+	/*@*/
+{
   if (block) {
     lua_assert(checkblocksize(block, size));
     block = checkblock(block, size);
@@ -154,7 +160,9 @@ void *debug_realloc (void *block, size_t oldsize, size_t size) {
 */
 
 
-static char *buildop (Proto *p, int pc, char *buff) {
+static char *buildop (Proto *p, int pc, char *buff)
+	/*@*/
+{
   Instruction i = p->code[pc];
   OpCode o = GET_OPCODE(i);
   const char *name = luaP_opnames[o];
@@ -188,7 +196,9 @@ void luaI_printcode (Proto *pt, int size) {
 #endif
 
 
-static int listcode (lua_State *L) {
+static int listcode (lua_State *L)
+	/*@*/
+{
   int pc;
   Proto *p;
   luaL_argcheck(L, lua_isfunction(L, 1) && !lua_iscfunction(L, 1),
@@ -207,7 +217,9 @@ static int listcode (lua_State *L) {
 }
 
 
-static int listk (lua_State *L) {
+static int listk (lua_State *L)
+	/*@*/
+{
   Proto *p;
   int i;
   luaL_argcheck(L, lua_isfunction(L, 1) && !lua_iscfunction(L, 1),
@@ -223,7 +235,9 @@ static int listk (lua_State *L) {
 }
 
 
-static int listlocals (lua_State *L) {
+static int listlocals (lua_State *L)
+	/*@*/
+{
   Proto *p;
   int pc = luaL_checkint(L, 2) - 1;
   int i = 0;
@@ -241,7 +255,9 @@ static int listlocals (lua_State *L) {
 
 
 
-static int get_limits (lua_State *L) {
+static int get_limits (lua_State *L)
+	/*@*/
+{
   lua_newtable(L);
   setnameval(L, "BITS_INT", BITS_INT);
   setnameval(L, "LFPF", LFIELDS_PER_FLUSH);
@@ -253,7 +269,9 @@ static int get_limits (lua_State *L) {
 }
 
 
-static int mem_query (lua_State *L) {
+static int mem_query (lua_State *L)
+	/*@*/
+{
   if (lua_isnone(L, 1)) {
     lua_pushintegral(L, memdebug_total);
     lua_pushintegral(L, memdebug_numblocks);
@@ -267,7 +285,9 @@ static int mem_query (lua_State *L) {
 }
 
 
-static int hash_query (lua_State *L) {
+static int hash_query (lua_State *L)
+	/*@*/
+{
   if (lua_isnone(L, 2)) {
     luaL_argcheck(L, lua_type(L, 1) == LUA_TSTRING, 1, "string expected");
     lua_pushintegral(L, tsvalue(func_at(L, 1))->tsv.hash);
@@ -283,7 +303,9 @@ static int hash_query (lua_State *L) {
 }
 
 
-static int stacklevel (lua_State *L) {
+static int stacklevel (lua_State *L)
+	/*@*/
+{
   unsigned long a = 0;
   lua_pushintegral(L, (int)(L->top - L->stack));
   lua_pushintegral(L, (int)(L->stack_last - L->stack));
@@ -294,7 +316,9 @@ static int stacklevel (lua_State *L) {
 }
 
 
-static int table_query (lua_State *L) {
+static int table_query (lua_State *L)
+	/*@*/
+{
   const Table *t;
   int i = luaL_optint(L, 2, -1);
   luaL_checktype(L, 1, LUA_TTABLE);
@@ -327,7 +351,9 @@ static int table_query (lua_State *L) {
 }
 
 
-static int string_query (lua_State *L) {
+static int string_query (lua_State *L)
+	/*@*/
+{
   stringtable *tb = &G(L)->strt;
   int s = luaL_optint(L, 2, 0) - 1;
   if (s==-1) {
@@ -349,7 +375,9 @@ static int string_query (lua_State *L) {
 }
 
 
-static int tref (lua_State *L) {
+static int tref (lua_State *L)
+	/*@*/
+{
   int level = lua_gettop(L);
   int lock = luaL_optint(L, 2, 1);
   luaL_checkany(L, 1);
@@ -359,21 +387,27 @@ static int tref (lua_State *L) {
   return 1;
 }
 
-static int getref (lua_State *L) {
+static int getref (lua_State *L)
+	/*@*/
+{
   int level = lua_gettop(L);
   lua_getref(L, luaL_checkint(L, 1));
   assert(lua_gettop(L) == level+1);
   return 1;
 }
 
-static int unref (lua_State *L) {
+static int unref (lua_State *L)
+	/*@*/
+{
   int level = lua_gettop(L);
   lua_unref(L, luaL_checkint(L, 1));
   assert(lua_gettop(L) == level);
   return 0;
 }
 
-static int metatable (lua_State *L) {
+static int metatable (lua_State *L)
+	/*@*/
+{
   luaL_checkany(L, 1);
   if (lua_isnone(L, 2)) {
     if (lua_getmetatable(L, 1) == 0)
@@ -388,7 +422,9 @@ static int metatable (lua_State *L) {
 }
 
 
-static int upvalue (lua_State *L) {
+static int upvalue (lua_State *L)
+	/*@*/
+{
   int n = luaL_checkint(L, 2);
   luaL_checktype(L, 1, LUA_TFUNCTION);
   if (lua_isnone(L, 3)) {
@@ -405,7 +441,9 @@ static int upvalue (lua_State *L) {
 }
 
 
-static int newuserdata (lua_State *L) {
+static int newuserdata (lua_State *L)
+	/*@*/
+{
   size_t size = luaL_checkint(L, 1);
   char *p = cast(char *, lua_newuserdata(L, size));
   while (size--) *p++ = '\0';
@@ -413,19 +451,25 @@ static int newuserdata (lua_State *L) {
 }
 
 
-static int pushuserdata (lua_State *L) {
+static int pushuserdata (lua_State *L)
+	/*@*/
+{
   lua_pushlightuserdata(L, cast(void *, luaL_checkint(L, 1)));
   return 1;
 }
 
 
-static int udataval (lua_State *L) {
+static int udataval (lua_State *L)
+	/*@*/
+{
   lua_pushintegral(L, cast(int, lua_touserdata(L, 1)));
   return 1;
 }
 
 
-static int doonnewstack (lua_State *L) {
+static int doonnewstack (lua_State *L)
+	/*@*/
+{
   lua_State *L1 = lua_newthread(L);
   size_t l;
   const char *s = luaL_checklstring(L, 1, &l);
@@ -437,19 +481,25 @@ static int doonnewstack (lua_State *L) {
 }
 
 
-static int s2d (lua_State *L) {
+static int s2d (lua_State *L)
+	/*@*/
+{
   lua_pushnumber(L, *cast(const double *, luaL_checkstring(L, 1)));
   return 1;
 }
 
-static int d2s (lua_State *L) {
+static int d2s (lua_State *L)
+	/*@*/
+{
   double d = luaL_checknumber(L, 1);
   lua_pushlstring(L, cast(char *, &d), sizeof(d));
   return 1;
 }
 
 
-static int newstate (lua_State *L) {
+static int newstate (lua_State *L)
+	/*@*/
+{
   lua_State *L1 = lua_open();
   if (L1) {
     lua_userstateopen(L1);  /* init lock */
@@ -461,7 +511,9 @@ static int newstate (lua_State *L) {
 }
 
 
-static int loadlib (lua_State *L) {
+static int loadlib (lua_State *L)
+	/*@*/
+{
   static const luaL_reg libs[] = {
     {"mathlibopen", luaopen_math},
     {"strlibopen", luaopen_string},
@@ -478,14 +530,18 @@ static int loadlib (lua_State *L) {
   return 0;
 }
 
-static int closestate (lua_State *L) {
+static int closestate (lua_State *L)
+	/*@*/
+{
   lua_State *L1 = cast(lua_State *, cast(unsigned long, luaL_checknumber(L, 1)));
   lua_close(L1);
   lua_unlock(L);  /* close cannot unlock that */
   return 0;
 }
 
-static int doremote (lua_State *L) {
+static int doremote (lua_State *L)
+	/*@*/
+{
   lua_State *L1 = cast(lua_State *,cast(unsigned long,luaL_checknumber(L, 1)));
   size_t lcode;
   const char *code = luaL_checklstring(L, 2, &lcode);
@@ -510,12 +566,16 @@ static int doremote (lua_State *L) {
 }
 
 
-static int log2_aux (lua_State *L) {
+static int log2_aux (lua_State *L)
+	/*@*/
+{
   lua_pushintegral(L, luaO_log2(luaL_checkint(L, 1)));
   return 1;
 }
 
-static int int2fb_aux (lua_State *L) {
+static int int2fb_aux (lua_State *L)
+	/*@*/
+{
   int b = luaO_int2fb(luaL_checkint(L, 1));
   lua_pushintegral(L, b);
   lua_pushintegral(L, fb2int(b));
@@ -523,7 +583,9 @@ static int int2fb_aux (lua_State *L) {
 }
 
 
-static int test_do (lua_State *L) {
+static int test_do (lua_State *L)
+	/*@*/
+{
   const char *p = luaL_checkstring(L, 1);
   if (*p == '@')
     lua_dofile(L, p+1);
@@ -543,11 +605,15 @@ static int test_do (lua_State *L) {
 
 static const char *const delimits = " \t\n,;";
 
-static void skip (const char **pc) {
+static void skip (const char **pc)
+	/*@*/
+{
   while (**pc != '\0' && strchr(delimits, **pc)) (*pc)++;
 }
 
-static int getnum_aux (lua_State *L, const char **pc) {
+static int getnum_aux (lua_State *L, const char **pc)
+	/*@*/
+{
   int res = 0;
   int sig = 1;
   skip(pc);
@@ -565,7 +631,9 @@ static int getnum_aux (lua_State *L, const char **pc) {
   return sig*res;
 }
   
-static const char *getname_aux (char *buff, const char **pc) {
+static const char *getname_aux (char *buff, const char **pc)
+	/*@*/
+{
   int i = 0;
   skip(pc);
   while (**pc != '\0' && !strchr(delimits, **pc))
@@ -581,7 +649,9 @@ static const char *getname_aux (char *buff, const char **pc) {
 #define getname	(getname_aux(buff, &pc))
 
 
-static int testC (lua_State *L) {
+static int testC (lua_State *L)
+	/*@*/
+{
   char buff[30];
   const char *pc = luaL_checkstring(L, 1);
   for (;;) {
@@ -741,11 +811,15 @@ static int testC (lua_State *L) {
 ** =======================================================
 */
 
-static void yieldf (lua_State *L, lua_Debug *ar) {
+static void yieldf (lua_State *L, lua_Debug *ar)
+	/*@*/
+{
   lua_yield(L, 0);
 }
 
-static int setyhook (lua_State *L) {
+static int setyhook (lua_State *L)
+	/*@*/
+{
   if (lua_isnoneornil(L, 1))
     lua_sethook(L, NULL, 0, 0);  /* turn off hooks */
   else {
@@ -760,7 +834,9 @@ static int setyhook (lua_State *L) {
 }
 
 
-static int coresume (lua_State *L) {
+static int coresume (lua_State *L)
+	/*@*/
+{
   int status;
   lua_State *co = lua_tothread(L, 1);
   luaL_argcheck(L, co, 1, "coroutine expected");
@@ -815,7 +891,9 @@ static const struct luaL_reg tests_funcs[] = {
 };
 
 
-static void fim (void) {
+static void fim (void)
+	/*@*/
+{
   if (!islocked)
     lua_close(lua_state);
   lua_assert(memdebug_numblocks == 0);
@@ -823,7 +901,9 @@ static void fim (void) {
 }
 
 
-static int l_panic (lua_State *L) {
+static int l_panic (lua_State *L)
+	/*@*/
+{
   UNUSED(L);
   fprintf(stderr, "unable to recover; exiting\n");
   return 0;
diff --git a/lua/ltm.c b/lua/ltm.c
index 21dc34b28..519c21608 100644
--- a/lua/ltm.c
+++ b/lua/ltm.c
@@ -1,5 +1,5 @@
 /*
-** $Id: ltm.c,v 1.1 2004/03/16 21:58:30 niemeyer Exp $
+** $Id: ltm.c,v 1.2 2004/03/23 05:09:14 jbj Exp $
 ** Tag methods
 ** See Copyright Notice in lua.h
 */
@@ -19,6 +19,7 @@
 
 
 
+/*@observer@*/
 const char *const luaT_typenames[] = {
   "nil", "boolean", "userdata", "number",
   "string", "table", "function", "userdata", "thread"
@@ -26,6 +27,7 @@ const char *const luaT_typenames[] = {
 
 
 void luaT_init (lua_State *L) {
+/*@observer@*/
   static const char *const luaT_eventname[] = {  /* ORDER TM */
     "__index", "__newindex",
     "__gc", "__mode", "__eq",
@@ -56,7 +58,8 @@ const TObject *luaT_gettm (Table *events, TMS event, TString *ename) {
 }
 
 
-const TObject *luaT_gettmbyobj (lua_State *L, const TObject *o, TMS event) {
+const TObject *luaT_gettmbyobj (lua_State *L, const TObject *o, TMS event)
+{
   TString *ename = G(L)->tmname[event];
   switch (ttype(o)) {
     case LUA_TTABLE:
diff --git a/lua/ltm.h b/lua/ltm.h
index b6d8fa1fe..67d9322b7 100644
--- a/lua/ltm.h
+++ b/lua/ltm.h
@@ -1,5 +1,5 @@
 /*
-** $Id: ltm.h,v 1.1 2004/03/16 21:58:30 niemeyer Exp $
+** $Id: ltm.h,v 1.2 2004/03/23 05:09:14 jbj Exp $
 ** Tag methods
 ** See Copyright Notice in lua.h
 */
@@ -42,10 +42,16 @@ typedef enum {
 #define fasttm(l,et,e)	gfasttm(G(l), et, e)
 
 
-const TObject *luaT_gettm (Table *events, TMS event, TString *ename);
-const TObject *luaT_gettmbyobj (lua_State *L, const TObject *o, TMS event);
-void luaT_init (lua_State *L);
+/*@observer@*/ /*@null@*/
+const TObject *luaT_gettm (Table *events, TMS event, TString *ename)
+	/*@modifies events @*/;
+/*@observer@*/
+const TObject *luaT_gettmbyobj (lua_State *L, const TObject *o, TMS event)
+	/*@*/;
+void luaT_init (lua_State *L)
+	/*@modifies L @*/;
 
+/*@unchecked@*/
 extern const char *const luaT_typenames[];
 
 #endif
diff --git a/lua/lua/.cvsignore b/lua/lua/.cvsignore
new file mode 100644
index 000000000..28a08d461
--- /dev/null
+++ b/lua/lua/.cvsignore
@@ -0,0 +1,3 @@
+.dirstamp
+.libs
+lua
diff --git a/lua/lua/lua.c b/lua/lua/lua.c
index 2de41782f..b9feede28 100644
--- a/lua/lua/lua.c
+++ b/lua/lua/lua.c
@@ -1,5 +1,5 @@
 /*
-** $Id: lua.c,v 1.1 2004/03/16 21:58:30 niemeyer Exp $
+** $Id: lua.c,v 1.2 2004/03/23 05:09:14 jbj Exp $
 ** Lua stand-alone interpreter
 ** See Copyright Notice in lua.h
 */
@@ -61,12 +61,16 @@
 #endif
 
 
+/*@unchecked@*/ /*@relnull@*/
 static lua_State *L = NULL;
 
+/*@-readonlytrans@*/
+/*@unchecked@*/ /*@relnull@*/
 static const char *progname = PROGNAME;
 
 
 
+/*@unchecked@*/
 static const luaL_reg lualibs[] = {
   {"base", luaopen_base},
   {"table", luaopen_table},
@@ -79,24 +83,33 @@ static const luaL_reg lualibs[] = {
   LUA_EXTRALIBS
   {NULL, NULL}
 };
+/*@=readonlytrans@*/
 
 
 
-static void lstop (lua_State *l, lua_Debug *ar) {
+static void lstop (lua_State *l, lua_Debug *ar)
+	/*@modifies l @*/
+{
   (void)ar;  /* unused arg. */
   lua_sethook(l, NULL, 0, 0);
   luaL_error(l, "interrupted!");
 }
 
 
-static void laction (int i) {
+static void laction (int i)
+	/*@globals internalState @*/
+	/*@modifies internalState @*/
+{
   signal(i, SIG_DFL); /* if another SIGINT happens before lstop,
                               terminate process (default action) */
   lua_sethook(L, lstop, LUA_MASKCALL | LUA_MASKRET | LUA_MASKCOUNT, 1);
 }
 
 
-static void print_usage (void) {
+static void print_usage (void)
+	/*@globals fileSystem @*/
+	/*@modifies fileSystem @*/
+{
   fprintf(stderr,
   "usage: %s [options] [script [args]].\n"
   "Available options are:\n"
@@ -110,13 +123,19 @@ static void print_usage (void) {
 }
 
 
-static void l_message (const char *pname, const char *msg) {
+static void l_message (/*@null@*/ const char *pname, const char *msg)
+	/*@globals fileSystem @*/
+	/*@modifies fileSystem @*/
+{
   if (pname) fprintf(stderr, "%s: ", pname);
   fprintf(stderr, "%s\n", msg);
 }
 
 
-static int report (int status) {
+static int report (int status)
+	/*@globals fileSystem @*/
+	/*@modifies fileSystem @*/
+{
   const char *msg;
   if (status) {
     msg = lua_tostring(L, -1);
@@ -128,7 +147,10 @@ static int report (int status) {
 }
 
 
-static int lcall (int narg, int clear) {
+static int lcall (int narg, int clear)
+	/*@globals internalState @*/
+	/*@modifies internalState @*/
+{
   int status;
   int base = lua_gettop(L) - narg;  /* function index */
   lua_pushliteral(L, "_TRACEBACK");
@@ -142,12 +164,17 @@ static int lcall (int narg, int clear) {
 }
 
 
-static void print_version (void) {
+static void print_version (void)
+	/*@globals fileSystem @*/
+	/*@modifies fileSystem @*/
+{
   l_message(NULL, LUA_VERSION "  " LUA_COPYRIGHT);
 }
 
 
-static void getargs (char *argv[], int n) {
+static void getargs (char *argv[], int n)
+	/*@*/
+{
   int i;
   lua_newtable(L);
   for (i=0; argv[i]; i++) {
@@ -162,23 +189,35 @@ static void getargs (char *argv[], int n) {
 }
 
 
-static int docall (int status) {
+static int docall (int status)
+	/*@globals fileSystem, internalState @*/
+	/*@modifies fileSystem, internalState @*/
+{
   if (status == 0) status = lcall(0, 1);
   return report(status);
 }
 
 
-static int file_input (const char *name) {
+static int file_input (/*@null@*/ const char *name)
+	/*@globals fileSystem, internalState @*/
+	/*@modifies fileSystem, internalState @*/
+{
   return docall(luaL_loadfile(L, name));
 }
 
 
-static int dostring (const char *s, const char *name) {
+static int dostring (const char *s, const char *name)
+	/*@globals fileSystem, internalState @*/
+	/*@modifies fileSystem, internalState @*/
+{
   return docall(luaL_loadbuffer(L, s, strlen(s), name));
 }
 
 
-static int load_file (const char *name) {
+static int load_file (const char *name)
+	/*@globals fileSystem, internalState @*/
+	/*@modifies fileSystem, internalState @*/
+{
   lua_pushliteral(L, "require");
   lua_rawget(L, LUA_GLOBALSINDEX);
   if (!lua_isfunction(L, -1)) {  /* no `require' defined? */
@@ -214,7 +253,10 @@ static int load_file (const char *name) {
 #endif
 
 
-static int readline (lua_State *l, const char *prompt) {
+static int readline (lua_State *l, const char *prompt)
+	/*@globals fileSystem @*/
+	/*@modifies l, fileSystem @*/
+{
   static char buffer[MAXINPUT];
   if (prompt) {
     fputs(prompt, stdout);
@@ -231,7 +273,10 @@ static int readline (lua_State *l, const char *prompt) {
 #endif
 
 
-static const char *get_prompt (int firstline) {
+/*@observer@*/
+static const char *get_prompt (int firstline)
+	/*@*/
+{
   const char *p = NULL;
   lua_pushstring(L, firstline ? "_PROMPT" : "_PROMPT2");
   lua_rawget(L, LUA_GLOBALSINDEX);
@@ -242,7 +287,9 @@ static const char *get_prompt (int firstline) {
 }
 
 
-static int incomplete (int status) {
+static int incomplete (int status)
+	/*@*/
+{
   if (status == LUA_ERRSYNTAX &&
          strstr(lua_tostring(L, -1), "near `<eof>'") != NULL) {
     lua_pop(L, 1);
@@ -253,7 +300,10 @@ static int incomplete (int status) {
 }
 
 
-static int load_string (void) {
+static int load_string (void)
+	/*@globals fileSystem @*/
+	/*@modifies fileSystem @*/
+{
   int status;
   lua_settop(L, 0);
   if (lua_readline(L, get_prompt(1)) == 0)  /* no input? */
@@ -275,7 +325,10 @@ static int load_string (void) {
 }
 
 
-static void manual_input (void) {
+static void manual_input (void)
+	/*@globals progname, fileSystem, internalState @*/
+	/*@modifies progname, fileSystem, internalState @*/
+{
   int status;
   const char *oldprogname = progname;
   progname = NULL;
@@ -296,7 +349,10 @@ static void manual_input (void) {
 }
 
 
-static int handle_argv (char *argv[], int *interactive) {
+static int handle_argv (char *argv[], int *interactive)
+	/*@globals fileSystem, internalState @*/
+	/*@modifies *interactive, fileSystem, internalState @*/
+{
   if (argv[1] == NULL) {  /* no more arguments? */
     if (stdin_is_tty()) {
       print_version();
@@ -377,7 +433,9 @@ static int handle_argv (char *argv[], int *interactive) {
 }
 
 
-static void openstdlibs (lua_State *l) {
+static void openstdlibs (lua_State *l)
+	/*@modifies l @*/
+{
   const luaL_reg *lib = lualibs;
   for (; lib->func; lib++) {
     lib->func(l);  /* open library */
@@ -386,7 +444,10 @@ static void openstdlibs (lua_State *l) {
 }
 
 
-static int handle_luainit (void) {
+static int handle_luainit (void)
+	/*@globals fileSystem, internalState @*/
+	/*@modifies fileSystem, internalState @*/
+{
   const char *init = getenv("LUA_INIT");
   if (init == NULL) return 0;  /* status OK */
   else if (init[0] == '@')
@@ -398,12 +459,16 @@ static int handle_luainit (void) {
 
 struct Smain {
   int argc;
+/*@relnull@*/
   char **argv;
   int status;
 };
 
 
-static int pmain (lua_State *l) {
+static int pmain (lua_State *l)
+	/*@globals L, progname, fileSystem, internalState @*/
+	/*@modifies l, L, progname, fileSystem, internalState @*/
+{
   struct Smain *s = (struct Smain *)lua_touserdata(l, 1);
   int status;
   int interactive = 0;
@@ -420,7 +485,10 @@ static int pmain (lua_State *l) {
 }
 
 
-int main (int argc, char *argv[]) {
+int main (int argc, char *argv[])
+	/*@globals fileSystem, internalState @*/
+	/*@modifies fileSystem, internalState @*/
+{
   int status;
   struct Smain s;
   lua_State *l = lua_open();  /* create state */
diff --git a/lua/luac/.cvsignore b/lua/luac/.cvsignore
new file mode 100644
index 000000000..cd5eefd59
--- /dev/null
+++ b/lua/luac/.cvsignore
@@ -0,0 +1,3 @@
+.dirstamp
+.libs
+luac
diff --git a/lua/lundump.c b/lua/lundump.c
index 4ef46eccc..896cbd974 100644
--- a/lua/lundump.c
+++ b/lua/lundump.c
@@ -1,5 +1,5 @@
 /*
-** $Id: lundump.c,v 1.1 2004/03/16 21:58:30 niemeyer Exp $
+** $Id: lundump.c,v 1.2 2004/03/23 05:09:14 jbj Exp $
 ** load pre-compiled Lua chunks
 ** See Copyright Notice in lua.h
 */
@@ -23,15 +23,18 @@ typedef struct {
  ZIO* Z;
  Mbuffer* b;
  int swap;
+/*@observer@*/
  const char* name;
 } LoadState;
 
 static void unexpectedEOZ (LoadState* S)
+	/*@modifies S @*/
 {
  luaG_runerror(S->L,"unexpected end of file in %s",S->name);
 }
 
 static int ezgetc (LoadState* S)
+	/*@modifies S @*/
 {
  int c=zgetc(S->Z);
  if (c==EOZ) unexpectedEOZ(S);
@@ -39,12 +42,14 @@ static int ezgetc (LoadState* S)
 }
 
 static void ezread (LoadState* S, void* b, int n)
+	/*@modifies S, *b @*/
 {
  int r=luaZ_read(S->Z,b,n);
  if (r!=0) unexpectedEOZ(S);
 }
 
 static void LoadBlock (LoadState* S, void* b, size_t size)
+	/*@modifies S, *b @*/
 {
  if (S->swap)
  {
@@ -57,6 +62,7 @@ static void LoadBlock (LoadState* S, void* b, size_t size)
 }
 
 static void LoadVector (LoadState* S, void* b, int m, size_t size)
+	/*@modifies S, *b @*/
 {
  if (S->swap)
  {
@@ -74,6 +80,7 @@ static void LoadVector (LoadState* S, void* b, int m, size_t size)
 }
 
 static int LoadInt (LoadState* S)
+	/*@modifies S @*/
 {
  int x;
  LoadBlock(S,&x,sizeof(x));
@@ -82,6 +89,7 @@ static int LoadInt (LoadState* S)
 }
 
 static size_t LoadSize (LoadState* S)
+	/*@modifies S @*/
 {
  size_t x;
  LoadBlock(S,&x,sizeof(x));
@@ -89,13 +97,16 @@ static size_t LoadSize (LoadState* S)
 }
 
 static lua_Number LoadNumber (LoadState* S)
+	/*@modifies S @*/
 {
  lua_Number x;
  LoadBlock(S,&x,sizeof(x));
  return x;
 }
 
+/*@null@*/
 static TString* LoadString (LoadState* S)
+	/*@modifies S @*/
 {
  size_t size=LoadSize(S);
  if (size==0)
@@ -109,6 +120,7 @@ static TString* LoadString (LoadState* S)
 }
 
 static void LoadCode (LoadState* S, Proto* f)
+	/*@modifies S, f @*/
 {
  int size=LoadInt(S);
  f->code=luaM_newvector(S->L,size,Instruction);
@@ -117,6 +129,7 @@ static void LoadCode (LoadState* S, Proto* f)
 }
 
 static void LoadLocals (LoadState* S, Proto* f)
+	/*@modifies S, f @*/
 {
  int i,n;
  n=LoadInt(S);
@@ -131,6 +144,7 @@ static void LoadLocals (LoadState* S, Proto* f)
 }
 
 static void LoadLines (LoadState* S, Proto* f)
+	/*@modifies S, f @*/
 {
  int size=LoadInt(S);
  f->lineinfo=luaM_newvector(S->L,size,int);
@@ -139,6 +153,7 @@ static void LoadLines (LoadState* S, Proto* f)
 }
 
 static void LoadUpvalues (LoadState* S, Proto* f)
+	/*@modifies S, f @*/
 {
  int i,n;
  n=LoadInt(S);
@@ -150,9 +165,12 @@ static void LoadUpvalues (LoadState* S, Proto* f)
  for (i=0; i<n; i++) f->upvalues[i]=LoadString(S);
 }
 
-static Proto* LoadFunction (LoadState* S, TString* p);
+/*@null@*/
+static Proto* LoadFunction (LoadState* S, /*@null@*/ TString* p)
+	/*@modifies S @*/;
 
 static void LoadConstants (LoadState* S, Proto* f)
+	/*@modifies S, f @*/
 {
  int i,n;
  n=LoadInt(S);
@@ -185,6 +203,7 @@ static void LoadConstants (LoadState* S, Proto* f)
 }
 
 static Proto* LoadFunction (LoadState* S, TString* p)
+	/*@modifies S @*/
 {
  Proto* f=luaF_newproto(S->L);
  f->source=LoadString(S); if (f->source==NULL) f->source=p;
@@ -205,6 +224,7 @@ static Proto* LoadFunction (LoadState* S, TString* p)
 }
 
 static void LoadSignature (LoadState* S)
+	/*@modifies S @*/
 {
  const char* s=LUA_SIGNATURE;
  while (*s!=0 && ezgetc(S)==*s)
@@ -213,6 +233,7 @@ static void LoadSignature (LoadState* S)
 }
 
 static void TestSize (LoadState* S, int s, const char* what)
+	/*@modifies S @*/
 {
  int r=LoadByte(S);
  if (r!=s)
@@ -224,6 +245,7 @@ static void TestSize (LoadState* S, int s, const char* what)
 #define V(v)		v/16,v%16
 
 static void LoadHeader (LoadState* S)
+	/*@modifies S @*/
 {
  int version;
  lua_Number x,tx=TEST_NUMBER;
@@ -251,7 +273,9 @@ static void LoadHeader (LoadState* S)
   luaG_runerror(S->L,"unknown number format in %s",S->name);
 }
 
+/*@null@*/
 static Proto* LoadChunk (LoadState* S)
+	/*@modifies S @*/
 {
  LoadHeader(S);
  return LoadFunction(S,NULL);
diff --git a/lua/lundump.h b/lua/lundump.h
index f80bdec22..556fea248 100644
--- a/lua/lundump.h
+++ b/lua/lundump.h
@@ -1,5 +1,5 @@
 /*
-** $Id: lundump.h,v 1.1 2004/03/16 21:58:30 niemeyer Exp $
+** $Id: lundump.h,v 1.2 2004/03/23 05:09:14 jbj Exp $
 ** load pre-compiled Lua chunks
 ** See Copyright Notice in lua.h
 */
@@ -11,16 +11,22 @@
 #include "lzio.h"
 
 /* load one chunk; from lundump.c */
-Proto* luaU_undump (lua_State* L, ZIO* Z, Mbuffer* buff);
+/*@null@*/
+Proto* luaU_undump (lua_State* L, ZIO* Z, Mbuffer* buff)
+	/*@*/;
 
 /* find byte order; from lundump.c */
-int luaU_endianness (void);
+int luaU_endianness (void)
+	/*@*/;
 
 /* dump one chunk; from ldump.c */
-void luaU_dump (lua_State* L, const Proto* Main, lua_Chunkwriter w, void* data);
+void luaU_dump (lua_State* L, const Proto* Main, lua_Chunkwriter w, void* data)
+	/*@*/;
 
 /* print one chunk; from print.c */
-void luaU_print (const Proto* Main);
+/*@unused@*/
+void luaU_print (const Proto* Main)
+	/*@*/;
 
 /* definitions for headers of binary files */
 #define	LUA_SIGNATURE	"\033Lua"	/* binary files start with "<esc>Lua" */
diff --git a/lua/lvm.c b/lua/lvm.c
index 5b4feae8e..9216cce04 100644
--- a/lua/lvm.c
+++ b/lua/lvm.c
@@ -1,5 +1,5 @@
 /*
-** $Id: lvm.c,v 1.2 2004/03/19 21:14:32 niemeyer Exp $
+** $Id: lvm.c,v 1.3 2004/03/23 05:09:14 jbj Exp $
 ** Lua virtual machine
 ** See Copyright Notice in lua.h
 */
@@ -64,7 +64,9 @@ int luaV_tostring (lua_State *L, StkId obj) {
 }
 
 
-static void traceexec (lua_State *L) {
+static void traceexec (lua_State *L)
+	/*@modifies L @*/
+{
   lu_byte mask = L->hookmask;
   if (mask & LUA_MASKCOUNT) {  /* instruction-hook set? */
     if (L->hookcount == 0) {
@@ -96,7 +98,9 @@ static void traceexec (lua_State *L) {
 
 
 static void callTMres (lua_State *L, const TObject *f,
-                       const TObject *p1, const TObject *p2) {
+                       const TObject *p1, const TObject *p2)
+	/*@modifies L @*/
+{
   setobj2s(L->top, f);  /* push function */
   setobj2s(L->top+1, p1);  /* 1st argument */
   setobj2s(L->top+2, p2);  /* 2nd argument */
@@ -109,7 +113,9 @@ static void callTMres (lua_State *L, const TObject *f,
 
 
 static void callTM (lua_State *L, const TObject *f,
-                    const TObject *p1, const TObject *p2, const TObject *p3) {
+                    const TObject *p1, const TObject *p2, const TObject *p3)
+	/*@modifies L @*/
+{
   setobj2s(L->top, f);  /* push function */
   setobj2s(L->top+1, p1);  /* 1st argument */
   setobj2s(L->top+2, p2);  /* 2nd argument */
@@ -120,8 +126,11 @@ static void callTM (lua_State *L, const TObject *f,
 }
 
 
+/*@observer@*/
 static const TObject *luaV_index (lua_State *L, const TObject *t,
-                                  TObject *key, int loop) {
+                                  TObject *key, int loop)
+	/*@modifies L, t @*/
+{
   const TObject *tm = fasttm(L, hvalue(t)->metatable, TM_INDEX);
   if (tm == NULL) return &luaO_nilobject;  /* no TM */
   if (ttisfunction(tm)) {
@@ -131,8 +140,11 @@ static const TObject *luaV_index (lua_State *L, const TObject *t,
   else return luaV_gettable(L, tm, key, loop);
 }
 
+/*@observer@*/
 static const TObject *luaV_getnotable (lua_State *L, const TObject *t,
-                                       TObject *key, int loop) {
+                                       TObject *key, int loop)
+	/*@modifies L @*/
+{
   const TObject *tm = luaT_gettmbyobj(L, t, TM_INDEX);
   if (ttisnil(tm))
     luaG_typeerror(L, t, "index");
@@ -140,7 +152,9 @@ static const TObject *luaV_getnotable (lua_State *L, const TObject *t,
     callTMres(L, tm, t, key);
     return L->top;
   }
+/*@-modobserver@*/
   else return luaV_gettable(L, tm, key, loop);
+/*@=modobserver@*/
 }
 
 
@@ -193,7 +207,9 @@ void luaV_settable (lua_State *L, const TObject *t, TObject *key, StkId val) {
 
 
 static int call_binTM (lua_State *L, const TObject *p1, const TObject *p2,
-                       StkId res, TMS event) {
+                       StkId res, TMS event)
+	/*@modifies L @*/
+{
   ptrdiff_t result = savestack(L, res);
   const TObject *tm = luaT_gettmbyobj(L, p1, event);  /* try first operand */
   if (ttisnil(tm))
@@ -206,8 +222,11 @@ static int call_binTM (lua_State *L, const TObject *p1, const TObject *p2,
 }
 
 
+/*@null@*/
 static const TObject *get_compTM (lua_State *L, Table *mt1, Table *mt2,
-                                  TMS event) {
+                                  TMS event)
+	/*@modifies mt1, mt2 @*/
+{
   const TObject *tm1 = fasttm(L, mt1, event);
   const TObject *tm2;
   if (tm1 == NULL) return NULL;  /* no metamethod */
@@ -221,7 +240,9 @@ static const TObject *get_compTM (lua_State *L, Table *mt1, Table *mt2,
 
 
 static int call_orderTM (lua_State *L, const TObject *p1, const TObject *p2,
-                         TMS event) {
+                         TMS event)
+	/*@modifies L @*/
+{
   const TObject *tm1 = luaT_gettmbyobj(L, p1, event);
   const TObject *tm2;
   if (ttisnil(tm1)) return -1;  /* no metamethod? */
@@ -233,7 +254,9 @@ static int call_orderTM (lua_State *L, const TObject *p1, const TObject *p2,
 }
 
 
-static int luaV_strcmp (const TString *ls, const TString *rs) {
+static int luaV_strcmp (const TString *ls, const TString *rs)
+	/*@*/
+{
   const char *l = getstr(ls);
   size_t ll = ls->tsv.len;
   const char *r = getstr(rs);
@@ -269,7 +292,9 @@ int luaV_lessthan (lua_State *L, const TObject *l, const TObject *r) {
 }
 
 
-static int luaV_lessequal (lua_State *L, const TObject *l, const TObject *r) {
+static int luaV_lessequal (lua_State *L, const TObject *l, const TObject *r)
+	/*@modifies L @*/
+{
   int res;
   if (ttype(l) != ttype(r))
     return luaG_ordererror(L, l, r);
@@ -346,7 +371,9 @@ void luaV_concat (lua_State *L, int total, int last) {
 
 
 static void Arith (lua_State *L, StkId ra,
-                   const TObject *rb, const TObject *rc, TMS op) {
+                   const TObject *rb, const TObject *rc, TMS op)
+	/*@modifies L, ra @*/
+{
   TObject tempb, tempc;
   const TObject *b, *c;
   if ((b = luaV_tonumber(rb, &tempb)) != NULL &&
@@ -691,8 +718,10 @@ StkId luaV_execute (lua_State *L) {
           luaG_runerror(L, "`for' initial value must be a number");
         if (!tonumber(plimit, ra+1))
           luaG_runerror(L, "`for' limit must be a number");
+/*@-modobserver@*/
         if (!tonumber(pstep, ra+2))
           luaG_runerror(L, "`for' step must be a number");
+/*@=modobserver@*/
         step = nvalue(pstep);
         idx = nvalue(ra) + step;  /* increment index */
         limit = nvalue(plimit);
diff --git a/lua/lvm.h b/lua/lvm.h
index a468077f2..2f28114aa 100644
--- a/lua/lvm.h
+++ b/lua/lvm.h
@@ -1,5 +1,5 @@
 /*
-** $Id: lvm.h,v 1.1 2004/03/16 21:58:30 niemeyer Exp $
+** $Id: lvm.h,v 1.2 2004/03/23 05:09:14 jbj Exp $
 ** Lua virtual machine
 ** See Copyright Notice in lua.h
 */
@@ -22,14 +22,25 @@
 	(ttype(o1) == ttype(o2) && luaV_equalval(L, o1, o2))
 
 
-int luaV_lessthan (lua_State *L, const TObject *l, const TObject *r);
-int luaV_equalval (lua_State *L, const TObject *t1, const TObject *t2);
-const TObject *luaV_tonumber (const TObject *obj, TObject *n);
-int luaV_tostring (lua_State *L, StkId obj);
+int luaV_lessthan (lua_State *L, const TObject *l, const TObject *r)
+	/*@modifies L @*/;
+int luaV_equalval (lua_State *L, const TObject *t1, const TObject *t2)
+	/*@modifies L, t1, t2 @*/;
+/*@observer@*/ /*@null@*/
+const TObject *luaV_tonumber (const TObject *obj, TObject *n)
+	/*@modifies n @*/;
+int luaV_tostring (lua_State *L, StkId obj)
+	/*@modifies L, obj @*/;
+/*@observer@*/
 const TObject *luaV_gettable (lua_State *L, const TObject *t, TObject *key,
-                              int loop);
-void luaV_settable (lua_State *L, const TObject *t, TObject *key, StkId val);
-StkId luaV_execute (lua_State *L);
-void luaV_concat (lua_State *L, int total, int last);
+                              int loop)
+	/*@modifies L, t @*/;
+void luaV_settable (lua_State *L, const TObject *t, TObject *key, StkId val)
+	/*@modifies L, t @*/;
+/*@null@*/
+StkId luaV_execute (lua_State *L)
+	/*@modifies L @*/;
+void luaV_concat (lua_State *L, int total, int last)
+	/*@modifies L @*/;
 
 #endif
diff --git a/lua/lzio.h b/lua/lzio.h
index 2a38fb041..0571648f8 100644
--- a/lua/lzio.h
+++ b/lua/lzio.h
@@ -1,5 +1,5 @@
 /*
-** $Id: lzio.h,v 1.1 2004/03/16 21:58:30 niemeyer Exp $
+** $Id: lzio.h,v 1.2 2004/03/23 05:09:14 jbj Exp $
 ** Buffered streams
 ** See Copyright Notice in lua.h
 */
@@ -22,19 +22,24 @@ typedef struct Zio ZIO;
 
 #define zname(z)	((z)->name)
 
-void luaZ_init (ZIO *z, lua_Chunkreader reader, void *data, const char *name);
-size_t luaZ_read (ZIO* z, void* b, size_t n);	/* read next n bytes */
-int luaZ_lookahead (ZIO *z);
+void luaZ_init (ZIO *z, lua_Chunkreader reader, void *data, const char *name)
+	/*@modifies z @*/;
+size_t luaZ_read (ZIO* z, void* b, size_t n)	/* read next n bytes */
+	/*@modifies z, *b @*/;
+int luaZ_lookahead (ZIO *z)
+	/*@modifies z @*/;
 
 
 
 typedef struct Mbuffer {
+/*@relnull@*/
   char *buffer;
   size_t buffsize;
 } Mbuffer;
 
 
-char *luaZ_openspace (lua_State *L, Mbuffer *buff, size_t n);
+char *luaZ_openspace (lua_State *L, Mbuffer *buff, size_t n)
+	/*@modifies L, buff @*/;
 
 #define luaZ_initbuffer(L, buff) ((buff)->buffer = NULL, (buff)->buffsize = 0)
 
@@ -52,6 +57,7 @@ char *luaZ_openspace (lua_State *L, Mbuffer *buff, size_t n);
 
 struct Zio {
   size_t n;			/* bytes still unread */
+/*@relnull@*/
   const char *p;		/* current position in buffer */
   lua_Chunkreader reader;
   void* data;			/* additional data */
@@ -59,6 +65,7 @@ struct Zio {
 };
 
 
-int luaZ_fill (ZIO *z);
+int luaZ_fill (ZIO *z)
+	/*@modifies z @*/;
 
 #endif