CBMC detects a possible unsigned addition overflow in the following lines:
l = (t + *b)&(0xffffffffL);
c += (l < t);
I agree that there is a possibility of an overflow in the first line, but I am taking care of the carry in the next line which CBMC is not able to look at. If in case there is an overflow I am setting the carry 1. So since I am aware of this and this and this is how I want my code to work I would like to move on with the verification process. So, how is it that I tell the CBMC to overlook this bug and move on?
TL;DR It depends on what the actual types of the variables are. In all cases, CBMC detects an actual bug that could cause undefined behaviour. This means, you should fix your code rather than disable the message in CBMC.
Full answer:
Generally: To the best of my knowledge, CBMC does not allow the exclusion of specific properties (on the other hand, you can check only one single specific property using the
--propertyflag). If you would like a official answer/opinion or make a feature request, I would recommend posting in the CProver Support group.(Of course, one could use
__CPROVER_assumein order to make CBMC exclude the traces leading to the error, but this would be a very, very, very bad idea, as this might make other problems unreachable.)Variant 1: I assume your code looks something like (related to this: please, please post self-contained examples and explain precisely what the issue is, it's hard to guess these things)
and you are running
cbmc --signed-overflow-check test.cgiving an output similar to the following one?
CBMC version 5.1 64-bit x86_64 macos Parsing test.c Converting Type-checking test Generating GOTO Program Adding CPROVER library Function Pointer Removal Partial Inlining Generic Property Instrumentation Starting Bounded Model Checking size of program expression: 41 steps simple slicing removed 3 assignments Generated 2 VCC(s), 2 remaining after simplification Passing problem to propositional reduction converting SSA Running propositional reduction Post-processing Solving with MiniSAT 2.2.0 with simplifier 792 variables, 2302 clauses SAT checker: negated claim is SATISFIABLE, i.e., does not hold Runtime decision procedure: 0.006s Building error trace Counterexample: State 17 file test.c line 4 function main thread 0 ---------------------------------------------------- l=0 (0000000000000000000000000000000000000000000000000000000000000000) State 18 file test.c line 4 function main thread 0 ---------------------------------------------------- l=0 (0000000000000000000000000000000000000000000000000000000000000000) State 19 file test.c line 5 function main thread 0 ---------------------------------------------------- c=0 (00000000000000000000000000000000) State 20 file test.c line 5 function main thread 0 ---------------------------------------------------- c=0 (00000000000000000000000000000000) State 21 file test.c line 6 function main thread 0 ---------------------------------------------------- t=0 (0000000000000000000000000000000000000000000000000000000000000000) State 22 file test.c line 6 function main thread 0 ---------------------------------------------------- t=-9223372036854775808 (1000000000000000000000000000000000000000000000000000000000000000) State 23 file test.c line 7 function main thread 0 ---------------------------------------------------- s=0 (0000000000000000000000000000000000000000000000000000000000000000) State 24 file test.c line 7 function main thread 0 ---------------------------------------------------- s=-9223372036854775807 (1000000000000000000000000000000000000000000000000000000000000001) State 25 file test.c line 8 function main thread 0 ---------------------------------------------------- b=((long int *)NULL) (0000000000000000000000000000000000000000000000000000000000000000) State 26 file test.c line 8 function main thread 0 ---------------------------------------------------- b=&s!0@1 (0000001000000000000000000000000000000000000000000000000000000000) Violated property: file test.c line 10 function main arithmetic overflow on signed + in t + *b !overflow("+", signed long int, t, *b) VERIFICATION FAILEDI do not think you should disable this property check, even if you could. The reason for this is, as you say, that this addition can overflow, and, integer overflow is undefined behaviour in C, or, as this answer to the question How to check integer overflow in C? nicely puts it:
See also Integer overflow and undefined behavior and How disastrous is integer overflow in C++?.
Thus, this is an actual bug and CBMC has a good reason for telling you about it. What you actually should do is adapt your code so that there are no potential overflows! The answer mentioned above suggests something like (remember to include
limits.h):Variant 2: Here, I assume, your code looks something like:
and you are running
cbmc --unsigned-overflow-check test.cgiving an output similar to the following one?
CBMC version 5.1 64-bit x86_64 macos Parsing test.c Converting Type-checking test Generating GOTO Program Adding CPROVER library Function Pointer Removal Partial Inlining Generic Property Instrumentation Starting Bounded Model Checking size of program expression: 42 steps simple slicing removed 3 assignments Generated 3 VCC(s), 3 remaining after simplification Passing problem to propositional reduction converting SSA Running propositional reduction Post-processing Solving with MiniSAT 2.2.0 with simplifier 519 variables, 1306 clauses SAT checker: negated claim is SATISFIABLE, i.e., does not hold Runtime decision procedure: 0.01s Building error trace Counterexample: State 17 file test.c line 4 function main thread 0 ---------------------------------------------------- l=0 (00000000000000000000000000000000) State 18 file test.c line 4 function main thread 0 ---------------------------------------------------- l=0 (00000000000000000000000000000000) State 19 file test.c line 5 function main thread 0 ---------------------------------------------------- c=0 (00000000000000000000000000000000) State 20 file test.c line 5 function main thread 0 ---------------------------------------------------- c=0 (00000000000000000000000000000000) State 21 file test.c line 6 function main thread 0 ---------------------------------------------------- t=0 (00000000000000000000000000000000) State 22 file test.c line 6 function main thread 0 ---------------------------------------------------- t=4187126263 (11111001100100100111100111110111) State 23 file test.c line 7 function main thread 0 ---------------------------------------------------- s=0 (00000000000000000000000000000000) State 24 file test.c line 7 function main thread 0 ---------------------------------------------------- s=3329066504 (11000110011011011000011000001000) State 25 file test.c line 8 function main thread 0 ---------------------------------------------------- b=((unsigned int *)NULL) (0000000000000000000000000000000000000000000000000000000000000000) State 26 file test.c line 8 function main thread 0 ---------------------------------------------------- b=&s!0@1 (0000001000000000000000000000000000000000000000000000000000000000) Violated property: file test.c line 10 function main arithmetic overflow on unsigned + in t + *b !overflow("+", unsigned int, t, *b) VERIFICATION FAILEDAgain, this is an actual bug and CBMC has a good reason for telling you about it. This one could be fixed by
which gives
Variant 3: If things are as the previous one, but you have
signed intinstead ofunsigned int, things get a bit more complicated. Here, assuming you use (written in a slightly more elaborate way to better see what is going on)and run
cbmc --signed-overflow-check test.cyou will get
Or, written more concisely, if you have
then
and an attempt to convert this into a
signed intis trouble, because it is out of range (see also Does cast between signed and unsigned int maintain exact bit pattern of variable in memory? ).As you can see, this counterexample also is an actual bug, and again, CBMC is right in telling you about it. This means in particular, your masking/maths does not work as expected (your masking turns a negative number into a positive number that is out of bounds) and you need to fix your code, so that the result is within the necessary range. (It's probably worthwhile to carefully think about what you actually want to do in order to make sure you get the right results.)