-
2 votesanswersviews
将WhyML映射到SMT逻辑的确切机制
美好的一天，自动扣除和验证黑客！ 为了更深入地了解WhyML究竟如何为ACSL注释的C程序提供证据，我试图手动“重现”Why3对WhyML程序的工作，同时将其转换为SMT逻辑并将其提供给Z3证明器 . 假设我们有以下C片段： const int L = 3; int a[L] = {0}; int i = 0; while (i < L) { a[i] = i; i++; } ass... -
5 votesanswersviews
依赖于无符号整数溢出的代码的证明？
我应该如何证明代码的正确性，如下所示，为了避免一些低效率，依赖于模运算？ #include <stdint.h> uint32_t my_add(uint32_t a, uint32_t b) { uint32_t r = a + b; if (r < a) return UINT32_MAX; return r; } 我已经尝试了WP... -
2 votesanswersviews
了解Frama-C逻辑标签
当我尝试使用默认逻辑标签LoopEntry和LoopCurrent时，我遇到了一些麻烦 . 这是一个简单的例子，我使用的不同证明器（alt-ergo，coq，cvc3，z3）无法证明： /*@ requires n > 0;*/ void f(int n){ int i = 0; /*@ loop invariant \at(i,LoopEntry) == 0; ... -
2 votesanswersviews
尽管有很强的证据，SMT证明者仍然会产生'unknown'
假设我们有以下C注释代码： #define L 3 int a[L] = {0}; /*@ requires \valid(a+(0..(L - 1))); ensures \forall int j; 0 <= j < L ==> (a[j] == j); */ int main() { int i = 0; /*@ loop assi... -
2 votesanswersviews
如何在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 ... -
1 votesanswersviews
Frama-c：麻烦理解WP内存模型
我正在寻找WP选项/模型，可以让我证明基本的C内存操作，如： memcpy ：我试图证明这个简单的代码： struct header_src{ char t1; char t2; char t3; char t4; }; struct header_dest{ short t1; short t2; }; /*@ requires 0<=n<=UINT_...