Page MenuHomePhabricator

mikhail.ramalho (Mikhail Ramalho)
User

Projects

User does not belong to any projects.

User Details

User Since
Jan 23 2017, 5:12 AM (138 w, 3 d)

Recent Activity

Apr 6 2019

mikhail.ramalho added a comment to D54978: Move the SMT API to LLVM.

My own out-of-tree pass #include <llvm/Support/SMTAPI.h> and use cmake's add_llvm_library to compile it into a .so
However, opt -load-pass-plugin=my-pass.so -passes="foo" bar.ll fails:
opt: symbol lookup error: Passes/libStackPasses.so: undefined symbol: _ZN4llvm14CreateZ3SolverEv
(c++filt: llvm::CreateZ3Solver())
If I move the content of Z3Solver.cpp into another file of llvm/Support (like llvm/Support/raw_ostream.cpp)
everything works.

Apr 6 2019, 6:05 AM · Restricted Project, Restricted Project

Mar 27 2019

mikhail.ramalho committed rGf5f8d27d3912: New methods to check for under-/overflow in the SMT API (authored by mikhail.ramalho).
New methods to check for under-/overflow in the SMT API
Mar 27 2019, 9:55 AM

Mar 26 2019

mikhail.ramalho added a comment to D54978: Move the SMT API to LLVM.

I'm afraid this broke some bots that build with LLVM_ENABLE_MODULES=1.

For example:

http://green.lab.llvm.org/green/view/LLDB/job/lldb-cmake/22411/consoleFull#710926295dd1929ea-7054-4089-b7ef-4624c3781fa4

Undefined symbols for architecture x86_64:
  "llvm::errs()", referenced from:
      llvm::SMTExpr::dump() const in liblldbDebugserverCommon.a(RNBSocket.cpp.o)
      llvm::SMTSolver::dump() const in liblldbDebugserverCommon.a(RNBSocket.cpp.o)
      llvm::SMTSort::dump() const in liblldbDebugserverCommon.a(RNBSocket.cpp.o)
      llvm::SMTExpr::dump() const in liblldbDebugserverCommon.a(SocketAddress.cpp.o)
      llvm::SMTSolver::dump() const in liblldbDebugserverCommon.a(SocketAddress.cpp.o)
      llvm::SMTSort::dump() const in liblldbDebugserverCommon.a(SocketAddress.cpp.o)

Long story short: You can't have an LLVM_DUMP_METHOD defined inline inside of a module.

One way to fix this would be to move the function body of the various

LLVM_DUMP_METHOD void dump() const { print(llvm::errs()); }

functions into .cpp files.

Mar 26 2019, 7:25 AM · Restricted Project, Restricted Project
mikhail.ramalho committed rG25f9094d89d0: Moved body of methods dump to .cpp file to fix compilation when modules are… (authored by mikhail.ramalho).
Moved body of methods dump to .cpp file to fix compilation when modules are…
Mar 26 2019, 7:25 AM

Mar 25 2019

mikhail.ramalho created D59796: New methods to check for under-/overflow in the SMT API.
Mar 25 2019, 1:13 PM · Restricted Project
mikhail.ramalho committed rGdb695c834f2c: Moved everything SMT-related to LLVM and updated the cmake scripts. (authored by mikhail.ramalho).
Moved everything SMT-related to LLVM and updated the cmake scripts.
Mar 25 2019, 10:49 AM
mikhail.ramalho added a comment to D54978: Move the SMT API to LLVM.

! In D54978#1441417, @mikhail.ramalho wrote:
Sure, I'll create a new revision with the added functions tonight.

I am very happy with your quickly reply.
btw, Z3_get_bv_sort_size is also needed :)
Thanks for your nice job!

Mar 25 2019, 8:21 AM · Restricted Project, Restricted Project
mikhail.ramalho added a comment to D54978: Move the SMT API to LLVM.

! In D54978#1440464, @ddcc wrote:

Do you know if this configuration builds fine now?

Mar 25 2019, 7:24 AM · Restricted Project, Restricted Project

Mar 19 2019

mikhail.ramalho added a comment to D54978: Move the SMT API to LLVM.

Fixed.

Mar 19 2019, 8:17 AM · Restricted Project, Restricted Project
mikhail.ramalho updated the diff for D54978: Move the SMT API to LLVM.

Fix copy-and-paste error.

Mar 19 2019, 8:16 AM · Restricted Project, Restricted Project

Mar 18 2019

mikhail.ramalho added a comment to D54978: Move the SMT API to LLVM.

Hi all,

Mar 18 2019, 1:14 PM · Restricted Project, Restricted Project
mikhail.ramalho updated the diff for D54978: Move the SMT API to LLVM.

Updated script to parse Z3's headers and changed the workflow to handle cross compilation cases.

Mar 18 2019, 1:08 PM · Restricted Project, Restricted Project
mikhail.ramalho updated the diff for D54978: Move the SMT API to LLVM.

Fixes:

  • FindZ3.cmake format .
  • Wrong SMTExpr namespace in SMTConstraintManager.h.
Mar 18 2019, 8:18 AM · Restricted Project, Restricted Project

Mar 15 2019

mikhail.ramalho added a comment to D54978: Move the SMT API to LLVM.

The only relevant commit that I can find is https://github.com/Z3Prover/z3/commit/2cb4223979cc94e2ebc4e49a9e83adbdcd2b6979 , but it first landed in z3 4.6.0. It looks like it's specific to CMake though, so is it different if you use the python build? I haven't tried the CMake build.

Mar 15 2019, 8:13 PM · Restricted Project, Restricted Project
mikhail.ramalho added a comment to D54978: Move the SMT API to LLVM.

Sorry for the massive delay, but I just updated the FindZ3 script to retrieve the version from the lib. I changed it to use try_run instead of try_compile so we can get the version number.

I tried to use @brzycki code to get the version from the header, however, it's not working for Z3 4.8.4. In Z3 4.8.3 the FULL_VERSION is a nice "Z3 4.8.3.0" but in version 4.8.4 it's "Z3 4.8.4.10272 d6df51951f4c master z3-4.8.4" and cmake fails with the following message:

Thanks for making the changes! Is this being parsed from e.g. /usr/include/z3_version.h? I checked their code, and I have a local build of z3 4.8.5.0, but I'm not seeing those changes to the version string:

#define Z3_FULL_VERSION    "Z3 4.8.5.0"
Mar 15 2019, 7:40 PM · Restricted Project, Restricted Project
mikhail.ramalho added a comment to D54978: Move the SMT API to LLVM.

Hi all,

Mar 15 2019, 1:55 PM · Restricted Project, Restricted Project
mikhail.ramalho updated the diff for D54978: Move the SMT API to LLVM.

Update Z3 script to use cmake's try_run in order to retrieve the version from the lib.

Mar 15 2019, 1:46 PM · Restricted Project, Restricted Project

Feb 13 2019

mikhail.ramalho added a comment to D54978: Move the SMT API to LLVM.

Hi guys,

Feb 13 2019, 3:24 PM · Restricted Project, Restricted Project
mikhail.ramalho updated the diff for D54978: Move the SMT API to LLVM.

Update FindZ3.cmake to do a runtime check of the version.

Feb 13 2019, 3:21 PM · Restricted Project, Restricted Project

Feb 12 2019

mikhail.ramalho added a comment to D54978: Move the SMT API to LLVM.

I'm wondering if we can remove the binary requirement all together: is it possible to run a small program that would return EXIT_SUCCESS if the library is the correct version?

Hi @mikhail.ramalho, I don't think this is feasible unfortunately. If we're using a cross-compiler the emitted binary won't be native to the platform. In other words, you cannot test for Z3 as a run-time property.

Feb 12 2019, 4:02 PM · Restricted Project, Restricted Project
mikhail.ramalho added a comment to D54978: Move the SMT API to LLVM.

Looks like my last email got lost:

Feb 12 2019, 3:00 PM · Restricted Project, Restricted Project
mikhail.ramalho added a comment to D54978: Move the SMT API to LLVM.

I found a CHECK_CXX_SOURCE_COMPILES, which seems to be used in a number of places in LLVM. I'll give it a try.

Feb 12 2019, 2:56 PM · Restricted Project, Restricted Project

Feb 11 2019

mikhail.ramalho added a comment to D54975: [analyzer] Generalised the SMT state constraints .

To be clear, this patch breaks compilation with Visual Studio 2015. Running tests requires that the code can be built, so no I didn't run the tests.

Feb 11 2019, 2:30 PM · Restricted Project

Feb 10 2019

mikhail.ramalho added a comment to D54978: Move the SMT API to LLVM.

@brzycki, I can't reproduce your error. Maybe you're missing -DLLVM_ENABLE_Z3_SOLVER=OFF?

Feb 10 2019, 11:56 AM · Restricted Project, Restricted Project
mikhail.ramalho added a project to D54978: Move the SMT API to LLVM: Restricted Project.
Feb 10 2019, 11:46 AM · Restricted Project, Restricted Project
mikhail.ramalho reopened D54978: Move the SMT API to LLVM.

Reopening the revision as it was reverted.

Feb 10 2019, 11:44 AM · Restricted Project, Restricted Project

Feb 8 2019

mikhail.ramalho added a comment to D54975: [analyzer] Generalised the SMT state constraints .

@michaelplatings, thanks for the report.

Feb 8 2019, 4:59 PM · Restricted Project
mikhail.ramalho added a comment to D54978: Move the SMT API to LLVM.

Hi everyone, I just saw your messages and reverted the commits.

Feb 8 2019, 4:53 PM · Restricted Project, Restricted Project
mikhail.ramalho committed rG3289ccd848b3: This reverts commit 1440a848a635849b97f7a5cfa0ecc40d37451f5b. and commit… (authored by mikhail.ramalho).
This reverts commit 1440a848a635849b97f7a5cfa0ecc40d37451f5b. and commit…
Feb 8 2019, 4:46 PM

Feb 6 2019

mikhail.ramalho committed rGeac500f0c340: Move the SMT API to LLVM (authored by mikhail.ramalho).
Move the SMT API to LLVM
Feb 6 2019, 7:20 PM
mikhail.ramalho committed rG5f16ad9a1be8: Moved the whole SMT API to a single file. NFC. (authored by mikhail.ramalho).
Moved the whole SMT API to a single file. NFC.
Feb 6 2019, 7:19 PM
mikhail.ramalho committed rGc1f8cad19110: Got rid of the `Z3ConstraintManager` class (authored by mikhail.ramalho).
Got rid of the `Z3ConstraintManager` class
Feb 6 2019, 7:19 PM
mikhail.ramalho committed rGc9cd50726364: Generalised the SMT state constraints (authored by mikhail.ramalho).
Generalised the SMT state constraints
Feb 6 2019, 7:19 PM

Feb 2 2019

Herald added a reviewer for D54978: Move the SMT API to LLVM: serge-sans-paille.

ping

Feb 2 2019, 6:38 AM · Restricted Project, Restricted Project

Dec 17 2018

mikhail.ramalho added inline comments to D54975: [analyzer] Generalised the SMT state constraints .
Dec 17 2018, 7:57 AM · Restricted Project

Dec 10 2018

mikhail.ramalho added a parent revision for D54978: Move the SMT API to LLVM: D54977: [analyzer] Moved the whole SMT API to a single file. NFC..
Dec 10 2018, 12:30 PM · Restricted Project, Restricted Project
mikhail.ramalho added a child revision for D54977: [analyzer] Moved the whole SMT API to a single file. NFC.: D54978: Move the SMT API to LLVM.
Dec 10 2018, 12:30 PM · Restricted Project
mikhail.ramalho added inline comments to D54976: [analyzer] Got rid of the `Z3ConstraintManager` class.
Dec 10 2018, 12:22 PM · Restricted Project
mikhail.ramalho updated the diff for D54978: Move the SMT API to LLVM.

Updates:

  • Don't abort cmake if enabling Z3 but not the CSA.
  • Fixed guards in llvm/Support/SMTAPI.h
  • Moved using namespace llvm; to outside the #if
Dec 10 2018, 12:15 PM · Restricted Project, Restricted Project
mikhail.ramalho added inline comments to D54975: [analyzer] Generalised the SMT state constraints .
Dec 10 2018, 11:59 AM · Restricted Project

Nov 30 2018

mikhail.ramalho updated the diff for D54978: Move the SMT API to LLVM.
  • Updated patch due to changes in D54976.
Nov 30 2018, 7:58 AM · Restricted Project, Restricted Project
mikhail.ramalho updated the diff for D54976: [analyzer] Got rid of the `Z3ConstraintManager` class.

In the future, CreateZ3Solver should be renamed CreateSMTSolver to handle all backends.

Nov 30 2018, 7:34 AM · Restricted Project
mikhail.ramalho added a comment to D54977: [analyzer] Moved the whole SMT API to a single file. NFC..

The advantage is it's easier to find stuff with a 1-1 correspondence between class names and files.
Thus for this change I see a disadvantage and no clear advantages.

Nov 30 2018, 7:30 AM · Restricted Project

Nov 27 2018

mikhail.ramalho added a comment to D54975: [analyzer] Generalised the SMT state constraints .

TBH this seems overly complicated. Z3 already hash-conses all objects; I don't think there is benefit of doing it again on the LLVM side.

What is the benefit from this patch, apart from being able to use ImmutableSet?

Nov 27 2018, 3:33 PM · Restricted Project
mikhail.ramalho added inline comments to D54974: [analyzer] Cleanup constructors in the Z3 backend.
Nov 27 2018, 2:46 PM
mikhail.ramalho added reviewers for D54978: Move the SMT API to LLVM: NoQ, george.karpenkov, alexandre.isoard.
Nov 27 2018, 2:40 PM · Restricted Project, Restricted Project
mikhail.ramalho created D54978: Move the SMT API to LLVM.
Nov 27 2018, 2:38 PM · Restricted Project, Restricted Project
mikhail.ramalho added a parent revision for D54977: [analyzer] Moved the whole SMT API to a single file. NFC.: D54976: [analyzer] Got rid of the `Z3ConstraintManager` class.
Nov 27 2018, 2:36 PM · Restricted Project
mikhail.ramalho added a child revision for D54976: [analyzer] Got rid of the `Z3ConstraintManager` class: D54977: [analyzer] Moved the whole SMT API to a single file. NFC..
Nov 27 2018, 2:35 PM · Restricted Project
mikhail.ramalho created D54977: [analyzer] Moved the whole SMT API to a single file. NFC..
Nov 27 2018, 2:35 PM · Restricted Project
mikhail.ramalho added a parent revision for D54976: [analyzer] Got rid of the `Z3ConstraintManager` class: D54975: [analyzer] Generalised the SMT state constraints .
Nov 27 2018, 2:33 PM · Restricted Project
mikhail.ramalho added a child revision for D54975: [analyzer] Generalised the SMT state constraints : D54976: [analyzer] Got rid of the `Z3ConstraintManager` class.
Nov 27 2018, 2:33 PM · Restricted Project
mikhail.ramalho created D54976: [analyzer] Got rid of the `Z3ConstraintManager` class.
Nov 27 2018, 2:33 PM · Restricted Project
mikhail.ramalho added a parent revision for D54975: [analyzer] Generalised the SMT state constraints : D54974: [analyzer] Cleanup constructors in the Z3 backend.
Nov 27 2018, 2:27 PM · Restricted Project
mikhail.ramalho added a child revision for D54974: [analyzer] Cleanup constructors in the Z3 backend: D54975: [analyzer] Generalised the SMT state constraints .
Nov 27 2018, 2:27 PM
mikhail.ramalho created D54975: [analyzer] Generalised the SMT state constraints .
Nov 27 2018, 2:26 PM · Restricted Project
mikhail.ramalho added a reviewer for D54974: [analyzer] Cleanup constructors in the Z3 backend: NoQ.
Nov 27 2018, 2:17 PM
mikhail.ramalho created D54974: [analyzer] Cleanup constructors in the Z3 backend.
Nov 27 2018, 2:16 PM

Nov 14 2018

mikhail.ramalho added a comment to D54391: Fix compatibility with z3-4.8.1.

Since we're supporting version 4.8.1 now, the cmake file should be changed to "minimum" instead of "exact".

Nov 14 2018, 6:32 AM · Restricted Project

Oct 25 2018

mikhail.ramalho added a reviewer for D53694: [analyzer] Move canReasonAbout from Z3ConstraintManager to SMTConstraintManager: NoQ.
Oct 25 2018, 5:56 AM
mikhail.ramalho created D53694: [analyzer] Move canReasonAbout from Z3ConstraintManager to SMTConstraintManager.
Oct 25 2018, 5:55 AM
mikhail.ramalho added a comment to D53637: [analyzer] Fixed bitvector from model always being unsigned.

It doesn't make any difference in practice, for now.

Oct 25 2018, 5:35 AM

Oct 24 2018

mikhail.ramalho created D53637: [analyzer] Fixed bitvector from model always being unsigned.
Oct 24 2018, 3:38 AM

Sep 21 2018

mikhail.ramalho created D52365: [analyzer] Improvements to the SMT API.
Sep 21 2018, 10:24 AM

Sep 15 2018

mikhail.ramalho added a comment to D51667: [analyzer] Dump stable identifiers for exploded nodes.

Hey guys, the assertion is being triggered for me (I'm using clang r342322):

$ cat ~/main.c
void foo(unsigned width)
{
  int base;
  int i = 0;
Sep 15 2018, 9:43 AM

Aug 16 2018

mikhail.ramalho updated subscribers of D50818: [analyzer] Improved cmake configuration for Z3.

Nit. Rename this something like CLANG_ANALYZER_Z3_INSTALL_PREFIX. The

description is also not very accurate

  • Again this is an install prefix, just saying prefix is too vague.
  • Z3 is a constraint solver, not a constraint manager.
  • builds the static analyzer? I presume you mean this option being on implies the static analyzer is built? Maybe say Implies CLANG_ANALYZER_BUILD_Z3?

Prefix is the location where Z3 is installed on the machine. You can see
it's used in FindZ3.cmake:

Aug 16 2018, 4:58 PM · Restricted Project
mikhail.ramalho added a comment to D50818: [analyzer] Improved cmake configuration for Z3.

Yeah, although the C API is considered to be fairly stable, it looks like a bunch of types have changed around recently. As of Z3 4.8.0, they've moved to stdbool.h and stdint.h, so I believe there's a couple of reinterpret_cast that can be removed from the code now. It looks like Z3_bool is also now typedef'd to a bool instead of an int. The configuration options can also be bit unstable, and my impression is that they've changed around over time.

Aug 16 2018, 6:28 AM · Restricted Project

Aug 15 2018

mikhail.ramalho updated the diff for D50773: [analyzer] added cache for SMT queries in the SMTConstraintManager.

Add comment to the cache member

Aug 15 2018, 5:53 AM
mikhail.ramalho added a child revision for D50772: [analyzer] Moved all CSA code from the SMT API to a new header, `SMTConv.h`. NFC.: D50773: [analyzer] added cache for SMT queries in the SMTConstraintManager.
Aug 15 2018, 5:46 AM
mikhail.ramalho added a parent revision for D50773: [analyzer] added cache for SMT queries in the SMTConstraintManager: D50772: [analyzer] Moved all CSA code from the SMT API to a new header, `SMTConv.h`. NFC..
Aug 15 2018, 5:46 AM
mikhail.ramalho created D50773: [analyzer] added cache for SMT queries in the SMTConstraintManager.
Aug 15 2018, 5:45 AM
mikhail.ramalho retitled D50768: [analyzer] Delete SMTContext. NFC. from [analyzer] Delete SMTContext to [analyzer] Delete SMTContext. NFC..
Aug 15 2018, 5:30 AM
mikhail.ramalho retitled D50770: [analyzer] Templatefy SMTConstraintManager so more generic code can be moved from solver specific implementations. NFC. from [analyzer] Templatefy SMTConstraintManager so more generic code can be moved from solver specific implementations to [analyzer] Templatefy SMTConstraintManager so more generic code can be moved from solver specific implementations. NFC..
Aug 15 2018, 5:29 AM
mikhail.ramalho added a child revision for D50770: [analyzer] Templatefy SMTConstraintManager so more generic code can be moved from solver specific implementations. NFC.: D50772: [analyzer] Moved all CSA code from the SMT API to a new header, `SMTConv.h`. NFC..
Aug 15 2018, 5:29 AM
mikhail.ramalho created D50772: [analyzer] Moved all CSA code from the SMT API to a new header, `SMTConv.h`. NFC..
Aug 15 2018, 5:29 AM
mikhail.ramalho added a parent revision for D50772: [analyzer] Moved all CSA code from the SMT API to a new header, `SMTConv.h`. NFC.: D50770: [analyzer] Templatefy SMTConstraintManager so more generic code can be moved from solver specific implementations. NFC..
Aug 15 2018, 5:29 AM
mikhail.ramalho added a child revision for D50768: [analyzer] Delete SMTContext. NFC.: D50770: [analyzer] Templatefy SMTConstraintManager so more generic code can be moved from solver specific implementations. NFC..
Aug 15 2018, 5:18 AM
mikhail.ramalho added a parent revision for D50770: [analyzer] Templatefy SMTConstraintManager so more generic code can be moved from solver specific implementations. NFC.: D50768: [analyzer] Delete SMTContext. NFC..
Aug 15 2018, 5:18 AM
mikhail.ramalho created D50770: [analyzer] Templatefy SMTConstraintManager so more generic code can be moved from solver specific implementations. NFC..
Aug 15 2018, 5:17 AM
mikhail.ramalho created D50768: [analyzer] Delete SMTContext. NFC..
Aug 15 2018, 5:09 AM

Aug 13 2018

mikhail.ramalho added a comment to D50594: [analyzer] [NFC] Introduce separate targets for testing the analyzer: check-clang-analyzer and check-clang-analyzer-z3.

I can't comment on the code but it works correctly for me.

Aug 13 2018, 1:14 PM

Jul 31 2018

mikhail.ramalho created D50090: [analyzer] WIP: Move `TimerGroup` to Analyzer's options.
Jul 31 2018, 11:13 AM

Jul 25 2018

mikhail.ramalho added a comment to D49536: [Analyzer] Quick Fix for exponential execution time when simpilifying complex additive expressions.

Uhm, dunno, plist/FileCheck tests are annoying. What i usually do to make sense out of them is update the tested output with the actual output and look at git diff. From that it's usually obvious what exactly happened (warnings added, warnings removed, warnings moved to a different location, intermediate diagnostics added, intermediate diagnostics removed, intermediate diagnostics moved to a different location). Could you do that and see if it makes sense or attach the diff here so that we could have a look?

Jul 25 2018, 6:15 PM
mikhail.ramalho added a comment to D49536: [Analyzer] Quick Fix for exponential execution time when simpilifying complex additive expressions.

I getting the following error when analyzing test/Analysis/plist-macros.cpp, usign z3 as constraint manager (-analyzer-constraints=z3 -DANALYZER_CM_Z3):

/home/mgadelha/llvm/tools/clang/test/Analysis/plist-macros.cpp:640:16: error: CHECK-NEXT: expected string not found in input
// CHECK-NEXT: <key>line</key><integer>36</integer>
               ^
/home/mgadelha/llvm/build/tools/clang/test/Analysis/Output/plist-macros.cpp.tmp.plist:562:2: note: scanning from here
 <key>line</key><integer>37</integer>
 ^
Jul 25 2018, 5:42 PM
mikhail.ramalho updated the diff for D49818: [analyzer] Fixed method to get APSInt model.

Added a comment explaining why we have a weird if condition in toAPSInt.

Jul 25 2018, 2:57 PM
mikhail.ramalho added inline comments to D49818: [analyzer] Fixed method to get APSInt model.
Jul 25 2018, 2:32 PM
mikhail.ramalho created D49818: [analyzer] Fixed method to get APSInt model.
Jul 25 2018, 1:06 PM
mikhail.ramalho added a comment to D49749: [analyzer] Admit that we can't simplify the newly produced mixed Loc/NonLoc expressions..

It fixes Xerces verification. Thanks.

Jul 25 2018, 8:54 AM
mikhail.ramalho created D49799: [analyzer] Update SMT API documentation and methods.
Jul 25 2018, 7:59 AM

Jul 24 2018

mikhail.ramalho added inline comments to D49768: [analyzer] Removed API used by the Refutation Manager from SMTConstraintManager and replace by proper calls to SMTSolver.
Jul 24 2018, 5:03 PM
mikhail.ramalho retitled D49769: [analyzer] Use the macro REGISTER_TRAIT_WITH_PROGRAMSTATE in the Z3 backend from [analyzer] Use the macro REGISTER_TRAIT_WITH_PROGRAMSTATE in the Z3 backedn to [analyzer] Use the macro REGISTER_TRAIT_WITH_PROGRAMSTATE in the Z3 backend.
Jul 24 2018, 5:01 PM
mikhail.ramalho edited parent revisions for D49769: [analyzer] Use the macro REGISTER_TRAIT_WITH_PROGRAMSTATE in the Z3 backend, added: 1; removed: 1.
Jul 24 2018, 4:45 PM
mikhail.ramalho added a child revision for D49768: [analyzer] Removed API used by the Refutation Manager from SMTConstraintManager and replace by proper calls to SMTSolver: D49769: [analyzer] Use the macro REGISTER_TRAIT_WITH_PROGRAMSTATE in the Z3 backend.
Jul 24 2018, 4:45 PM
mikhail.ramalho removed a child revision for D49767: [analyzer] Moved code from SMTConstraintManager to SMTSolver: D49769: [analyzer] Use the macro REGISTER_TRAIT_WITH_PROGRAMSTATE in the Z3 backend.
Jul 24 2018, 4:45 PM
mikhail.ramalho added a parent revision for D49769: [analyzer] Use the macro REGISTER_TRAIT_WITH_PROGRAMSTATE in the Z3 backend: D49767: [analyzer] Moved code from SMTConstraintManager to SMTSolver.
Jul 24 2018, 4:36 PM
mikhail.ramalho added a child revision for D49767: [analyzer] Moved code from SMTConstraintManager to SMTSolver: D49769: [analyzer] Use the macro REGISTER_TRAIT_WITH_PROGRAMSTATE in the Z3 backend.
Jul 24 2018, 4:36 PM
mikhail.ramalho created D49769: [analyzer] Use the macro REGISTER_TRAIT_WITH_PROGRAMSTATE in the Z3 backend.
Jul 24 2018, 4:36 PM
mikhail.ramalho retitled D49767: [analyzer] Moved code from SMTConstraintManager to SMTSolver from [analyzer] Moved non ConstraintManager code to SMTSolver to [analyzer] Moved code from SMTConstraintManager to SMTSolver.
Jul 24 2018, 4:32 PM
mikhail.ramalho added a parent revision for D49768: [analyzer] Removed API used by the Refutation Manager from SMTConstraintManager and replace by proper calls to SMTSolver: D49767: [analyzer] Moved code from SMTConstraintManager to SMTSolver.
Jul 24 2018, 4:31 PM
mikhail.ramalho added a child revision for D49767: [analyzer] Moved code from SMTConstraintManager to SMTSolver: D49768: [analyzer] Removed API used by the Refutation Manager from SMTConstraintManager and replace by proper calls to SMTSolver.
Jul 24 2018, 4:31 PM