豫豫言文档API ATLAS
入口包说明.html
326 模块3507 名称
← 全部模块

模块 / 107

编译步骤/代码生成/网页汇编栈填充证明。豫

编译步骤/代码生成/网页汇编栈填充证明。豫

10公开名称

栈填表达

公开
「元类型」

文言:每步一写,索进一,余参不移,值为索之一次式,乃可并写。汉语:输入须通过 SSA、表示及封闭调用图验证。这里只证明单数组、单存储、无读取或其他调用的正向填充;退出必须为单元,扫描每步加一,其他参数保持原样。值表达式限加减乘且对扫描为常系数一次式,系数限制在-16..16,树大小不超过64。调用者仍须检查0≤扫描≤上界≤数组长度,不能据此省略根初始化。

栈填原子

公开
化「正则原子」而「栈填表达」

暂无说明。

栈填二元

公开
化「字符串」而化「栈填表达」而化「栈填表达」而「栈填表达」

暂无说明。

栈填已知

公开
「元类型」

暂无说明。

栈填证

公开
「元类型」

暂无说明。

取栈填式

公开
化(「数组引用类」于(「或可有」于(「栈填表达」合「整数」合「整数」)))而化「正则原子」而(「或可有」于(「栈填表达」合「整数」合「整数」))

暂无说明。

栈填小常数

公开
化「栈填表达」而(「或可有」于「整数」)

暂无说明。

合栈填式

公开
化「字符串」而化(「或可有」于(「栈填表达」合「整数」合「整数」))而化(「或可有」于(「栈填表达」合「整数」合「整数」))而(「或可有」于(「栈填表达」合「整数」合「整数」))

暂无说明。

验栈填方向

公开
化((「列」于「整数」)合「整数」)而化(「字符串」合「爻」合(「列」于「整数」)合「正则区域」合「整数」)而化「整数」而化「整数」而化「整数」而(「或可有」于(「整数」合「整数」合「整数」合「栈填表达」合「整数」))

暂无说明。

验栈填充

公开
化((「列」于「整数」)合「整数」)而化(「字符串」合「爻」合(「列」于「整数」)合「正则区域」合「整数」)而(「或可有」于(「整数」合「整数」合「整数」合「栈填表达」合「整数」))

暂无说明。