- html - 出于某种原因,IE8 对我的 Sass 文件中继承的 html5 CSS 不友好?
- JMeter 在响应断言中使用 span 标签的问题
- html - 在 :hover and :active? 上具有不同效果的 CSS 动画
- html - 相对于居中的 html 内容固定的 CSS 重复背景?
我正在尝试使用 alt-ergo 证明器在 frama-c 上运行测试文件。但是,我在使用 alt-ergo 时遇到以下错误。所有其他 frama-c 检查都很好。我知道问题不在于测试文件。
------------------------------------------------------------
--- Alt-Ergo (stderr) :
------------------------------------------------------------
Fatal error: exception Sys_error("/tmp/wpf0dd65.dir/typed/test_post_2_Alt-Ergo.mlw: No such file or directory")
------------------------------------------------------------
[wp] [Alt-Ergo] Goal typed_test_post_2 : Failed
Error: Alt-Ergo exits with status [2]
我在 Windows 计算机上并通过 cygwin 在管理员模式下执行所有安装我得到了 frama-C Neon 并使用 ./configure & make & make-install
安装了它,安装成功(所有 frama-c 检查都在我的测试文件中通过)
我从 http://alt-ergo.ocamlpro.com/download.php 获得了以下版本的 alt-ergo Linux x86_64 二进制文件:alt-ergo-0.95.2-x86_64 。我选择了这个版本,因为 frama-c 文档要求版本 0.95。
我按照以下说明安装了 alt-ergo ( https://www.lri.fr/~marche/MPRI-2-36-1/install.html )
安装 Alt-ergo
最简单的方法是获取 alt-ergo 的二进制文件。下载名为“Linux x86_64 二进制文件”的文件然后:
chmod +x alt-ergo-0.95.2-x86_64
sudo cp alt-ergo-0.95.2-x86_64 /usr/bin/alt-ergo
当调用which
时,但frama-c和alt-ergo有正确的路径
$ which frama-c
/usr/bin/frama-c
$ which alt-ergo
/usr/bin/alt-ergo
我还安装了 Why3 并且它检测到了 ergo 证明器
$ why3 config --detect-provers
Found prover Alt-Ergo version 0.95.2, Ok.
1 provers detected and 0 provers detected with unsupported version
Save config to /home/username/.why3.conf
<小时/>
编辑
我使用在线示例创建了以下 test.mlw
type 'a set
logic add : 'a , 'a set -> 'a set
logic mem : 'a , 'a set -> prop
axiom mem_add:
forall x, y : 'a. forall s : 'a set.
mem(x, add(y, s)) <->
(x = y or mem(x, s))
logic is1, is2 : int set
logic iss : int set set
goal g:
is1 = is2 ->
mem (is1, add (is2, iss))
运行 alt-ergo 结果是:
alt-ergo test.mlw
File "file.mlw", line 1, characters 1-26:Valid (0.0156) (0)
有什么想法吗?
最佳答案
以下症状可以治疗:使用带有 Windows 路径的 -wp-out 标志将解决该问题
例如
frama-c -wp -wp-print -wp-out c:/Users/userName/Desktop/tmp2 ../../cygdrive/c/Users/userName/Desktop/swap.c
关于frama-c - alt-ergo 不能通过 cygwin 在 Windows 上运行,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/25896913/
/* 补丁.hoc v. 1.2 2001 年 10 月 19 日 NTC */load_file("nrngui.hoc")创建 soma//模型拓扑访问 soma//默认部分 = soma 体细胞
我正在尝试使用 Frama-c 测试一个函数: /*@ ensures \result >= x && \result >= y; ensures \result == x || \r
我正在尝试使用 alt-ergo 证明器在 frama-c 上运行测试文件。但是,我在使用 alt-ergo 时遇到以下错误。所有其他 frama-c 检查都很好。我知道问题不在于测试文件。 ----
我是一名优秀的程序员,十分优秀!