Remove unused int concatenation irep_id

[forejtv]

ID_cprover_string_concat_int_func is defined and used once to substitute StringBuffer.append(int) Java method call, but then never again. As a result, any use of StringBuffer.append(int) will make jbmc crash with invariant violation. This commit removes ID_cprover_string_concat_int_func completely, which makes it possible to define behaviour of StringBuffer.append(int) in Java code.

• 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.

[JohnDumbell]

I just put up a PR to try and add this in (#4632). I don't really mind which way we go - in Java or the C++, whichever's easier.

[allredj]

I think removing the ID_cprover_string_concat_int_func function is the way to go. But why only do it for the int case? The double, float and long cases as still there.

[romainbrenguier]

@JohnDumbell

I just put up a PR to try and add this in (#4632). I don't really mind which way we go - in Java or the C++, whichever's easier.

Implementing it in Java has the advantage that the string_concat_builtin_functiont class will take care of dependencies to simplify constraints that are not needed and we don't need to reimplement the class for string_concat_int_builtin_functiont.

@allredj

I think removing the ID_cprover_string_concat_int_func function is the way to go. But why only do it for the int case? The double, float and long cases as still there.

I guess they will come one by one.

[forejtv]

@JohnDumbell I'd prefer Java, that makes maintenance easier, string solver is already hard to follow for many :-)

@allredj Indeed the rest will come later. The reason is that it will be a slightly bigger and more controversial change, due to us not having reliable conversion from double to string anywhere and so we'll need to cut some corners. The int to string should be a non-controversial.

[JohnDumbell]

That's cool, I actually agree. Closed my PR.