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

模块 / 112

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

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

5公开名称

栈表示签

公开
「元类型」

文言:先定诸值之形,乃可去装;不以整数冒爻,不以引用入栈。汉语:零表示未证明,一为完整整数,二为布尔,三为单元,四为栈数组地址。该分析只消费合法 SSA;签名是待组合的调用约定,调用者仍须完成闭合、逃逸、入口类型守卫及分配容量证明。返回成功时给出每个局部值的表示,失败不产生可用证书。

栈值表示

公开
化(「数组引用类」于「整数」)而化「正则原子」而「整数」

暂无说明。

栈诸值合签

公开
化(「数组引用类」于「整数」)而化(「列」于「正则原子」)而化(「列」于「整数」)而「爻」

暂无说明。

栈原语签

公开
化「字符串」而((「列」于「整数」)合「整数」)

暂无说明。

验栈表示

公开
化化「字符串」而((「列」于「整数」)合「整数」)而化((「列」于「整数」)合「整数」)而化「整数」而化(「字符串」合「爻」合(「列」于「整数」)合「正则区域」合「整数」)而(「或可有」于(「数组引用类」于「整数」))

暂无说明。