验证无无符号整数绕组的情况

Question

Frama-c似乎允许无符号整数数学进行包围，而它却假设有符号整数数学不会溢出，这一点是需要以后通过 -wp-rte 标志。(我个人使用的是Frama-C 20.0 Calcium。)我想以某种方式创建一个保证计算属性不溢出的要求。我试图处理的问题的一个简化版本是。

#include <stdint.h>

struct example_struct {
  unsigned int a;
  unsigned int b;
};

/*@
  predicate valid_example_struct_one{L}(struct example_struct ex_struct) =
    ex_struct.a * ex_struct.b <= UINT_MAX;
*/

很明显，由于无符号整数数学的包围，上面的谓词总是真。我希望能够将a，和b投为不会溢出的整数类型，或者用其他方法指定它不能溢出。下面的方法似乎有点用。

/*@
  predicate valid_example_struct_two{L}(struct example_struct ex_struct) =
    1 <= UINT_MAX / ex_struct.a / ex_struct.b;
*/

但是，我不确定上面的方法是否真的是等价的，因为它很难证明（注意到a和b的交换）:

  1 <= UINT_MAX / ex_struct.b / ex_struct.a;

如果我要求它在输入的情况下证明有效_example_struct_two。有没有人有建议说a * b小于uint_max（不做包围）？

Answer 1

你的谓词

/*@
  predicate valid_example_struct_one{L}(struct example_struct ex_struct) =
    ex_struct.a * ex_struct.b <= UINT_MAX;
*/

并不是 "由于对无符号整数数学的包络，总是为真"。正如ACSL手册中提到的，ACSL中所有的算术运算都是在 integer (或 real)类型，即没有包围。因此，它是表达没有算术溢出的标准方式，也是RTE和Eva在发出相关告警时使用的方式。

也就是说，RTE完全可以发出无符号溢出的断言，但这必须通过内核选项明确激活 -warn-unsigned-overflow (见 Frama-C用户手册符号溢出，第6.3节。这个选项没有被默认激活的原因是，与有符号溢出不同的是，无符号溢出在C语言中有着完美的语义定义。