Open VikiVozarova opened 8 years ago
main.c, main.ll: ring_buffer.zip
symdivine reachability main.ll gives error:
symdivine reachability main.ll
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.
main.c, main.ll: ring_buffer.zip
symdivine reachability main.llgives error:Edit: After declaring variable ringBuffer as global, SymDivine is able to verify the model, might be problem with big structures on stack.