Closed
Description
#include <stdio.h>
void test_shift_fail() {
int x = 1;
x <<= -1; // undefined behavior in C: negative shift count
}
int main() {
test_shift_fail();
return 0;
}l$ esbmc test.c
ESBMC version 7.9.0 64-bit x86_64 linux
Target: 64-bit little-endian x86_64-unknown-linux with esbmclibc
Parsing test.c
test.c:5:7: warning: shift count is negative [-Wshift-count-negative]
x <<= -1; // undefined behavior in C: negative shift count
^ ~~
Converting
Generating GOTO Program
GOTO program creation time: 0.890s
GOTO program processing time: 0.005s
Starting Bounded Model Checking
Symex completed in: 0.003s (13 assignments)
Slicing time: 0.000s (removed 12 assignments)
Generated 0 VCC(s), 0 remaining after simplification (1 assignments)
BMC program time: 0.003s
VERIFICATION SUCCESSFUL
Metadata
Metadata
Assignees
Labels
No labels