diff --git a/regression/cbmc/cpp2/main.cpp b/regression/cbmc/cpp2/main.cpp new file mode 100644 index 00000000000..9f49a0da733 --- /dev/null +++ b/regression/cbmc/cpp2/main.cpp @@ -0,0 +1,47 @@ +#include +#include +#include + +#undef HOTFIX + +typedef struct { + uint32_t value_31_0 : 32; +} signal32_t; + +typedef struct { + uint8_t value_0_0 : 1; +} signal1_t; + +static inline bool yosys_simplec_get_bit_25_of_32(const signal32_t *sig) +{ + return (sig->value_31_0 >> 25) & 1; +} + +struct rvfi_insn_srai_state_t +{ + signal32_t rvfi_insn; + signal32_t rvfi_rs1_rdata; + signal1_t _abc_1398_n364; + signal1_t _abc_1398_n363; +}; + +void test(rvfi_insn_srai_state_t state, bool valid) +{ +#ifndef HOTFIX + state._abc_1398_n364.value_0_0 = yosys_simplec_get_bit_25_of_32(&state.rvfi_insn) ? + yosys_simplec_get_bit_25_of_32(&state.rvfi_rs1_rdata) : state._abc_1398_n363.value_0_0; +#else + state._abc_1398_n364.value_0_0 = yosys_simplec_get_bit_25_of_32(&state.rvfi_insn) ? + yosys_simplec_get_bit_25_of_32(&state.rvfi_rs1_rdata) : (bool)state._abc_1398_n363.value_0_0; +#endif + + assert(valid); +} + +int main(int argc, char* argv[]) +{ + rvfi_insn_srai_state_t state; + bool valid; + test(state, valid); + return 0; +} diff --git a/regression/cbmc/cpp2/test.desc b/regression/cbmc/cpp2/test.desc new file mode 100644 index 00000000000..eb6229bb599 --- /dev/null +++ b/regression/cbmc/cpp2/test.desc @@ -0,0 +1,11 @@ +KNOWNBUG +main.cpp + +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring +^equality without matching types +-- +This has been reported as #933.