-
Notifications
You must be signed in to change notification settings - Fork 273
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
[TG-1157] New class for specialised generic class types. #1606
[TG-1157] New class for specialised generic class types. #1606
Conversation
60ddbe3
to
fdbbca8
Compare
src/java_bytecode/java_types.h
Outdated
return type.get_bool(ID_C_specialised_generic_java_class); | ||
} | ||
|
||
inline java_specialised_generic_class_typet |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Write const and non-const versions, and return by reference like all the rest of these cast functions
src/java_bytecode/java_types.h
Outdated
~java_specialised_generic_class_typet() {} | ||
}; | ||
|
||
inline const bool java_is_specialised_generic_class_type(const typet &type) |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
const pointless in by-value return type
src/util/irep_ids.def
Outdated
@@ -830,6 +830,7 @@ IREP_ID_ONE(integer_dereference) | |||
IREP_ID_TWO(C_java_generic_parameter, #java_generic_parameter) | |||
IREP_ID_TWO(C_java_generic_type, #java_generic_type) | |||
IREP_ID_TWO(C_java_generics_class_type, #java_generics_class_type) | |||
IREP_ID_TWO(C_specialised_generic_java_class, #specialised_class) |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
#specialised_generic_java_class
please, it'll be more clear in irep dumps
@@ -70,8 +80,9 @@ symbolt generate_java_generic_typet::operator()( | |||
pre_modification_size==after_modification_size, | |||
"All components in the original class should be in the new class"); | |||
|
|||
const java_class_typet &new_java_class = construct_specialised_generic_type( | |||
generic_class_definition, new_tag, replacement_components); | |||
const java_specialised_generic_class_typet &new_java_class = |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Get by value (the return is by-value, and the reference relies on flaky lifetime-extension magic)
@@ -41,6 +50,7 @@ symbolt generate_java_generic_typet::operator()( | |||
|
|||
const irep_idt new_tag = | |||
build_generic_tag(existing_generic_type, generic_class_definition); | |||
|
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
remove unrelated change
const std::string java_lang("java::java.lang"); | ||
const std::string package_name(java_class_to_package(fqn_java_type)); | ||
if(package_name==java_lang) | ||
return fqn_java_type.substr(java_lang.length()+1); |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Rename "pretty-print" or something, since this produces types that should only be used for human readable output. Perhaps move this into type2cleanjava?
fdbbca8
to
e4600fb
Compare
@@ -11,6 +11,15 @@ | |||
#include <java_bytecode/java_types.h> | |||
#include <java_bytecode/java_utils.h> | |||
|
|||
static std::string pretty_print_java_type(const std::string &fqn_java_type) |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Could you add some Doxygen to this, in particular, with some example of the input/output of the function? I'm also wondering if this is really the best name for this function, because it seems to me its doing more than just pretty printing if I'm reading this code correctly? It's striping off the leading java::java.lang
- from java types that include that, so maybe the function name should make that clearer?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
A suggestion for naming: strip_package_from_java_class
??? That's just a random suggestion, but it might be nice if the name was somewhat orthogonal to the exisiting java_class_to_package
function that gets called below.
const std::string java_lang("java::java.lang"); | ||
const std::string package_name(java_class_to_package(fqn_java_type)); | ||
if(package_name==java_lang) | ||
return fqn_java_type.substr(java_lang.length() + 1); |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Rather than having a hard coded '+1' in here, is it better to just add .
into the java_lang
string variable?
generate_java_generic_typet::construct_specialised_generic_type( | ||
const java_generic_class_typet &generic_class_definition, | ||
const irep_idt &new_tag, | ||
const struct_typet::componentst &new_components) const | ||
{ | ||
java_class_typet specialised_class = generic_class_definition; | ||
java_specialised_generic_class_typet specialised_class{}; |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Rather than constructing an empty java_specialised_generic_class_typet
and then filling in it's fields with a bunch of set
s, would it be cleaner/safer to actually add a proper constructor to the class type?
src/java_bytecode/java_types.h
Outdated
}; | ||
|
||
inline bool java_is_specialised_generic_class_type(const typet &type) | ||
{ |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
IIRC the correspondant predicates are named is_java_generic_FOO_BAR
, please check and change name here to adapt
src/java_bytecode/java_types.h
Outdated
@@ -374,4 +374,45 @@ void get_dependencies_from_generic_parameters( | |||
const typet &, | |||
std::set<irep_idt> &); | |||
|
|||
class java_specialised_generic_class_typet : public java_generic_class_typet |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
The coding guidelines ask for American spelling for identifiers. The same applies to virtually any other hunk in the diff ;)
e4600fb
to
bbcbc57
Compare
src/java_bytecode/java_types.h
Outdated
{ | ||
set(ID_C_specialised_generic_java_class, true); | ||
// We are specialising the logic - so we don't want to be marked as generic | ||
set(ID_C_java_generics_class_type, false); |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
If this is true, in what sense is this a child of java_generic_class_typet
?
src/java_bytecode/java_types.h
Outdated
/// \param new_components: The specialised components | ||
/// \return The newly constructed class. | ||
java_specialized_generic_class_typet( | ||
const java_generic_class_typet &generic_class_definition, |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Unused parameter?
b172e74
to
17aa11a
Compare
set(ID_C_specialized_generic_java_class, true); | ||
// We are specialising the logic - so we don't want to be marked as generic | ||
set(ID_C_java_generics_class_type, false); | ||
set(ID_name, "java::" + id2string(new_tag)); |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Suggest not using name
, which is a bit vague. How about ID_java_generic_tag
or something?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I think this should be staying like this. The point is it should be creating symbols that look a little bit like this:
0: struct
* name: java::reifiedArrayNB<java::java.lang.Float>
* tag: reifiedArrayNB
* base_name: reifiedArrayNB<java::java.lang.Float>
* components:
// We are specialising the logic - so we don't want to be marked as generic | ||
set(ID_C_java_generics_class_type, false); | ||
set(ID_name, "java::" + id2string(new_tag)); | ||
set(ID_base_name, id2string(new_tag)); |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Suggest not storing this redundant info unless you really need to
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
My understanding of the specification (and the implementation of generics thus far) is that all of the base_name
, name
and tag
are needed.
set(ID_base_name, id2string(new_tag)); | ||
components() = new_components; | ||
const std::string &class_tag = id2string(new_tag); | ||
set_tag(class_tag.substr(0, class_tag.find('<'))); |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Are you sure multiple distinct types with matching tags is okay?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
It is my understanding that for a type GenericWrapper<IWrapper>
the tag of the class should always be GenericWrapper
. That's what I have understood from discussions with @thk123 . I suggest we leave it as it is for now, as I don't have access to the specification and I don't want to make a change against the specification at this point.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
@smowton this is the case we have currently, I am not aware of any problems, AFAIK the idea is still that the use of generics should be transparent for non-generics aware code
src/java_bytecode/java_types.h
Outdated
set_tag(class_tag.substr(0, class_tag.find('<'))); | ||
} | ||
|
||
~java_specialized_generic_class_typet() |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Might as well delete this empty destructor
…retisation functions to use that.
17aa11a
to
f390795
Compare
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Still looks suspicious but I'll take it up with @thk123; go for it for now.
… class signatures.
12445a0
to
cbb2eff
Compare
/// \param new_tag: The new name for the class (like Generic<java::Float>) | ||
/// \param new_components: The specialised components | ||
/// \return The newly constructed class. | ||
java_class_typet | ||
java_specialized_generic_class_typet | ||
generate_java_generic_typet::construct_specialised_generic_type( |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Minor nit (non-blocking): We're getting quite a mix of specialised
and specialized
now, e.g. both spellings in the same function signature here. Ideally we'd clean this up, but if you don't clean it up in this PR, please raise a technical debt issue to review all the generics work and cleanup the naming in functions/comments/etc.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Looks good to me - would be nice to cleanup naming, but I recognise the mix of spellings was there before this PR, so I'm happy for this to go in as it is.
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
This PR introduces a new class that is going to be used inside the generics concretisation code to represent a generic class after it has been instantiated.