漂移:用于推断细化类型的基于抽象解释的静态分析

时间:2024-03-10 05:34:57
【文件属性】:

文件名称:漂移:用于推断细化类型的基于抽象解释的静态分析

文件大小:12.61MB

文件格式:ZIP

更新时间:2024-03-10 05:34:57

OCaml

数据流细化类型推断工具(DRIFT) DRIFT实现了基于抽象解释的静态分析,以推断功能程序中的细化类型。 该分析概括了Liquid类型推断,并且与用于表示类型细化的抽象域是参数化的。 DRIFT以OCaml的子集为目标。 当前,它支持高阶递归函数,对原始类型(例如整数和布尔值),数组和列表的操作。 该工具会自动检查所有数组访问是否在范围内。 此外,它支持验证用户提供的断言。 安装要求 版本> = 4.06 版本> = 2.0.4 请使用opam install安装以下opam库: menhir ,版本> = 20181113 conf-ppl版本> = 1 apron ,版本> = 0.9.10 请在终端中执行以下命令以满足这些要求。 我们在这里假设使用Ubuntu / Debian系统,但其他Linux发行版和Mac OS的设置将非常相似。 如果使用现有的opam OCa


网友评论