Move expr_cast from refinement to util/convert_expr.h #1572

romainbrenguier · 2017-11-08T11:48:31Z

This moves these utility functions to util which is more appropriate.
The file and functions are also renamed to avoid confusion with util/expr_cast.h

tautschnig

This is a very partial review: introducing from_expr with a very different meaning than the pre-existing from_expr API is confusing.

tautschnig · 2017-11-08T11:58:57Z

src/util/convert_expr.h

 template<typename T>
-struct expr_cast_implt final { };
+struct from_expr_implt final { };


Apparently this is more than just a plain file renaming? It's also a very confusing one, as there already are functions called from_expr.

from_expr functions convert an expression to something else (which is also the case here). Here the type we are converting to is given as template argument so the meaning should be clear. But I'm open to suggestions for better names.

To be honest, I'm not very happy with the "convert" terminology. You are doing (partly) checked type casts, nothing more and nothing less. To me, "convert" suggests that there is some sort of transformation going on (which would be true of the existing from_expr code).

In that vein: checked_cast_... maybe? Also call the file checked_expr_cast.h?

Checked typecast is more what is done in expr_cast.h and it is a bit different from these functions.
In particular expr_checked_cast is already used there.

Thank you very much for providing further detail -- what does it even mean to "cast" an exprt in this way? Anyway at least I believe I understand what the code is supposed to do. I have no idea how this code ever made it into the code base in its current form, but then that's a different question that the approvers of #1241 need to answer.

Anyway, it seems util/arith_tools.h seems to be the place for most of them.

I don't think that conversion from exprt to string or from one exprt to another is an arithmetic operation.

It made its way into the code, as it provides saner way of doing those things compared to existing 15+ line dance with tons of INVARIANTS every time someone wanted to cast const_exprt to its C++ representation. The only "problem" is the name, which is debatable.

I don't think that conversion from exprt to string or from one exprt to another is an arithmetic operation.

Indeed, I generalised too quickly - the integer conversion ones should go in arith_tools.h, exprt to *_exprt should go in expr_cast.h, and exprt to string I have no idea what that is.

The only "problem" is the name, which is debatable.

The problems certainly include the complete absence of documentation as well as poor choice of placement in the file system. Is it saner? I don't know, because I don't know what it's supposed to do (as there is no documentation).

Re: expr_dynamic_cast and returning pointers vs. optionalt, I believe @reuk was the person advocating pointers because the syntax to use them is briefer -- optionalt<reference_wrapper<T>> requires an explicit .get() operation a little too often.

@smowton Before expr_dynamic_cast, there was this, which was intended to return optional<T> instead of optional<reference_wrapper<T>>. Old casts (to_****_expr) were doing that, because it's not inefficient, so I followed, as it was the safest and most concise way of doing those things.

I'd suggest the reviewers of #1241 take this one forward.

smowton

I think the two casts we can see here are different enough to deserve different names. The cast to refined_string_exprt should be a case of expr_dynamic_cast and implemented as such, whereas the to-integer conversions are helpers on top of util/arith_tools.h. I suggest:

Implement can_cast_expr and validate_expr in a string-refinement header (alongside the definition of refined_string_exprt) so that you can use expr_dynamic_cast with it.
Move the constant-expr-to-integer stuff into arith_tools.h. Deprecate the existing to_integer and to_unsigned_integer (but don't remove them) and replace with your new optional-returning or throwing versions.

romainbrenguier · 2017-11-10T07:48:50Z

@smowton Thanks for the suggestion. I didn't deprecate to_unsigned_integer yet because for now there is no from_expr<unsigned> implemented, but it would be easy to add.

smowton · 2017-11-10T09:47:28Z

Hmmm, two more nitpicks:

I think you should take constant_exprt rather than exprt, even though that's a bit more verbose at certain use-sites. It distinguishes failure because this was the wrong kind of exprt vs. failure because the constant wasn't numeric / was too large / whatever.
std::size_t's range may differ from long (as in to_long()), how about using std::numeric_limits<...>.max() etc to check in range, and thus generalise the size_t case into any integer type?

tautschnig · 2017-11-10T12:31:59Z

std::size_t's range may differ from long (as in to_long()), how about using std::numeric_limits<...>.max() etc to check in range, and thus generalise the size_t case into any integer type?

There's integer2size_t covering this, and that's really what should be used here.

smowton · 2017-11-10T14:02:04Z

Whichever function does the conversion, I'd suggest templating on a numeric type rather than manually enumerating integer2long, integer2size_t, integer2uint16_t, ...

tautschnig · 2017-11-10T15:11:18Z

Whichever function does the conversion, I'd suggest templating on a numeric type rather than manually enumerating integer2long, integer2size_t, integer2uint16_t, ...

True, but either way it should only be done in one place. If someone wants to step up with a PR doing the refactoring that's fine with me.

romainbrenguier · 2017-11-13T18:01:21Z

@smowton @tautschnig

Whichever function does the conversion, I'd suggest templating on a numeric type rather than manually enumerating integer2long, integer2size_t, integer2uint16_t, ...

Not sure that it is exactly what you had in mind but I implemented some conversion template which should help with that: #1582

allredj · 2017-11-14T09:53:00Z

Shall I review this or is it still likely to change?

romainbrenguier · 2017-11-14T09:57:14Z

@allredj please wait for #1582 to be merged, I will then adapt this one

tautschnig · 2017-11-24T16:20:39Z

It seems #1582 has been merged, so it may be possible to continue on this one?

romainbrenguier · 2017-11-24T17:31:54Z

@tautschnig yes but at the moment I'm blocked by the visual studio compilation problem. If someone has an idea?

tautschnig · 2017-11-24T17:49:25Z

I believe the VS failure is due to https://connect.microsoft.com/VisualStudio/feedback/details/1211985. You'll need to make those runtime checks for MSVC, I'm afraid.

smowton · 2017-11-24T17:54:19Z

Gah, https://connect.microsoft.com/VisualStudio/feedback/details/1211985

As @tautschnig says. https://en.wikipedia.org/wiki/Microsoft_Visual_C%2B%2B suggests !defined(_MSC_VER) || _MSC_VER >= 1900 should diagnose a compiler with a properly constexpr max() method.

romainbrenguier · 2017-12-01T17:14:57Z

@smowton

As in you can numeric_cast from mp_integert to size_t for example?

Yes you can (and to any integral type)

Can you also numeric_cast between primitives?

Not at the moment but it could be added if someone finds it useful.

smowton · 2017-12-01T17:19:42Z

OK, understood. In this case removing the source template arg is beyond my skill level, but @reuk or @LAJW can probably work magic if asked nicely :)

reuk · 2017-12-01T18:06:58Z

I'm pretty sure that's possible, yeah. I think you just need an overload of numeric_cast in the struct for each possible Source type.

reuk · 2017-12-01T18:53:40Z

Having said that, this does require moving the exprt overload back into the declaration in mp_arith.h, which I think is what you're trying to avoid...

reuk · 2017-12-01T19:31:18Z

Created a pr showing how this might look

allredj · 2017-12-04T15:49:10Z

src/util/string_expr.h

+template <>
+inline bool can_cast_expr<refined_string_exprt>(const exprt &base)
+{
+  return base.id() == ID_struct && base.operands().size() == 2;


Shouldn't we check anything about the type of operands?

allredj · 2017-12-04T16:00:51Z

src/util/arith_tools.h

+      std::numeric_limits<T>::min() >=
+      std::numeric_limits<decltype(mpi.to_long())>::min(),
+      "Numeric cast only works for types smaller than long long");
+#else


Could you please add the same comment as below?

allredj · 2017-12-04T16:03:45Z

src/util/arith_tools.h

+///         empty optional otherwise.
+template <typename T>
+struct numeric_castt<T,
+  typename std::enable_if<std::is_integral<T>::value &&


This seems to be the same function as above, except for the mpi function called. Could we refactor?

I refactored a bit to have only one structure for the conversion to integral type, but I still have one function for mpi to signed and one function from mpi to unsigned because all the checks are different.

Are you sure? I'm pretty sure the checks can be made the same (I show how this is done in my proposal PR)

Yes it can be done, I will try that.

allredj · 2017-12-04T16:06:57Z

src/util/arith_tools.h

+/// \param arg: expression to convert
+/// \return optional integer of type T if conversion is possible,
+///         empty optional otherwise.
+template <typename Target>


Why do we call that Target here and not T? Update the doc header.

this is to make it clear this is the type we convert to, and not from.

allredj · 2017-12-04T16:08:09Z

src/util/arith_tools.h

+  return *maybe;
+}
+
+/// Convert anexpression to integral type Target


anexpression -> an expression

allredj · 2017-12-04T16:10:08Z

src/util/arith_tools.h

+/// \param arg: mp_integer
+/// \return value of type Target
+template <typename Target>
+Target numeric_cast_v(const mp_integer &arg)


What does _v mean?

It stands for value (this is to distinguish from optionalt). This was the notation used in the expr_cast I removed, but I'm open to better suggestions.

tautschnig · 2017-12-05T15:23:34Z

src/solvers/refinement/string_constraint_generator_transformation.cpp

-  const auto expr1_length=expr_cast<size_t>(expr1_str.length());
-  const auto expr2_length=expr_cast<size_t>(expr2_str.length());
+  const auto expr1_length = numeric_cast<size_t>(expr1_str.length());
+  const auto expr2_length = numeric_cast<size_t>(expr2_str.length());


std::size_t for consistency. (Also applies above.)

peterschrammel · 2017-12-06T16:00:28Z

src/solvers/refinement/string_refinement.cpp

  if(arr.type().id()!=ID_array)
      return std::string("");

  exprt size_expr=to_array_type(arr.type()).size();
-  PRECONDITION(size_expr.id()==ID_constant);
-  to_unsigned_integer(to_constant_expr(size_expr), n);
+  auto n = numeric_cast_v<unsigned>(size_expr);


Why do you use sometimes unsigned and sometimes sizet for values that denote sizes?

peterschrammel

Lgtm

peterschrammel · 2017-12-08T12:35:30Z

src/solvers/refinement/string_refinement.cpp

-      unsigned idx;
-      if(!to_unsigned_integer(to_constant_expr(index), idx) && idx<n)
-        initial_map[idx] = arr_val.operands()[i + 1];
+      if(auto idx = numeric_cast<std::size_t>(index))


I'd appreciate braces here.

This requires moving some declarations to arith_tools, because overload needs to be declared in the same struct. This also adds a numeric_cast_v function which returns a value instead of an optional but an invariant can fail.

This is to demonstrate the use of numeric_cast

numeric_cast can now be used instead.

ca5aa95 Merge remote-tracking branch 'upstream/develop' into merge-develop-20171212 c545369 Merge pull request diffblue#1663 from smowton/smowton/fix/guarded_gotos a2e2f74 Merge pull request diffblue#1636 from svorenova/inner_classes_tg1190_part2 2b835c6 Ensure guarded_gotos is cleared after converting each function 2fd9300 Adding a unit test for specialisation of implicitly generic classes 9617a41 Moving a utility function to utility function file 90a8230 Adding specialisation for implicitly generic classes 98017ce Merge pull request diffblue#1662 from janmroczkowski/janmroczkowski/unified_difft-iterator-check-fix-more ec89991 Merge pull request diffblue#1572 from romainbrenguier/refactor/expr_cast_to_util 5cd0f2f Merge pull request diffblue#1659 from reuk/reuk/jmp_buf-sym e324de6 Merge pull request diffblue#1656 from tautschnig/double-preproc 479e6cf Extra fix for lcss needed 9a811d8 Change type of size to std::size_t 77b7d77 Change length argument type to size_t 898f965 Remove solvers/refinement/expr_cast.h 5683fb5 Use numeric_cast instead of other conversion fc294f8 Use numeric_cast instead of refinement/expr_cast 946b6e2 Extend numeric_cast for constant expressions 20b5366 Add validate and can_cast method to string_exprt cf187c8 Merge pull request diffblue#1654 from NlightNFotis/fotis/pb10_develop 18f9079 Type consistent string preprocessing for floating-point expressions a61ea38 Merge pull request diffblue#1655 from diffblue/bugfix/string-last-index-of#TG592 b5faf52 Fix the handling of recursive data types. cd60782 Fix for the constant arrays marked as nondet issue. 3ab853e Test comparing jbmc lastIndexOf with loop version 985684a Prevent overflow with argument of lastIndexOf 04766b2 Merge pull request diffblue#1658 from tautschnig/fix-appveyor ed5f719 Move of alias code from VSA to LVSA. a44becc Requests in the PR (structure of comments). ef51720 Updates requested in the PR (added comments). 377a515 Introducing function 'get_may_alias_values'. bf4d2c5 Include setjmp.h if the jmp_buf symbol is used 65a3545 Overwrite files when unpacking unconditionally a3e19f7 Merge pull request diffblue#1644 from NathanJPhillips/feature/string-functions-on-demand 9b1ef1a Merge pull request diffblue#1645 from martin-cs/goto-analyzer-6-part3 1cc22f5 Merge pull request diffblue#1651 from thk123/bugfix/TG-1157/store-generic-info-in-specialized-class ea7646b Collect string solver function calls 0393027 Merge pull request diffblue#1639 from reuk/reuk/windows-fixes 3a46525 Renaming generic_tag to generic_name since not a tag 58f8482 Add the generic type arguments to the specalised type 7310281 Tidying of java_specialized_generic_class_typet 1667307 Merge pull request diffblue#1469 from antlechner/antonia/fix/ci_lazy_method_exception_types 6c3fb17 Update appveyor config 33d71aa Disable use of unistd in flex outputs adb7f55 Add Windows dependency information to the COMPILING file 6388940 Fix 'missing return statement' errors in miniBDD_new 23711d7 Print exported attribute in expr2c 0e71658 Initialise string solver function parameter names d556380 Make string solver functions get converted correctly first time ada4475 Replace map to pair with a more specialized type 0ac4d28 Don't store pointers to symbols in map 4b245f8 Use optionalt instead of safe_pointer c69b00d Rename things to better reflect true meaning 94a6ad4 Add test for NegativeArraySizeException 9cc3192 Rename test to NegativeArraySizeException1 51b1d38 Add test for ClassCastException 200017a Add test for ArrayIndexOutOfBoundsException 379e415 Add regression test for NullPointerException 41d77f4 Add regression test for ArithmeticException 4c472e9 Always load classes with throw_runtime_exceptions 2f7ee60 Store list of runtime exceptions in new variable da379bd Update and extend the regression tests for goto-analyse. db75611 Convert returned numbers to the appropriate symbolic exit codes and correct a few cases. 27304c0 Update the use of assert in unreachable_instructions. 1275983 Convert --unreachable-instructions, --unreachable-functions and --reachable-functions from specific to general tasks. e936c50 Convert --intervals and --non-null from being specific to general analysis. f79b73e Refactor doit() in goto analyzer to catch exceptions thrown during analysis. 9e02d7f Add a new set of options that allow task, abstract interpreter and domain to be picked independently. 71d2053 Refactor the command line handling of specific analyses. 396adaf Fix include statements in java_bytecode_instrument c99c2e4 Merge pull request diffblue#1650 from owen-jones-diffblue/owen-jones-diffblue/remove-unneeded-code a708711 Merge pull request diffblue#1648 from janmroczkowski/janmroczkowski/unified_difft-iterator-check-fix 7176f49 Remove unneeded code ae368b8 Fix to unified_difft::lcss for it not to error on iterator check 7660a98 Merge pull request diffblue#1627 from romainbrenguier/bugfix/string-last-index-of#TG-592 9749321 Merge pull request diffblue#1588 from polgreen/freezing_fix aa0e2e3 fix iterator in freeze_lazy_contraints ab9e585 Merge pull request diffblue#1218 from reuk/reuk/master-static-init-order 038ed78 Merge pull request diffblue#1625 from karkhaz/kk-symext-is-messaget b9372f1 Merge pull request diffblue#1516 from andreast271/mingw-D__int64-workaround 0f32076 Make string_container static init more resilient 9ebdc88 Test for String.lastIndexOf with empty argument 707ed94 Refactoring in axioms for lastIndexOf(char) e1f30e1 Fix bounds in axioms for lastIndexOf(char) 9437fa0 Fix special case of empty string in (last)IndexOf 6c6f873 Make goto_symext a subtype of messaget 9940370 Merge pull request diffblue#1633 from diffblue/enhancement/load_important_library_classes f8ca7e2 Remove quotes inside preprocessor defines to avoid problems with shell quote. c0de6fb Merge pull request diffblue#273 from diffblue/smowton/fix/end_to_end_tests 49fc50e Merge pull request diffblue#1586 from polgreen/get_source_location_for_property 14f6721 Merge pull request diffblue#1629 from owen-jones-diffblue/owen-jones-diffblue/refactor-vsa-objectt 92bec6c Add force loading parameter `--java-load-class` cd86eb8 Merge pull request diffblue#1477 from andreast271/travis-NDEBUG-build c543892 Replace objectt in value_set_fivrns.* cc8495a Replace objectt in value_set_fivr.* 5ecee62 Replace objectt in value_set_fi.* 1a51d67 Replace objectt with optional<mp_integer> 821403d Merge pull request diffblue#1640 from owen-jones-diffblue/owen-jones-diffblue/replace-unsigned-with-number-type 2200ac9 Replace unsigned with more precise type dd7ebd3 Merge pull request diffblue#1626 from tautschnig/fix-same_set 2935028 Merge pull request diffblue#1635 from reuk/patch-2 1019be2 Update Windows dependencies in Compiling.md db8f52d Fix copy&paste error in same_set 51cef3c Fix escape analysis 5c65731 Merge pull request diffblue#1612 from reuk/reuk/more-iterator-fixes 48ee475 Merge pull request diffblue#1616 from svorenova/inner_classes_tg1190_part1 37e5b80 Add `override` in a few places 0163362 Adding a unit test for implicitly generic classes ba05f18 Introducing a new type for implicitly generic classes 263fef4 Merge pull request diffblue#1628 from owen-jones-diffblue/owen-jones-diffblue/doc/fix-typos-in-vsa-docs 82b25c4 Fix a few typos in function comments d423c65 Mark tests which fail due to invariant violations 21439f4 Merge pull request diffblue#1614 from polgreen/cegis_cbmc 91ef19e Merge pull request diffblue#1593 from diffblue/chrisr-diffblue/parallel-regression-tests dfeccfd Merge pull request diffblue#1617 from NlightNFotis/fotis/pretty_print_bugfix ff1cf5d Run regression test directories in parallel during CI 24b3f75 Merge pull request diffblue#1618 from romainbrenguier/bugfix/string-equals#TG1619 8a9aa0f Move the pretty printing function from generate_java_generic_type to java_utils. 0dd029d Prevent use of CharSequence as a class_identifier f4c9719 Test for String.equals with class identifier check 17d230f Fix String.equals to check for class identifier 02e7b4a Merge pull request diffblue#1499 from smowton/smowton/feature/vsa_take_two 6ebceca Document value_sett 8bcca68 Add unit tests for value-set-analysis customisation 34dc4a9 Enable value-set to handle DEAD statements 8fb6da2 Templatize and virtualize value-set analysis 991d2b7 Fix goto program hash function ef929ea Fix iterator equality check bug in constant_propagator.cpp 47933cb Fix heap use-after-free in string_refinement.cpp 194ac7c Fix null dereference bug in cpp_typecheck_compound_type.cpp c44ed8c Avoid dereferencing past-the-end iterator in cover.cpp 18656b2 Fix iterator equality check bug in graphml_witness.cpp 60ef5aa Fix use-after-free in c_typecheck_initializer.cpp 82d42e5 Fix expr iterator mutation bug 8de0ea3 Fix iterator equality check bug in ai.h 6297085 Fix iterator comparison bug in expr_iterator af314f5 Fix iterator equality check bug in custom_bitvector_analysis.cpp e0605b7 Fix iterator equality check bug in dependence_graph.cpp 394c42d Fix iterator comparison bug in reaching_definitions.cpp 386a3bc Merge pull request diffblue#1621 from tautschnig/fix-1620 54f987b Use stable data structure for BV refinement approximations 0a0fa08 Fixed the pretty printing type function and fix the tests failing, and introduce test for the pretty printing function. 653dcb6 Fix taint instrumenter handling array initalisers 79defb5 Merge pull request diffblue#1605 from romainbrenguier/bugfix/failed-tests-printer-removed 134c77d Find source location from a property irep_idt 8a389f9 Hook for cegis to freeze program variables 8b1f65e Added range-based symex operations 1a33c87 refactoring bmc.cpp a6af95d Use -p option of test.pl instead of printer script 1821b1a Merge pull request diffblue#1615 from romainbrenguier/bugfix/string-allocation#TG1619 008b8d5 Merge pull request diffblue#1611 from mgudemann/enhancement/make_available_erase_type_arguments_gather_full_class_name dc769f1 Merge pull request diffblue#1583 from polgreen/debug_code_fix 550be1d Make two helper functions available 03c86a8 change #if0 to #ifdef DEBUG 7d37272 Fix the pretty printing routine to pp types that have java:: as their prefix only ea0c70a Remove redundant pointer to array association 89c123e Adapt unit test for allocation of string data 2e760b3 Add invariant on array to pointer association 2a22a2e Fix allocation of infinite char arrays 1957426 Merge pull request diffblue#1607 from mgudemann/fix/add_missing_class_file_awrapper f8e38fb Add edge type parameter to ai transform method a1bc2a2 Merge pull request diffblue#1606 from NlightNFotis/fotis_tg1157/pretty_printing 9091faa Use stdlib debug mode in Travis cbb2eff Changes in the generics concretisation tests to correspond to the new class signatures. f390795 Add a class to represent specialised generic classes, and change concretisation functions to use that. edc75fa Merge pull request diffblue#1604 from romainbrenguier/bugfix/string-nondet-init#TG1581 3d16d36 Merge pull request diffblue#1608 from smowton/smowton/fix/msvc14_headers 9829a58 Add headers needed to build under MSVC14 / Visual Studio 2015 558cb7a Add AWrapper.class which was missing from regression test 523f60e Change template of value_set_analysis_baset ac2a599 Correct unit test for gen_nondet_string 10d3857 Add test for instanceof String 12ca989 Document class_identifier argument of root class 5524078 Correct class_id of nondet strings efae909 Merge pull request diffblue#1603 from romainbrenguier/feature/cproverValidate#TG1313 4fd14b2 Adapt cproverNondetInitialize call for static case 4f45985 Merge pull request diffblue#271 from diffblue/smowton/merge_develop_2017_11_16 6d2d6c4 Test for cproverNondetInitialize with lazy-methods bf9a8c2 Load cproverNondetInitialize with lazy-methods 54d943d Test for the cproverNondetInitialize feature a1acecb Add call to cproverNondetInitialize in nondet-init aa88e27 Merge pull request diffblue#1590 from reuk/reuk/numbering-api-update bff25c5 Object numbering: Remove duplication e3e5e48 Object numbering: Remove function call operator c4b3335 Object numbering: Add trailing underscores for data members ad17a85 Object numbering: Switch typedef to using 7619d15 Rename ID_lvsa_mode to ID_lvsa_evs_type da6fa5d Don't mutate parameters in numbering class 161787b Merge pull request diffblue#1597 from diffblue/bugfix/add_generic_type_args_to_dependencies e707be3 Merge pull request diffblue#1591 from diffblue/print_assignment 645f631 Merge pull request diffblue#1600 from diffblue/chrisr-diffblue/ccache-fixups 62b52ba Merge pull request diffblue#1598 from peterschrammel/simplify-string-const-equalities a656e7b Remove obsolete equal/notequal cases in simplify_expr c7d8ea6 Tests for simplifying ID_string equalities ddf6c92 Simplify equalities of constants 81cc65f Merge pull request diffblue#1599 from NathanJPhillips/move-show-symbol-table-from-module-pass e8f5e08 Add regression tests for generic type arg dependencies fae14fc Add type parameters in signatures as dependencies fb493da Fixups for ccache configuration in travis 1a7dfdf Fix location of show-symbol-table 471180d Adapt to upstream CBMC changes 0da026b Merge pull request diffblue#1596 from NlightNFotis/bugfix/TG-1422/remove_evaluator_precondition c93dd78 Remove too tight precondition in evaluator that was causing an invariant violation in some cases. 5a0dcc7 boolbvt::print_assignment should call the print_assignment of the base class 10131ed make debug code compile in value_set.cpp 2177bbc Remove extra build with NDEBUG that compiles but doesn't test. Instead, add NDEBUG to a linux clang build that runs regression. 4fa3ba5 Create separate clang build with NDEBUG and CPROVER_INVARIANT_DO_NOT_CHECK Fix INVARIANT macros for CPROVER_INVARIANT_DO_NOT_CHECK and CPROVER_INVARIANT_ASSERT In NDEBUG build, disable known warnings caused by the disabled versions of the INVARIANT macros. git-subtree-dir: cbmc git-subtree-split: ca5aa95

romainbrenguier requested review from kroening, martin-cs, peterschrammel and tautschnig as code owners November 8, 2017 11:48

tautschnig previously requested changes Nov 8, 2017

View reviewed changes

LAJW approved these changes Nov 8, 2017

View reviewed changes

romainbrenguier requested review from smowton and allredj November 9, 2017 08:08

smowton suggested changes Nov 9, 2017

View reviewed changes

romainbrenguier force-pushed the refactor/expr_cast_to_util branch 2 times, most recently from a31d664 to f44654d Compare November 10, 2017 09:04

romainbrenguier mentioned this pull request Nov 13, 2017

Numerical cast #1582

Merged

romainbrenguier added the do not merge label Nov 15, 2017

romainbrenguier force-pushed the refactor/expr_cast_to_util branch 2 times, most recently from 5919cc1 to dc3d851 Compare November 17, 2017 10:29

tautschnig assigned romainbrenguier Nov 30, 2017

romainbrenguier force-pushed the refactor/expr_cast_to_util branch from dc3d851 to 051d6ff Compare December 1, 2017 09:32

romainbrenguier force-pushed the refactor/expr_cast_to_util branch 2 times, most recently from d69a2dd to 7fbfeec Compare December 4, 2017 14:12

allredj reviewed Dec 4, 2017

View reviewed changes

romainbrenguier requested review from smowton and allredj December 5, 2017 09:12

romainbrenguier force-pushed the refactor/expr_cast_to_util branch from 41ed112 to 062508f Compare December 5, 2017 10:04

smowton approved these changes Dec 5, 2017

View reviewed changes

tautschnig reviewed Dec 5, 2017

View reviewed changes

romainbrenguier force-pushed the refactor/expr_cast_to_util branch from 062508f to 6efa7a2 Compare December 6, 2017 13:30

peterschrammel reviewed Dec 6, 2017

View reviewed changes

romainbrenguier force-pushed the refactor/expr_cast_to_util branch 3 times, most recently from 09264e7 to 70598c4 Compare December 8, 2017 10:17

peterschrammel approved these changes Dec 8, 2017

View reviewed changes

romainbrenguier added 7 commits December 8, 2017 13:11

Add validate and can_cast method to string_exprt

20b5366

Extend numeric_cast for constant expressions

946b6e2

This requires moving some declarations to arith_tools, because overload needs to be declared in the same struct. This also adds a numeric_cast_v function which returns a value instead of an optional but an invariant can fail.

Use numeric_cast instead of refinement/expr_cast

fc294f8

Use numeric_cast instead of other conversion

5683fb5

This is to demonstrate the use of numeric_cast

Remove solvers/refinement/expr_cast.h

898f965

numeric_cast can now be used instead.

Change length argument type to size_t

77b7d77

Change type of size to std::size_t

9a811d8

romainbrenguier force-pushed the refactor/expr_cast_to_util branch from 70598c4 to 9a811d8 Compare December 8, 2017 13:12

allredj approved these changes Dec 8, 2017

View reviewed changes

romainbrenguier merged commit ec89991 into diffblue:develop Dec 8, 2017

Move expr_cast from refinement to util/convert_expr.h #1572

Move expr_cast from refinement to util/convert_expr.h #1572

Conversation

romainbrenguier commented Nov 8, 2017

tautschnig left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

LAJW Nov 8, 2017 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

smowton left a comment

Choose a reason for hiding this comment

romainbrenguier commented Nov 10, 2017

smowton commented Nov 10, 2017

tautschnig commented Nov 10, 2017

smowton commented Nov 10, 2017

tautschnig commented Nov 10, 2017

romainbrenguier commented Nov 13, 2017

allredj commented Nov 14, 2017

romainbrenguier commented Nov 14, 2017

tautschnig commented Nov 24, 2017

romainbrenguier commented Nov 24, 2017

tautschnig commented Nov 24, 2017

smowton commented Nov 24, 2017

romainbrenguier commented Dec 1, 2017

smowton commented Dec 1, 2017

reuk commented Dec 1, 2017

reuk commented Dec 1, 2017

reuk commented Dec 1, 2017

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

tautschnig Dec 5, 2017 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

peterschrammel left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

LAJW Nov 8, 2017 •

edited

Loading

tautschnig Dec 5, 2017 •

edited

Loading