小编Aci*_*urn的帖子

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

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

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