-
Notifications
You must be signed in to change notification settings - Fork 273
Complete typet documentation [DOC-12] #2771
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
Conversation
src/util/type.cpp
Outdated
@@ -36,8 +47,8 @@ bool is_number(const typet &type) | |||
id==ID_fixedbv; | |||
} | |||
|
|||
/// Identify if a given type is constant itself or | |||
/// contains constant components. Examples include: | |||
/// Identify if a given type is constant itself or contains constant components. |
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.
Nit pick: s/if a/whether a/
src/util/type.h
Outdated
/// modeled with two subs named “subtype” (a single type) and “subtypes” | ||
/// (a vector of types). The class typet only adds specialized methods | ||
/// for accessing the subtype information to the interface of irept. | ||
/// Pre-defined types: |
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.
Two requests here, although this may be in partial conflict with the documentation-only push taking place:
- I think the list of pre-defined types should live in
std_types.h
- The functions
is_number
and (less clear)is_constant_or_has_constant_components
should also move tostd_types.h
. It isstd_types.{h,cpp}
that actually declares the various "number" types.
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 can do the second point in a separate PR where I will be cleaning the code a bit too - adding can_cast_type
to those types that don;t have it yet.
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 list can go away. It's incomplete and outdated.
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 list of pre-defined types seems vastly out of date to me. I would just remove it. Do you think it would be of use to have an exhaustive list of defined types in std_types.h file description?
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 see Peter suggested to remove it, removing.
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.
(But I'm still in favour of the follow-up PR moving is_number
to a different file.)
src/util/type_eq.cpp
Outdated
|
||
#include "type_eq.h" | ||
|
||
#include "namespace.h" | ||
#include "std_types.h" | ||
#include "symbol.h" | ||
|
||
/// Check types for equality. If either of the types is a symbol type, i.e. a |
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 have never quite understood when to use type_eq
vs base_type_eq
. I would appreciate if the documentation introduced could please sort this out.
src/util/std_types.h
Outdated
|
||
/*! \brief The proper Booleans | ||
*/ | ||
/// The boolean 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.
s/boolean/Boolean/
src/util/std_types.h
Outdated
@@ -39,8 +31,7 @@ class bool_typet:public typet | |||
} | |||
}; | |||
|
|||
/*! \brief The NIL type | |||
*/ | |||
/// The NIL 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.
So ... what is it?
This comment was marked as resolved.
This comment was marked as resolved.
Sorry, something went wrong.
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.
Though why is there a void_typet
and an empty_typet
I have no idea
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.
Yes, this is the explanation I got for nil
vs void/empty
. void
and empty
are two names for the same thing.
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 have created #2780 for void_typet
vs empty_typet
.
src/util/std_types.cpp
Outdated
@@ -73,6 +79,7 @@ typet struct_union_typet::component_type( | |||
return c.type(); | |||
} | |||
|
|||
/// Returns true if the object is a prefix of \param other. |
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.
object -> struct ?
src/util/std_types.h
Outdated
@@ -59,14 +49,12 @@ class empty_typet:public typet | |||
} | |||
}; | |||
|
|||
/*! \brief The void type | |||
*/ | |||
/// The void 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.
What's the difference between void and empty?
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.
There's no difference :)
src/util/std_types.h
Outdated
template <> | ||
inline bool can_cast_type<symbol_typet>(const typet &type) | ||
{ | ||
return type.id() == ID_symbol_type; | ||
} | ||
|
||
/*! \brief Base type of C structs and unions, and C++ classes | ||
*/ | ||
/// Base type of C structs and unions, and C++ classes |
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.
also Java classes...
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.
Maybe:
/// Base type for structs and unions
/// E.g. C structs, C unions, C++ classes, Java classes```
src/util/std_types.h
Outdated
*/ | ||
/// \brief Cast a generic typet to a \ref symbol_typet. | ||
/// | ||
/// This is an unchecked conversion. \param type must be known to be |
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.
Maybe say that the conversion will fail with a precondition violation if type doesn't match.
src/util/std_types.h
Outdated
template <> | ||
inline bool can_cast_type<struct_typet>(const typet &type) | ||
{ | ||
return type.id() == ID_struct; | ||
} | ||
|
||
/*! \brief C++ class type | ||
*/ | ||
/// C++ class 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.
also Java
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.
Maybe:
/// Class type
/// E.g. in C++ or Java
bool is_reference(const typet &type); | ||
/*! \brief TO_BE_DOCUMENTED | ||
*/ | ||
|
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.
document
inline c_bool_typet &to_c_bool_type(typet &type) | ||
{ | ||
PRECONDITION(type.id()==ID_c_bool); | ||
return static_cast<c_bool_typet &>(type); | ||
} | ||
|
||
/*! \brief TO_BE_DOCUMENTED | ||
*/ | ||
/// String 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.
What is it? Where is it used?
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.
This is actually not used anywhere. That's not true, it is used, will add explanation.
src/util/std_types.h
Outdated
inline const range_typet &to_range_type(const typet &type) | ||
{ | ||
PRECONDITION(type.id()==ID_range); | ||
return static_cast<const range_typet &>(type); | ||
} | ||
|
||
/*! \brief A constant-size array type | ||
*/ | ||
/// A constant-size array 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.
What's the difference to array?
src/util/type.h
Outdated
/// modeled with two subs named “subtype” (a single type) and “subtypes” | ||
/// (a vector of types). The class typet only adds specialized methods | ||
/// for accessing the subtype information to the interface of irept. | ||
/// Pre-defined types: |
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 list can go away. It's incomplete and outdated.
src/util/type_eq.cpp
Outdated
@@ -1,20 +1,26 @@ | |||
/*******************************************************************\ | |||
|
|||
Module: Type Checking | |||
Module: Type checking |
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 that title is inappropriate
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.
Nothing wrong AFAICT - but I still have some questions that it would be good for the docs to answer if possible.
|
||
Author: Daniel Kroening, [email protected] | ||
Maria Svorenova, [email protected] |
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 don't know, but should the additional Author be Diffblue @peterschrammel?
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 followed @peterschrammel recommendation from Slack but happy to change it to whatever makes more sense.
src/util/std_types.cpp
Outdated
@@ -73,6 +79,7 @@ typet struct_union_typet::component_type( | |||
return c.type(); | |||
} | |||
|
|||
/// Returns true if the object is a prefix of \param other. |
This comment was marked as resolved.
This comment was marked as resolved.
Sorry, something went wrong.
src/util/std_types.h
Outdated
@@ -39,8 +31,7 @@ class bool_typet:public typet | |||
} | |||
}; | |||
|
|||
/*! \brief The NIL type | |||
*/ | |||
/// The NIL type |
This comment was marked as resolved.
This comment was marked as resolved.
Sorry, something went wrong.
src/util/std_types.h
Outdated
@@ -39,8 +31,7 @@ class bool_typet:public typet | |||
} | |||
}; | |||
|
|||
/*! \brief The NIL type | |||
*/ | |||
/// The NIL 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.
Though why is there a void_typet
and an empty_typet
I have no idea
src/util/std_types.h
Outdated
* | ||
* \ingroup gr_std_types | ||
*/ | ||
/// \brief Cast a generic typet to a \ref symbol_typet. |
This comment was marked as resolved.
This comment was marked as resolved.
Sorry, something went wrong.
src/util/type.h
Outdated
/// unsignedbv | ||
/// signedbv - two's complement | ||
/// floatbv - IEEE floating point format | ||
/// code |
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.
- type of a function
src/util/type.h
Outdated
/// Pre-defined types: | ||
/// universe - super type | ||
/// type - another type | ||
/// predicate - predicate expression (subtype and predicate) |
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.
No predicate_typet
so don't know what this means?
src/util/type.h
Outdated
/// universe - super type | ||
/// type - another type | ||
/// predicate - predicate expression (subtype and predicate) | ||
/// uninterpreted - uninterpreted type with identifier |
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.
No uninterpreted_typet
so don't know what this means, symbol_typet
perhaps?
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.
symbol_typet
appears later in the list
src/util/type.h
Outdated
/// enum - with elements, the ordering does not matter | ||
/// tuple - with components: each component has type, | ||
/// the ordering matters | ||
/// mapping - domain -> range |
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.
This also doesn't seem to be defined so perhaps should go
src/util/type.h
Outdated
/// complex | ||
/// string | ||
/// enum - with elements, the ordering does not matter | ||
/// tuple - with components: each component has 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.
This doesn't seem to be defined should go
@tautschnig @peterschrammel @thk123 Ready for re-review. @smowton Please proof read if you would have time. |
831553d
to
aecf1c8
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.
Looks great! Couple of minor things but would be very happy to see this merged as is.
@@ -329,6 +338,10 @@ bool base_type_eq( | |||
return base_type_eq.base_type_eq(type1, type2); | |||
} | |||
|
|||
/// Check expressions for equality across all levels of hierarchy. |
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.
Sorry I don't understand the meaning of this - perhaps a short example as you've given for the typet
overload
/*! \brief The NIL type | ||
*/ | ||
/// The NIL type, i.e., an invalid type, no value. Use `optional<typet>` | ||
/// instead where possible. | ||
class nil_typet:public 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.
You might even want to deprecate this (though not sure you can deprecate a class, I think it would look like:
class DEPRECATED nil_typet : public 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.
Will do this in a follow-up PR
src/util/std_types.h
Outdated
/*! \brief A union tag type | ||
*/ | ||
|
||
/// A union tag type, i.e., a union type with an identifier |
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.
With each of these tag_typet
you might also like to refer to to the untagged type
/// Check types for equality at the top level. If either of the types is a | ||
/// symbol type, i.e., a reference into the symbol table, retrieve it from | ||
/// the namespace and compare but don't do this recursively. For equality | ||
/// across all level in the hierarchy use \ref base_type_eq. |
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.
Ok, thanks a lot for elaborating, this is very helpful. But it makes me wonder when this is the right thing to do/to use?
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.
After a bit of out-of-band discussion: #2808.
Squashed and rebased, waiting for CI. @tautschnig @thk123 Here is the follow-up PR #2815 |
b0a0002 Merge pull request diffblue#2751 from diffblue/unicode-format 9d8abbf Merge pull request diffblue#2846 from peterschrammel/jbmc-no-cover-tests 86aea9b use status() to output VCCs f2fa169 draw Gentzen turnstile using Unicode e152c92 JBMC tests should not use --cover d33bd22 Merge pull request diffblue#2839 from diffblue/java_class_loader_base f8ef8dc Merge pull request diffblue#2842 from diffblue/cbmc-help 12637a4 Merge pull request diffblue#2843 from diffblue/split_string_cleanup 049dd2f Merge pull request diffblue#2795 from thomasspriggs/tas/doxygen_styling 646a9d8 use split_string that returns its result 0b9b01a Move `.css` file into `doc` directory 30f055b help: --drop-unused-functions belongs with the transformation 5513c79 remove help for --smt1 option 708acf4 missing newline in help 0881bf2 split_string with return value now also has 'strip' and 'remove_empty' 0a53059 factor out classpath functionality into separate class f0221b8 Merge pull request diffblue#2782 from mgudemann/doc/doc-20/document-class-files a6da811 Merge pull request diffblue#2834 from diffblue/protect-exprt-methods 4bfbb48 Correct section entries 3bc445e Merge pull request diffblue#2788 from johnnonweiler/doc/update-folder-walkthrough b38b671 Merge pull request diffblue#2837 from diffblue/type-convert_dowhile 2e3fd61 Merge pull request diffblue#2832 from diffblue/stack-trace 56c7da7 add typing for convert_dowhile a594f9f cbmc can now print stack traces cbe16b3 Merge pull request diffblue#2833 from diffblue/object_descriptor_exprt-root_object 2542c8e Merge pull request diffblue#2835 from johnnonweiler/bugfix/janalyzer_module_dependencies 47c741c Add directory dependencies diagram d4c4298 Merge pull request diffblue#2816 from smowton/smowton/feature/json-symbol-table 278d2ff Remove jdiff from janalyzer/module_dependencies.txt 84f09a9 move object_descriptor_exprt::root_object into .cpp 68f95d2 add protection to internal methods of exprt 0f0d50b Merge pull request diffblue#2766 from diffblue/jar_index 20e5d89 Implement --show-symbol-table in JSON-UI mode c5901e0 JSON stream: support streaming a key-value pair to an object 8d2a748 removed jar_indext types and data structures 27d0ae0 java_class_loadert::load_entire_jar now returns the classes loaded 7797757 Merge pull request diffblue#2828 from diffblue/cpp-constructor-optional f7fc6a9 Merge pull request diffblue#2790 from allredj/doc_exprt 0d5e588 Clean up show_symbol_table da6e5d7 cpp_typecheckt::cpp_destructor now returns optionalt<codet> instead of an expression fd5c528 rewrite a no-op e7d1180 cpp_typecheckt::cpp_constructor now returns optionalt<codet> instead of an expression d68708f Merge pull request diffblue#2658 from svorenova/bugfix_tg4365 6749aaf Merge pull request diffblue#2670 from mgudemann/feature/multi_object_input_parameter 9dc1f0e Document util/expr.{cpp,h} 4ed36c6 Fix naming in variables for non-deterministic values f623c0b Simplify code for alternative parameter types 6e96333 Change from optional set to simply set d2bc012 Allow multi object type parameter in entry point function call cb0f310 Add nondet.{h.cpp} e37d051 Add a comment to static field with the name of the field 437be99 Perform nondet-init in clinit_wrapper even if clinit doesn't exist 46d47e0 Add a regression test for nondet-static 2ecf8e8 Add nondet-static option to JBMC 9e6caba Mark final fields in Java as constants 48797b0 Nondet-initialize variables in clinit_wrapper constructor 5fe44ed Pass information to clinit_wrapper constructors 655978c Record nondet-static option in java_bytecode_language 82a1bd3 Merge pull request diffblue#2819 from diffblue/trace-with-arguments2 8646fdd Merge pull request diffblue#2817 from NathanJPhillips/cleanup/lazy-loading 7e6ff00 Merge pull request diffblue#2525 from peterschrammel/range-set-neg-offset-test 4c45282 Merge pull request diffblue#2807 from Degiorgio/ssa-doc bf717d3 show function arguments in trace 08cbe58 add arguments of function calls to goto_trace 668c4f3 Merge pull request diffblue#2772 from mgudemann/doc/doc-21/java_load_jar e4bc16e Minor code cleanup related to lazy loading ccd9783 Merge pull request diffblue#2818 from diffblue/trace-with-arguments 91ad280 Merge pull request diffblue#2812 from allredj/fix-readme-label 333527a Merge pull request diffblue#2801 from antlechner/antonia/doc-13-codet 9e68603 Documentation: updates goto-symex/README.md fc2e8da Document java_class_loader c4cd791 Documentation for jar_file 0e6efc7 Documentation for class_loader_limit 43c149d rename 'identifier' to 'function_identifier' 2ebbb24 Merge pull request diffblue#2771 from svorenova/doc_typet 0be9f18 Deconflict labels 12efeab Merge pull request diffblue#2781 from smowton/smowton/docs/fi-analysis 53fac78 Merge pull request diffblue#2813 from diffblue/java-char-literals-are-char a5ce804 Merge pull request diffblue#2783 from smowton/smowton/docs/goto-program 6493c4a Merge pull request diffblue#2796 from smowton/smowton/docs/goto-symex ad7902a Merge pull request diffblue#2811 from sonodtt/invariant-docs-change e37e9b8 Remove unneeded header f08773b Amend DATA_INVARIANT docs 592b114 Add documentation to std_types 7ad664c Add documentation to type_eq a54746f Add documentation to typet 1273eac Merge pull request diffblue#2804 from NathanJPhillips/cleanup/switch-lazy-mode a78b5bd First part of codet documentation ed7dc1d no need for cast for Java char literals 156e3d3 Document class file content for JBMC / java_bytecode readme 93b3e9c Merge pull request diffblue#2752 from NathanJPhillips/feature/parse-parameter-annotations 667738a Use a switch statement for clarity 8d38c5d Briefly document flow-insensitive analysis a812ba2 Improve goto-symex documentation 45933d0 Update docs for goto-programs 78d22fb Merge pull request diffblue#2763 from diffblue/classpath b7c430d Merge pull request diffblue#2797 from owen-jones-diffblue/doc/fix-doxygen-errors 61c44d2 Merge pull request diffblue#2799 from apaschos/doxy 589a584 Merge pull request diffblue#2779 from antlechner/antonia/doc-util-readme c679e55 Merge pull request diffblue#2776 from smowton/smowton/docs/call-graph dc03c8a Merge pull request diffblue#2778 from smowton/smowton/docs/constant-prop abae6a0 Merge pull request diffblue#2774 from smowton/smowton/docs/object-numbering 849f256 Merge pull request diffblue#2770 from smowton/smowton/docs/symbol-table 03b7bf2 Enable parsing of annotations on parameters db7c127 Combine padding specifiers 284137a Add extra spacing to code blocks 64dd1af Set style of left hand navigation tree 4b827eb Set link colours to mustard initially and purple for visited 740eed7 Collapse by default the dependency graphs 4bbaa9d Remove references from and to other functions 5e8308f Merge pull request diffblue#2769 from smowton/smowton/docs/irept a3b652c Change the order of appearance of class methods e4224a1 Fix colons in doxygen 68ca9a1 Correct parameter names to stop doxygen warning dc686bc Reduce heading sizes 712c168 Fix unclosed ``` causing doxygen warning f8d0fb8 Add overview of constant propagator 665e183 Add call-graph overview ef5ff03 Add a little more detail and discussion on irept b227eee Document symbol table and namespace 3f2537d Document dstring to string conversions 2675090 Add documentation for object numbering af6efcb Make inline code more distinctive 8095948 Add custom style sheet for doxygen html output 096decd Remove links to clobber and memory-models in doc 53b3c4a remove redundant class loader limit test dbd6988 Merge pull request diffblue#2750 from johnnonweiler/documentation-structure ba7e06f precompute the category of the classpath entry 5dbd48c unify jar list and classpath 24cbfc6 Merge pull request diffblue#2765 from diffblue/jar_pool 76dbb2a Remove links to classes from high level overview 384f0d4 use jar_poolt in java_class_loadert d601a44 factor out pool for JARs into jar_poolt 4dddd0c Merge pull request diffblue#2760 from diffblue/jar_pool_cleanup dbc95f8 java_class_loadert: remove unused parameter 8640288 Merge pull request diffblue#2698 from diffblue/clang-builtins 4ffc2a4 Merge pull request diffblue#2744 from danpoe/feature/invariants-with-diagnostic-information d0be385 Merge pull request diffblue#2619 from JohnDumbell/jd/bugfix/java_annotation_array_fix ac6c7d4 Parse java arrays in annotations properly cb090bf add clang's __builtin_ia32_undefX and __builtin_nontemporal_store and __builtin_nontemporal_load 1ad6b5d Merge pull request diffblue#2754 from antlechner/antonia/ci-lazy-loading-rec-clinit 03bdf37 Merge pull request diffblue#2755 from diffblue/COMPILING-again df0605e Add test for enum field of argument type ad1b1d8 Red Hat and Fedora now use dnf instead of yum c1ef758 jbmc build now uses Maven, not unzip aa1de84 implement clang's builtin_convertvector 49089b1 Fix lazy loading of enum static initializers e1fc49f Merge pull request diffblue#2720 from tautschnig/replace_symbol-cleanup1 e327ef2 replace_symbolt: hide {expr,type}_map 3f487c3 Merge pull request diffblue#2724 from tautschnig/replace-symbolt-unit-test 963b866 format_expr now produces unicode c55d032 Unit test of replace_symbolt 544671e Move 'Flattening' section in solvers/README.md 794ba03 Change heading in java-bytecode docs 1e2fda3 Workaround for Visual Studio not expanding __VA_ARGS__ on macro invocation f2f2156 Tests for invariant macros with diagnostic output 8a37a2d Invariant macros with diagnostic information bcb7c76 Merge pull request diffblue#2747 from diffblue/cleanup-message-handler 0d8ea2c remove sequence number from message_handler interface 4557374 use size_t for message counts ccf3c50 Add outline to module docs 0b7c4fb Add sections to java_bytecode/README.md 85a81ea Merge pull request diffblue#2594 from thk123/array_type_check 2becafd Merge pull request diffblue#2738 from diffblue/remove-memory-models c2825ef Merge pull request diffblue#2741 from diffblue/remove_asm_function_id aa7b89f Merge pull request diffblue#2742 from diffblue/symbol_type_fix 1f06cde Merge pull request diffblue#2743 from tautschnig/boolbv-width ba57a14 remove memory-models 4e95060 Merge pull request diffblue#2739 from diffblue/remove-clobber 0661075 Delete one word ('testing') d6755b0 Move solvers API description to solvers module f7bcd0a Move java_bytecode explanations to module doc ccaa87c Move examples from code-walkthrough to linked module d33628e Fix boolbv_widtht::get_entry and fail for unknown types a1d59d2 remove clobber ef509a5 two further instances of symbol_type ef4bb3c properly set function id on instructions added by remove_asm 0695df6 Switch one file from ## to using sections 124d012 Combined many pages of developer docs into one 96dc0a3 Fix minor typos d42821f Adding can_cast_type for array_typet 35e278e Move docs from guide to module-level docs 147c5d9 Add header for orphaned diagram 3eee998 Add references to class-level documentation d924247 Add in empty lines after headings 3b74238 Fix apostrophe 90e43d9 Fix "#" being converted to "::" in doxygen c423bb6 Add links to module level documentation 2034faf Move two items out of list 37128c0 Improve how a sentence reads 2ea73b8 Move "Tutorial" section to the right place dfcb7cd Describe the aim of the documentation marked as "For contributors" 1920f17 Test for byte extract with negative offset git-subtree-dir: cbmc git-subtree-split: b0a0002
No description provided.