Andrew V. Teylu

Here's our minimal example: ``` #include typedef struct { int x; int y; struct { int a; } w; } sta; void foo(sta s) { } int main(void) { sta...

@kren1 Hmm, good point. Is it correct then to think that this impacts KLEE's ability to print stuff like "potential NULL pointer dereference", rather than the capability to generate test-cases...

I'm sure other people have found this, but in relation to this issue, the LLVM code is here: - https://github.com/llvm/llvm-project/blob/release/6.x/llvm/lib/IR/Verifier.cpp#L2777 ``` if (I->getFunction()->getSubprogram() && CS.getCalledFunction() && CS.getCalledFunction()->getSubprogram()) AssertDI(I->getDebugLoc(), "inlinable function...

I think the answer is _yes_: KLEE calls `createVerifierPass` which has a default argument of `bool FatalErrors = true`. If KLEE were to call `createVerifierPass` (inside of `lib/Module/Optimize.cpp`) with an...

@ccadar actually, I think it _does_ help: With the change: ``` KLEE: output directory is "/home/avj/klee_build/klee/build/../klee-out-1" KLEE: Using STP solver backend inlinable function call in a function with debug info...

@MartinNowack result!!! `$ klee --disable-verify ../test.bc`: ``` KLEE: output directory is "/home/avj/klee_build/klee/build/../klee-out-5" KLEE: Using STP solver backend KLEE: done: total instructions = 413 KLEE: done: completed paths = 1 KLEE:...

@2994186010: the branch is here -- https://github.com/stp/stp/tree/cadical

I have no idea who is responsible for these packages, but ... if you go here https://formulae.brew.sh/formula/infer#default and view the JSON for this bottle: https://formulae.brew.sh/api/formula/infer.json then all three of the...

If you don't want to use Homebrew, you could use the official 1.0 release from here: - https://github.com/facebook/infer/releases/tag/v1.0.0 (scroll to "infer-osx-v1.0.0.tar.xz")

Are you saying the official macOS release did not work for you?