frama-c - 依赖于无符号整数溢出的代码的证明？

Question

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

#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 插件仍然需要并为上面的无符号加法注入(inject)溢出断言 PO。

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

我正在使用 Frama-C Fluorine-20130601，作为引用，使用 alt-ergo 95.1。

Answer 1

I'm working with Frama-C Fluorine-20130601

很高兴看到您找到了使用最新版本的方法。

以下是一些随机信息，尽管它们不能完全回答您的问题，但不适合 StackOverflow 评论:

杰西有:

#pragma JessieIntegerModel(modulo)

上面的编译指示考虑到所有溢出(未定义的有符号和已定义的无符号)都回绕(与有符号溢出相同，在 2 的补码算术中)。生成的证明义务要困难得多，因为它们到处都包含额外的模运算。在自动定理证明器中，通常只有 Simplify 能够对它们做一些事情。

在 Fluorine 中，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;
  …

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