文件名称：vellvm-legacy
文件大小：568KB
文件格式：ZIP
更新时间：2024-07-13 20:39:30
Coq
Vellvm-Legacy 这是原始 Vellvm 存储库的“清理”副本，不包括我们无权重新分发的发布来源、实验结果以及代码、测试用例和基准测试。 所需修改的第三方库的源已从历史记录中删除，而是通过补丁提供。 用于解析器、解释器和经过验证的检测/优化传递的修改后的 OCaml 绑定与较新版本的 LLVM 可用的内容大不相同，并且无法编译。 存储库中当前不包含绑定、SoftBound 或 Vmem2reg 传递。 可以提取解释器，但目前无法将 LLVM 位码解析为 Vellvm AST。 依赖关系 camlp4（对于方程插件——从 4.02 开始不再包含在 OCaml 中） Coq 8.4pl4，配置了-usecamlp4选项 建造 在 repo 的*目录中，运行scripts/fetch-libs.sh将所有第三方源下载到 lib/src 中，提取并应用补丁。 运行make li
【文件预览】：
vellvm-legacy-master
----.dir-locals.el(1KB)
----Make(3KB)
----src()
--------Vellvm()
--------Interpreter()
--------Parser()
--------.gitignore(84B)
----.gitignore(125B)
----patch()
--------compcert.patch(617KB)
--------metalib.patch(11KB)
--------cpdtlib.patch(680B)
--------equations.patch(36KB)
--------graphbasics.patch(98KB)
----Makefile(1KB)
----README.md(1KB)
----scripts()
--------fetch-libs.sh(2KB)
--------clone.sh(853B)