-
Notifications
You must be signed in to change notification settings - Fork 277
Open
Labels
awsBugs or features of importance to AWS CBMC usersBugs or features of importance to AWS CBMC userspending merge
Description
It seems that it only applies at the statement level, but there is no warning given when compiling this with CBMC
int nondet_int();
void main() {
int a = nondet_int();
int b = nondet_int();
int c = a +
#pragma CPROVER check disable "signed-overflow"
a + b;
#pragma CPROVER check pop
}
╰─$ cbmc test.c --signed-overflow-check
CBMC version 5.43.0 (cbmc-5.43.0-19-g6dfd3f78d) 64-bit x86_64 macos
Parsing test.c
Converting
Type-checking test
Generating GOTO Program
Adding CPROVER library (x86_64)
Removal of function pointers and virtual functions
Generic Property Instrumentation
Running with 8 object bits, 56 offset bits (default)
Starting Bounded Model Checking
Runtime Symex: 0.00661267s
size of program expression: 50 steps
simple slicing removed 3 assignments
Generated 2 VCC(s), 2 remaining after simplification
Runtime Postprocess Equation: 3.8862e-05s
Passing problem to propositional reduction
converting SSA
Runtime Convert SSA: 0.00422007s
Running propositional reduction
Post-processing
Runtime Post-process: 0.000268633s
Solving with MiniSAT 2.2.1 with simplifier
438 variables, 1345 clauses
SAT checker: instance is SATISFIABLE
Runtime Solver: 0.00387758s
Runtime decision procedure: 0.00834528s
Running propositional reduction
Solving with MiniSAT 2.2.1 with simplifier
438 variables, 1 clauses
SAT checker: instance is SATISFIABLE
Runtime Solver: 7.3659e-05s
Runtime decision procedure: 0.000119505s
** Results:
/Library/Developer/CommandLineTools/SDKs/MacOSX.sdk/usr/include/stdio.h function __sputc
[__sputc.overflow.1] line 261 arithmetic overflow on signed - in _p->_w - 1: SUCCESS
test.c function main
[main.overflow.1] line 9 arithmetic overflow on signed + in a + a: FAILURE
[main.overflow.2] line 11 arithmetic overflow on signed + in a + a + b: FAILURE
** 2 of 3 failed (3 iterations)
VERIFICATION FAILED
Metadata
Metadata
Assignees
Labels
awsBugs or features of importance to AWS CBMC usersBugs or features of importance to AWS CBMC userspending merge