		Search-engine friendly clone of the ACL2 documentation.

Svstmt-compile

Signature
(svstmt-compile x st sclimit nb-delayp blk-masks nonblk-masks xcond) → (mv ok warnings1 st1 jst new-blk-masks new-nonblk-masks)
Arguments: x — Guard (svstmt-p x).; st — Guard (svstate-p st).; sclimit — Guard (natp sclimit).; blk-masks — Guard (4vmask-alist-p blk-masks).; nonblk-masks — Guard (4vmask-alist-p nonblk-masks).
Returns: warnings1 — Type (vl-warninglist-p warnings1).; st1 — Type (svstate-p st1).; jst — Type (svjumpstate-p jst).; new-blk-masks — Type (4vmask-alist-p new-blk-masks).; new-nonblk-masks — Type (4vmask-alist-p new-nonblk-masks).

Svstmt-compile.lisp
Svstate: Structure containing currently assigned variable values for blocking and nonblocking assignments.