Description
When working on a --dump-c
for the Rust Model Checker, we are running into issues with rol
and ror
not being generated properly into C code.
CBMC version: 5.34.0 (cbmc-5.32.1-183-gc50985444)
Operating system: macOS Big Sur v11.4
Exact command line resulting in the issue: symtab2gb test.json --out test.goto; goto-instrument --dump-c test.goto > test.c
with test.json
produces test.c
What behaviour did you expect: The contents of test.c
is valid C code.
What happened instead: The rol
operator translates into an irep
function call:
unsigned char rol8=irep("(\"rol\" \"\" (\"constant\" \"type\" (\"unsignedbv\" \"width\" (\"8\")) \"value\" (\"38\")) \"\" (\"constant\" \"type\" (\"unsignedbv\" \"width\" (\"8\")) \"value\" (\"3\")) \"type\" (\"unsignedbv\" \"width\" (\"8\")))");