alt-ergo

    2热度

    1回答

    SMT证明产量“未知”尽管有强有力的成熟的断言

    假设我们有下面的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 assigns i, a[
    z3 verification frama-c alt-ergo 2015-07-20

    2热度

    1回答

    是否存在不可解释函数的理论（同余分析）？

    我有一组符号变量的： int a, b, c, d, e; 一组未知函数，由若干公理的约束： f1(a, b) = f2(c, b) f1(d, e) = f1(e, d) f3(b, c, e) = f1(b, e) c = f1(a, b) b = d 在此功能f1，f2，f3是未知的，但固定的。所以它不是uninterpreted functions的理论。 我要证明以下断言
    z3 verification smt stp alt-ergo 2016-08-29

    1热度

    1回答

    如何使用Alt-Ergo执行以下SMT-LIB代码

    以下SMT-LIB代码在Z3，MathSat和CVC4中运行时没有问题，但它不在Alt-Ergo中运行，请让我知道会发生什么，非常感谢： (set-logic QF_UF) (set-option :incremental true) (set-option :produce-models true) (declare-fun m() Bool) (declare-fun p() Bool
    z3 smt cvc4 alt-ergo 2013-06-01

    1热度

    1回答

    确保证明代码有缺陷？

    在下面，当相关的C代码被注释掉时，行为neg_limit的后置条件如何被证明是真实的？ 安全 - >检查算术溢出之一是不可证明的，如预期的，但它似乎像neg_limit也应该是无法证明的。 语境：我使用的邮资-C-硼，杰西，并通过gWhy，按住Alt键人体工程学，以学习如何编写规范和证明功能的满足他们。任何关于规范策略，工具等的提示，RTFMing等也是值得赞赏的。到目前为止，我正在阅读ACSL
    frama-c alt-ergo 2013-07-30

    1热度

    1回答

    邮资-C WP常量变量和常量数组

    我想证明与邮资-C的WP插件一些C代码，并与下面的例子有问题： typedef unsigned char uint8_t; const uint8_t globalStringArray[] = "demo"; const int STRING_LEN = 5; /*@ requires \valid(src) && \valid(dest) && len < 32 ; */ voi
    c frama-c alt-ergo 2015-10-05

    5热度

    2回答

    依赖无符号整数溢出的代码证明？

    我应该如何处理验证代码的正确性，以避免效率低下，依赖于模块化算法？ #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的“INT”的模
    frama-c alt-ergo 2013-08-02

    3热度

    1回答

    邮资-C WP插件无法验证从手动

    交换函数如何使frama-c -wp验证从wp manual的示例 - 一个微不足道swap函数（swap.c）： /* @ requires \valid(a) && \valid(b); @ ensures A: *a == \old(*b); @ ensures B: *b == \old(*a); @ assigns *a,*b; @*/ void
    frama-c alt-ergo 2015-09-04
最新问题