[TG-1190] Parse generic information of outer classes #1616

majakusber · 2017-11-23T11:49:06Z

In symbol table, inner classes of generic outer classes are marked as implicitly generic.

majakusber · 2017-11-23T14:31:19Z

CI is crashing due to a test in which .class files of the outer classes are not available and this makes a precondition fail. After talking to @smowton I will add a workaround which will fail gracefully if any outer class is missing and create a JIRA issue to fix this.

mgudemann · 2017-11-23T14:22:45Z

src/java_bytecode/java_bytecode_convert_class.cpp

+  // get the name of the parameter, e.g., `T` from `java::Class::T`
+  std::string parameter_full_name =
+    as_string(parameter.type_variable_ref().get_identifier());
+  std::string parameter_name =


both can be const

mgudemann · 2017-11-23T14:26:01Z

src/java_bytecode/java_bytecode_convert_class.cpp

+        replacement_parameter_full_name.substr(
+          replacement_parameter_full_name.rfind(':') + 1);
+      return parameter_name == replacement_parameter_name;
+    });


if I understand correctly, then this will test on the generic parameter name only? Is then the hypothesis that replacement_parameters will only contain viable candidates? If so, please add this in the documentation.

Added to documentation and also added a precondition.

mgudemann · 2017-11-23T14:33:13Z

src/java_bytecode/java_bytecode_convert_class.cpp

+    });
+
+  // if a replacement parameter was found, update the identifier
+  if(replacement_parameter_p != replacement_parameters.end())


as std::find_if returns an iterator to the first matching element, would it make sense to try to find a next one, too ? Or is there a hypothesis that a single matching one exists?

Yes, at most one matching should exist. The reason is that if an inner class, e.g., Inner, would try to introduce a type parameter Inner<T> that matches the name of the parameter of an outer class Outer<T>, it gets a warning that it's shadowing the name, so it can either use the already introduced parameter java::Outer::T or introduce a new one with unique name.

mgudemann · 2017-11-23T14:42:36Z

src/java_bytecode/java_bytecode_convert_class.cpp

+/// corresponding outer classes.
+/// \param class_name
+/// \param symbol_table
+void check_java_implicitly_generic_class_type(


the function name hints to a predicate, not really the side effects it can have

mgudemann · 2017-11-23T14:44:58Z

src/java_bytecode/java_bytecode_convert_class.cpp

+  }
+
+  // retrieve the symbol for the class
+  std::string qualified_class_name = "java::" + id2string(class_name);


mgudemann · 2017-11-23T14:47:47Z

src/java_bytecode/java_bytecode_convert_class.cpp

+  else
+  {
+    return;
+  }


else block is not needed here

mgudemann · 2017-11-23T14:49:58Z

src/java_bytecode/java_bytecode_language.cpp

+  for(java_class_loadert::class_mapt::const_iterator
+        c_it=java_class_loader.class_map.begin();
+      c_it!=java_class_loader.class_map.end();
+      c_it++)


used ranged for

mgudemann · 2017-11-23T14:50:59Z

src/java_bytecode/java_types.h

@@ -313,6 +320,67 @@ inline const typet &java_generic_class_type_bound(size_t index, const typet &t)
  return gen_type.subtype();
 }

+/// Class to hold a class that is implicitly generic, e.g., an inner


maybe write "Class to hold a Java class ..."

mgudemann · 2017-11-23T14:53:13Z

src/java_bytecode/java_types.h

@@ -17,6 +17,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/std_types.h>
 #include <util/c_types.h>
 #include <util/optional.h>
+#include <util/irep_ids.h>


is this needed?

mgudemann · 2017-11-23T14:54:04Z

src/java_bytecode/java_types.h

+
+  const implicit_generic_typest &implicit_generic_types() const
+  {
+    return (


in general no "(" ")" around return value

The parentheses are for casting, I changed the formatting.

smowton

Some minor issues to fix. Also please add a regression test, to verify that not only does the micro-level code behave as expected, but it also works as expected at a macro-level.

smowton · 2017-11-24T08:44:23Z

src/java_bytecode/java_bytecode_convert_class.cpp

+    replacement_parameters.end(),
+    [&parameter_name](const java_generic_parametert &replacement_param)
+    {
+      std::string replacement_parameter_full_name =


can save a copy, taking this as const std::string &

smowton · 2017-11-24T08:45:49Z

src/java_bytecode/java_bytecode_convert_class.cpp

+    {
+      std::string replacement_parameter_full_name =
+        as_string(replacement_param.type_variable().get_identifier());
+      std::string replacement_parameter_name =


Can do the substring and compare in one operation (and without a copy) using std::string::compare

smowton · 2017-11-24T08:46:51Z

src/java_bytecode/java_bytecode_convert_class.cpp

+  if(replacement_parameter_p != replacement_parameters.end())
+  {
+    const auto &replacement_parameter = *replacement_parameter_p;
+    const std::string replacement_parameter_full_name =


Take by ref again here

smowton · 2017-11-24T08:49:14Z

src/java_bytecode/java_bytecode_convert_class.cpp

+      replacement_parameter_full_name.substr(
+        0, replacement_parameter_full_name.length() - 3);
+    PRECONDITION(
+      std::equal(


Comment on why exactly 3 characters are trimmed from replacement_parameter_full_name?

This actually assumes that the parameter name is a single character such as T, I replaced with something more clever, and used compare and substr to do it in one operation again.

smowton · 2017-11-24T08:56:41Z

src/java_bytecode/java_bytecode_convert_class.cpp

+        to_java_class_type(outer_class_symbol.type);
+      if(is_java_generic_class_type(outer_class_type))
+      {
+        std::vector<java_generic_parametert> outer_generic_type_parameters =


smowton · 2017-11-24T09:01:05Z

src/java_bytecode/java_bytecode_language.cpp

@@ -209,6 +209,21 @@ bool java_bytecode_languaget::typecheck(
      return true;
  }

+  // find and mark all implicitly generic class types
+  // this can only be done once all the class symbols have been created
+  for(auto c : java_class_loader.class_map)


const auto &?

smowton · 2017-11-24T09:01:32Z

src/java_bytecode/java_bytecode_language.cpp

+      mark_java_implicitly_generic_class_type(c.first, symbol_table);
+    }
+    catch(missing_outer_class_symbol_exceptiont &)
+    {


Consider printing a warning (perhaps later downgraded to debug message) when this bails out

smowton · 2017-11-24T09:02:43Z

src/java_bytecode/java_types.h

+  typedef std::vector<java_generic_parametert> implicit_generic_typest;
+
+  static const java_implicitly_generic_class_typet &from_java_class_type(
+    java_class_typet &class_type,


Take by const ref (both parameters)

This function has been now removed, and I use a constructor to do the job instead.

smowton · 2017-11-24T09:02:57Z

src/java_bytecode/java_types.h

+    java_class_typet &class_type,
+    implicit_generic_typest implicit_generic_types)
+  {
+    class_type.set(ID_C_java_implicitly_generic_class_type, true);


Return something derived rather than altering in place

This function has been now removed, and I use a constructor to do the job instead.

smowton · 2017-11-24T09:03:26Z

src/java_bytecode/java_types.h

+
+  const implicit_generic_typest &implicit_generic_types() const
+  {
+    return (const implicit_generic_typest&)(


Use static_cast rather than a C-style cast

static_cast is invalid here. I've created both functions implicit_generic_types based on generic_types in java_generic_class_typet.

majakusber · 2017-11-24T17:08:01Z

@smowton @mgudemann Thank you for reviews. Could you please take a look again?
@smowton The changes only consider symbol table, no changes are visible on macro-level. This PR is only a partial solution to TG-1190 - parsing the desired information. The second step (with its own PR) will be to use the new info during specialisation in tests.

smowton

One more nitpick, and please make any functions that are defined file-local and not exposed in a header file static (avoids polluting the linker namespace, and speeds its job up a little, as well as allowing the compiler to optimise more and warn you about unused functions)

smowton · 2017-11-24T17:14:28Z

src/java_bytecode/java_bytecode_convert_class.cpp

+      symbol_table.get_writeable_ref(qualified_class_name);
+    java_class_typet &class_type = to_java_class_type(class_symbol.type);
+
+    class_type = java_implicitly_generic_class_typet(


Recommend assigning to class_symbol.type. The effect is the same, but it'll be clearer that you're overwriting the symbol type not a local.

NlightNFotis

I have some things I would want to be checked, I might be wrong on them, but I think it's worth checking them out and seeing if there might be problems. Otherwise this looks good. Ping me with the results of your investigation.

NlightNFotis · 2017-11-27T11:10:35Z

src/java_bytecode/java_types.h

+  explicit java_implicitly_generic_class_typet(
+    const java_class_typet &class_type,
+    const implicit_generic_typest &generic_types)
+    : java_class_typet(class_type)


Why does this need to be called? Are you trying to achieve something in particular? Normally you wouldn't want to pass a base class object to the derived class constructor, and call the superclass' constructor like this, to my understanding. If you leave it be, without calling it, the superclass' default constructor should be called automatically, which I'm assuming should do some sensible initialisation.

Another problem this can create is that you can pass a subclass of java_class_typet to this constructor and it will essentially clobber internal state that doesn't match the java_class_typet which can cause some very nasty bugs in the future.

After further discussion, this will stay as it is as it's not causing the nasty bug mentioned above.

NlightNFotis · 2017-11-27T11:11:33Z

src/java_bytecode/java_types.h

+
+/// \param type: the type to check
+/// \return true if type is a implicitly generic java class type
+inline bool is_java_implicitly_generic_class_type(const typet &type)


I may be wrong, but you may also need a version of this function that accepts a non-const typet

@smowton Could you advise on this, is another version needed?

No, non-const is implicitly castable to const, and this is inherently a read-only operation. @NlightNFotis is probably thinking of the to_* cast functions, which do want a const and a non-const flavour.

NlightNFotis · 2017-11-27T11:17:15Z

src/java_bytecode/java_types.h

+  type_variablet &type_variable_ref() const
+  {
+    PRECONDITION(!type_variables().empty());
+    return const_cast<type_variablet &>(type_variables().front());


I think this is wrong, and could create a very nasty bug in the future. It's a method marked const, which means that it guarantees that it won't mutate the internal state of the object, but what it does is it fetches an object from a member container, and removes const from that, meaning that you can mutate the object this returns, and therefore mutate the internal state of the object this method is being called at, violating the const guarantee of this method.

I might be wrong though.

Good catch, const removed.

NlightNFotis

My comments have been addressed. LGTM

majakusber · 2017-11-27T14:36:07Z

One more change introduced - static inner classes are now not marked as implicitly generic and the unit test is extended accordingly.

Non-static inner classes of generic outer classes are marked as implicitly generic and a vector of implicit generic type parameters is stored. The identifiers of the implicit generic type parameters used in the inner classes are updated to point to the outer class.

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

majakusber requested review from cesaro, kroening, mgudemann, peterschrammel, smowton, tautschnig and thk123 as code owners November 23, 2017 11:49

majakusber force-pushed the inner_classes_tg1190_part1 branch from 50f9371 to a30cb93 Compare November 23, 2017 12:00

mgudemann suggested changes Nov 23, 2017

View reviewed changes

majakusber force-pushed the inner_classes_tg1190_part1 branch 3 times, most recently from 09ec5e8 to f7aee1c Compare November 23, 2017 17:12

smowton reviewed Nov 24, 2017

View reviewed changes

majakusber force-pushed the inner_classes_tg1190_part1 branch from f7aee1c to 10861ed Compare November 24, 2017 17:02

smowton reviewed Nov 24, 2017

View reviewed changes

majakusber force-pushed the inner_classes_tg1190_part1 branch from 10861ed to c489b5c Compare November 27, 2017 09:39

NlightNFotis suggested changes Nov 27, 2017

View reviewed changes

mgudemann approved these changes Nov 27, 2017

View reviewed changes

NlightNFotis approved these changes Nov 27, 2017

View reviewed changes

majakusber force-pushed the inner_classes_tg1190_part1 branch from c489b5c to 7ee4c0e Compare November 27, 2017 14:32

majakusber force-pushed the inner_classes_tg1190_part1 branch 3 times, most recently from e5a7bd4 to 88b38b7 Compare November 27, 2017 15:45

majakusber added 2 commits November 27, 2017 17:11

Adding a unit test for implicitly generic classes

0163362

majakusber force-pushed the inner_classes_tg1190_part1 branch from 88b38b7 to 0163362 Compare November 27, 2017 17:11

smowton approved these changes Nov 27, 2017

View reviewed changes

smowton merged commit 48ee475 into diffblue:develop Nov 27, 2017

majakusber deleted the inner_classes_tg1190_part1 branch November 28, 2017 09:58

majakusber mentioned this pull request Nov 28, 2017

[TG-1190] Specialisation for implicitly generic classes #1636

Merged

[TG-1190] Parse generic information of outer classes #1616

[TG-1190] Parse generic information of outer classes #1616

Conversation

majakusber commented Nov 23, 2017

majakusber commented Nov 23, 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

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

smowton 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

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

majakusber commented Nov 24, 2017

smowton left a comment • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

NlightNFotis left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

majakusber Nov 27, 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

Choose a reason for hiding this comment

Choose a reason for hiding this comment

NlightNFotis left a comment

Choose a reason for hiding this comment

majakusber commented Nov 27, 2017

majakusber commented Nov 23, 2017 •

edited

Loading

smowton left a comment •

edited

Loading

majakusber Nov 27, 2017 •

edited

Loading