Merge pull request #2801 from antlechner/antonia/doc-13-codet

First part of DOC-13 codet documentation

Author: tautschnig

src/util/README.md

@@ -136,6 +136,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`.

src/util/std_code.cpp

@@ -1,11 +1,13 @@
 /*******************************************************************\
 
-Module:
+Module: Data structures representing statements in a program
 
 Author: Daniel Kroening, [email protected]
 
 \*******************************************************************/
 
+/// \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<code_blockt &>(*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();

src/util/std_code.h

@@ -1,6 +1,6 @@
 /*******************************************************************\
 
-Module:
+Module: Data structures representing statements in a program
 
 Author: Daniel Kroening, [email protected]
 
@@ -16,8 +16,17 @@ Author: Daniel Kroening, [email protected]
 #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<codet &>(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_blockt &>(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<code_skipt>(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_assignt &>(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_declt &>(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_ifthenelset &>(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_switcht &>(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_whilet &>(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_dowhilet &>(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_fort &>(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_gotot &>(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_function_callt &>(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_returnt &>(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_labelt &>(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_switch_caset &>(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_breakt &>(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_continuet &>(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<const code_asmt &>(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<const code_expressiont &>(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<const side_effect_exprt &>(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<const side_effect_expr_nondett &>(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<const side_effect_expr_function_callt &>(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<const code_landingpadt &>(code);
 }
 
-/*! \brief A try/catch block
-*/
+/// \ref codet representation of a try/catch block.
 class code_try_catcht:public codet
 {
 public: