标签: cbmc

CBMC在以下行中检测到可能的无符号加法溢出:

l = (t + *b)&(0xffffffffL);
c += (l < t);

我同意第一行有可能出现溢出,但我正在处理CBMC无法查看的下一行的进位.如果有溢出,我设置进位1.所以,因为我知道这个,这就是我希望我的代码工作的方式,我想继续进行验证过程.那么,我怎么告诉CBMC忽略这个错误并继续前进呢？

我正在尝试在 GitHub 的开源 C 项目上使用 CBMC（C 边界模型检查：https://www.cprover.org/cbmc/ ）。为了这个问题的目的，让我们考虑以下项目：https://github.com/reubenhwk/radvd

当我用 gcc 编译项目时出现问题。我能够获得调用 cbmc 的可执行文件，例如

cbmc radvd

但我收到以下错误消息：

CBMC version 5.8 64-bit x86_64 linux
failed to open input file radvd`

原因应该是我使用了 gcc 而不是 goto-cc （如下所述： http: //www.cprover.org/cprover-manual/goto-cc.html），所以可能无法识别该文件。我还尝试使用 goto-cc，如上一个链接和http://www.cprover.org/goto-cc/examples/nanosat.html等示例中所述。然而，由于它们是指导性示例，因此使 cbmc 工作似乎很容易。make CC=goto-cc当我对其他项目（例如链接的项目（radvd））执行相同的过程并使用 goto-cc 而不是 gcc 时，我在运行命令 时收到以下消息：

make  all-am
make[1]: Entering directory '/home/stefano/Documents/github/radvd'
  YACC     gram.c
updating gram.h
  CC       libradvd_parser_a-gram.o
/usr/include/stdlib.h:133:1: error: syntax error before 'strtof128'
PARSING ERROR
Makefile:941: recipe for target 'libradvd_parser_a-gram.o' failed
make[1]: *** …