Open
Description
On this program:
#include <stdint.h>
#include <stdlib.h>
#include <string.h>
#define M 4
typedef struct {
uint8_t val[M];
} s;
size_t nondet_size_t();
int main() {
size_t n = nondet_size_t();
__CPROVER_assume(0 < n && n <= 10);
s *s1 = malloc(n * sizeof(s));
uint8_t *buf = malloc(n * M);
size_t i = nondet_size_t();
if (i < n) {
s *x = &s1[i];
memcpy(&buf[0], x->val, M);
}
}Verification passes without --smt2 but fails with --smt2:
Without:
$ cbmc test.c
CBMC version 5.81.0 (cbmc-5.81.0) 64-bit x86_64 linux
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.00352765s
size of program expression: 127 steps
simple slicing removed 35 assignments
Generated 3 VCC(s), 3 remaining after simplification
Runtime Postprocess Equation: 3.8991e-05s
Passing problem to propositional reduction
converting SSA
Runtime Convert SSA: 0.00141905s
Running propositional reduction
Post-processing
Runtime Post-process: 7.3871e-05s
Solving with MiniSAT 2.2.1 with simplifier
2178 variables, 3603 clauses
SAT checker: instance is UNSATISFIABLE
Runtime Solver: 0.00748485s
Runtime decision procedure: 0.00895971s
** Results:
<builtin-library-malloc> function malloc
[malloc.assertion.1] line 31 max allocation size exceeded: SUCCESS
[malloc.assertion.2] line 36 max allocation may fail: SUCCESS
test.c function main
[main.precondition_instance.1] line 23 memcpy src/dst overlap: SUCCESS
[main.precondition_instance.2] line 23 memcpy source region readable: SUCCESS
[main.precondition_instance.3] line 23 memcpy destination region writeable: SUCCESS
** 0 of 5 failed (1 iterations)
VERIFICATION SUCCESSFUL
With:
$ cbmc test.c --smt2
CBMC version 5.81.0 (cbmc-5.81.0) 64-bit x86_64 linux
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.00352345s
size of program expression: 127 steps
simple slicing removed 35 assignments
Generated 3 VCC(s), 3 remaining after simplification
Runtime Postprocess Equation: 1.2231e-05s
Passing problem to SMT2 QF_AUFBV using Z3
converting SSA
Runtime Convert SSA: 0.000627752s
Running SMT2 QF_AUFBV using Z3
Runtime Solver: 0.031041s
Runtime decision procedure: 0.0317815s
Running SMT2 QF_AUFBV using Z3
Runtime Solver: 0.0198296s
Runtime decision procedure: 0.0198902s
** Results:
<builtin-library-malloc> function malloc
[malloc.assertion.1] line 31 max allocation size exceeded: SUCCESS
[malloc.assertion.2] line 36 max allocation may fail: SUCCESS
test.c function main
[main.precondition_instance.1] line 23 memcpy src/dst overlap: SUCCESS
[main.precondition_instance.2] line 23 memcpy source region readable: FAILURE
[main.precondition_instance.3] line 23 memcpy destination region writeable: SUCCESS
** 1 of 5 failed (2 iterations)
VERIFICATION FAILED
CBMC version: 5.81.0
Operating system: Ubuntu 20.04
Exact command line resulting in the issue: cbmc test.c --smt2
What behaviour did you expect: Verification successful
What happened instead: Verification failed