Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Verilog Parser 4.4 has problems with file #30

Open
mgudemann opened this issue Sep 13, 2017 · 3 comments
Open

Verilog Parser 4.4 has problems with file #30

mgudemann opened this issue Sep 13, 2017 · 3 comments
Labels

Comments

@mgudemann
Copy link
Contributor

in this (https://groups.google.com/forum/#!topic/cprover-support/rQrlv7NY79A)[thread] a user posted a Verilog file for which apparently properties can only be specified on the command line, properties in the file give

        file or1200_if.v line 222: syntax error before ' ( '
        PARSING ERROR

version 4.4 fails even when the property is specified on the command line

Parsing or1200_if.v
Converting
Type-checking Verilog::or1200_if
Type-checking Verilog::main
--- begin invariant violation report ---
Invariant check failed
File ../../lib/cbmc/src/util/message.h function get_message_handler line 129
Reason: message handler is setBacktrace:
Backtrace
ebmc() [0x46e191]
ebmc() [0x46e706]
ebmc() [0x42ccbd]
ebmc() [0x42cc8b]
ebmc() [0x42a868]
ebmc() [0x5f3ea4]
ebmc() [0x42add0]
ebmc() [0x4267de]
ebmc() [0x4299ba]
ebmc() [0x4441ad]
ebmc() [0x417ca2]
/lib/x86_64-linux-gnu/libc.so.6(__libc_start_main+0xf0) [0x7f25b62b6830]
ebmc() [0x40c2a9]


--- end invariant violation report ---
fish: “ebmc  or1200_if.v --module main…” terminated by signal SIGABRT (Abort)

which works with 4.2

@mgudemann mgudemann added the bug label Sep 13, 2017
@mgudemann
Copy link
Contributor Author

#31 solves the invariant violation

@mgudemann mgudemann self-assigned this Sep 15, 2017
@kroening
Copy link
Member

This may be fixed by #264

@kroening
Copy link
Member

I would be grateful if you could confirm whether #264 (now merged) has fixed this.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
Projects
None yet
Development

No branches or pull requests

2 participants