Skip to content

Support for the GCC __builtin_bswap* intrinsics is unimplemented for the incremental smt2 decision procedure #8064

@thomasspriggs

Description

@thomasspriggs

Gcc defines the following builtin / intrinsic functions -

uint16_t __builtin_bswap16(uint16_t);
uint32_t __builtin_bswap32(uint32_t);
uint64_t __builtin_bswap64(uint64_t);

They reverse the order of the bytes which the integers are composed from. These functions arrive at the decision procedure as bswap_exprt or byte swap expressions. This functionality is covered by the regression test cbmc/gcc_bswap1/test.desc.

Metadata

Metadata

Assignees

No one assigned

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions