This repository has been archived by the owner on Apr 4, 2019. It is now read-only.

memory layout assertion failed #6

Open

VikiVozarova opened this issue Apr 19, 2016 · 0 comments

VikiVozarova commented Apr 19, 2016 •

edited

Loading

main.c, main.ll: ring_buffer.zip

symdivine reachability main.ll gives error:

symdivine: /home/xvozarov/SymDIVINE/src/llvmsym/memorylayout.h:127: bool llvm_sym::MemoryLayout::isMultival(llvm_sym::MemoryLayout::Value) const: Assertion `v.variable.offset < variablesFlags[ v.variable.segmentId ].size()' failed.

Edit: After declaring variable ringBuffer as global, SymDivine is able to verify the model, might be problem with big structures on stack.

The text was updated successfully, but these errors were encountered:

yaqwsx mentioned this issue

symdivine ltl error #10

Open

Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.