This is an archive of the discontinued LLVM Phabricator instance.

[Analyzer] Fix Z3ConstraintManager crash (PR37646)
ClosedPublic

Authored by vlad.tsyrklevich on May 31 2018, 9:34 PM.

Diff Detail

Repository
rC Clang

Event Timeline

vlad.tsyrklevich retitled this revision from [Analyzer] Fix Z3 crash (PR37646) to [Analyzer] Fix Z3ConstraintManager crash (PR37646).May 31 2018, 10:30 PM
george.karpenkov requested changes to this revision.Jun 1 2018, 10:44 AM

LGTM with a nit on a test name.

test/Analysis/pr37646.c
1 ↗(On Diff #149396)

The tests are already quite messy, but adding a new file per each bug seems excessive. Could we take your test and test/Analysis/apsint.c and combine them into e.g. z3_apsint_encoding.c ? (also adding a link to bugzilla)

This revision now requires changes to proceed.Jun 1 2018, 10:44 AM
NoQ added a comment.Jun 1 2018, 10:50 AM

We might as well make a directory for z3-specific tests. Eg., z3/bool-bit-width.c.

Also does this test need to be z3-specific? We would also not like to crash here without z3.

ddcc added a comment.Jun 1 2018, 1:09 PM

LGTM with a nit on a test name.

Same.

In D47617#1119268, @NoQ wrote:

Also does this test need to be z3-specific? We would also not like to crash here without z3.

I had the same though originally about the REQUIRES line. Since this code path is very specific to Z3ConstraintManager, it didn't seem useful to run the test on normal buildbots. But I have no preference either way.

In D47617#1119268, @NoQ wrote:

Also does this test need to be z3-specific? We would also not like to crash here without z3.

I originally did that so I could specify enabling and testing the z3 backend; however, looking at the testing infra more I realize that z3 is supposed to be run on the analyzer tests but it seems like z3 tests have been broken since October when r315627 landed. I submitted a fix in https://reviews.llvm.org/D47722

  • Merge test with apsint.c and move to z3/apsint.c
This revision is now accepted and ready to land.Jun 4 2018, 12:05 PM
This revision was automatically updated to reflect the committed changes.
lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp