diff --git a/src/util/README.md b/src/util/README.md index d955f320e45..a2196f295c9 100644 --- a/src/util/README.md +++ b/src/util/README.md @@ -85,6 +85,8 @@ a minus expression then you have to check its [id()](\ref irept::id()) (or use \subsection codet_section codet +See documentation at \ref 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`. diff --git a/src/util/std_code.cpp b/src/util/std_code.cpp index 0f399a4a41b..8dd7a6d03a1 100644 --- a/src/util/std_code.cpp +++ b/src/util/std_code.cpp @@ -1,11 +1,13 @@ /*******************************************************************\ -Module: +Module: Data structures representing statements in a program Author: Daniel Kroening, kroening@kroening.com \*******************************************************************/ +/// \file +/// Data structure representing different types of statements in a program #include "std_code.h" @@ -21,6 +23,10 @@ const irep_idt &code_deadt::get_identifier() const return to_symbol_expr(symbol()).get_identifier(); } +/// If this `codet` is a \ref code_blockt (i.e.\ it represents a block of +/// statements), return the unmodified input. Otherwise (i.e.\ the `codet` +/// represents a single statement), convert it to a \ref code_blockt with the +/// original statement as its only operand and return the result. code_blockt &codet::make_block() { if(get_statement()==ID_block) @@ -35,6 +41,8 @@ code_blockt &codet::make_block() return static_cast(*this); } +/// In the case of a `codet` type that represents multiple statements, return +/// the first of them. Otherwise return the `codet` itself. codet &codet::first_statement() { const irep_idt &statement=get_statement(); @@ -50,6 +58,7 @@ codet &codet::first_statement() return *this; } +/// \copydoc first_statement() const codet &codet::first_statement() const { const irep_idt &statement=get_statement(); @@ -65,6 +74,8 @@ const codet &codet::first_statement() const return *this; } +/// In the case of a `codet` type that represents multiple statements, return +/// the last of them. Otherwise return the `codet` itself. codet &codet::last_statement() { const irep_idt &statement=get_statement(); @@ -80,6 +91,7 @@ codet &codet::last_statement() return *this; } +/// \copydoc last_statement() const codet &codet::last_statement() const { const irep_idt &statement=get_statement(); diff --git a/src/util/std_code.h b/src/util/std_code.h index 1e047ff9525..d28a45da81a 100644 --- a/src/util/std_code.h +++ b/src/util/std_code.h @@ -1,6 +1,6 @@ /*******************************************************************\ -Module: +Module: Data structures representing statements in a program Author: Daniel Kroening, kroening@kroening.com @@ -16,8 +16,17 @@ Author: Daniel Kroening, kroening@kroening.com #include "expr.h" #include "expr_cast.h" -/*! \brief A statement in a programming language -*/ +/// Data structure for representing an arbitrary statement in a program. Every +/// specific type of statement (e.g. block of statements, assignment, +/// if-then-else statement...) is represented by a subtype of `codet`. +/// `codet`s are represented to be subtypes of \ref exprt since statements can +/// occur in an expression context in C: for example, the assignment `x = y;` +/// is an expression with return value `y`. For other types of statements in an +/// expression context, see e.g. +/// https://gcc.gnu.org/onlinedocs/gcc/Statement-Exprs.html. +/// To distinguish a `codet` from other [exprts](\ref exprt), we set its +/// [id()](\ref irept::id) to `ID_code`. To distinguish different types of +/// `codet`, we use a named sub `ID_statement`. class codet:public exprt { public: @@ -26,6 +35,9 @@ class codet:public exprt { } + /// \param statement: Specifies the type of the `codet` to be constructed, + /// e.g. `ID_block` for a \ref code_blockt or `ID_assign` for a + /// \ref code_assignt. explicit codet(const irep_idt &statement): exprt(ID_code, typet(ID_code)) { @@ -84,8 +96,8 @@ inline codet &to_code(exprt &expr) return static_cast(expr); } -/*! \brief Sequential composition -*/ +/// A \ref codet representing sequential composition of program statements. +/// Each operand represents a statement in the block. class code_blockt:public codet { public: @@ -174,8 +186,7 @@ inline code_blockt &to_code_block(codet &code) return static_cast(code); } -/*! \brief Skip -*/ +/// A \ref codet representing a `skip` statement. class code_skipt:public codet { public: @@ -191,8 +202,10 @@ template<> inline bool can_cast_expr(const exprt &base) // there is no to_code_skip, so no validate_expr is provided for code_skipt -/*! \brief Assignment -*/ +/// A \ref codet representing an assignment in the program. +/// For example, if an expression `e1` is represented as an \ref exprt `expr1` +/// and an expression `e2` is represented as an \ref exprt `expr2`, the +/// assignment `e1 = e2;` can be represented as `code_assignt(expr1, expr2)`. class code_assignt:public codet { public: @@ -249,8 +262,10 @@ inline code_assignt &to_code_assign(codet &code) return static_cast(code); } -/*! \brief A declaration of a local variable -*/ +/// A `codet` representing the declaration of a local variable. +/// For example, if a variable (symbol) `x` is represented as a +/// \ref symbol_exprt `sym`, then the declaration of this variable can be +/// represented as `code_declt(sym)`. class code_declt:public codet { public: @@ -302,8 +317,8 @@ inline code_declt &to_code_decl(codet &code) return static_cast(code); } -/*! \brief A removal of a local variable -*/ +/// A \ref codet representing the removal of a local variable going out of +/// scope. class code_deadt:public codet { public: @@ -461,8 +476,7 @@ inline code_assertt &to_code_assert(codet &code) code_blockt create_fatal_assertion( const exprt &condition, const source_locationt &source_location); -/*! \brief An if-then-else -*/ +/// \ref codet representation of an if-then-else statement. class code_ifthenelset:public codet { public: @@ -533,8 +547,7 @@ inline code_ifthenelset &to_code_ifthenelse(codet &code) return static_cast(code); } -/*! \brief A `switch' instruction -*/ +/// \ref codet representing a `switch` statement. class code_switcht:public codet { public: @@ -596,8 +609,7 @@ inline code_switcht &to_code_switch(codet &code) return static_cast(code); } -/*! \brief A `while' instruction -*/ +/// \ref codet representing a `while` statement. class code_whilet:public codet { public: @@ -659,8 +671,7 @@ inline code_whilet &to_code_while(codet &code) return static_cast(code); } -/*! \brief A `do while' instruction -*/ +/// \ref codet representation of a `do while` statement. class code_dowhilet:public codet { public: @@ -722,8 +733,7 @@ inline code_dowhilet &to_code_dowhile(codet &code) return static_cast(code); } -/*! \brief A `for' instruction -*/ +/// \ref codet representation of a `for` statement. class code_fort:public codet { public: @@ -798,8 +808,7 @@ inline code_fort &to_code_for(codet &code) return static_cast(code); } -/*! \brief A `goto' instruction -*/ +/// \ref codet representation of a `goto` statement. class code_gotot:public codet { public: @@ -848,13 +857,11 @@ inline code_gotot &to_code_goto(codet &code) return static_cast(code); } -/*! \brief A function call - - The function call instruction has three operands. - The first is the expression that is used to store - the return value. The second is the function called. - The third is a vector of argument values. -*/ +/// \ref codet representation of a function call statement. +/// The function call statement has three operands. +/// The first is the expression that is used to store the return value. +/// The second is the function called. +/// The third is a vector of argument values. class code_function_callt:public codet { public: @@ -918,8 +925,7 @@ inline code_function_callt &to_code_function_call(codet &code) return static_cast(code); } -/*! \brief Return from a function -*/ +/// \ref codet representation of a "return from a function" statement. class code_returnt:public codet { public: @@ -972,8 +978,7 @@ inline code_returnt &to_code_return(codet &code) return static_cast(code); } -/*! \brief A label for branch targets -*/ +/// \ref codet representation of a label for branch targets. class code_labelt:public codet { public: @@ -1040,8 +1045,8 @@ inline code_labelt &to_code_label(codet &code) return static_cast(code); } -/*! \brief A switch-case -*/ +/// \ref codet representation of a switch-case, i.e.\ a `case` statement within +/// a `switch`. class code_switch_caset:public codet { public: @@ -1110,8 +1115,8 @@ inline code_switch_caset &to_code_switch_case(codet &code) return static_cast(code); } -/*! \brief A break for `for' and `while' loops -*/ +/// \ref codet representation of a `break` statement (within a `for` or `while` +/// loop). class code_breakt:public codet { public: @@ -1140,8 +1145,8 @@ inline code_breakt &to_code_break(codet &code) return static_cast(code); } -/*! \brief A continue for `for' and `while' loops -*/ +/// \ref codet representation of a `continue` statement (within a `for` or +/// `while` loop). class code_continuet:public codet { public: @@ -1170,8 +1175,7 @@ inline code_continuet &to_code_continue(codet &code) return static_cast(code); } -/*! \brief An inline assembler statement -*/ +/// \ref codet representation of an inline assembler statement. class code_asmt:public codet { public: @@ -1215,8 +1219,8 @@ inline const code_asmt &to_code_asm(const codet &code) return static_cast(code); } -/*! \brief An expression statement -*/ +/// \ref codet representation of an expression statement. +/// It has one operand, which is the expression it stores. class code_expressiont:public codet { public: @@ -1266,8 +1270,11 @@ inline const code_expressiont &to_code_expression(const codet &code) return static_cast(code); } -/*! \brief An expression containing a side effect -*/ +/// An expression containing a side effect. +/// Note that unlike most classes in this file, `side_effect_exprt` and its +/// subtypes are not subtypes of \ref codet, but they inherit directly from +/// \ref exprt. They do have a `statement` like [codets](\ref codet), but their +/// [id()](\ref irept::id) is `ID_side_effect`, not `ID_code`. class side_effect_exprt:public exprt { public: @@ -1335,8 +1342,7 @@ inline const side_effect_exprt &to_side_effect_expr(const exprt &expr) return static_cast(expr); } -/*! \brief A side effect that returns a non-deterministically chosen value -*/ +/// A \ref side_effect_exprt that returns a non-deterministically chosen value. class side_effect_expr_nondett:public side_effect_exprt { public: @@ -1390,8 +1396,7 @@ inline const side_effect_expr_nondett &to_side_effect_expr_nondet( return static_cast(side_effect_expr_nondet); } -/*! \brief A function call side effect -*/ +/// A \ref side_effect_exprt representation of a function call side effect. class side_effect_expr_function_callt:public side_effect_exprt { public: @@ -1486,8 +1491,8 @@ inline const side_effect_expr_function_callt return static_cast(expr); } -/*! \brief A side effect that throws an exception -*/ +/// A \ref side_effect_exprt representation of a side effect that throws an +/// exception. class side_effect_expr_throwt:public side_effect_exprt { public: @@ -1534,12 +1539,12 @@ inline const side_effect_expr_throwt &to_side_effect_expr_throw( /// exception_tag1 -> label1 /// exception_tag2 -> label2 /// ... -/// When used in a GOTO program instruction, the corresponding -/// opcode must be CATCH, and the instruction's `targets` must +/// When used in a GOTO program statement, the corresponding +/// opcode must be CATCH, and the statement's `targets` must /// be in one-to-one correspondence with the exception tags. /// The labels may be unspecified for the case where -/// there is no corresponding source-language label, in whic -/// case the GOTO instruction targets must be set at the same +/// there is no corresponding source-language label, in which +/// case the GOTO statement targets must be set at the same /// time. class code_push_catcht:public codet { @@ -1702,8 +1707,7 @@ static inline const code_landingpadt &to_code_landingpad(const codet &code) return static_cast(code); } -/*! \brief A try/catch block -*/ +/// \ref codet representation of a try/catch block. class code_try_catcht:public codet { public: