invariant check failed

12 views
Skip to first unread message

Song YANG

unread,
Dec 10, 2019, 5:48:12 AM12/10/19
to CProver Support

Hello,
I got errors such as invariant check failed, when I verified my project using CBMC-5.11.
Does anyone know how to solve this?
The error message is shown below :

--- begin invariant violation report ---
Invariant check failed
File: flattening/bv_pointers.cpp:461 function: convert_pointer_type
Condition: expr.id() != ID_byte_update_little_endian
Reason: byte-wise pointer updates are unsupported
Backtrace:
cbmc(+0x1aec7d) [0x5624355f5c7d]
cbmc(+0x1af1df) [0x5624355f61df]
cbmc(+0x10d2fc) [0x5624355542fc]
cbmc(+0x55ed57) [0x5624359a5d57]
cbmc(+0x55a8e3) [0x5624359a18e3]
cbmc(+0x52a2c6) [0x5624359712c6]
cbmc(+0x5569dd) [0x56243599d9dd]
cbmc(+0x558750) [0x56243599f750]
cbmc(+0x558bab) [0x56243599fbab]
cbmc(+0x527763) [0x56243596e763]
cbmc(+0x55a808) [0x5624359a1808]
cbmc(+0x52a2c6) [0x5624359712c6]
cbmc(+0x5263f3) [0x56243596d3f3]
cbmc(+0x5264b6) [0x56243596d4b6]
cbmc(+0x4da9b0) [0x5624359219b0]
cbmc(+0x4e4fce) [0x56243592bfce]
cbmc(+0x21c911) [0x562435663911]
cbmc(+0x21827c) [0x56243565f27c]
cbmc(+0x219b0c) [0x562435660b0c]
cbmc(+0x21d1ab) [0x5624356641ab]
cbmc(+0x221fa5) [0x562435668fa5]
cbmc(+0x222834) [0x562435669834]
cbmc(+0x235c81) [0x56243567cc81]
cbmc(+0x104445) [0x56243554b445]
cbmc(+0x101dc1) [0x562435548dc1]
/lib/x86_64-linux-gnu/libc.so.6(__libc_start_main+0xf0) [0x7fcfe3ef7830]
cbmc(+0x10478a) [0x56243554b78a]


--- end invariant violation report ---


Have a good day.

Martin Nyx Brain

unread,
Dec 10, 2019, 1:37:07 PM12/10/19
to cprover...@googlegroups.com
On Tue, 2019-12-10 at 02:32 -0800, Song YANG wrote:
> Hello,
> I got errors such as invariant check failed, when I verified my
> project
> using CBMC-5.11.
> Does anyone know how to solve this?

Possibly. What is happening is that you are triggering an internal
error in the back-end of CBMC. Is the code you are analysing
manipulating pointers in unusual ways?

There are three things that would help diagnose this:

A. Exactly which version of CBMC you are using, what platform, what
flags are set, etc.

B. A small sample of the code that triggers this problem.

C. If you are building CBMC from source on Linux please, uncomment the
following lines in config.inc:

# Select optimisation or debug info
#CXXFLAGS += -O2 -DNDEBUG
CXXFLAGS += -O0 -g

# With GCC this adds function names in stack backtraces
LINKFLAGS = -rdynamic

rebuild (make clean ; make) and run so that the backtrace contains more
information.

HTH

Cheers,
- Martin


Reply all
Reply to author
Forward
0 new messages