Changes between Initial Version and Version 1 of Ticket #7, comment 1


Ignore:
Timestamp:
08/20/2018 02:19:16 PM (6 years ago)
Author:
Vladimír Štill
Comment:

Legend:

Unmodified
Added
Removed
Modified

  • Ticket #7, comment 1

    initial v1  
    114. `divine check -C,-fgnu89-inline --svcomp --symbolic ~/repo/sv-benchmarks/c/pthread-ext/39_rand_lock_p0_vs_true-unreach-call.c` -- there is a (probably) spurious memory error on line 46 (invalid dereference, the line manipulates only global and local variables, not allocated variables)
     25. `divine check --symbolic ~/repo/sv-benchmarks/c/pthread-wmm/mix016_power.opt_false-unreach-call.c` -- in debug version of DIVINE fails with
     3{{{
     4loading bitcode … LART … divine: /home/xstill/DIVINE/wip/llvm/lib/IR/Instructions.cpp:299: void llvm::CallInst::init(llvm::FunctionType *, llvm::Value *, ArrayRef<llvm::Value *>, ArrayRef<llvm::OperandBundleDef>, const llvm::Twine &): Assertion `(i >= FTy->getNumParams() || FTy->getParamType(i) == Args[i]->getType()) && "Calling a function with a bad signature!"' failed.
     5}}}
     6  in release mode proceeds to verification and then ends with SEGV.