Closed
Description
I find CBMC 5.84 reports an unsound result for the following test case:
#include <stdio.h>
#ifdef CBMC
#else
#define __CPROVER_assert(...)
#endif
int main(void) {
volatile int x = 0;
int y;
// This statement exhibits both unspecified behaviour on evalation order,
// and also Undefined Behaviour, owing to more than one side-effect to
// a single object before a single sequence point
y = (x = 2) + (x = 1);
__CPROVER_assert(y == 0, "Oops0..."); // FAILURE
__CPROVER_assert(y == 1, "Oops1..."); // FAILURE
__CPROVER_assert(y == 2, "Oops2..."); // SUCCESS ?!?!?
__CPROVER_assert(y == 3, "Oops3..."); // FAILURE
printf ("y is %d\n", y); // Prints "y is 3" with clang 14.0.3
}
An attempt to verify shows that CBMC thinks that the final value of y is 2:
rodchap@f4d4889dcf6d try % cbmc --version
5.84.0 (cbmc-5.84.0)
rodchap@f4d4889dcf6d try % cbmc -DCBMC rogu.c
CBMC version 5.84.0 (cbmc-5.84.0) 64-bit arm64 macos
Parsing rogu.c
Converting
Type-checking rogu
Generating GOTO Program
Adding CPROVER library (arm64)
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.000527709s
size of program expression: 44 steps
simple slicing removed 21 assignments
Generated 4 VCC(s), 3 remaining after simplification
Runtime Postprocess Equation: 5.792e-06s
Passing problem to propositional reduction
converting SSA
Runtime Convert SSA: 5.75e-05s
Running propositional reduction
Post-processing
Runtime Post-process: 2.5e-06s
Solving with MiniSAT 2.2.1 with simplifier
64 variables, 0 clauses
SAT checker: instance is SATISFIABLE
Runtime Solver: 1.5708e-05s
Runtime decision procedure: 8.6625e-05s
** Results:
rogu.c function main
[main.assertion.1] line 17 Oops0...: FAILURE
[main.assertion.2] line 18 Oops1...: FAILURE
[main.assertion.3] line 19 Oops2...: SUCCESS
[main.assertion.4] line 20 Oops3...: FAILURE
** 3 of 4 failed (2 iterations)
VERIFICATION FAILED
Compling with clang 14.0.3 (on Apple M1 macOS 13.3.1):
rodchap@f4d4889dcf6d try % gcc --version
Apple clang version 14.0.3 (clang-1403.0.22.14.1)
Target: arm64-apple-darwin22.4.0
Thread model: posix
InstalledDir: /Library/Developer/CommandLineTools/usr/bin
rodchap@f4d4889dcf6d try % gcc -o rogu rogu.c
rogu.c:15:10: warning: multiple unsequenced modifications to 'x' [-Wunsequenced]
y = (x = 2) + (x = 1);
^ ~
1 warning generated.
rodchap@f4d4889dcf6d try % ./rogu
y is 3
I would hope that CBMC would detect the undefined behaviour (as clang does) and reject the program.