标签: alt-ergo

我应该如何证明代码的正确性,如下所示,为了避免一些低效率,依赖于模运算？

#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"模型,但是,如果我理解正确,那个模型会在PO中配置逻辑整数的语义,而不是C代码的正式模型.例如,当使用"int"模型时,WP和RTE插件仍然需要并为上面的无符号加法注入溢出断言PO.

在这种情况下,我可以添加规定语句或基本块的逻辑模型的注释,所以我可以告诉Frama-C特定编译器如何实际解释语句？如果是这样,我可以使用其他验证技术来处理定义但通常是缺陷诱导的行为,如无符号环绕,编译器定义的行为,非标准行为(内联组件？)等,然后证明其正确性.周围的代码.我正在想象一些类似于(但更强大)的"断言修复",用于告知某些静态分析器,当某些属性无法为自己派生属​​性时,它们会保留.

我正在使用Frama-C Fluorine-20130601作为参考,使用alt-ergo 95.1.

如何frama-c -wp从wp手册验证示例- 一个简单的swap函数(swap.c):

/* @ requires \valid(a) && \valid(b);
   @ ensures A: *a == \old(*b);
   @ ensures B: *b == \old(*a);
   @ assigns *a,*b;
   @*/
void swap(int * a, int * b);

void swap(int * a, int * b) {
    int tmp = * a;
    *a = *b;
    *b = tmp;
    return ;
}

调用

$ frama -c -wp -wp-rte swap.c

得到:

[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing swap.c (with preprocessing)
[wp] Running …

我正在尝试使用 Frama-c 测试一个函数：

/*@
    ensures \result >= x && \result >= y;
    ensures \result == x || \result == y;
*/

int max( int x, int y){
    return (x>y) ? x : y;
}   

安装完所有要求后：OPAM、why3、alt-ergo 每当我执行frama-c -wp fct.c我收到：

[kernel] Parsing fct.c (with preprocessing)
[wp] Warning: Missing RTE guards
[wp] User Error: Prover 'alt-ergo' not found in why3.conf
[wp] Goal typed_max_ensures : not tried
[wp] Goal typed_max_ensures_2 : not tried
[wp] User Error: Deferred error message was emitted during …