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

我应该如何处理验证代码的正确性，以避免效率低下，依赖于模块化算法？依赖无符号整数溢出的代码证明？

#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”的模式，但是，如果我理解正确的话，这种模式配置逻辑整数的采购订单中的语义，而不是C代码的正式模型。例如，在使用“int”模型时，WP和RTE插件仍然需要并注入上面的无符号加法的溢出断言PO。

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

我正在使用Frama-C氟-20130601作为参考，使用alt-ergo 95.1。

来源

2013-08-02 Barrie Slaymaker

一你的代码有问题：让'a'为'UINT32_MIN'并让'b'为'-1'。这是如何处理的？（我没有你的工具/特定编译器的背景） – BLaZuRE

@BLaZuRE：b是无符号的，所以不能是-1。 –

我与邮资-C氟20130601

高兴地看到，你找到了一个方法，可使用最新版本。

这里有一些信息的随机位，虽然他们并没有完全回答你的问题，不适合在StackOverflow的评论：

杰西有：

#pragma JessieIntegerModel(modulo)

以上编译使它考虑所有溢出（包括未定义的符号和定义的未符号的符号）都会回绕（与2的补码运算中的符号溢出相同）。生成的证明义务要难得多，因为它们在任何地方都包含其他模操作。对于自动化的定理证明器，通常只有Simplify能够对它们做些什么。

在氟，RTE并不警告默认情况下，A + B：

$ frama-c -rte t.c -then -print 
[kernel] preprocessing with "gcc -C -E -I. t.c" 
[rte] annotating function my_add 
/* Generated by Frama-C */ 
typedef unsigned int uint32_t; 
uint32_t my_add(uint32_t a, uint32_t b) 
{ 
    uint32_t __retres; 
    uint32_t r; 
    r = a + b; 
    if (r < a) { 
    __retres = 4294967295U; 
    goto return_label; 
    } 
    __retres = r; 
    return_label: return __retres; 
}

RTE可以作出警告无符号除了与选项-warn-unsigned-overflow：

$ frama-c -warn-unsigned-overflow -rte t.c -then -print 
[kernel] preprocessing with "gcc -C -E -I. t.c" 
[rte] annotating function my_add 
/* Generated by Frama-C */ 
typedef unsigned int uint32_t; 
uint32_t my_add(uint32_t a, uint32_t b) 
{ 
    uint32_t __retres; 
    uint32_t r; 
    /*@ assert rte: unsigned_overflow: 0 ≤ a+b; */ 
    /*@ assert rte: unsigned_overflow: a+b ≤ 4294967295; */ 
    r = a + b; 
    …

但是，这恰恰是与你想要的相反，所以我不明白你为什么要这么做。

来源

2013-08-02 22:29:38

我认为问题在于r = a + b的模型似乎没有允许溢出的方式，然后可以用来推断下一条语句完成的溢出检测。我在Windows上尝试过Jessie（模），或许我会在这里再试一次。我也会看着简化; alt-ergo可能无法证明（在不同的例程中）当a和b被限制以防止溢出时，r = a * b不会溢出。再次感谢您的快速回复。 –

您没有提供您一直使用的确切命令行。我想这是frama-c -wp -wp-rte file.c -pp-annot。在这种情况下，确实会产生RTE可能发出的所有断言。但是，您可以通过指示frama-c首先生成您感兴趣的RTE类别（请注意，它们由两种选项控制：frama-c -rte-help和-warn-{signed,unsigned}-{overflow,downcast}定义的选项在内核中），然后在结果上启动wp。这是通过frama-c -rte -pp-annot file.c -then -wp完成的默认情况下，RTE不考虑签名溢出是一个错误，使之与上面的命令行，我能证明你的函数尊重以下规范：

/*@ 
    behavior no_overflow: 
    assumes a + b <= UINT32_MAX; 
    ensures \result == a+b; 
    behavior saturate: 
    assumes a+b > UINT32_MAX; 
    ensures \result == UINT32_MAX; 
*/ 
uint32_t my_add(uint32_t a,uint32_t b);

来源

2013-08-08 12:38:47 Virgile

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

回答

相关问题