verification and linting of lua implementations

[David Manura <dm.lua@...>]

A new page has been added on the topic of correctness validation of
Lua implementations
<http://lua-users.org/wiki/LuaImplementationVerification>.    Also,
below are some warnings reported by Gimpel PC-Lint on 5.2.0-beta after
spending some hours tuning it tonight.  Unfortunately, I think all the
extensive casting and crazy things in the Lua source make linting
difficult (not to even speak of LuaJIT), so I only bothered extracting
the superficial/easy results.  Properly doing this may require
spending days/weeks molding the source code to make it more amenable
to analysis.  I also wonder if anyone has tried any formal or other
verification methods.  Maybe verification would be easier if Lua were
not even written in C.  In fact, one thing I've wondered about: If you
were to design a programming language specialized only for creating
Lua-like VM's, what would it look like?  (In LuaJIT, metaprogramming
things like DynASM may partly answer that, while the standard Lua
implementation resorts mainly to C macros.)

    _
    luaL_addvalue(b);
src\ltablib.c(89) : Warning 539: Did not expect positive indentation from line
    86
	
  lua_assert(dyd->actvar.n == 0 && dyd->gt.n == 0 && dyd->label.n == 0);
src\lparser.c(1600) : Warning 527: Unreachable code at token ';'

..\lua.lnt(86) : Info 750: local macro 'numints' (line 70, file src\ltable.c)
    not referenced
src\ltable.c(70) : Info 830: Location cited in prior message

Info 755: global macro 'MIN_LMEM' (line 33, file src\llimits.h) not referenced
src\llimits.h(33) : Info 830: Location cited in prior message

Info 755: global macro 'SETARG_Ax' (line 110, file src\lopcodes.h) not
    referenced
src\lopcodes.h(110) : Info 830: Location cited in prior message

Info 755: global macro 'set2bits' (line 66, file src\lgc.h) not referenced
src\lgc.h(66) : Info 830: Location cited in prior message

Info 755: global macro 'reset2bits' (line 67, file src\lgc.h) not referenced
src\lgc.h(67) : Info 830: Location cited in prior message

Info 755: global macro 'BASIC_CI_SIZE' (line 50, file src\lstate.h) not
    referenced
src\lstate.h(50) : Info 830: Location cited in prior message

..\lua.lnt(90) : Info 750: local macro 'Sizeof' (line 221, file src\luac.c) not
    referenced
src\luac.c(221) : Info 830: Location cited in prior message

    default: api_check(L, 0, "invalid option"); i = 0;
src\lapi.c(318) : Warning 527: Unreachable code at token 'i'

src\ldo.c(374) : Warning 438: Last value assigned to variable 'ci' (defined at
    line 356) not used
src\ldo.c(356) : Info 830: Location cited in prior message

..\lua.lnt(69) : Info 754: local structure member 'c' (line 268, file
    src\lbaselib.c) not referenced

  p->closef = &io_noclose;  /* keep file opened */
src\liolib.c(582) : Warning 546: Suspicious use of &
  (this occurs in other places too, where the & on the function
pointer can be omitted)