Add doxygen to add-failed-symbols

Author: smowton

src/pointer-analysis/add_failed_symbols.cpp

@@ -15,11 +15,19 @@ Author: Daniel Kroening, [email protected]
 #include <util/namespace.h>
 #include <util/std_expr.h>
 
+/// Get the name of the special symbol used to denote an unknown referee pointed
+/// to by a given pointer-typed symbol.
+/// \param id: base symbol id
+/// \return id of the corresponding unknown-object ("failed") symbol.
 irep_idt failed_symbol_id(const irep_idt &id)
 {
   return id2string(id)+"$object";
 }
 
+/// Create a failed-dereference symbol for the given base symbol if it is
+/// pointer-typed; if not, do nothing.
+/// \param symbol: symbol to created a failed symbol for
+/// \param symbol_table: global symbol table
 void add_failed_symbol(symbolt &symbol, symbol_table_baset &symbol_table)
 {
   if(symbol.type.id()==ID_pointer)
@@ -43,6 +51,11 @@ void add_failed_symbol(symbolt &symbol, symbol_table_baset &symbol_table)
   }
 }
 
+/// Create a failed-dereference symbol for the given base symbol if it is
+/// pointer-typed, an lvalue, and doesn't already have one. If any of these
+/// conditions are not met, do nothing.
+/// \param symbol: symbol to created a failed symbol for
+/// \param symbol_table: global symbol table
 void add_failed_symbol_if_needed(
   const symbolt &symbol, symbol_table_baset &symbol_table)
 {
@@ -55,6 +68,9 @@ void add_failed_symbol_if_needed(
   add_failed_symbol(*symbol_table.get_writeable(symbol.name), symbol_table);
 }
 
+/// Create a failed-dereference symbol for all symbols in the given table that
+/// need one (i.e. pointer-typed lvalues).
+/// \param symbol_table: global symbol table
 void add_failed_symbols(symbol_table_baset &symbol_table)
 {
   // the symbol table iterators are not stable, and
@@ -68,6 +84,11 @@ void add_failed_symbols(symbol_table_baset &symbol_table)
     add_failed_symbol_if_needed(*symbol, symbol_table);
 }
 
+/// Get the failed-dereference symbol for the given symbol
+/// \param expr: symbol expression to get a failed symbol for
+/// \param ns: global namespace
+/// \return symbol expression for the failed-dereference symbol, or nil_exprt
+///   if none exists.
 exprt get_failed_symbol(
   const symbol_exprt &expr,
   const namespacet &ns)