Skip to content

goto-instrument --dump-c does not propery generate for rol or ror operators. #6241

Closed
@vecchiot-aws

Description

@vecchiot-aws

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\")))");

Metadata

Metadata

Assignees

Labels

Type

No type

Projects

No projects

Milestone

No milestone

Relationships

None yet

Development

No branches or pull requests

Issue actions