Skip to content

Conversation

@forejtv
Copy link
Contributor

@forejtv forejtv commented May 10, 2019

A follow-up from #4633, this PR is a shift towards handling more of the string operations in Java. All it does is to remove a couple of bindings from Java methods to string solver, so that the actual Java implementation is used.

There is an accompanying PR for java-models-library: diffblue/java-models-library#23.

  • Each commit message has a non-empty body, explaining why the change was made.
  • Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
  • The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
  • Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
  • My commit message includes data points confirming performance improvements (if claimed).
  • My PR is restricted to a single feature or bugfix.
  • White-space or formatting changes outside the feature-related changed lines are in commits of their own.

Copy link
Contributor

@thk123 thk123 left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Less code is good if no tests start failing :)

Copy link
Collaborator

@martin-cs martin-cs left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Yeah... less axiom instantiation built in is generally a good thing.

@tautschnig
Copy link
Collaborator

@forejtv cprover_string_concat_double_func now needs to be removed from irep_ids.def as it is no longer used.

@forejtv
Copy link
Contributor Author

forejtv commented May 12, 2019

This is now ready to go, I'll just wait for diffblue/java-models-library#23 to be approved so that we don't lose any existing functionality.

Copy link
Contributor

@allredj allredj left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

✔️
Passed Diffblue compatibility checks (cbmc commit: af7bdaa).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/111782136

@tautschnig
Copy link
Collaborator

@forejtv I'll leave it to you to merge this so that you can make sure that the submodule pointer points to exactly the right commit.

@forejtv forejtv merged commit f541d64 into diffblue:develop May 15, 2019
@forejtv forejtv deleted the forejtv/floats-to-string branch May 15, 2019 08:35
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

5 participants