why3

2热度

1回答

如何在coq中证明why3生成的脚本？

我使用frama-C WP并希望调试我的ACSL注释（了解为什么证明者说我“不知道”）。 我有一些绿色或橙色的结果。我打开why3 IDE并查看生成的脚本。然后我从列表中选择一个理论/目标，并能够启动Alt-Ergo或Coq IDE。我想在Coq IDE中使用生成的代码。我看到一些公理定理，然后WP 然后，例如： intros a a_1 i_3 i_2 i_1 i t_2 t_1 t t_8 t

coq frama-c coqide why3 2017-08-26

---

1热度

1回答

Jessie插件与Frama-c铝的集成

如何集成 Jessie外部插件（为什么2.36）与 Frama-c铝？

static-analysis frama-c why3 2016-09-22

---

0热度

1回答

下水邮资-C霓虹灯与杰西

我已经安装了邮资-c和why3但是当我尝试推出邮资-C我得到jessie3一个错误。 frama-c -verbose 2 [kernel] warning: cannot load plug-in `Jessie3' (incompatible with Neon-20140301). The exact failure is: error loading shared library:

frama-c why3 2014-10-29

---

1热度

1回答

z3 4.3.2未能找到Why3生成（可满足）目标的模型

我试图使用Why3的Z3后端为了检索模型，然后可以用于派生测试案例展示程序中的错误。但是，对于任何Why3目标而言，Z3 4.3.2版似乎无法回答sat。它看起来像Why3使用的某些公理化定义混淆了Z3。例如，下面的例子（其是什么Why3产生一小部分） (declare-fun abs1 (Int) Int) ;; abs_def (assert (forall ((x I

z3 why3 2015-02-23

---