Splint annotations.

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

5 files changed, 137 insertions, 12 deletions

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;