lvc：LVC验证的编译器

LVC编译器项目 LVC代表线性验证编译器。 编译器基于线性一阶语言IL [1,2]。 该项目的目标是表明功能性SSA，即使用功能性样式词法变量绑定为静态单一分配（SSA）提供了可行的语义基础。 CoqDoc文档可。 依存关系 辅酶Q 来源使用Coq版本8.7.2（2018年3月）进行编译。 其他版本可能会起作用。 OCaml （包括ocamlbuild） 源代码使用ocaml 4.04.2版进行编译，其他版本也可以使用。 OCaml应该包括ocamlbuild。 门希尔 解析器生成器主要与ocamlyacc兼容（但更能解释冲突）： ://gallium.inria.fr/~fpottier/menhir/源代码使用20171013版进行编译。其他版本也可以使用。 Ruby[可选] 如果要输出构建时间，则需要使用ruby。 建筑LVC 通过获取源代码 git clone https://github.com/sigurdschneider/lvc git submodule update --init --recursive 安装依赖项后，您可以（但如果您没有更改蒽，