Lua 实现验证

wiki

源代码中的调试宏

请参阅源代码中的LUA_USE_APICHECK和lua_assert宏。

测试套件

请参阅UnitTesting，其中链接到 Lua 5.0 - 5.2beta 的测试套件。

Valgrid

许多人使用 Valgrid 等工具进行动态分析（[搜索 lua-l]）。

Gimpel PC lint

以下是一组使用[Gimpel PC-lint]对 Lua 进行 lint 的初始定义。可以进行许多改进。不幸的是，Lua 的源代码及其所有类型转换等使得 lint 成为一项挑战，有效地执行此操作可能需要对源代码进行许多更改。

// lua.lnt
// gimpel lint 9.00h on Lua 5.2.0rc1.
// David Manura, 2011-11.

// safe to ignore
-e537 // repeated include file (superfluous warnings)
-e801 // use of goto is deprecated
-e834 // operator '-' followed by operator '+' is confusing.  Use parentheses.
-esym(438,argp) // last value assigned to variable not used (debug.c vararg)
-esym(123,gch,luai_num*,luaL_checkint) // macro defined with arguments
-esym(750,LUA_LIB) // local macro not referenced
-esym(750,l*_c) // local macro not referenced
-e845 // the right argument to operator is certain to  be 0
-e778 // constant expression evaluates to 0 in operation
-e835 // a zero has been given as right argument to operator
-e730 // boolean argument to function

// functions that don't return
-sem(cannot, r_no)
-sem(luaL_error, r_no)
-sem(luaL_argerror, r_no)
-sem(luaX_syntaxerror, r_no)
-sem(tag_error, r_no)
-sem(error_expected, r_no)
-sem(errorlimit, r_no)
-sem(escerror, r_no)
-sem(fileerror, r_no)
-sem(lexerror, r_no)
-sem(semerror, r_no)
-sem(typeerror, r_no)
// all below are marked 'l_noret' in the code
-sem(luaD_throw, r_no)
-sem(luaB_error, r_no)
-sem(luaG_typeerror, r_no)
-sem(luaG_concaterror, r_no)
-sem(luaG_aritherror, r_no)
-sem(luaG_ordererror, r_no)
-sem(luaG_errormsg, r_no)
-sem(luaG_runerror, r_no)
-sem(resume_error, r_no)


-esym(767,setnvalue,TValuefields,NILCONSTANT,numfield,
          val_,num_,rttype,ttisnumber,ttisequal,checktag,settt_,setobj)
          // macro defined differently in another module
          // https://lua-users.lua.ac.cn/lists/lua-l/2011-10/msg00007.html
-e546 // suspicious use of &

// check these later (these are numerous)
-e534 // ignoring return value of function
-e648 // overflow in computing constant for operation
-e508 // extern used with definition
-e641 // converting enum to int
-e679 // suspicious truncation in arithmetic expression
-e818 // Pointer parameter could be declared as pointing to const
-e826 // suspicious pointer-to-pointer conversion
-e661 // possible access of out-of-bounds pointer
-e662 // possible creation of out-of-bounds pointer
-e613 // possible use of null pointer
-e416 // likely creation of out-of-bounds pointer
-e420 // apparent access beyond array for function
-e670 // possible access beyond array for function
-e669 // possible data overrun for function
-e419 // apparent data overrun for function
-e415 // likely access of out-of-bounds pointer
-e732 // loss of sign
-e737 // loss of sign in promotion
-e506 // constant value Boolean
// note: other warnings (less numerous) also remain

// Avoids assembly code not understood by lint (MS_ASMTRICK)
-u_M_IX86  // WARNING: undefining this causes problems in setjmp.h

-esym(750, _FILE_OFFSET_BITS) // local macro not referenced
   // This macro not used on non-POSIX systems

// TO FIX
-esym(760,LUA_FILEHANDLE)
/*
#define LUA_FILEHANDLE		"FILE*"
src\lualib.h(15) : Info 760: Redundant macro 'LUA_FILEHANDLE' defined
    identically at line 183, file src\lauxlib.h, module src\lauxlib.c
src\lauxlib.h(183) : Info 830: Location cited in prior message
*/


//-passes(3)

-header(lint.h)

src/lapi.c
src/lauxlib.c
src/lbaselib.c
src/lbitlib.c
src/lcode.c
src/lcorolib.c
src/lctype.c
src/ldblib.c
src/ldebug.c
src/ldo.c
src/ldump.c
src/lfunc.c
src/lgc.c
src/linit.c
src/liolib.c
src/llex.c
src/lmathlib.c
src/lmem.c
src/loadlib.c
src/lobject.c
src/lopcodes.c
src/loslib.c
src/lparser.c
src/lstate.c
src/lstring.c
src/lstrlib.c
src/ltable.c
src/ltablib.c
src/ltm.c
src/lua.c
src/luac.c
src/lundump.c
src/lvm.c
src/lzio.c

.

//lint.h

//lint -sem(myexit, r_no)
extern int myexit(void);
#define LUA_LINT_FALLTHROUGH /*lint -fallthrough*/
  // NOTE: edit the Lua source code to add this macro at the end of
  // switch cases labeled "/* go through */"
#define lua_assert(p) ((p) ? 0 : myexit())

#define LUA_LINT_UNREACHABLE /*lint --e{527} */
  // NOTE: edit the Lua source code to add this macro at end of
  // all lines that are unreachable

#define LUA_LINT_LOOPVARCHANGED(x) /*lint --e{850} */
  // NOTE: edit the Lua source to add add this macro inside any
  // loop that modifies variable x.

.

usage: lint lua.lnt

Lua 手册（HTML）验证

可以使用[w3c 验证器]等工具检查 HTML 格式的 Lua 手册。grep 技术也很有用。

形式化验证技术

有人尝试过吗？[1]