Assertion failed when translating safe/Arbiter/main.v

[nianzelee]

Hello,

I ran into an assertion failure when I tried to translate the file safe/Arbiter/main.v by the following command:

./v2c-bin/v2c verilog-c/safe/Arbiter/main.v --module main main.c

The error is:

v2c: /users/rajdeep/cbmc/trunk/src/util/std_expr.h:206: symbol_exprt& to_symbol_expr(exprt&): Assertion `expr.id()==dstring(57, 0) && !expr.has_operands()' failed.
Aborted (core dumped)

I downloaded v2c (version 0.1, accessed 2022-09-05) from this website and the input Verilog file is at commit 0b46ae0. My OS is Ubuntu 20.04.

Could you please let me know how to obtain the translated C file safe/Arbiter/main.c?

Thank you!

[Po-Chun-Chien]

I tried to compile v2c from the source but did not succeed.

v2c uses cbmc and hw-cbmc as external libraries.

In src/config.inc

CBMC = ~/cbmc/trunk
HW_CBMC= ~/hw-cbmc/trunk

include $(CBMC)/src/config.inc
include $(CBMC)/src/common

CXXFLAGS+=-g

However, v2c does not work with the latest versions of cbmc and hw-cbmc. Could you also provide the versions you used for compilation? Thanks!

[Gary-oak-Star]

I tried to compile v2c from the source but did not succeed.

v2c uses cbmc and hw-cbmc as external libraries.

In src/config.inc

CBMC = ~/cbmc/trunk
HW_CBMC= ~/hw-cbmc/trunk

include $(CBMC)/src/config.inc
include $(CBMC)/src/common

CXXFLAGS+=-g

However, v2c does not work with the latest versions of cbmc and hw-cbmc. Could you also provide the versions you used for compilation? Thanks!

Hi, did you solve the issue?