invariant check failed

[Song YANG]

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]

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