diff options
Diffstat (limited to 'lua')
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 @@ -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; @@ -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 @@ -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; @@ -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; @@ -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: @@ -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" */ @@ -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); @@ -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 |