Doc/move irep docs from util to irep #2618

owen-mc-diffblue · 2018-07-25T16:05:48Z

No description provided.

smowton

Might as well update this while we're doing this

smowton · 2018-07-25T16:59:14Z

src/util/irep.h

+/// The `irept::pretty` function outputs the contents of an `irept` directly
+/// and can be used to understand and debug problems with `irept`s.
+///
+/// On their own `irept`s do not “mean” anything; they are effectively


Mix of smart and normal quotes

smowton · 2018-07-25T17:02:29Z

src/util/irep.h

+///   is used for named children, i.e.  subexpressions, parameters, etc.
+///
+/// * `comments`:   Another map from `irep_namet` to `irept` which is used
+///   for annotations and other ‘non-semantic’ information


Probably worth mentioning the caveat about these not being taken into account by the default operator== here

smowton · 2018-07-25T17:03:51Z

src/util/irep.h

+/// On their own `irept`s do not “mean” anything; they are effectively
+/// generic tree nodes. Their interpretation depends on the contents of
+/// result of the `id` function (the `data`) field. `util/irep_ids.txt`
+/// contains the complete list of `id` values. During the build process it


Nah, ireps that use other strings (e.g. irept("Hello world") are not common but are definitely present in the codebase

smowton · 2018-07-25T17:06:16Z

src/util/irep.h

+/// with the architecture of the code.
+///
+/// Many of the key descendant of `exprt` are declared in `std_expr.h`. All
+/// expressions have a named subfield / annotation which gives the type of


named subexpression with ID "type" would probably be clearer

smowton · 2018-07-25T17:07:11Z

src/util/irep.h

+/// expressions have a named subfield / annotation which gives the type of
+/// the expression (slightly simplified from C/C++ as `unsignedbv_typet`,
+/// `signedbv_typet`, `floatbv_typet`, etc.). All type conversions are
+/// explicit with an expression with `id() == ID_typecast` and an ‘interface


"interface class" is not used anywhere else, just say "i.e. a typecast_exprt" instead

smowton · 2018-07-25T17:07:37Z

src/util/irep.h

+/// using the `get_identifier` accessor function.
+///
+/// `codet` inherits from `exprt` and is defined in `std_code.h`. It
+/// represents executable code; statements in C rather than expressions. In


...a C-like language...

smowton · 2018-07-25T17:08:11Z

src/util/irep.h

+/// the front-end there are versions of these that hold whole code blocks,
+/// but in goto-programs these have been flattened so that each `irept`
+/// represents one sequence point (almost one line of code / one
+/// semi-colon). The most common descendants of `codet` are `code_assignt`


is code_assignt

allredj

Passed Diffblue compatibility checks (cbmc commit: 105e297).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/80008898

peterschrammel · 2018-07-25T21:37:52Z

src/util/dstring.h

+/// of the same string you only have to store the whole string once, which
+/// saves space.
+///
+/// `irep_idt` and `irep_namet` are typedef-ed to `dstringt` in irep.h unless


unless what?

peterschrammel · 2018-07-25T21:38:48Z

src/util/irep.h

+///
+/// On their own `irept`s do not “mean” anything; they are effectively
+/// generic tree nodes. Their interpretation depends on the contents of
+/// result of the `id` function (the `data`) field. `util/irep_ids.txt`


This is irep_ids.def now.

peterschrammel · 2018-07-25T21:41:04Z

src/util/irep.h

+/// * `sub`:   A vector of `irept` which is used to store ordered but
+///   unnamed children.
+///
+/// The `irept::pretty` function outputs the contents of an `irept` directly


maybe say that it prints the explicit tree structure instead of 'directly'

peterschrammel · 2018-07-25T21:43:05Z

src/util/irep.h

+/// * `data`:   A string[^2], which is returned when the `id()` function is
+///   used.
+///
+/// * `named_sub`:   A map from `irep_namet` (a string) to `irept`. This


Use as many \ref as possible

Annoyingly, doxygen sometimes can't get the \ref to work if the name is in backticks, but sometimes it can

peterschrammel · 2018-07-25T21:44:05Z

src/util/irep.h

+/// so a common pattern is to cast the `codet` to an assignment and then
+/// recurse on the expression on either side.
+///
+/// [^1]: Or references, if reference counted data sharing is enabled. It is


Maybe inline these footnotes.

owen-mc-diffblue · 2018-07-26T10:59:31Z

I have addressed all the review comments

allredj

Passed Diffblue compatibility checks (cbmc commit: ae66e65).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/80350969

allredj

Passed Diffblue compatibility checks (cbmc commit: 6b0dfb6).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/80355880

owen-mc-diffblue · 2018-07-31T08:58:33Z

@peterschrammel @smowton Please re-review.

smowton · 2018-07-31T09:22:11Z

src/util/irep.h

+///
+/// * \ref irept::dt::comments : Another map from `irep_namet` to \ref irept
+///   which is used for annotations and other ‘non-semantic’ information. Note
+///   that this map is ignore by the default \ref operator==.


smowton · 2018-07-31T09:22:38Z

src/util/irep.h

+/// result of the \ref id() function, i.e. the `data` field. `util/irep_ids.def`
+/// contains a list of `id` values. During the build process it is used
+/// to generate `util/irep_ids.h` which gives constants for each id
+/// (named `ID_`). You can also make `irep_id`s which do not come from


smowton · 2018-07-31T09:24:04Z

src/util/irep.h

+/// type of the expression (slightly simplified from C/C++ as \ref
+/// unsignedbv_typet, \ref signedbv_typet, \ref floatbv_typet, etc.). All type
+/// conversions are explicit with an expression with `id() == ID_typecast`
+/// and a \ref typecast_exprt. One key descendant of \ref exprt is \ref


The typecast_exprt is the expression with id() == ID_typecast

It was in the documentation for the util folder.

It often doesn't work when backticks are used, so I've removed them. They don't affect how the text appears that much when I look at the html.

allredj

This PR failed Diffblue compatibility checks (cbmc commit: 0855872).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/80546022
Status will be re-evaluated on next push.
Please contact @peterschrammel, @thk123, or @allredj for support.

Common spurious failures:

the cbmc commit has disappeared in the mean time (e.g. in a force-push)
the author is not in the list of contributors (e.g. first-time contributors).

6a10f1a Merge pull request diffblue#2462 from tautschnig/vs-goto-inline 96fc7b1 Merge pull request diffblue#2654 from peterschrammel/update-jml8 1847066 Update jbmc/lib/java-models-library to java-models-library#8 (remove sun.* imports) c157ba7 Revert "CMake version.cpp: switch back to add_custom_target" 7a009d6 Merge pull request diffblue#2650 from diffblue/aws-codebuild-clcache 63652fc add clcache to Windows build 6f72b3b Merge pull request diffblue#2657 from smowton/smowton/fix/cmake-version-cpp 35d09d5 CMake version.cpp: switch back to add_custom_target 80331d8 Merge pull request diffblue#2638 from diffblue/CBMC_VERSION_string 7c066f9 Merge pull request diffblue#2618 from owen-jones-diffblue/doc/move-irep-docs-from-util-to-irep ad5c375 use a string instead of macro for version number b6258db Merge pull request diffblue#2509 from danpoe/feature/sharing-map-stats eb71a01 Merge pull request diffblue#2639 from thk123/array-element-type c5519ec Merge pull request diffblue#2640 from allredj/support-for-load-containing-class-only 0855872 Address review comments diffblue#2 eaa7664 Wrap lines properly e682eb9 Add \ref in lots of places 3023cca Address review comments 758f069 Move dstringt documentation to above dstringt a54c82d Move documentation of irept to be above irept b827ea4 Use type equality check in unit tests 77185fd Merge pull request diffblue#2607 from jeannielynnmoulton/jeannie/ParseThrownExceptions2 1f4ef40 Add class loader debug output 4ae8eb6 Move sharing map friends declarations to unit tests 186897c Sharing stats for the sharing map 4438b43 Fix sharing map internal assertion 332febe Remove wrong sharing map internal assertions be7e140 Activate internal checks for the sharing map unit tests 713d3fe Merge pull request diffblue#2636 from polgreen/fix_function_map 87f90ee Add replace_all string utility ea2d393 Make test work on windows 4fa9943 Make array element type be not a comment 655248a Add unit test for when there are no exceptions. a6e7c4b Refactors interface for exceptions to not use irepts. 1134bba Creates java_method_typet which extends code_typet aa83622 Unit tests method get_super_class 565c999 Unit tests throws exceptions parsing. eb88509 Use parsed information for thrown exceptions. 5c7dcac Parses the exception attribute 7fcc42d Adds const to get/set_outer_class 5994dd8 Add method to get super class from java class type. fbad2d9 Rename variable extends to super_class 6d0776f if function is not in the function map, treat as if it has no body da86bdb Merge pull request diffblue#2602 from diffblue/__CPROVER_r/w_ok 0202f34 refactor pointer_validity_check using address_check 4a24ad4 use __CPROVER_r/w_ok in string.c library 732ce2a expand __CPROVER_r/w_ok in goto_check acfea65 __CPROVER_r_ok and __CPROVER_w_ok added to ANSI-C front-end 0618f7d Merge pull request diffblue#2628 from diffblue/clang-extensions 5e43131 Merge pull request diffblue#2608 from diffblue/ms_cl_int64 7c56091 Merge pull request diffblue#2634 from qaphla/local_bitvector_analysis_regression 44ef8d5 Merge pull request diffblue#2630 from diffblue/invalid-pointer-flattening f74c161 test for __float80 and __float128 8288a72 __float80 is a typedef, not a keyword 5495625 FreeBSD: default flavor is now CLANG e63402e added _Null_unspecified clang extension 16a49a7 bugfix: __float128 3849bb0 rename APPLE flavor to CLANG 060b59c separate pointer check for integer addresses 9b5847e fix flattening of ID_invalid_pointer 432dcf1 Added a regression test checking that --pointer-check does not generate excess checks if local_bitvector_analysis can gather information on the pointer being checked. cbfcc5c added support for _int64 keyword 0148347 Avoid signed/unsigned casts and conversion in goto_inline git-subtree-dir: cbmc git-subtree-split: 6a10f1a

owen-mc-diffblue requested review from kroening, peterschrammel, pkesseli, smowton and tautschnig as code owners July 25, 2018 16:05

smowton reviewed Jul 25, 2018

View reviewed changes

allredj reviewed Jul 25, 2018

View reviewed changes

peterschrammel reviewed Jul 25, 2018

View reviewed changes

peterschrammel assigned owen-mc-diffblue Jul 25, 2018

owen-mc-diffblue mentioned this pull request Jul 26, 2018

Create CBMC developer guide documentation #2615

Merged

owen-mc-diffblue force-pushed the doc/move-irep-docs-from-util-to-irep branch from ee59bed to ae66e65 Compare July 30, 2018 09:54

allredj reviewed Jul 30, 2018

View reviewed changes

smowton approved these changes Jul 31, 2018

View reviewed changes

Owen Jones added 6 commits July 31, 2018 17:36

Move documentation of irept to be above irept

a54c82d

It was in the documentation for the util folder.

Move dstringt documentation to above dstringt

758f069

Address review comments

3023cca

Add \ref in lots of places

e682eb9

It often doesn't work when backticks are used, so I've removed them. They don't affect how the text appears that much when I look at the html.

Wrap lines properly

eaa7664

Address review comments diffblue#2

0855872

owen-mc-diffblue force-pushed the doc/move-irep-docs-from-util-to-irep branch from 6b0dfb6 to 0855872 Compare July 31, 2018 16:36

peterschrammel approved these changes Jul 31, 2018

View reviewed changes

allredj reviewed Jul 31, 2018

View reviewed changes

owen-mc-diffblue merged commit 7c066f9 into diffblue:develop Aug 1, 2018

owen-mc-diffblue deleted the doc/move-irep-docs-from-util-to-irep branch August 1, 2018 09:17

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Doc/move irep docs from util to irep #2618

Doc/move irep docs from util to irep #2618

owen-mc-diffblue commented Jul 25, 2018

smowton left a comment

smowton Jul 25, 2018

smowton Jul 25, 2018

smowton Jul 25, 2018

smowton Jul 25, 2018

smowton Jul 25, 2018

smowton Jul 25, 2018

smowton Jul 25, 2018

allredj left a comment

peterschrammel Jul 25, 2018

peterschrammel Jul 25, 2018

peterschrammel Jul 25, 2018

peterschrammel Jul 25, 2018

owen-mc-diffblue Jul 26, 2018

peterschrammel Jul 25, 2018

owen-mc-diffblue commented Jul 26, 2018

allredj left a comment

allredj left a comment

owen-mc-diffblue commented Jul 31, 2018

smowton Jul 31, 2018

smowton Jul 31, 2018

smowton Jul 31, 2018

allredj left a comment

Doc/move irep docs from util to irep #2618

Doc/move irep docs from util to irep #2618

Conversation

owen-mc-diffblue commented Jul 25, 2018

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

allredj 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

owen-mc-diffblue commented Jul 26, 2018

allredj left a comment

Choose a reason for hiding this comment

allredj left a comment

Choose a reason for hiding this comment

owen-mc-diffblue commented Jul 31, 2018

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

allredj left a comment

Choose a reason for hiding this comment