diff --git a/doc/architectural/background-concepts.md b/doc/architectural/background-concepts.md index ca973284bca..3b477d762ef 100644 --- a/doc/architectural/background-concepts.md +++ b/doc/architectural/background-concepts.md @@ -3,30 +3,30 @@ \author Martin Brain, Peter Schrammel -# Representations # +\section representations_section Representations -## AST: types, globals, variables, functions, code blocks, language primitives, assignments, expressions, variables ## +\subsection AST_section AST: types, globals, variables, functions, code blocks, language primitives, assignments, expressions, variables To be documented. -## CFG ## +\subsection CFG_section CFG To be documented. -## SSA ## +\subsection SSA_section SSA To be documented. -# Analysis techniques # +\section analysis_techniques_section Analysis techniques -## Bounded model checking ## +\subsection BMC_section Bounded model checking To be documented (can copy from the CBMC manual). -## SAT and SMT ## +\subsection SAT_section SAT and SMT To be documented. -## Static analysis ## +\subsection static_analysis_section Static analysis To be documented. diff --git a/doc/architectural/bmct-class.md b/doc/architectural/bmct-class.md deleted file mode 100644 index 1cc7ee39404..00000000000 --- a/doc/architectural/bmct-class.md +++ /dev/null @@ -1,8 +0,0 @@ -\ingroup module_hidden -\page bmct-class Bmct class - -\author - -## equation ## - -To be documented. diff --git a/doc/architectural/cbmc-architecture.md b/doc/architectural/cbmc-architecture.md index 38b621f3f7f..810bb6e6e75 100644 --- a/doc/architectural/cbmc-architecture.md +++ b/doc/architectural/cbmc-architecture.md @@ -52,7 +52,7 @@ be output to files (this is what `goto-cc` does) and are (informally) referred to as “goto binaries” or “goto programs”. The back-end are tools process this format, either directly from the front-end or from it’s saved output. These include a wide range of analysis and -transformation tools (see \ref section-other-tools). +transformation tools (see \ref other-tools). # Concepts # ## {C, java bytecode} → Parse tree → Symbol table → GOTO programs → GOTO program transformations → BMC → counterexample (goto_tracet) → printing ## diff --git a/doc/architectural/code-walkthrough.md b/doc/architectural/code-walkthrough.md new file mode 100644 index 00000000000..008f52d855b --- /dev/null +++ b/doc/architectural/code-walkthrough.md @@ -0,0 +1,53 @@ +\ingroup module_hidden +\page code-walkthrough Code Walkthrough + +\author Cesar Rodriguez, Owen Jones + +\section data-structures-core-structures-and-ast-section Data structures: core structures and AST + +The core structures used for representing abstract syntax trees are all +documented in \ref util. + +\section data-structures-from-ast-to-goto-program-section Data structures: from AST to GOTO program + +See \ref goto-programs, \ref goto_programt and [instructiont](\ref goto_programt::instructiont). + +\section front-end-languages-generating-codet-from-multiple-languages-section Front-end languages: generating codet from multiple languages + +\subsection language-uit-section language_uit, language_filest, languaget classes: + +See \ref langapi. + +\subsection languages-c-section C + +See \ref ansi-c. + +\subsection languages-cpp-section C++ + +See \ref cpp. + +\subsection languages-java-section Java bytecode + +See \ref java_bytecode. + +\section bmct-class-section Bmct class + +\subsection equation-section equation + +See \ref symex-overview. + + +\section symbolic-executors-section Symbolic executors + +\subsection symbolic-execution-section Symbolic execution + +See \ref symex-overview. + + +\section solvers-infrastructure-section Solvers infrastructure + +See \ref solvers-overview. + +\section static-analysis-apis-section Static analysis APIs + +See \ref analyses and \ref pointer-analysis. diff --git a/doc/architectural/compilation-and-development.md b/doc/architectural/compilation-and-development.md index 9f7a7dba5aa..5bbcaf76b5f 100644 --- a/doc/architectural/compilation-and-development.md +++ b/doc/architectural/compilation-and-development.md @@ -24,7 +24,7 @@ To be documented. The regression tests are contained in the `regression/` folder. They are grouped into directories for each of the tools/modules. Each of these contains multiple directories, each of which contains -input files and one or more`.desc` files that describe what command +input files and one or more `.desc` files that describe what command to run, what output is expected and so on. There is a Perl script, `test.pl` that is used to invoke the tests as: diff --git a/doc/architectural/data-structures-core-structures-and-ast.md b/doc/architectural/data-structures-core-structures-and-ast.md deleted file mode 100644 index 4b0c1b1a3a8..00000000000 --- a/doc/architectural/data-structures-core-structures-and-ast.md +++ /dev/null @@ -1,102 +0,0 @@ -\ingroup module_hidden -\page data-structures-core-structures-and-ast Data structures: core structures and AST - -\author Martin Brain, Peter Schrammel, Owen Jones - -## Strings: dstringt, the string_container and the ID_* ## -Within cbmc, strings are represented using `irep_idt`. By default this is -typedefed to \ref dstringt, which stores a string as an index into a large -static table of strings. This makes it easy to compare if two `irep_idt`s -are equal (just compare the index) and it makes it efficient to store -many copies of the same string. The static list of strings is initially populated -from `irep_ids.def`, so for example the fourth entry in `irep_ids.def` is -“IREP_ID_ONE(type)”, so the string “type” has index 3. You can refer to -this `irep_idt` as `ID_type`. The other kind of line you see is -“IREP_ID_TWO(C_source_location, #source_location)”, which means the -`irep_idt` for the string “#source_location” can be referred to as -`ID_C_source_location`. The “C” is for comment, which will be explained -in the next section. Any strings that need to be stored as `irep_id`s which -aren't in `irep_ids.def` are added to the end of the table when they are -first encountered, and the same index is used for all instances. - -See documentation at \ref dstringt. - -## irept: a 4-triple (data, named-sub, comments, sub) ## -See documentation at \ref irept. - -As that documentation says, `irept`s are generic tree nodes. You should -think of them as having a single string (data, actually an `irep_idt`) and -lots of child nodes, some of which are numbered (sub) and some of which are -labelled, and the label can either start with a “#” (comments-sub) or without -one (named-sub). The meaning of the “#” is that this child should not be -considered important, for example it shouldn’t be counted when comparing two -`irept`s for equality. - -## typet ## - -To be documented. - -### symbol_typet ### - -To be documented. - -## exprt ## -\ref exprt is the class to represent an expression. It inherits from \ref irept, -and the only things it adds to it are that every \ref exprt has a named sub -containing its type and everything in the sub of an \ref exprt is again an -\ref exprt, not just an \ref irept. You can think of \ref exprt as a node in the -abstract syntax tree for an expression. There are many classes that -inherit from \ref exprt and which represent more specific things. For -example, there is \ref minus_exprt, which has a sub of size 2 (for the two -argument of minus). - -Recall that every \ref irept has one piece of data of its own, i.e. its -`id()`, and all other information is in its `named_sub`, `comments` or -`sub`. For `exprt`s, the `id()` is used to specify why kind of \ref exprt this is, -so a \ref minus_exprt has `ID_minus` as its `id()`. This means that a -\ref minus_exprt can be passed wherever an \ref exprt is expected, and if you -want to check if the expression you are looking at is a minus -expression then you have to check its `id()` (or use -`can_cast_expr`). - -## codet ## -\ref exprt represents expressions and \ref codet represents statements. \ref codet -inherits from \ref exprt, so all `codet`s are `exprt`s, with `id()` `ID_code`. -Many different kinds of statements inherit from \ref codet, and they are -distinguished by their `statement()`. For example, a while loop would be -represented by a \ref code_whilet, which has `statement()` `ID_while`. -\ref code_whilet has two operands in its sub, and helper functions to make -it easier to use: `cond()` returns the first subexpression, which -is the condition for the while loop, and `body()` returns the second -subexpression, which is the body of the while loop - this has to be -a \ref codet, because the body of a while loop is a statement. - -## symbolt, symbol_table, and namespacet ## - -To be documented. - -### Symbol lifetimes, symbol modes, name, base-name, pretty-name; semantic of lifetimes for symex? ### - -To be documented. - -### Storing symbols and hiding symbols (namespacet) ### - -To be documented. - -### ns.follow ## - -To be documented. - -## Examples: how to represent the AST of statements, in C and in java ## - -### x = y + 123 ### - -To be documented.. - -### if (x > 10) { y = 2 } else { v[3] = 4 } ### - -To be documented. - -### Java arrays: struct Array { int length, int *data }; ### - -To be documented. diff --git a/doc/architectural/data-structures-from-ast-to-goto-program.md b/doc/architectural/data-structures-from-ast-to-goto-program.md deleted file mode 100644 index b16394a72a5..00000000000 --- a/doc/architectural/data-structures-from-ast-to-goto-program.md +++ /dev/null @@ -1,42 +0,0 @@ -\ingroup module_hidden -\page data-structures-from-ast-to-goto-program Data structures: from AST to GOTO program - -\author Martin Brain, Peter Schrammel - -## goto_programt ## - -See \ref goto_programt. - -### instructiont ### - -See [instructiont](\ref goto_programt::instructiont). - -#### Types, motivation of each type ##### - -See [instructiont](\ref goto_programt::instructiont). - -#### Accepted code (codet) values #### - -To be documented. - -#### Accepted guard (exprt) values #### - -To be documented. - -## goto_functionst ## - -\ref goto_functionst is a map from function names to function bodies (CFGs). - -To be documented. - -## goto_modelt ## - -\ref goto_modelt is a compilation unit. - -To be documented. - -## Example: ## - -### Unsigned mult (unsigned a, unsigned b) { int acc, i; for (i = 0; i < b; i++) acc += a; return acc; } ### - -To be documented. diff --git a/doc/architectural/front-end-languages-generating-codet-from-multiple-languages.md b/doc/architectural/front-end-languages-generating-codet-from-multiple-languages.md deleted file mode 100644 index 3519239cfea..00000000000 --- a/doc/architectural/front-end-languages-generating-codet-from-multiple-languages.md +++ /dev/null @@ -1,36 +0,0 @@ -\ingroup module_hidden -\page front-end-languages-generating-codet-from-multiple-languages Front-end languages: generating codet from multiple languages - -\author Martin Brain, Peter Schrammel - -## language_uit, language_filest, languaget classes: ## - -### Purpose ### - -To be documented. - -### Parse ### - -To be documented. - -### Typecheck ### - -To be documented. - -### Final ### - -To be documented. - -## Java bytecode ## - -### Explain how a java program / class is represented in a .class ### - -To be documented. - -### Explain the 2 step conversion from bytecode to codet ### - -To be documented. - -### A worked example of converting java bytecode to codet ### - -To be documented. diff --git a/doc/architectural/front-page.md b/doc/architectural/front-page.md index 2498dfcd8c0..b6c71607264 100644 --- a/doc/architectural/front-page.md +++ b/doc/architectural/front-page.md @@ -68,6 +68,10 @@ you can access it Modules - link gives an overview of a directory in the CProver codebase. - -* If you already know exactly what you're looking for, the API reference - is generated from the codebase. You can search for classes and class - members in the search bar at top-right or use one of the links in the - sidebar. - * The \subpage tutorial "CBMC Developer Tutorial" helps new contributors to CProver to get their feet wet through a series of programming exercises - mostly modifying goto-instrument, and thus learning to manipulate the main data structures used within CBMC. +For higher-level architectural information, each of the pages under +the Modules +link gives an overview of a directory in the CProver codebase. + +If you already know exactly what you're looking for, the best place +to look is the API reference, which +is generated from the codebase. You can search for classes and class +members in the search bar at top-right or use one of the links in the +sidebar. + \defgroup module_hidden _hidden diff --git a/doc/architectural/solvers-infrastructure.md b/doc/architectural/solvers-infrastructure.md deleted file mode 100644 index 0a0c9e15f36..00000000000 --- a/doc/architectural/solvers-infrastructure.md +++ /dev/null @@ -1,16 +0,0 @@ -\ingroup module_hidden -\page solvers-infrastructure Solvers infrastructure - -\author - -## Flattening ## - -To be documented. - -## SMT solving API ## - -To be documented. - -## SAT solving API ## - -To be documented. diff --git a/doc/architectural/static-analysis-apis.md b/doc/architectural/static-analysis-apis.md deleted file mode 100644 index 507ecd2ce8d..00000000000 --- a/doc/architectural/static-analysis-apis.md +++ /dev/null @@ -1,6 +0,0 @@ -\ingroup module_hidden -\page static-analysis-apis Static analysis APIs - -\author - -To be documented. diff --git a/doc/architectural/symbolic-executors.md b/doc/architectural/symbolic-executors.md deleted file mode 100644 index 2b7ce201298..00000000000 --- a/doc/architectural/symbolic-executors.md +++ /dev/null @@ -1,8 +0,0 @@ -\ingroup module_hidden -\page symbolic-executors Symbolic executors - -\author - -## Symex class ## - -To be documented. diff --git a/jbmc/src/java_bytecode/README.md b/jbmc/src/java_bytecode/README.md index 7b8812aa0b3..b590319830d 100644 --- a/jbmc/src/java_bytecode/README.md +++ b/jbmc/src/java_bytecode/README.md @@ -1,6 +1,70 @@ \ingroup module_hidden \defgroup java_bytecode java_bytecode -# Folder java_bytecode +This module provides a front end for Java. -This module providesy a front end for Java. +\section java-bytecode-conversion-section Overview of conversion from bytecode to codet + +To be documented. + +\section java-bytecode-object-factory Object Factory + +To be documented. + +\subsection java-bytecode-pointer-type-selection Pointer type selection + +To be documented. + +\subsection java-bytecode-genereic-substitution Generic substitution + +To be documented. + +\section java-bytecode-parsing Java bytecode parsing (parser, convert_class, convert_method) + +To be documented. + +\subsection java-class-section How a java program / class is represented in a .class + +To be documented. + +\section java-bytecode-runtime-exceptions Adding runtime exceptions (java_bytecode_instrument) + +To be documented. + +\section java-bytecode-concurrency-instrumentation Concurrency instrumentation + +To be documented. + +\section java-bytecode-remove-java-new Remove java new + +To be documented. + +\section java-bytecode-remove-exceptions remove_exceptions + +To be documented. + +\section java-bytecode-method-stubbing Method stubbing + +To be documented. + +\section java-bytecode-lazy-methods-v1 Context Insensitive lazy methods (aka lazy methods v1) + +To be documented. + +\section java-bytecode-core-models-library Core Models Library + +To be documented. + +\section java-bytecode-java-types java_types + +To be documented. + +\section java-bytecode-string-library String library + +To be documented. + +See also \ref string-solver-interface. + +\section java-bytecode-conversion-example-section A worked example of converting java bytecode to codet + +To be documented. diff --git a/src/analyses/README.md b/src/analyses/README.md index 7d5bb5ef268..f3ecd34a976 100644 --- a/src/analyses/README.md +++ b/src/analyses/README.md @@ -6,5 +6,112 @@ This contains the abstract interpretation framework `ai.h` and several static analyses that instantiate it. -FIXME: put here a good introduction describing what is contained -in this folder. +\section analyses-frameworks Frameworks: + +\subsection analyses-ait Abstract interpreter framework (ait) + +To be documented. + +\subsection analyses-static-analysist Old Abstract interpreter framework (static_analysist) + +This is obsolete. + +\subsection analyses-flow-insensitive-analysis Flow-insensitive analysis (flow_insensitive_analysist) + +To be documented. + +\section analyses-specific-analyses Specific analyses: + +\subsection analyses-call-graph Call graph and associated helpers (call_grapht) + +To be documented. + +\subsection analyses-dominator Dominator analysis (cfg_dominators_templatet) + +To be documented. + +\subsection analyses-constant-propagation Constant propagation (constant_propagator_ait) + +To be documented. + +\subsection analyses-taint Taint analysis (custom_bitvector_analysist) + +To be documented. + +\subsection analyses-dependence-graph Data- and control-dependence analysis (dependence_grapht) + +To be documented. + +\subsection analyses-dirtyt Address-taken lvalue analysis (dirtyt) + +To be documented. + +\subsection analyses-const-cast-removal const_cast removal analysis (does_remove_constt) + +To be documented. + +\subsection analyses-escape Escape analysis (escape_analysist) + +To be documented. + +\subsection analyses-global-may-alias Global may-alias analysis (global_may_aliast) + +To be documented. + +\subsection analyses-rwt Read-write range analysis (goto_rwt) + +To be documented. + +\subsection analyses-invariant-propagation Invariant propagation (invariant_propagationt) + +To be documented. + +\subsection analyses-is-threaded Multithreaded program detection (is_threadedt) + +To be documented. + +\subsection analyses-pointer-classification Pointer classification analysis (is-heap-pointer, might-be-null, etc -- local_bitvector_analysist) + +To be documented. + +\subsection analyses-cfg Control-flow graph (local_cfgt) + +To be documented. + +\subsection analyses-local-may-alias Local may-alias analysis (local_may_aliast) + +To be documented. + +\subsection analyses-safe-dereference Safe dereference analysis (local_safe_pointerst) + +To be documented. + +\subsection analyses-locals Address-taken locals analysis (localst) + +To be documented. + +\subsection analyses-natural-loop Natural loop analysis (natural_loops_templatet) + +To be documented. + +\subsection analyses-reaching-definitions Reaching definitions (reaching_definitions_analysist) + +To be documented. + +\subsection analyses-uncaught-exceptions Uncaught exceptions analysis (uncaught_exceptions_domaint) + +To be documented. + +\subsection analyses-uninitialized-locals Uninitialized locals analysis (uninitialized_analysist) + +To be documented. + +\section analyses-transformations Transformations (arguably in the wrong directory): + +\subsection analyses-goto-checkt Pointer / overflow / other check insertion (goto_checkt) + +To be documented. + +\subsection analyses-interval-analysist Integer interval analysis (interval_analysist) -- both an analysis and a transformation + +To be documented. diff --git a/src/goto-programs/README.md b/src/goto-programs/README.md index 4bccc9de726..51328732c4b 100644 --- a/src/goto-programs/README.md +++ b/src/goto-programs/README.md @@ -5,7 +5,7 @@ \author Kareem Khazem, Martin Brain -\section overview Overview +\section goto-programs-overview Overview Goto programs are the intermediate representation of the CPROVER tool chain. They are language independent and similar to many of the compiler intermediate languages. Section \ref goto-programs describes the @@ -371,3 +371,9 @@ previous stage: block. This stage concludes the *analysis-independent* program transformations. + +\subsection goto-program-example-section Example: + +\subsubsection goto-program-example-1-section Unsigned mult (unsigned a, unsigned b) { int acc, i; for (i = 0; i < b; i++) acc += a; return acc; } + +To be documented. diff --git a/src/langapi/README.md b/src/langapi/README.md index b39599ea20f..e3c3e94f684 100644 --- a/src/langapi/README.md +++ b/src/langapi/README.md @@ -10,3 +10,23 @@ language front ends. Developers only really need look at this if they are adding support for a new language. It’s main users are the language front-ends such as `ansi-c/` and `cpp/`. + +\section langapi-languaget The languaget interface + +To be documented. + +\section langapi-language-files Language files (language_filet, language_filest) + +To be documented. + +\section langapi-manipulation-framework The top-level language-file manipulation framework (language_uit, obsolete, replaced by initialize_goto_model) + +To be documented. + +\section langapi-mode-related-utils Symbol mode-related utilities (everything in mode.h) + +To be documented. + +\section langapi-pretty-printing Pretty-printing expressions and types (language_util.h) + +To be documented. diff --git a/src/pointer-analysis/README.md b/src/pointer-analysis/README.md index 0ef8b89f44b..5fd38dcc4af 100644 --- a/src/pointer-analysis/README.md +++ b/src/pointer-analysis/README.md @@ -10,3 +10,45 @@ arbitrary pointers, some alias analysis is needed. `pointer-analysis` contains the three levels of analysis; flow and context insensitive, context sensitive and flow and context sensitive. The code needed is subtle and sophisticated and thus there may be bugs. + +\section pointer-analysis-utilities Utilities: + +\subsection pointer-analysis-object-numbering Object / expression numbering (object_numberingt) + +To be documented. + +\subsection pointer-analysis-pointer-offset-sum Pointer-offset sum (pointer_offset_sum) + +To be documented. + +\subsection pointer-analysis-rewrite-index Rewrite index (x[i] -> *(x+i)) (rewrite_index) + +To be documented. + +\section pointer-analysis-analysis Value-set Analysis: + +To be documented. + +\subsection pointer-analysis-variants Variants: + +\subsubsection pointer-analysis-flow-insensitive Flow-insensitive + +To be documented. + +\subsubsection pointer-analysis-flow-insensitive-with-vr Flow-insensitive with 'vr' (value reduction?) + +To be documented. + +\subsubsection pointer-analysis-flow-insensitive-with-vr-ns Flow-insensitive with 'vr' and 'ns' (value reduction, ???) + +To be documented. + +\section pointer-analysis-transformations Transformations: + +\subsection pointer-analysis-add-failed-symbols + +This is obsolete. + +\subsection pointer-analysis-dereference-removal Dereference removal (*x -> x == &o1 ? o1 : ...) -- dereferencet, dereference_callbackt, value_set_dereferencet, goto_program_dereferencet, etc + +To be documented. diff --git a/src/solvers/README.md b/src/solvers/README.md index 4fb75cebaad..33fc3d5801b 100644 --- a/src/solvers/README.md +++ b/src/solvers/README.md @@ -4,7 +4,7 @@ \authors Romain Brenguier, Kareem Khazem, Martin Brain -\section overview Overview +\section solvers-overview Overview The basic role of solvers is to answer whether the set of equations given is satisfiable. @@ -60,6 +60,20 @@ different decision procedures, roughly one per directory. * sat/: Back-ends for a variety of SAT solvers and DIMACS output. +\section flattening-section Flattening + +To be documented. + +\section solver-apis Solver APIs + +\subsection smt-solving-api-section SMT solving API + +To be documented. + +\subsection sat-solving-api-section SAT solving API + +To be documented. + \section sat-smt-encoding SAT/SMT Encoding In the \ref solvers directory. @@ -81,7 +95,6 @@ digraph G { } \enddot - --- \section decision-procedure Decision Procedure diff --git a/src/util/README.md b/src/util/README.md index d72acf4507f..d955f320e45 100644 --- a/src/util/README.md +++ b/src/util/README.md @@ -7,20 +7,117 @@ \section data_structures Data Structures -This section discusses some of the key data-structures used in the +\ref util contains some of the key data-structures used in the CPROVER codebase. -\subsection irept_section Irept Data Structure +\subsection irept_section irept: a 4-tuple (data, named-sub, comments, sub) -See \ref irept for more information. +See documentation at \ref irept. -\subsection irep_idt_section Irep_idt and Dstringt +As that documentation says, [irept](\ref irept)s are generic tree nodes. You +should think of them as having a single string ([data](irept::data), actually +an \ref irep_idt) and lots of child nodes, some of which are numbered +([sub](\ref irept::dt::sub)) and some of which are labelled, and the label +can either start with a “\#” ([comments](\ref irept::dt::comments)) or without +one ([named_sub](\ref irept::dt::named_sub)). The meaning of the “\#” is that +this child should not be considered important, for example it shouldn't be +counted when comparing two [irept](\ref irept)s for equality. -Inside \ref irept, strings are stored as irep_idts, or irep_namets for -keys to named_sub or comments. By default both irep_idt and irep_namet -are typedefed to \ref dstringt, unless USE_STD_STRING is set, in which -case they are typedefed to std::string (this can be used for debugging -purposes). +\subsection irep_idt_section Strings: dstringt, the string_container and the ID_* + +Within cbmc, strings are represented using \ref irep_idt, or \ref irep_namet +for keys to [named_sub](\ref irept::dt::named_sub) or +[comments](\ref irept::dt::comments). By default these are both +typedefed to \ref dstringt. For debugging purposes you can set `USE_STD_STRING`, +in which case they are both typedefed to `std::string`. + +\ref dstringt stores a string as an index into a large +static table of strings. This makes it easy to compare if two +[irep_idt](\ref irep_idt)s are equal (just compare the index) and it makes it +efficient to store many copies of the same string. The static list of strings +is initially populated from `irep_ids.def`, so for example the fourth entry +in `irep_ids.def` is `“IREP_ID_ONE(type)”`, so the string “type” has index 3. +You can refer to this \ref irep_idt as `ID_type`. The other kind of line you +see is `“IREP_ID_TWO(C_source_location, #source_location)”`, which means the +\ref irep_idt for the string “#source_location” can be referred to as +`ID_C_source_location`. The “C” is for comment, meaning that it should be +stored in the ([comments](\ref irept::dt::comments). Any strings that need +to be stored as [irep_idt](\ref irep_idt)s which aren't in `irep_ids.def` +are added to the end of the table when they are first encountered, and the +same index is used for all instances. + +See documentation at \ref dstringt. + +\subsection typet_section typet + +See \ref typet. + +To be documented. + +\subsubsection symbol_typet_section symbol_typet + +See \ref symbol_typet. + +To be documented. + +\subsection exprt_section exprt + +\ref exprt is the class to represent an expression. It inherits from \ref +irept, and the only things it adds to it are that (1) every \ref exprt has +an entry in [named_sub](\ref irept::dt::named_sub) containing its type and +(2) everything in the [sub](\ref irept::dt::sub) of an \ref exprt is again an +\ref exprt, not just an \ref irept. You can think of \ref exprt as a node in +the abstract syntax tree for an expression. There are many classes that +inherit from \ref exprt and which represent more specific things. For +example, there is \ref minus_exprt, which has a [sub](\ref irept::dt::sub) +of size 2 (for the two arguments of minus). + +Recall that every \ref irept has one piece of data of its own, i.e. its +[id()](\ref irept::id()), and all other information is in its +[named_sub](\ref irept::dt::named_sub), [comments](\ref irept::dt::comments) +or [sub](\ref irept::dt::sub). For [exprt](\ref exprt)s, the +[id()](\ref irept::id()) is used to specify why kind of \ref exprt this is, +so a \ref minus_exprt has `ID_minus` as its [id()](\ref irept::id()). This +means that a \ref minus_exprt can be passed wherever an \ref exprt is +expected, and if you want to check if the expression you are looking at is +a minus expression then you have to check its [id()](\ref irept::id()) (or use +[can_cast_expr](\ref can_cast_expr)``). + +\subsection codet_section codet + +\ref exprt represents expressions and \ref codet represents statements. +\ref codet inherits from \ref exprt, so all [codet](\ref codet)s are +[exprt](\ref exprt)s, with [id()](\ref irept::id()) `ID_code`. +Many different kinds of statements inherit from \ref codet, and they are +distinguished by their [statement](\ref codet::get_statement()). For example, +a while loop would be represented by a \ref code_whilet, which has +[statement](\ref codet::get_statement()) `ID_while`. \ref code_whilet has +two operands in its [sub](\ref irept::dt::sub), and helper functions to make +it easier to use: [cond()](\ref code_whilet::cond()) returns the first +subexpression, which is the condition for the while loop, and +[body()](\ref code_whilet::body()) returns the second subexpression, which +is the body of the while loop - this has to be a \ref codet, because the body +of a while loop is a statement. + +\subsection symbolt_section symbolt, symbol_tablet, and namespacet + +To be documented. + +\subsubsection symbol_lifetimes_section Symbol lifetimes, symbol modes, name, base-name, pretty-name; semantic of lifetimes for symex? + +To be documented. + +\subsubsection storing_symbols_section Storing symbols and hiding symbols (namespacet) + +To be documented. + +\subsubsection ns_follow_section ns.follow + +To be documented. + +\subsection cmdlinet + +See \ref cmdlinet. \dot digraph G { @@ -33,3 +130,17 @@ digraph G { 2 -> 3 [label="Command line options, file names"]; } \enddot + +\subsection ast-examples-section Examples: how to represent the AST of statements, in C and in java + +\subsubsection ast-example-1-section x = y + 123 + +To be documented.. + +\subsubsection ast-example-2-section if (x > 10) { y = 2 } else { v[3] = 4 } + +To be documented. + +\subsubsection ast-example-3-section Java arrays: struct Array { int length, int *data }; + +To be documented.