[cfe-dev] Static Analyzer - symbolic expressions in a program

[Bhargava Shastry via cfe-dev]

Update: I got it to work in a hacky way. Biggest problem was figuring
out a build configuration in which minisat and stp libraries could be
statically linked into the SMTConstraintMgr plugin.

Regards,
Bhargava

On 12/09/2015 10:57 AM, Bhargava Shastry wrote:
> I realized the previous patch is too big for review. The relevant diff
> to get your STP patch to work on top of (clang 3457cd) is attached. Hope
> it helps!
> 
> Regards,
> Bhargava
> 
> On 12/09/2015 10:50 AM, Bhargava Shastry wrote:
>> Hi Ryan,
>>
>> I have been trying to get your Clang SA STP patch to work on a local
>> fork of Clang (3.7, commit 3457cd5). After making a few changes, I got
>> it to compile on my Unix system (Ubuntu 12.04) which is great because
>> (according to the README) it hasn't been tested on non-Mac systems.
>>
>> However, I run into issues when I invoke your plug in, like so:
>> ```
>> clang -Xclang -load -Xclang
>> ~/workspace/llvm/lib/SMTConstraintManagerPlugin.so -Xanalyzer
>> -analyzer-constraints=smt --analyze tmp.c
>>
>> : CommandLine Error: Option 'debug' registered more than once!
>> fatal error: error in backend: inconsistency in registered CommandLine
>> options
>> clang-3.7: error: clang frontend command failed with exit code 70 (use
>> -v to see invocation)
>> clang version 3.7.0 (http://llvm.org/git/clang.git
>> 3457cd5516ac741fa106623d9578f5ac88593f4d)
>> Target: x86_64-unknown-linux-gnu
>> Thread model: posix
>> clang-3.7: note: diagnostic msg: PLEASE submit a bug report to
>> http://llvm.org/bugs/ and include the crash backtrace, preprocessed
>> source, and associated run script.
>> clang-3.7: note: diagnostic msg: Error generating preprocessed source(s).
>> ```
>>
>> Any ideas what might be happening here. My patch attached. I am happy to
>> contribute to a future stp patch to clang sa!
>>
>> Regards,
>> Bhargava
>>
> 

-- 
Bhargava Shastry <bshastry at sec.t-labs.tu-berlin.de>
Security in Telecommunications
TU Berlin / Telekom Innovation Laboratories
Ernst-Reuter-Platz 7, Sekr TEL 17 / D - 10587 Berlin, Germany
phone: +49 30 8353 58235