小编Bar*_*ker的帖子

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

#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.