--- /dev/null
+.deps
+Makefile
+Makefile.in
+.libs
+*.la
+*.lcd
+*.lo
--- /dev/null
+-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 #
+LINT = splint
+
noinst_LTLIBRARIES = liblua.la
noinst_PROGRAMS = lua/lua luac/luac
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)
+
/*
-** $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
*/
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 @*/;
typedef struct luaL_Buffer {
+/*@dependent@*/
char *p; /* current position in buffer */
int lvl; /* number of strings in the stack (level) */
lua_State *L;
#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 @*/;
/* }====================================================== */
*/
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
/*
-** $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
*/
#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 */
/*
-** $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
*/
#include "lvm.h"
+/*@unused@*/
const char lua_ident[] =
"$Lua: " LUA_VERSION " " LUA_COPYRIGHT " $\n"
"$Authors: " LUA_AUTHORS " $\n"
-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;
}
-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;
}
-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);
api_incr_top(L);
lua_unlock(L);
lua_userstateopen(L1);
+/*@-kepttrans@*/
return L1;
+/*@=kepttrans@*/
}
** 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);
}
};
-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);
setuvalue(L->top, u);
api_incr_top(L);
lua_unlock(L);
+/*@-kepttrans@*/
return u + 1;
+/*@=kepttrans@*/
}
}
+/*@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;
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]);
}
}
/*
-** $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
*/
#include "lobject.h"
-void luaA_pushobject (lua_State *L, const TObject *o);
+void luaA_pushobject (lua_State *L, const TObject *o)
+ /*@modifies L @*/;
#endif
/*
-** $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
*/
}
-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);
}
-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 */
}
-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;
** 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;
}
-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);
}
-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;
}
}
-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);
}
-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));
}
-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 */
}
-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: {
}
-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);
}
-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 */
}
-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);
}
-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) {
}
-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: {
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);
/*
-** $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
*/
#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
/*
-** $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
*/
-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 */
}
-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 */
}
-static Proto *getluaproto (CallInfo *ci) {
+/*@null@*/
+static Proto *getluaproto (CallInfo *ci)
+ /*@*/
+{
return (isLua(ci) ? ci_func(ci)->l.p : NULL);
}
}
-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]";
}
-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--) {
}
-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;
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) {
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)
-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);
}
-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:
}
-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) */
}
-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]);
}
-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 */
}
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;
}
-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) */
/* 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;
}
-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)) ?
}
-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 */
/*
-** $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
*/
#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
/*
-** $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
*/
};
-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));
}
-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);
/* }====================================================== */
-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;
}
-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 {
}
-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;
}
-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);
}
-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? */
}
-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;
}
-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);
}
-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);
}
-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;
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;
/*
-** $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
*/
/* 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
/*
-** $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
*/
} DumpState;
static void DumpBlock(const void* b, size_t size, DumpState* D)
+ /*@*/
{
lua_unlock(D->L);
(*D->write)(D->L,b,size,D->data);
}
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);
}
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);
}
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);
}
static void DumpFunction(const Proto* f, const TString* p, DumpState* D)
+ /*@*/
{
DumpString((f->source==p) ? NULL : f->source,D);
DumpInt(f->lineDefined,D);
}
static void DumpHeader(DumpState* D)
+ /*@*/
{
DumpLiteral(LUA_SIGNATURE,D);
DumpByte(VERSION,D);
/*
-** $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
*/
#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
/*
-** $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
*/
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;
-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) {
break;
}
case LUA_TTHREAD: {
+/*@-onlytrans@*/
gcototh(o)->gclist = st->tmark;
+/*@=onlytrans@*/
st->tmark = o;
break;
}
}
-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 */
}
}
/* 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;
}
-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 */
-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 */
}
-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... */
}
-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));
}
-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: {
}
case LUA_TTHREAD: {
lua_State *th = gcototh(st->tmark);
+/*@-dependenttrans@*/
st->tmark = th->gclist;
+/*@=dependenttrans@*/
traversestack(st, th);
break;
}
}
-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);
/*
** 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);
/*
** 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;
}
-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;
}
-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) {
}
else {
count++;
+/*@-dependenttrans@*/
*p = curr->gch.next;
+/*@=dependenttrans@*/
freeobj(L, curr);
}
}
}
-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);
}
-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)
}
-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);
/* 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));
}
-static size_t mark (lua_State *L) {
+static size_t mark (lua_State *L)
+ /*@modifies L @*/
+{
size_t deadmem;
GCState st;
GCObject *wkv;
/*
-** $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
*/
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
/*
-** $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
*/
}
-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));
}
** =======================================================
*/
-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);
}
-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 */
#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 {
}
-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 */
*/
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;
}
-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);
} 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;
*/
-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)) {
}
-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 */
}
/*
-** $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
*/
** 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");
}
-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);
}
-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)
}
-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);
}
-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,
}
-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;
}
-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);
}
-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 */
}
-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? */
}
-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));
}
-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);
}
-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))
}
-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, */
}
-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? */
}
-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 {
}
-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);
}
-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);
}
-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!"));
}
-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);
}
-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);
}
-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);
}
-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? */
}
-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)
#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);
}
-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 */
}
-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;
}
-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);
/* }====================================================== */
+/*@-readonlytrans@*/
+/*@unchecked@*/
static const luaL_reg base_funcs[] = {
{"error", luaB_error},
{"getmetatable", luaB_getmetatable},
{"require", luaB_require},
{NULL, NULL}
};
+/*@=readonlytrans@*/
/*
** =======================================================
*/
-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");
}
-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");
}
-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) {
}
-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");
}
-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");
}
+/*@-readonlytrans@*/
+/*@unchecked@*/
static const luaL_reg co_funcs[] = {
{"create", luaB_cocreate},
{"wrap", luaB_cowrap},
{"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 */
/*
-** $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
*/
-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)) {
}
-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? */
}
-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");
}
-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);
}
-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);
}
-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;
}
-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';
}
-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 */
}
-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);
}
-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);
#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;
}
+/*@-readonlytrans@*/
+/*@unchecked@*/
static const luaL_reg dblib[] = {
{"getlocal", getlocal},
{"getinfo", getinfo},
{"traceback", errorfb},
{NULL, NULL}
};
+/*@=readonlytrans@*/
LUALIB_API int luaopen_debug (lua_State *L) {
/*
-** $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
*/
#include "lauxlib.h"
#include "lualib.h"
+/*@access FILE @*/
/*
#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;
}
-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)
}
-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");
** 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);
** 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) {
}
-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 */
}
-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));
}
-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);
}
-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)
}
-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);
}
-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;
}
-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);
}
-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);
}
-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 */
*/
-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);
}
-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);
}
-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 (;;) {
}
-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;
}
-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;
}
-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");
/* }====================================================== */
-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++) {
}
-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);
}
-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},
};
+/*@unchecked@*/
static const luaL_reg flib[] = {
{"flush", f_flush},
{"read", f_read},
{"__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");
** =======================================================
*/
-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;
}
-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;
}
** =======================================================
*/
-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);
}
-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);
}
-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;
}
-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 {
}
-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;
/* }====================================================== */
-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);
}
-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},
{"tmpname", io_tmpname},
{NULL, NULL}
};
+/*@=readonlytrans@*/
/* }====================================================== */
/*
-** $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
*/
#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;
}
-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;
}
-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;
}
-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},
{"randomseed", math_randomseed},
{NULL, NULL}
};
+/*@=readonlytrans@*/
/*
/*
-** $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
*
#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);
#include <windows.h>
static void pusherror(lua_State *L)
+ /*@modifies L @*/
{
int error=GetLastError();
char buffer[128];
}
static int loadlib(lua_State *L)
+ /*@modifies L @*/
{
const char *path=luaL_checkstring(L,1);
const char *init=luaL_checkstring(L,2);
#endif
static int loadlib(lua_State *L)
+ /*@modifies L @*/
{
lua_pushnil(L);
lua_pushliteral(L,LOADLIB);
/*
-** $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
*/
#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);
}
-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 */
}
-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 */
}
-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' */
}
-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);
*/
-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);
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] */
} /* 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? */
/* }====================================================== */
+/*@-readonlytrans@*/
+/*@unchecked@*/
static const luaL_reg tab_funcs[] = {
{"concat", str_concat},
{"foreach", luaB_foreach},
{"remove", luaB_tremove},
{NULL, NULL}
};
+/*@=readonlytrans@*/
LUALIB_API int luaopen_table (lua_State *L) {
/*
-** $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
*/
/* ORDER RESERVED */
+/*@observer@*/ /*@unchecked@*/
static const char *const token2string [] = {
"and", "break", "do", "else", "elseif",
"end", "false", "for", "function", "if",
}
-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);
}
}
-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
}
-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");
#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 {
/* 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);
}
-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);
}
-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);
/*
-** $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
*/
typedef union {
lua_Number r;
+/*@null@*/
TString *ts;
} SemInfo; /* semantics information */
} 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
/*
-** $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
*/
#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)
/*
-** $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
*/
-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);
}
/*
-** $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
*/
** 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
/*
** Union of all Lua values
*/
typedef union {
+/*@relnull@*/
GCObject *gc;
void *p;
lua_Number n;
*/
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' */
int sizep; /* size of `p' */
int sizelocvars;
int lineDefined;
+/*@relnull@*/
GCObject *gclist;
lu_byte nups; /* number of upvalues */
lu_byte numparams;
typedef struct LocVar {
+/*@relnull@*/
TString *varname;
int startpc; /* first point where variable is active */
int endpc; /* first point where variable is dead */
typedef struct UpVal {
CommonHeader;
+/*@null@*/
TObject *v; /* points to stack or to its own value */
TObject value; /* the value (when closed) */
} 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;
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;
+/*@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
#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";
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))
{
}
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);
}
static void storenumber(lua_State *L, const char *name, lua_Number value)
+ /*@modifies L @*/
{
lua_pushstring(L, name);
lua_pushnumber(L, value);
}
static int pusherror(lua_State *L, const char *info)
+ /*@modifies L @*/
{
lua_pushnil(L);
if (info==NULL)
}
static int pushresult(lua_State *L, int i, const char *info)
+ /*@modifies L @*/
{
if (i != -1)
{
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;
}
static gid_t mygetgid(lua_State *L, int i)
+ /*@modifies L @*/
{
if (lua_isnone(L, i))
return -1;
static int Perrno(lua_State *L) /** errno() */
+ /*@modifies L @*/
{
lua_pushstring(L, strerror(errno));
lua_pushnumber(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);
static int aux_files(lua_State *L)
+ /*@modifies L @*/
{
DIR *d = lua_touserdata(L, lua_upvalueindex(1));
struct dirent *entry;
}
static int Pfiles(lua_State *L) /** files([path]) */
+ /*@globals fileSystem @*/
+ /*@modifies L, fileSystem @*/
{
const char *path = luaL_optstring(L, 1, ".");
DIR *d = opendir(path);
static int Pgetcwd(lua_State *L) /** getcwd() */
+ /*@modifies L @*/
{
char buf[MYBUFSIZ];
if (getcwd(buf, sizeof(buf)) == NULL)
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);
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);
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);
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);
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);
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);
static int Preadlink(lua_State *L) /** readlink(path) */
+ /*@globals fileSystem @*/
+ /*@modifies L, fileSystem @*/
{
char buf[MYBUFSIZ];
const char *path = luaL_checkstring(L, 1);
static int Paccess(lua_State *L) /** access(path,[mode]) */
+ /*@modifies L @*/
{
int mode=F_OK;
const char *path=luaL_checkstring(L, 1);
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);
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);
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);
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);
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));
static int Pputenv(lua_State *L) /** putenv(string) */
+ /*@modifies L @*/
{
size_t l;
const char *s=luaL_checklstring(L, 1, &l);
#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);
static int Punsetenv(lua_State *L) /** unsetenv(name) */
+ /*@modifies L @*/
{
const char *name=luaL_checkstring(L, 1);
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++)
static int Pumask(lua_State *L) /** umask([mode]) */
+ /*@globals fileSystem @*/
+ /*@modifies L, fileSystem @*/
{
char m[10];
mode_t mode;
static int Pchmod(lua_State *L) /** chmod(path,mode) */
+ /*@globals fileSystem @*/
+ /*@modifies L, fileSystem @*/
{
mode_t mode;
struct stat s;
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);
static int Putime(lua_State *L) /** utime(path,[mtime,atime]) */
+ /*@globals fileSystem @*/
+ /*@modifies L, fileSystem @*/
{
struct utimbuf times;
time_t currtime = time(NULL);
}
-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)
{
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));
}
static int Pctermid(lua_State *L) /** ctermid() */
+ /*@globals fileSystem @*/
+ /*@modifies L, fileSystem @*/
{
char b[L_ctermid];
lua_pushstring(L, ctermid(b));
static int Pgetlogin(lua_State *L) /** getlogin() */
+ /*@modifies L @*/
{
lua_pushstring(L, getlogin());
return 1;
static int Fgetpasswd(lua_State *L, int i, const void *data)
+ /*@modifies L @*/
{
const struct passwd *p=data;
switch (i)
return 1;
}
+/*@observer@*/ /*@unchecked@*/
static const char *const Sgetpasswd[] =
{
"name", "uid", "gid", "dir", "shell", "gecos", "passwd", NULL
static int Pgetpasswd(lua_State *L) /** getpasswd(name or id) */
+ /*@modifies L @*/
{
struct passwd *p=NULL;
if (lua_isnoneornil(L, 1))
static int Pgetgroup(lua_State *L) /** getgroup(name or id) */
+ /*@modifies L @*/
{
struct group *g=NULL;
if (lua_isnumber(L, 1))
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);
}
#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)
return 1;
}
+/*@observer@*/ /*@unchecked@*/
static const char *const Stimes[] =
{
"utime", "stime", "cutime", "cstime", "elapsed", NULL
#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);
{
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)
return 1;
}
+/*@observer@*/ /*@unchecked@*/
static const char *const Sstat[] =
{
"mode", "ino", "dev", "nlink", "uid", "gid",
};
static int Pstat(lua_State *L) /** stat(path,[selector]) */
+ /*@modifies L @*/
{
struct mystat s;
const char *path=luaL_checkstring(L, 1);
static int Puname(lua_State *L) /** uname([string]) */
+ /*@modifies L @*/
{
struct utsname u;
luaL_Buffer b;
}
+/*@observer@*/ /*@unchecked@*/
static const int Kpathconf[] =
{
_PC_LINK_MAX, _PC_MAX_CANON, _PC_MAX_INPUT, _PC_NAME_MAX, _PC_PATH_MAX,
};
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",
};
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,
-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",
};
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},
#endif
{NULL, NULL}
};
+/*@=readonlytrans@*/
LUALIB_API int luaopen_posix (lua_State *L)
{
#ifndef LPOSIX_H
#define LPOSIX_H
-int luaopen_posix (lua_State *L);
+int luaopen_posix (lua_State *L)
+ /*@modifies L @*/;
#endif
#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!
#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;
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++) {
}
}
-static int rex_match(lua_State *L) {
+static int rex_match(lua_State *L)
+ /*@modifies L @*/
+{
int res;
#ifdef REG_BASIC
size_t len;
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;
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 */
/* Open the library */
+/*@-readonlytrans@*/
+/*@unchecked@*/
static const luaL_reg rexlib[] = {
#ifdef WITH_POSIX
{"newPOSIX", rex_comp},
#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");
#ifndef LREXLIB_H
#define LREXLIB_H
-int luaopen_rex(lua_State *L);
+int luaopen_rex(lua_State *L)
+ /*@modifies L @*/;
#endif
typedef struct modeLookup modeLookup;
+/*@observer@*/ /*@unchecked@*/
static modeLookup modesel[] =
{
/* RWX char Posix Constant */
static int rwxrwxrwx(mode_t *mode, const char *p)
+ /*@modifies *mode @*/
{
int count;
mode_t tmp_mode = *mode;
default:
return -4; /* failed! -- bad rwxrwxrwx mode change */
+ /*@notreached@*/
break;
}
p++;
}
static void modechopper(mode_t mode, char *p)
+ /*@modifies *p @*/
{
/* requires char p[10] */
int count;
}
static int mode_munch(mode_t *mode, const char* p)
+ /*@modifies *mode @*/
{
char op=0;
/*
-** $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
*/
};
+/*@unchecked@*/
extern const lu_byte luaP_opmodes[NUM_OPCODES];
#define getOpMode(m) (cast(enum OpMode, luaP_opmodes[m] & 3))
/*
-** $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
*/
** 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 */
/*
** 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 */
}
-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;
}
-static void check (LexState *ls, int c) {
+static void check (LexState *ls, int c)
+ /*@modifies ls @*/
+{
if (!testnext(ls, c))
error_expected(ls, 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);
}
-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;
}
-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,
}
-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--) {
}
-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++) {
}
-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)
}
-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 {
}
-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) {
}
-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");
}
-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;
}
-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);
}
-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;
}
-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 */
}
-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;
/*============================================================*/
-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;
}
-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);
};
-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;
}
-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;
}
-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);
}
-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++;
}
-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;
-static void parlist (LexState *ls) {
+static void parlist (LexState *ls)
+ /*@modifies ls @*/
+{
/* parlist -> [ param { `,' param } ] */
int nparams = 0;
int dots = 0;
}
-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);
}
-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);
}
-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;
*/
-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 '(': {
}
-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;
}
-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) {
}
-static UnOpr getunopr (int op) {
+static UnOpr getunopr (int op)
+ /*@*/
+{
switch (op) {
case TK_NOT: return OPR_NOT;
case '-': return OPR_MINUS;
}
-static BinOpr getbinopr (int op) {
+static BinOpr getbinopr (int op)
+ /*@*/
+{
switch (op) {
case '+': return OPR_ADD;
case '-': return OPR_SUB;
}
+/*@unchecked@*/
static const struct {
lu_byte left; /* left priority for each binary operator */
lu_byte right; /* right priority */
** 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);
}
-static void expr (LexState *ls, expdesc *v) {
+static void expr (LexState *ls, expdesc *v)
+ /*@modifies ls @*/
+{
subexpr(ls, v, -1);
}
*/
-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:
}
-static void block (LexState *ls) {
+static void block (LexState *ls)
+ /*@modifies ls @*/
+{
/* block -> chunk */
FuncState *fs = ls->fs;
BlockCnt bl;
** 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;
}
-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");
}
-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 */
*/
#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;
}
-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);
}
-static int exp1 (LexState *ls) {
+static int exp1 (LexState *ls)
+ /*@modifies ls @*/
+{
expdesc e;
int k;
expr(ls, &e);
}
-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;
}
-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;
}
-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;
}
-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;
}
-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);
}
-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;
}
-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);
}
-static void localstat (LexState *ls) {
+static void localstat (LexState *ls)
+ /*@modifies ls @*/
+{
/* stat -> LOCAL NAME {`,' NAME} [`=' explist1] */
int nvars = 0;
int nexps;
}
-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);
}
-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;
}
-static void exprstat (LexState *ls) {
+static void exprstat (LexState *ls)
+ /*@modifies ls @*/
+{
/* stat -> func | assignment */
FuncState *fs = ls->fs;
struct LHS_assign v;
}
-static void retstat (LexState *ls) {
+static void retstat (LexState *ls)
+ /*@modifies ls @*/
+{
/* stat -> RETURN explist */
FuncState *fs = ls->fs;
expdesc e;
}
-static void breakstat (LexState *ls) {
+static void breakstat (LexState *ls)
+ /*@modifies ls @*/
+{
/* stat -> BREAK [NAME] */
FuncState *fs = ls->fs;
BlockCnt *bl = fs->bl;
}
-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 */
}
-static void chunk (LexState *ls) {
+static void chunk (LexState *ls)
+ /*@modifies ls @*/
+{
/* chunk -> { stat [`;'] } */
int islast = 0;
enterlevel(ls);
/*
-** $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
*/
/* 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' */
} 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
/*
-** $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
*/
** 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 {
}
-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;
}
-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);
}
/*
** 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);
}
-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;
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 */
}
+/*@null@*/
LUA_API lua_State *lua_open (void) {
lua_State *L = mallocstate(NULL);
if (L) { /* allocation OK? */
}
-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 */
}
/*
-** $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
*/
typedef struct stringtable {
+/*@null@*/
GCObject **hash;
ls_nstr nuse; /* number of elements */
int size;
** 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;
*/
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;
*/
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 */
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) */
};
#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
/*
-** $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
*/
}
-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;
/*
-** $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
*/
#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
/*
-** $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
*/
/*
** 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) */
** 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)));
** 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);
*/
-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 */
}
-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;
}
-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++)
}
-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)
}
-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;
}
-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);
** 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? */
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);
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))
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));
/*
-** $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
*/
#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
/*
-** $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
*/
#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);
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++)
}
-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);
*/
-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];
#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),
}
-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),
}
-static int listlocals (lua_State *L) {
+static int listlocals (lua_State *L)
+ /*@*/
+{
Proto *p;
int pc = luaL_checkint(L, 2) - 1;
int i = 0;
-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);
}
-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);
}
-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);
}
-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));
}
-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);
}
-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) {
}
-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);
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)
}
-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)) {
}
-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';
}
-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);
}
-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 */
}
-static int loadlib (lua_State *L) {
+static int loadlib (lua_State *L)
+ /*@*/
+{
static const luaL_reg libs[] = {
{"mathlibopen", luaopen_math},
{"strlibopen", luaopen_string},
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);
}
-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));
}
-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);
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);
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))
#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 (;;) {
** =======================================================
*/
-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 {
}
-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");
};
-static void fim (void) {
+static void fim (void)
+ /*@*/
+{
if (!islocked)
lua_close(lua_state);
lua_assert(memdebug_numblocks == 0);
}
-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;
/*
-** $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
*/
+/*@observer@*/
const char *const luaT_typenames[] = {
"nil", "boolean", "userdata", "number",
"string", "table", "function", "userdata", "thread"
void luaT_init (lua_State *L) {
+/*@observer@*/
static const char *const luaT_eventname[] = { /* ORDER TM */
"__index", "__newindex",
"__gc", "__mode", "__eq",
}
-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:
/*
-** $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
*/
#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
--- /dev/null
+.dirstamp
+.libs
+lua
/*
-** $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
*/
#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},
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"
}
-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);
}
-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");
}
-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++) {
}
-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? */
#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);
#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);
}
-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);
}
-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? */
}
-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;
}
-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();
}
-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 */
}
-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] == '@')
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;
}
-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 */
--- /dev/null
+.dirstamp
+.libs
+luac
/*
-** $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
*/
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);
}
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)
{
}
static void LoadVector (LoadState* S, void* b, int m, size_t size)
+ /*@modifies S, *b @*/
{
if (S->swap)
{
}
static int LoadInt (LoadState* S)
+ /*@modifies S @*/
{
int x;
LoadBlock(S,&x,sizeof(x));
}
static size_t LoadSize (LoadState* S)
+ /*@modifies S @*/
{
size_t x;
LoadBlock(S,&x,sizeof(x));
}
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)
}
static void LoadCode (LoadState* S, Proto* f)
+ /*@modifies S, f @*/
{
int size=LoadInt(S);
f->code=luaM_newvector(S->L,size,Instruction);
}
static void LoadLocals (LoadState* S, Proto* f)
+ /*@modifies S, f @*/
{
int i,n;
n=LoadInt(S);
}
static void LoadLines (LoadState* S, Proto* f)
+ /*@modifies S, f @*/
{
int size=LoadInt(S);
f->lineinfo=luaM_newvector(S->L,size,int);
}
static void LoadUpvalues (LoadState* S, Proto* f)
+ /*@modifies S, f @*/
{
int i,n;
n=LoadInt(S);
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);
}
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;
}
static void LoadSignature (LoadState* S)
+ /*@modifies S @*/
{
const char* s=LUA_SIGNATURE;
while (*s!=0 && ezgetc(S)==*s)
}
static void TestSize (LoadState* S, int s, const char* what)
+ /*@modifies S @*/
{
int r=LoadByte(S);
if (r!=s)
#define V(v) v/16,v%16
static void LoadHeader (LoadState* S)
+ /*@modifies S @*/
{
int version;
lua_Number x,tx=TEST_NUMBER;
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);
/*
-** $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
*/
#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" */
/*
-** $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
*/
}
-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) {
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 */
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 */
}
+/*@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)) {
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");
callTMres(L, tm, t, key);
return L->top;
}
+/*@-modobserver@*/
else return luaV_gettable(L, tm, key, loop);
+/*@=modobserver@*/
}
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))
}
+/*@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 */
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? */
}
-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);
}
-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);
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 &&
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);
/*
-** $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
*/
(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
/*
-** $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
*/
#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)
struct Zio {
size_t n; /* bytes still unread */
+/*@relnull@*/
const char *p; /* current position in buffer */
lua_Chunkreader reader;
void* data; /* additional data */
};
-int luaZ_fill (ZIO *z);
+int luaZ_fill (ZIO *z)
+ /*@modifies z @*/;
#endif
projects / tools / librpm-tizen.git / commitdiff