replica
/
diffblue-cbmc
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity

Merge pull request #3620 from owen-jones-diffblue/fix_doxygen_param_formatting 

Fix doxygen param formatting
This commit is contained in:
owen-jones-diffblue 2019-01-04 10:08:22 +00:00 committed by GitHub
parent d32ab69a33 375b680440
commit 2ce99a7f71
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
139 changed files with 746 additions and 808 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

14
CODING_STANDARD.md
View File

@ -70,13 +70,17 @@ Formatting is enforced using clang-format. For more information about this, see
/// This sentence, until the first dot followed by whitespace, becomes
/// the brief description. More detailed text follows. Feel free to
/// break this into paragraphs to aid readability.
/// \param arg_name: This parameter doesn't need much description
/// \param [out] long_arg_name: This parameter is mutated by the function.
/// Extra info about the parameter gets indented an extra two columns,
/// \param arg: This parameter doesn't need much description
/// \param long_arg: This parameter needs a long description. Extra
/// information about the parameter gets indented an extra two columns,
/// like this.
/// \param [out] out_arg: This parameter is mutated by the function, and
/// its value at the beginning of the function is not used
/// \param [in,out] in_out_arg: This parameter is mutated by the function, and
/// its value at the beginning of the function is used
/// \return The return value is literally the value returned by the
/// function. For out-parameters, use "\param [out]".
return_typet my_function(argt arg_name, argt &long_arg_name)
/// function. For out-parameters, use "\param [out]" or "\param [in,out]".
ret_typet function(argt arg, argt long_arg, argt &out_arg, argt &in_out_arg)
```
- The priority of documentation is readability. Therefore, feel free to use
Doxygen features, or to add whitespace for multi-paragraph comment blocks if

3
jbmc/src/java_bytecode/character_refine_preprocess.cpp
View File

@ -125,14 +125,13 @@ codet character_refine_preprocesst::convert_compare(conversion_inputt &target)
return code_assignt(result, expr);
}
/// Converts function call to an assignment of an expression corresponding to
/// the java method Character.digit:(CI)I. The function call has one character
/// argument and an optional integer radix argument. If the radix is not given
/// it is set to 36 by default.
/// \param target: a position in a goto program
/// \return code assigning the result of the Character.digit function to the
/// left-hand-side of the given target
/// left-hand-side of the given target
codet character_refine_preprocesst::convert_digit_char(
conversion_inputt &target)
{

2
jbmc/src/java_bytecode/ci_lazy_methods.cpp
View File

@ -498,7 +498,7 @@ void ci_lazy_methodst::get_virtual_method_targets(
/// \param e: expression tree to search
/// \param symbol_table: global symbol table
/// \param [out] needed: Populated with global variable symbols referenced from
/// `e` or its children.
/// `e` or its children.
void ci_lazy_methodst::gather_needed_globals(
const exprt &e,
const symbol_tablet &symbol_table,

21
jbmc/src/java_bytecode/generic_parameter_specialization_map_keys.cpp
View File

@ -4,9 +4,9 @@
#include <iterator>
/// \param type Source type
/// \param type: Source type
/// \return The vector of implicitly generic and (explicitly) generic type
/// parameters of the given type.
/// parameters of the given type.
const std::vector<java_generic_parametert>
get_all_generic_parameters(const typet &type)
{
@ -37,8 +37,8 @@ get_all_generic_parameters(const typet &type)
/// Add pairs to the controlled map. Own the keys and pop from their stack
/// on destruction; otherwise do nothing.
/// \param parameters generic parameters that are the keys of the pairs to add
/// \param types a type to add for each parameter
/// \param parameters: generic parameters that are the keys of the pairs to add
/// \param types: a type to add for each parameter
void generic_parameter_specialization_map_keyst::insert_pairs(
const std::vector<java_generic_parametert> &parameters,
const std::vector<reference_typet> &types)
@ -87,9 +87,9 @@ void generic_parameter_specialization_map_keyst::insert_pairs(
/// Add a pair of a parameter and its types for each generic parameter of the
/// given generic pointer type to the controlled map. Own the keys and pop
/// from their stack on destruction; otherwise do nothing.
/// \param pointer_type pointer type to get the specialized generic types from
/// \param pointer_subtype_struct struct type to which the generic pointer
/// points, must be generic if the pointer is generic
/// \param pointer_type: pointer type to get the specialized generic types from
/// \param pointer_subtype_struct: struct type to which the generic pointer
/// points, must be generic if the pointer is generic
void generic_parameter_specialization_map_keyst::insert_pairs_for_pointer(
const pointer_typet &pointer_type,
const typet &pointer_subtype_struct)
@ -136,9 +136,10 @@ void generic_parameter_specialization_map_keyst::insert_pairs_for_pointer(
/// in the form of a symbol rather than a pointer (as opposed to the function
/// insert_pairs_for_pointer). Own the keys and pop from their stack
/// on destruction; otherwise do nothing.
/// \param struct_tag_type symbol type to get the specialized generic types from
/// \param symbol_struct struct type of the symbol type, must be generic if
/// the symbol is generic
/// \param struct_tag_type: symbol type to get the specialized generic types
/// from
/// \param symbol_struct: struct type of the symbol type, must be generic if
/// the symbol is generic
void generic_parameter_specialization_map_keyst::insert_pairs_for_symbol(
const struct_tag_typet &struct_tag_type,
const typet &symbol_struct)

8
jbmc/src/java_bytecode/jar_file.h
View File

@ -24,13 +24,13 @@ class jar_filet final
{
public:
/// Open java file for reading.
/// \param filename Name of the file
/// \param filename: Name of the file
/// \throw Throws std::runtime_error if file cannot be opened
explicit jar_filet(const std::string &filename);
/// Open a JAR file of size \p size loaded in memory at address \p data.
/// \param data memory buffer with the contents of the jar file
/// \param size size of the memory buffer
/// \param data: memory buffer with the contents of the jar file
/// \param size: size of the memory buffer
/// \throw Throws std::runtime_error if file cannot be opened
jar_filet(const void *data, size_t size);
@ -42,7 +42,7 @@ public:
/// Get contents of a file in the jar archive.
/// Returns nullopt if file doesn't exist.
/// \param filename Name of the file in the archive
/// \param filename: Name of the file in the archive
optionalt<std::string> get_entry(const std::string &filename);
/// Get contents of the Manifest file in the jar archive as a key-value map

12
jbmc/src/java_bytecode/jar_pool.h
View File

@ -19,16 +19,16 @@ class jar_poolt
{
public:
/// Load jar archive or retrieve from cache if already loaded
/// \param jar_path name of the file
/// \param jar_path: name of the file
// Throws an exception if the file does not exist
jar_filet &operator()(const std::string &jar_path);
/// Add a jar archive or retrieve from cache if already added
/// \param buffer_name name of the original file
/// \param pmem memory pointer to the contents of the file
/// \param size size of the memory buffer
/// Add a jar archive or retrieve from cache if already added.
/// Note that this mocks the existence of a file which may
/// or may not exist since the actual data bis retrieved from memory.
/// or may not exist since the actual data is retrieved from memory.
/// \param buffer_name: name of the original file
/// \param pmem: memory pointer to the contents of the file
/// \param size: size of the memory buffer
jar_filet &
add_jar(const std::string &buffer_name, const void *pmem, size_t size);

6
jbmc/src/java_bytecode/java_bytecode_concurrency_instrumentation.cpp
View File

@ -62,7 +62,7 @@ static symbolt add_or_get_symbol(
/// Retrieve the first label identifier. This is used to mark the start of
/// a thread block.
/// /param id: unique thread block identifier
/// /return: fully qualified label identifier
/// /return fully qualified label identifier
static const std::string get_first_label_id(const std::string &id)
{
return CPROVER_PREFIX "_THREAD_ENTRY_" + id;
@ -71,7 +71,7 @@ static const std::string get_first_label_id(const std::string &id)
/// Retrieve the second label identifier. This is used to mark the end of
/// a thread block.
/// /param id: unique thread block identifier
/// /return: fully qualified label identifier
/// /return fully qualified label identifier
static const std::string get_second_label_id(const std::string &id)
{
return CPROVER_PREFIX "_THREAD_EXIT_" + id;
@ -80,7 +80,7 @@ static const std::string get_second_label_id(const std::string &id)
/// Retrieves a thread block identifier from a function call to
/// CProver.startThread:(I)V or CProver.endThread:(I)V
/// /param code: function call to CProver.startThread or CProver.endThread
/// /return: unique thread block identifier
/// /return unique thread block identifier
static const std::string get_thread_block_identifier(
const code_function_callt &f_code)
{

18
jbmc/src/java_bytecode/java_bytecode_convert_class.cpp
View File

@ -176,9 +176,9 @@ private:
/// - class: A<T> extends B<T, Integer> implements C, D<T>
/// - signature: <T:Ljava/lang/Object;>B<TT;Ljava/lang/Integer;>;LC;LD<TT;>;
/// - returned superclass reference: B<TT;Ljava/lang/Integer;>;
/// \param signature Signature of the class
/// \param signature: Signature of the class
/// \return Reference of the generic superclass, or empty if the superclass
/// is not generic
/// is not generic
static optionalt<std::string>
extract_generic_superclass_reference(const optionalt<std::string> &signature)
{
@ -215,10 +215,10 @@ extract_generic_superclass_reference(const optionalt<std::string> &signature)
/// - signature: <T:Ljava/lang/Object;>B<TT;Ljava/lang/Integer;>;LC;LD<TT;>;
/// - returned interface reference for C: LC;
/// - returned interface reference for D: LD<TT;>;
/// \param signature Signature of the class
/// \param interface_name The interface name
/// \param signature: Signature of the class
/// \param interface_name: The interface name
/// \return Reference of the generic interface, or empty if the interface
/// is not generic
/// is not generic
static optionalt<std::string> extract_generic_interface_reference(
const optionalt<std::string> &signature,
const std::string &interface_name)
@ -982,8 +982,8 @@ bool java_bytecode_convert_class(
/// Example: if \p parameter has identifier `java::Outer$Inner::T` and
/// there is a replacement parameter with identifier `java::Outer::T`, the
/// identifier of \p parameter gets set to `java::Outer::T`.
/// \param parameter
/// \param replacement_parameters vector of generic parameters (only viable
/// \param parameter: The given generic type parameter
/// \param replacement_parameters: vector of generic parameters (only viable
/// ones, i.e., only those that can actually appear here such as generic
/// parameters of outer classes of the class specified by the prefix of \p
/// parameter identifier)
@ -1034,8 +1034,6 @@ static void find_and_replace_parameter(
/// Example: class `Outer<T>` has an inner class `Inner` that has a field
/// `t` of type `Generic<T>`. This function ensures that the parameter points to
/// `java::Outer::T` instead of `java::Outer$Inner::T`.
/// \param type
/// \param replacement_parameters
static void find_and_replace_parameters(
typet &type,
const std::vector<java_generic_parametert> &replacement_parameters)
@ -1118,8 +1116,6 @@ void convert_java_annotations(
/// any generic class. All uses of the implicit generic type parameters within
/// the inner class are updated to point to the type parameters of the
/// corresponding outer classes.
/// \param class_name
/// \param symbol_table
void mark_java_implicitly_generic_class_type(
const irep_idt &class_name,
symbol_tablet &symbol_table)

48
jbmc/src/java_bytecode/java_bytecode_convert_method.cpp
View File

@ -76,11 +76,11 @@ protected:
/// Iterates through the parameters of the function type \p ftype, finds a new
/// new name for each parameter and renames them in `ftype.parameters()` as
/// well as in the \p symbol_table.
/// \param[in,out] ftype:
/// \param [in,out] ftype:
/// Function type whose parameters should be named.
/// \param name_prefix:
/// Prefix for parameter names, typically the parent function's name.
/// \param[in,out] symbol_table:
/// \param [in,out] symbol_table:
/// Global symbol table.
/// \return Assigns parameter names (side-effects on `ftype`) to function stub
/// parameters, which are initially nameless as method conversion hasn't
@ -191,18 +191,14 @@ symbol_exprt java_bytecode_convert_methodt::tmp_variable(
/// Returns an expression indicating a local variable suitable to load/store
/// from a bytecode at address `address` a value of type `type_char` stored in
/// the JVM's slot `arg`.
///
/// \param arg
/// The local variable slot
/// \param type_char
/// The type of the value stored in the slot pointed by `arg`.
/// \param address
/// Bytecode address used to find a variable that the LVT declares to be live
/// and living in the slot pointed by `arg` for this bytecode.
/// \param do_cast
/// Indicates whether we should return the original symbol_exprt or a
/// typecast_exprt if the type of the symbol_exprt does not equal that
/// represented by `type_char`.
/// \param arg: The local variable slot
/// \param type_char: The type of the value stored in the slot pointed by `arg`
/// \param address: Bytecode address used to find a variable that the LVT
/// declares to be live and living in the slot pointed by `arg` for this
/// bytecode
/// \param do_cast: Indicates whether we should return the original symbol_exprt
/// or a typecast_exprt if the type of the symbol_exprt does not equal that
/// represented by `type_char`
/// \return symbol_exprt or type-cast symbol_exprt
exprt java_bytecode_convert_methodt::variable(
const exprt &arg,
@ -239,18 +235,12 @@ exprt java_bytecode_convert_methodt::variable(
}
/// Returns the member type for a method, based on signature or descriptor
/// \param descriptor
/// descriptor of the method
/// \param signature
/// signature of the method
/// \param class_name
/// string containing the name of the corresponding class
/// \param method_name
/// string containing the name of the method
/// \param message_handler
/// message handler to collect warnings
/// \return
/// the constructed member type
/// \param descriptor: descriptor of the method
/// \param signature: signature of the method
/// \param class_name: string containing the name of the corresponding class
/// \param method_name: string containing the name of the method
/// \param message_handler: message handler to collect warnings
/// \return the constructed member type
java_method_typet member_type_lazy(
const std::string &descriptor,
const optionalt<std::string> &signature,
@ -308,9 +298,9 @@ java_method_typet member_type_lazy(
/// Retrieves the symbol of the lambda method associated with the given
/// lambda method handle (bootstrap method).
/// \param lambda_method_handles Vector of lambda method handles (bootstrap
/// \param lambda_method_handles: Vector of lambda method handles (bootstrap
/// methods) of the class where the lambda is called
/// \param index Index of the lambda method handle in the vector
/// \param index: Index of the lambda method handle in the vector
/// \return Symbol of the lambda method if the method handle has a known type
optionalt<symbolt> java_bytecode_convert_methodt::get_lambda_method_symbol(
const java_class_typet::java_lambda_method_handlest &lambda_method_handles,
@ -3142,7 +3132,7 @@ irep_idt java_bytecode_convert_methodt::get_static_field(
/// Create temporary variables if a write instruction can have undesired side-
/// effects.
/// \param tmp_var_prefix: The prefix string to use for new temporary variables
/// \param[out] block: The code block the assignment is added to if required.
/// \param [out] block: The code block the assignment is added to if required.
/// \param write_type: The enumeration type of the write instruction.
/// \param identifier: The identifier of the symbol in the write instruction.
void java_bytecode_convert_methodt::save_stack_entries(

30
jbmc/src/java_bytecode/java_bytecode_instrument.cpp
View File

@ -87,11 +87,11 @@ const std::vector<std::string> exception_needed_classes = {
/// conditional GOTO such that exc_name is thrown when
/// cond is met.
/// \param cond: condition to be met in order
/// to throw an exception
/// to throw an exception
/// \param original_loc: source location in the original program
/// \param exc_name: the name of the exception to be thrown
/// \return Returns the code initialising the throwing the
/// exception
/// exception
code_ifthenelset java_bytecode_instrumentt::throw_exception(
const exprt &cond,
const source_locationt &original_loc,
@ -135,14 +135,13 @@ code_ifthenelset java_bytecode_instrumentt::throw_exception(
return if_code;
}
/// Checks whether there is a division by zero
/// and throws ArithmeticException if necessary.
/// Exceptions are thrown when the `throw_runtime_exceptions`
/// flag is set.
/// \return Based on the value of the flag `throw_runtime_exceptions`,
/// it returns code that either throws an ArithmeticException
/// or asserts a nonzero denominator.
/// it returns code that either throws an ArithmeticException
/// or asserts a nonzero denominator.
codet java_bytecode_instrumentt::check_arithmetic_exception(
const exprt &denominator,
const source_locationt &original_loc)
@ -172,8 +171,8 @@ codet java_bytecode_instrumentt::check_arithmetic_exception(
/// \param idx: index into the array
/// \param original_loc: source location in the original code
/// \return Based on the value of the flag `throw_runtime_exceptions`,
/// it returns code that either throws an ArrayIndexOutPfBoundsException
/// or emits an assertion checking the array access
/// it returns code that either throws an ArrayIndexOutPfBoundsException
/// or emits an assertion checking the array access
codet java_bytecode_instrumentt::check_array_access(
const exprt &array_struct,
const exprt &idx,
@ -215,8 +214,8 @@ codet java_bytecode_instrumentt::check_array_access(
/// \param class2: the super class
/// \param original_loc: source location in the original code
/// \return Based on the value of the flag `throw_runtime_exceptions`,
/// it returns code that either throws an ClassCastException or emits an
/// assertion checking the subtype relation
/// it returns code that either throws an ClassCastException or emits an
/// assertion checking the subtype relation
code_ifthenelset java_bytecode_instrumentt::check_class_cast(
const exprt &class1,
const exprt &class2,
@ -262,8 +261,8 @@ code_ifthenelset java_bytecode_instrumentt::check_class_cast(
/// \param expr: the checked expression
/// \param original_loc: source location in the original code
/// \return Based on the value of the flag `throw_runtime_exceptions`,
/// it returns code that either throws an NullPointerException or emits an
/// assertion checking the subtype relation
/// it returns code that either throws an NullPointerException or emits an
/// assertion checking the subtype relation
codet java_bytecode_instrumentt::check_null_dereference(
const exprt &expr,
const source_locationt &original_loc)
@ -291,8 +290,8 @@ codet java_bytecode_instrumentt::check_null_dereference(
/// \param length: the checked length
/// \param original_loc: source location in the original code
/// \return Based on the value of the flag `throw_runtime_exceptions`,
/// it returns code that either throws an NegativeArraySizeException
/// or emits an assertion checking the subtype relation
/// it returns code that either throws an NegativeArraySizeException
/// or emits an assertion checking the subtype relation
codet java_bytecode_instrumentt::check_array_length(
const exprt &length,
const source_locationt &original_loc)
@ -463,9 +462,8 @@ void java_bytecode_instrumentt::instrument_code(codet &code)
/// Computes the instrumentation for \p expr in the form of
/// either assertions or runtime exceptions.
/// \param expr: the expression for which we compute
/// instrumentation
/// \return: The instrumentation for \p expr if required
/// \param expr: the expression for which we compute instrumentation
/// \return The instrumentation for \p expr if required
optionalt<codet> java_bytecode_instrumentt::instrument_expr(const exprt &expr)
{
code_blockt result;

4
jbmc/src/java_bytecode/java_bytecode_language.cpp
View File

@ -43,8 +43,8 @@ Author: Daniel Kroening, kroening@kroening.com
#include "load_method_by_regex.h"
/// Parse options that are java bytecode specific.
/// \param cmd Command line
/// \param [out] options The options object that will be updated.
/// \param cmd: Command line
/// \param [out] options: The options object that will be updated.
void parse_java_language_options(const cmdlinet &cmd, optionst &options)
{
options.set_option(

2
jbmc/src/java_bytecode/java_bytecode_parse_tree.cpp
View File

@ -92,7 +92,7 @@ void java_bytecode_parse_treet::annotationt::element_value_pairt::output(
/// \param annotation_type_name: An irep_idt representing the name of the
/// annotation class, e.g. java::java.lang.SuppressWarnings
/// \return The first annotation with the given name in annotations if one
/// exists, an empty optionalt otherwise.
/// exists, an empty optionalt otherwise.
optionalt<java_bytecode_parse_treet::annotationt>
java_bytecode_parse_treet::find_annotation(
const annotationst &annotations,

8
jbmc/src/java_bytecode/java_bytecode_parser.cpp
View File

@ -1580,7 +1580,7 @@ void java_bytecode_parsert::relement_value_pairs(
/// Corresponds to the element_value structure
/// Described in Java 8 specification 4.7.16.1
/// https://docs.oracle.com/javase/specs/jvms/se8/html/jvms-4.html#jvms-4.7.16.1
/// \returns An exprt that represents the particular value of annotations field.
/// \return An exprt that represents the particular value of annotations field.
/// This is usually one of: a byte, number of some sort, string, character,
/// enum, Class type, array or another annotation.
exprt java_bytecode_parsert::get_relement_value()
@ -1949,8 +1949,8 @@ void java_bytecode_parsert::parse_local_variable_type_table(methodt &method)
/// Read method handle pointed to from constant pool entry at index, return type
/// of method handle and name if lambda function is found.
/// \param entry: the constant pool entry of the methodhandle_info structure
/// \returns: the method_handle type of the methodhandle_structure,
/// either for a recognized bootstrap method or for a lambda function
/// \return the method_handle type of the methodhandle_structure,
/// either for a recognized bootstrap method or for a lambda function
optionalt<java_bytecode_parsert::lambda_method_handlet>
java_bytecode_parsert::parse_method_handle(const method_handle_infot &entry)
{
@ -1994,7 +1994,7 @@ java_bytecode_parsert::parse_method_handle(const method_handle_infot &entry)
/// Read all entries of the `BootstrapMethods` attribute of a class file.
/// \param parsed_class: the class representation of the class file that is
/// currently parsed
/// currently parsed
void java_bytecode_parsert::read_bootstrapmethods_entry(classt &parsed_class)
{
u2 num_bootstrap_methods = read_u2();

2
jbmc/src/java_bytecode/java_class_loader.cpp
View File

@ -103,7 +103,7 @@ static bool is_overlay_class(const java_bytecode_parse_treet::classt &c)
/// to find the .class file.
/// \param class_loader_limit: Filter to decide whether to load classes
/// \param class_name: Name of class to load
/// \returns The list of valid implementations, including overlays
/// \return The list of valid implementations, including overlays
/// \remarks
/// Allows multiple definitions of the same class to appear on the
/// classpath, so long as all but the first definition are marked with the

4
jbmc/src/java_bytecode/java_entry_point.cpp
View File

@ -606,7 +606,7 @@ main_function_resultt get_main_symbol(
/// (deterministically) set to null. This is a source of underapproximation in
/// our approach to test generation, and should perhaps be fixed in the future.
///
/// \returns true if error occurred on entry point search
/// \return true if error occurred on entry point search
bool java_entry_point(
symbol_table_baset &symbol_table,
const irep_idt &main_class,
@ -662,7 +662,7 @@ bool java_entry_point(
/// \param assert_uncaught_exceptions: Add an uncaught-exception check
/// \param object_factory_parameters: Parameters for creation of arguments
/// \param pointer_type_selector: Logic for substituting types of pointers
/// \returns true if error occurred on entry point search, false otherwise
/// \return true if error occurred on entry point search, false otherwise
bool generate_java_start_function(
const symbolt &symbol,
symbol_table_baset &symbol_table,

2
jbmc/src/java_bytecode/java_local_variable_table.cpp
View File

@ -270,7 +270,7 @@ static void populate_variable_address_map(
/// range of local variable table entries to consider
/// \param live_variable_at_address:
/// map from bytecode address to table entry (drawn from firstvar-varlimit)
// live at that address
/// live at that address
/// \param amap:
/// map from bytecode address to instructions, this is the CFG of the java
/// method

74
jbmc/src/java_bytecode/java_object_factory.cpp
View File

@ -218,7 +218,7 @@ code_assignt java_object_factoryt::get_null_assignment(
/// \endcode
/// It is illegal to call the function with MAY_UPDATE_IN_PLACE.
///
/// \param[out] assignments:
/// \param [out] assignments:
/// A code_blockt where the initialization code will be emitted to.
/// \param expr:
/// Pointer-typed lvalue expression to initialize.
@ -368,7 +368,7 @@ static mp_integer max_value(const typet &type)
///
/// If the structure is not a nondeterministic structure, the call results in
/// a precondition violation.
/// \param struct_expr [out]: struct that we initialize
/// \param [out] struct_expr: struct that we initialize
/// \param code: block to add pre-requisite declarations (e.g. to allocate a
/// data array)
/// \param min_nondet_string_length: minimum length of strings to initialize
@ -731,21 +731,16 @@ void java_object_factoryt::gen_nondet_pointer_init(
/// // assign `expr` with a suitably casted pointer to new_object
/// A * p = &tmp_object
///
/// \param assignments
/// A block of code where we append the generated code.
/// \param lifetime:
/// Lifetime of the allocated objects (AUTOMATIC_LOCAL, STATIC_GLOBAL, or
/// DYNAMIC)
/// \param replacement_pointer
/// The type of the pointer we actually want to to create.
/// \param depth:
/// Number of times that a pointer has been dereferenced from the root of the
/// object tree that we are initializing.
/// \param location:
/// Source location associated with nondet-initialization.
/// \return
/// A symbol expression of type \p replacement_pointer corresponding to a
/// pointer to object `tmp_object` (see above).
/// \param assignments: A block of code where we append the generated code
/// \param lifetime: Lifetime of the allocated objects (AUTOMATIC_LOCAL,
/// STATIC_GLOBAL, or DYNAMIC)
/// \param replacement_pointer: The type of the pointer we actually want to
/// create
/// \param depth: Number of times that a pointer has been dereferenced from the
/// root of the object tree that we are initializing
/// \param location: Source location associated with nondet-initialization
/// \return A symbol expression of type \p replacement_pointer corresponding to
/// a pointer to object `tmp_object` (see above)
symbol_exprt java_object_factoryt::gen_nondet_subtype_pointer_init(
code_blockt &assignments,
lifetimet lifetime,
@ -811,32 +806,23 @@ alternate_casest get_string_input_values_code(
/// After initialization calls validation method
/// `expr.cproverNondetInitialize()` if it was provided by the user.
///
/// \param assignments:
/// The code block to append the new instructions to.
/// \param expr
/// Struct-typed lvalue expression to initialize.
/// \param is_sub:
/// If true, `expr` is a substructure of a larger object, which in Java
/// necessarily means a base class.
/// \param class_identifier:
/// Name of the parent class. Used to initialize the `@class_identifier` among
/// others.
/// \param skip_classid:
/// If true, skip initializing `@class_identifier`.
/// \param lifetime:
/// Lifetime of the allocated objects (AUTOMATIC_LOCAL, STATIC_GLOBAL, or
/// DYNAMIC)
/// \param struct_type:
/// The type of the struct we are initalizing.
/// \param depth:
/// Number of times that a pointer has been dereferenced from the root of the
/// object tree that we are initializing.
/// \param update_in_place:
/// \param assignments: The code block to append the new instructions to
/// \param expr: Struct-typed lvalue expression to initialize
/// \param is_sub: If true, `expr` is a substructure of a larger object, which
/// in Java necessarily means a base class
/// \param class_identifier: Name of the parent class. Used to initialize the
/// `@class_identifier` among others
/// \param skip_classid: If true, skip initializing `@class_identifier`
/// \param lifetime: Lifetime of the allocated objects (AUTOMATIC_LOCAL,
/// STATIC_GLOBAL, or DYNAMIC)
/// \param struct_type: The type of the struct we are initializing
/// \param depth: Number of times that a pointer has been dereferenced from the
/// root of the object tree that we are initializing
/// \param update_in_place: Enum instance with the following meaning.
/// NO_UPDATE_IN_PLACE: initialize `expr` from scratch
/// MUST_UPDATE_IN_PLACE: reinitialize an existing object
/// MAY_UPDATE_IN_PLACE: invalid input
/// \param location:
/// Source location associated with nondet-initialization.
/// \param location: Source location associated with nondet-initialization
void java_object_factoryt::gen_nondet_struct_init(
code_blockt &assignments,
const exprt &expr,
@ -1181,7 +1167,7 @@ const symbol_exprt java_object_factoryt::gen_nondet_int_init(
/// Allocates a fresh array and emits an assignment writing to \p lhs the
/// address of the new array. Single-use at the moment, but useful to keep as a
/// separate function for downstream branches.
/// \param[out] assignments:
/// \param [out] assignments:
/// Code is emitted here.
/// \param lhs:
/// Symbol to assign the new array structure.
@ -1528,8 +1514,8 @@ void java_object_factoryt::gen_nondet_enum_init(
/// The only new one is \p type, which is the type of the object to create.
///
/// \return The object created, the \p symbol_table gains any new symbols
/// created, and \p init_code gains any instructions requried to initialize
/// either the returned value or its child objects
/// created, and \p init_code gains any instructions required to initialize
/// either the returned value or its child objects
exprt object_factory(
const typet &type,
const irep_idt base_name,
@ -1591,7 +1577,7 @@ exprt object_factory(
///
/// \param expr:
/// Lvalue expression to initialize.
/// \param[out] init_code:
/// \param [out] init_code:
/// A code block where the initializing assignments will be appended to.
/// It gets an instruction sequence to initialize or reinitialize `expr` and
/// child objects it refers to.

4
jbmc/src/java_bytecode/java_object_factory_parameters.h
View File

@ -24,8 +24,8 @@ struct java_object_factory_parameterst final : public object_factory_parameterst
};
/// Parse the java object factory parameters from a given command line
/// \param cmdline Command line
/// \param [out] options The options object that will be updated
/// \param cmdline: Command line
/// \param [out] options: The options object that will be updated
void parse_java_object_factory_options(
const cmdlinet &cmdline,
optionst &options);

4
jbmc/src/java_bytecode/java_root_class.cpp
View File

@ -36,10 +36,10 @@ void java_root_class(symbolt &class_symbol)
}
/// Adds members for an object of the root class (usually java.lang.Object).
/// \param jlo [out] : object to initialize
/// \param [out] jlo: object to initialize
/// \param root_type: type of the root class
/// \param class_identifier: class identifier field, generally begins with
/// "java::" prefix.
/// "java::" prefix.
void java_root_class_init(
struct_exprt &jlo,
const struct_typet &root_type,

3
jbmc/src/java_bytecode/java_static_initializers.cpp
View File

@ -693,14 +693,13 @@ code_ifthenelset get_clinit_wrapper_body(
return code_ifthenelset(std::move(check_already_run), std::move(init_body));
}
/// Create static initializer wrappers for all classes that need them.
/// \param symbol_table: global symbol table
/// \param synthetic_methods: synthetic methods map. Will be extended noting
/// that any wrapper belongs to this code, and so `get_clinit_wrapper_body`
/// should be used to produce the method body when required.
/// \param thread_safe: if true state variables required to make the
/// clinit_wrapper thread safe will be created.
/// clinit_wrapper thread safe will be created.
void create_static_initializer_wrappers(
symbol_tablet &symbol_table,
synthetic_methods_mapt &synthetic_methods,

37
jbmc/src/java_bytecode/java_string_library_preprocess.cpp
View File

@ -33,7 +33,7 @@ Date: April 2017
#include "java_root_class.h"
/// \return tag of a struct prefixed by "java::" or symbolic tag
/// empty string if not symbol or struct
/// empty string if not symbol or struct
static irep_idt get_tag(const typet &type)
{
/// \todo Use follow instead of assuming tag to symbol relationship.
@ -286,7 +286,7 @@ exprt::operandst java_string_library_preprocesst::process_parameters(
/// Creates a string_exprt from the input exprt representing a char sequence
/// \param expr_to_process: an expression of a type which implements char
/// sequence
/// sequence
/// \param loc: location in the source
/// \param symbol_table: symbol table
/// \param init_code: code block, in which declaration will be added:
@ -297,7 +297,7 @@ exprt::operandst java_string_library_preprocesst::process_parameters(
/// cprover_string_content = a->data;
/// ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
/// \return the processed operand:
/// {content=cprover_string_content, length=cprover_string_length}
/// {content=cprover_string_content, length=cprover_string_length}
refined_string_exprt
java_string_library_preprocesst::convert_exprt_to_string_exprt(
const exprt &expr_to_process,
@ -495,7 +495,7 @@ symbol_exprt java_string_library_preprocesst::fresh_string(
/// fresh symbols.
/// \param loc: source location
/// \param symbol_table: the symbol table
/// \param code [out] : code block to which the declaration is added
/// \param [out] code: code block to which the declaration is added
/// \return refined string expr with fresh content and length symbols
refined_string_exprt java_string_library_preprocesst::decl_string_expr(
const source_locationt &loc,
@ -631,7 +631,7 @@ codet java_string_library_preprocesst::code_return_function_application(
/// \param symbol_table: the symbol table
/// \param loc: source location
/// \param function_id: name of the function containing the array
/// \param code [out] : code block where the declaration gets added
/// \param [out] code: code block where the declaration gets added
/// \return created symbol expression
exprt make_nondet_infinite_char_array(
symbol_table_baset &symbol_table,
@ -664,7 +664,7 @@ exprt make_nondet_infinite_char_array(
/// \param array: a character array expression
/// \param symbol_table: the symbol table
/// \param loc: source location
/// \param code [out] : code block to which declaration and calls get added
/// \param [out] code: code block to which declaration and calls get added
void add_pointer_to_array_association(
const exprt &pointer,
const exprt &array,
@ -698,7 +698,7 @@ void add_pointer_to_array_association(
/// \param length: integer expression
/// \param symbol_table: the symbol table
/// \param loc: source location
/// \param code [out] : code block to which declaration and calls get added
/// \param [out] code: code block to which declaration and calls get added
void add_array_to_length_association(
const exprt &array,
const exprt &length,
@ -729,11 +729,11 @@ void add_array_to_length_association(
/// \param pointer: a character pointer expression
/// \param length: length of the character sequence pointed by `pointer`
/// \param char_set: character set given by a range expression consisting of
/// two characters separated by an hyphen.
/// For instance "a-z" denotes all lower case ascii letters.
/// two characters separated by an hyphen. For instance "a-z" denotes all
/// lower case ascii letters.
/// \param symbol_table: the symbol table
/// \param loc: source location
/// \param code [out] : code block to which declaration and calls get added
/// \param [out] code: code block to which declaration and calls get added
void add_character_set_constraint(
const exprt &pointer,
const exprt &length,
@ -1179,14 +1179,14 @@ code_blockt java_string_library_preprocesst::make_assign_function_from_call(
/// Used to access the values of the arguments of `String.format`.
/// \param object: an expression representing a reference to an object
/// \param type_name: name of the corresponding primitive type, this can be
/// one of the following: ID_boolean, ID_char, ID_byte, ID_short, ID_int,
/// ID_long, ID_float, ID_double, ID_void
/// one of the following: ID_boolean, ID_char, ID_byte, ID_short, ID_int,
/// ID_long, ID_float, ID_double, ID_void
/// \param loc: a location in the source
/// \param symbol_table: the symbol table
/// \param code: code block to which we are adding some assignments
/// \return An expression contaning a symbol `tmp_type_name` where `type_name`
/// is the given argument (ie. boolean, char etc.). Which represents the
/// primitive value contained in the given object.
/// \return An expression containing a symbol `tmp_type_name` where `type_name`
/// is the given argument (ie. boolean, char etc.). Which represents the
/// primitive value contained in the given object.
optionalt<symbol_exprt>
java_string_library_preprocesst::get_primitive_value_of_object(
const exprt &object,
@ -1439,10 +1439,9 @@ struct_exprt java_string_library_preprocesst::make_argument_for_format(
/// \param loc: location in the program_invocation_name
/// \param function_id: function the generated code will be used in
/// \param symbol_table: symbol table
/// \return Code implementing the Java String.format function.
/// Since the exact class of the arguments is not known, we give as
/// argument to the internal format function a structure containing
/// the different possible types.
/// \return Code implementing the Java String.format function. Since the exact
/// class of the arguments is not known, we give as argument to the internal
// format function a structure containing the different possible types.
code_blockt java_string_library_preprocesst::make_string_format_code(
const java_method_typet &type,
const source_locationt &loc,

36
jbmc/src/java_bytecode/java_types.cpp
View File

@ -90,7 +90,7 @@ reference_typet java_lang_object_type()
/// Construct an array pointer type. It is a pointer to a symbol with identifier
/// java::array[]. Its ID_element_type is set to the corresponding primitive
/// type, or void* for arrays of references.
/// \param subtype Character indicating the type of array
/// \param subtype: Character indicating the type of array
reference_typet java_array_type(const char subtype)
{
std::string subtype_str;
@ -125,7 +125,7 @@ reference_typet java_array_type(const char subtype)
}
/// Return a const reference to the element type of a given java array type
/// \param array_symbol The java array type
/// \param array_symbol: The java array type
const typet &java_array_element_type(const struct_tag_typet &array_symbol)
{
DATA_INVARIANT(
@ -135,7 +135,7 @@ const typet &java_array_element_type(const struct_tag_typet &array_symbol)
}
/// Return a non-const reference to the element type of a given java array type
/// \param array_symbol The java array type
/// \param array_symbol: The java array type
typet &java_array_element_type(struct_tag_typet &array_symbol)
{
DATA_INVARIANT(
@ -158,8 +158,8 @@ bool is_java_array_type(const typet &type)
}
/// Checks whether the given type is a multi-dimensional array pointer type,
// i.e., a pointer to an array type with element type also being a pointer to an
/// array type.
/// i.e., a pointer to an array type with element type also being a pointer to
/// an array type.
bool is_multidim_java_array_type(const typet &type)
{
return is_java_array_type(type) && is_java_array_type(java_array_element_type(
@ -167,9 +167,9 @@ bool is_multidim_java_array_type(const typet &type)
}
/// See above
/// \param tag Tag of a struct
/// \param tag: Tag of a struct
/// \return True if the given string is a Java array tag, i.e., has a prefix
/// of java::array[
/// of java::array[
bool is_java_array_tag(const irep_idt& tag)
{
return has_prefix(id2string(tag), "java::array[");
@ -227,7 +227,7 @@ exprt java_bytecode_promotion(const exprt &expr)
}
/// Take a list of generic type arguments and parse them into the generic type.
/// \param generic_type [out]: The existing generic type to add the information
/// \param [out] generic_type: The existing generic type to add the information
/// to
/// \param type_arguments: The string representing the generic type arguments
/// for a signature. For example `<TT;Ljava/lang/Foo;LList<LInteger;>;>`
@ -449,8 +449,8 @@ build_class_name(const std::string &src, const std::string &class_name_prefix)
/// \param starting_point: The string position where the opening 'L' we want to
/// find the closing ';' for.
/// \return The string position corresponding to the matching ';'. For example:
/// LA;, we would return 2. For LA<TT;>; we would return 7.
/// See unit/java_bytecode/java_util_tests.cpp for more examples.
/// LA;, we would return 2. For LA<TT;>; we would return 7.
/// See unit/java_bytecode/java_util_tests.cpp for more examples.
size_t find_closing_semi_colon_for_reference_type(
const std::string src,
size_t starting_point)
@ -488,7 +488,7 @@ size_t find_closing_semi_colon_for_reference_type(
/// \param src: the string representation as used in the class file
/// \param class_name_prefix: name of class to append to generic type
/// variables/parameters
/// \returns internal type representation for GOTO programs
/// \return internal type representation for GOTO programs
typet java_type_from_string(
const std::string &src,
const std::string &class_name_prefix)
@ -671,7 +671,7 @@ char java_char_from_type(const typet &type)
///
/// For example for `HashMap<K, V>` a vector with two elements would be returned
///
/// \returns vector of java types representing the generic type variables
/// \return vector of java types representing the generic type variables
std::vector<typet> java_generic_type_from_string(
const std::string &class_name,
const std::string &src)
@ -792,10 +792,10 @@ bool is_valid_java_array(const struct_typet &type)
/// Compares the types, including checking element types if both types are
/// arrays.
/// \param type1 First type to compare
/// \param type2 Second type to compare
/// \param type1: First type to compare
/// \param type2: Second type to compare
/// \return True if the types are equal, including elemnt types if they are
/// both arrays
/// both arrays
bool equal_java_types(const typet &type1, const typet &type2)
{
bool arrays_with_same_element_type = true;
@ -868,7 +868,7 @@ void get_dependencies_from_generic_parameters_rec(
/// must be loaded but only appear as generic type argument, not as a field
/// reference.
/// \param signature: the string representation of the signature to analyze
/// \param refs [out]: the set to insert the names of the found dependencies
/// \param [out] refs: the set to insert the names of the found dependencies
void get_dependencies_from_generic_parameters(
const std::string &signature,
std::set<irep_idt> &refs)
@ -904,7 +904,7 @@ void get_dependencies_from_generic_parameters(
/// used to get information about class dependencies that must be loaded but
/// only appear as generic type argument, not as a field reference.
/// \param t: the type to analyze
/// \param refs [out]: the set to insert the names of the found dependencies
/// \param [out] refs: the set to insert the names of the found dependencies
void get_dependencies_from_generic_parameters(
const typet &t,
std::set<irep_idt> &refs)
@ -946,7 +946,7 @@ java_generic_struct_tag_typet::java_generic_struct_tag_typet(
/// Check if this symbol has the given generic type. If yes, return its index
/// in the vector of generic types.
/// \param type The parameter type we are looking for.
/// \param type: The parameter type we are looking for.
/// \return The index of the type in the vector of generic types.
optionalt<size_t> java_generic_struct_tag_typet::generic_type_index(
const java_generic_parametert &type) const

14
jbmc/src/java_bytecode/java_utils.cpp
View File

@ -188,10 +188,10 @@ dereference_exprt checked_dereference(const exprt &expr, const typet &type)
///
/// \param src: the source string to scan
/// \param open_pos: the initial position of the opening delimiter from where to
/// start the search
/// start the search
/// \param open_char: the opening delimiter
/// \param close_char: the closing delimiter
/// \returns the index of the matching corresponding closing delimiter in \p src
/// \return the index of the matching corresponding closing delimiter in \p src
size_t find_closing_delimiter(
const std::string &src,
size_t open_pos,
@ -229,8 +229,8 @@ size_t find_closing_delimiter(
/// Add the components in components_to_add to the class denoted by
/// class symbol.
/// \param class_symbol The symbol representing the class we want to modify.
/// \param components_to_add The vector with the components we want to add.
/// \param class_symbol: The symbol representing the class we want to modify.
/// \param components_to_add: The vector with the components we want to add.
void java_add_components_to_class(
symbolt &class_symbol,
const struct_union_typet::componentst &components_to_add)
@ -271,7 +271,7 @@ void declare_function(
/// \param type: return type of the function
/// \param symbol_table: a symbol table
/// \return a function application expression representing:
/// `function_name(arguments)`
/// `function_name(arguments)`
exprt make_function_application(
const irep_idt &function_name,
const exprt::operandst &arguments,
@ -302,9 +302,9 @@ irep_idt strip_java_namespace_prefix(const irep_idt &to_strip)
/// Strip the package name from a java type, for the type to be
/// pretty printed (java::java.lang.Integer -> Integer).
/// \param fqn_java_type The java type we want to pretty print.
/// \param fqn_java_type: The java type we want to pretty print.
/// \return The pretty printed type if there was a match of the
// qualifiers, or the type as it was passed otherwise.
/// qualifiers, or the type as it was passed otherwise.
std::string pretty_print_java_type(const std::string &fqn_java_type)
{
std::string result(fqn_java_type);

4
jbmc/src/java_bytecode/java_utils.h
View File

@ -75,8 +75,8 @@ dereference_exprt checked_dereference(const exprt &expr, const typet &type);
/// Add the components in components_to_add to the class denoted
/// by class symbol.
/// \param class_symbol The symbol representing the class we want to modify.
/// \param components_to_add The vector with the components we want to add.
/// \param class_symbol: The symbol representing the class we want to modify.
/// \param components_to_add: The vector with the components we want to add.
void java_add_components_to_class(
symbolt &class_symbol,
const struct_union_typet::componentst &components_to_add);

2
jbmc/src/java_bytecode/load_method_by_regex.cpp
View File

@ -34,7 +34,7 @@ static std::regex build_regex_from_pattern(const std::string &pattern)
/// is, does it have a colon separtor.
/// \param pattern: The user provided pattern
/// \return True if no descriptor is found (that is, the only : relates to the
/// java:: prefix.
/// java:: prefix.
bool does_pattern_miss_descriptor(const std::string &pattern)
{
const size_t descriptor_index = pattern.rfind(':');

10
jbmc/src/java_bytecode/mz_zip_archive.h
View File

@ -21,13 +21,13 @@ class mz_zip_archivet final
{
public:
/// Open a zip archive
/// \param filename Path of the zip archive
/// \param filename: Path of the zip archive
/// \throw Throws std::runtime_error if file cannot be opened
explicit mz_zip_archivet(const std::string &filename);
/// Loads a zip buffer
/// \param data pointer to the memory buffer
/// \param size size of the buffer
/// \param data: pointer to the memory buffer
/// \param size: size of the buffer
/// \throw Throws std::runtime_error if file cannot be opened
mz_zip_archivet(const void *data, size_t size);
@ -43,11 +43,11 @@ public:
/// Get number of files in the archive
size_t get_num_files();
/// Get file name of nth file in the archive
/// \param index id of the file in the archive
/// \param index: id of the file in the archive
/// \return Name of the file in the archive
std::string get_filename(size_t index);
/// Get contents of nth file in the archive
/// \param index id of the file in the archive
/// \param index: id of the file in the archive
/// \throw Throws std::runtime_error if file cannot be extracted
/// \return Contents of the file in the archive
std::string extract(size_t index);

14
jbmc/src/java_bytecode/remove_exceptions.cpp
View File

@ -260,13 +260,13 @@ void remove_exceptionst::instrument_exception_handler(
/// we note that try1{ try2 {} catch2c {} catch2d {}} catch1a() {} catch1b{}
/// must catch in the following order: 2c 2d 1a 1b hence the numerical index
/// is reversed whereas the letter ordering remains the same.
/// @param stack_catch exception table
/// @param goto_program program being evaluated
/// @param[out] universal_try returns the try block
/// corresponding to the desired exception handler
/// @param[out] universal_catch returns the catch block
/// corresponding to the exception desired exception handler
/// @return the desired exception handler
/// \param stack_catch: exception table
/// \param goto_program: program being evaluated
/// \param [out] universal_try: returns the try block corresponding to the
/// desired exception handler
/// \param [out] universal_catch: returns the catch block corresponding to the
/// exception desired exception handler
/// \return the desired exception handler
goto_programt::targett remove_exceptionst::find_universal_exception(
const remove_exceptionst::stack_catcht &stack_catch,
goto_programt &goto_program,

2
jbmc/src/java_bytecode/remove_instanceof.cpp
View File

@ -296,7 +296,7 @@ void remove_instanceof(
/// \param class_hierarchy: class hierarchy analysis of goto_model's symbol
/// table
/// \param message_handler: logging output
/// symbols to.
/// symbols to.
void remove_instanceof(
goto_modelt &goto_model,
const class_hierarchyt &class_hierarchy,

18
jbmc/src/java_bytecode/select_pointer_type.cpp
View File

@ -118,9 +118,9 @@ pointer_typet select_pointer_typet::specialize_generics(
///
/// Note that the top of the stacks for T and U create a recursion T -> U,
/// U-> T. We want to break it and specialize `T my.gen.t` to `String my.gen.t`.
/// \param parameter_name The name of the generic parameter type we want to have
/// instantiated
/// \param generic_parameter_specialization_map Map of type names to
/// \param parameter_name: The name of the generic parameter type we want to
/// have instantiated
/// \param generic_parameter_specialization_map: Map of type names to
/// specialization stack
/// \return The first instantiated type for the generic type or nothing if no
/// such instantiation exists.
@ -157,12 +157,12 @@ select_pointer_typet::get_recursively_instantiated_type(
/// See get_recursively instantiated_type, the additional parameters just track
/// the recursion to prevent visiting the same depth again and specify which
/// stack depth is analyzed.
/// \param parameter_name The name of the generic parameter type we want to have
/// instantiated
/// \param generic_parameter_specialization_map Map of type names to
/// specialization stack
/// \param visited Tracks the visited parameter names
/// \param depth Stack depth to analyze
/// \param parameter_name: The name of the generic parameter type we want to
/// have instantiated
/// \param generic_parameter_specialization_map: Map of type names to
/// specialization stack
/// \param visited: Tracks the visited parameter names
/// \param depth: Stack depth to analyze
/// \return if this type is not a generic type, it is returned as a valid
/// instantiation, if nothing can be found at the given depth, en empty
/// optional is returned

2
jbmc/unit/java-testing-utils/load_java_class.cpp
View File

@ -83,7 +83,7 @@ symbol_tablet load_java_class(
/// \param command_line: The command line used to configure the provided
/// language
/// \return The goto model containing both the functions and the symbol table
/// from loading this class.
/// from loading this class.
goto_modelt load_goto_model_from_java_class(
const std::string &java_class_name,
const std::string &class_path,

44
jbmc/unit/java-testing-utils/require_goto_statements.cpp
View File

@ -19,7 +19,7 @@ Author: Diffblue Ltd.
/// Expand value of a function to include all child codets
/// \param function_value: The value of the function (e.g. got by looking up
/// the function in the symbol table and getting the value)
/// \return: All ID_code statements in the tree rooted at \p function_value
/// \return All ID_code statements in the tree rooted at \p function_value
std::vector<codet>
require_goto_statements::get_all_statements(const exprt &function_value)
{
@ -37,7 +37,7 @@ require_goto_statements::get_all_statements(const exprt &function_value)
return statements;
}
/// \param symbol_table Symbol table for the test
/// \param symbol_table: Symbol table for the test
/// \return All codet statements of the __CPROVER_start function
const std::vector<codet>
require_goto_statements::require_entry_point_statements(
@ -60,8 +60,8 @@ require_goto_statements::require_entry_point_statements(
/// \param superclass_name: The name of the superclass (if given)
/// \param component_name: The name of the component of the superclass that
/// \param symbol_table: A symbol table to enable type lookups
/// should be assigned
/// \return: All the assignments to that component.
/// should be assigned
/// \return All the assignments to that component.
require_goto_statements::pointer_assignment_locationt
require_goto_statements::find_struct_component_assignments(
const std::vector<codet> &statements,
@ -150,8 +150,8 @@ require_goto_statements::find_struct_component_assignments(
}
/// Find assignment statements that set this->{component_name}
/// \param statements The statements to look through
/// \param component_name The name of the component whose assignments we are
/// \param statements: The statements to look through
/// \param component_name: The name of the component whose assignments we are
/// looking for.
/// \return A collection of all non-null assignments to this component
/// and, if present, a null assignment.
@ -200,8 +200,8 @@ require_goto_statements::find_this_component_assignment(
/// instructions.
/// \param pointer_name: The name of the variable
/// \param instructions: The instructions to look through
/// \return: A structure that contains the null assignment if found, and a
/// vector of all other assignments
/// \return A structure that contains the null assignment if found, and a
/// vector of all other assignments
require_goto_statements::pointer_assignment_locationt
require_goto_statements::find_pointer_assignments(
const irep_idt &pointer_name,
@ -290,13 +290,13 @@ const code_declt &require_goto_statements::require_declaration_of_name(
/// Checks that the component of the structure (possibly inherited from
/// the superclass) is assigned an object of the given type.
/// \param structure_name The name the variable
/// \param superclass_name The name of its superclass (if given)
/// \param component_name The name of the field of the superclass
/// \param component_type_name The name of the required type of the field
/// \param typecast_name The name of the type to which the object is cast (if
/// there is a typecast)
/// \param entry_point_instructions The statements to look through
/// \param structure_name: The name the variable
/// \param superclass_name: The name of its superclass (if given)
/// \param component_name: The name of the field of the superclass
/// \param component_type_name: The name of the required type of the field
/// \param typecast_name: The name of the type to which the object is cast (if
/// there is a typecast)
/// \param entry_point_instructions: The statements to look through
/// \param symbol_table: A symbol table to enable type lookups
/// \return The identifier of the variable assigned to the field
const irep_idt &require_goto_statements::require_struct_component_assignment(
@ -379,11 +379,11 @@ const irep_idt &require_goto_statements::require_struct_component_assignment(
/// Checks that the array component of the structure (possibly inherited from
/// the superclass) is assigned an array with given element type.
/// \param structure_name The name the variable
/// \param superclass_name The name of its superclass (if given)
/// \param array_component_name The name of the array field of the superclass
/// \param array_type_name The type of the array, e.g., java::array[reference]
/// \param entry_point_instructions The statements to look through
/// \param structure_name: The name the variable
/// \param superclass_name: The name of its superclass (if given)
/// \param array_component_name: The name of the array field of the superclass
/// \param array_type_name: The type of the array, e.g., java::array[reference]
/// \param entry_point_instructions: The statements to look through
/// \param symbol_table: A symbol table to enable type lookups
/// \return The identifier of the variable assigned to the field
const irep_idt &
@ -454,8 +454,8 @@ require_goto_statements::require_struct_array_component_assignment(
/// Checks that the input argument (of method under test) with given name is
/// assigned a single non-null object in the entry point function.
/// \param argument_name Name of the input argument of method under test
/// \param entry_point_statements The statements to look through
/// \param argument_name: Name of the input argument of method under test
/// \param entry_point_statements: The statements to look through
/// \return The identifier of the variable assigned to the input argument
const irep_idt &
require_goto_statements::require_entry_point_argument_assignment(

6
jbmc/unit/java-testing-utils/require_parse_tree.cpp
View File

@ -13,10 +13,10 @@ Author: Diffblue Ltd.
/// Find in the parsed class a specific entry within the
/// lambda_method_handle_map with a matching descriptor. Will fail if no
/// matching lambda entry found.
/// \param parsed_class the class to inspect
/// \param lambda_method_ref the reference/descriptor of the lambda method
/// \param parsed_class: the class to inspect
/// \param lambda_method_ref: the reference/descriptor of the lambda method
/// to which this lambda entry points to, must be unique
/// \param method_type the descriptor the lambda method should have
/// \param method_type: the descriptor the lambda method should have
/// \return
require_parse_tree::lambda_method_handlet
require_parse_tree::require_lambda_entry_for_descriptor(

8
jbmc/unit/java-testing-utils/require_type.cpp
View File

@ -65,7 +65,7 @@ code_typet require_type::require_code(const typet &type)
/// accepts a given number of parameters
/// \param type: The type to check
/// \param num_params: check the the given code_typet expects this
/// number of parameters
/// number of parameters
/// \return The type cast to a code_typet
code_typet
require_type::require_code(const typet &type, const size_t num_params)
@ -88,7 +88,7 @@ java_method_typet require_type::require_java_method(const typet &type)
/// accepts a given number of parameters
/// \param type: The type to check
/// \param num_params: check the the given java_method_typet expects this
/// number of parameters
/// number of parameters
/// \return The type cast to a java_method_typet
java_method_typet
require_type::require_java_method(const typet &type, const size_t num_params)
@ -102,7 +102,7 @@ require_type::require_java_method(const typet &type, const size_t num_params)
/// \param function_type: The type of the function
/// \param param_name: The name of the parameter
/// \return A reference to the parameter structure corresponding to this
/// parameter name.
/// parameter name.
code_typet::parametert require_type::require_parameter(
const code_typet &function_type,
const irep_idt &param_name)
@ -223,7 +223,7 @@ java_generic_parametert require_type::require_java_generic_parameter(
/// Test a type to ensure it is not a java generics type.
/// \param type: The type to test
/// \param expect_subtype: Optionally, also test that the subtype of the given
/// type matches this parameter
/// type matches this parameter
/// \return The value passed in the first argument
const typet &require_type::require_java_non_generic_type(
const typet &type,

4
jbmc/unit/java_bytecode/java_bytecode_convert_method/convert_initalizers.cpp
View File

@ -26,7 +26,7 @@ struct test_datat
/// Verify that a given descriptor is marked as a constructor in the symbol
/// table
/// \param test_data The data to run the test on
/// \param test_data: The data to run the test on
void require_is_constructor(const test_datat &test_data)
{
const symbolt &constructor =
@ -41,7 +41,7 @@ void require_is_constructor(const test_datat &test_data)
/// Verify that a given descriptor is not marked as a constructor in the symbol
/// table
/// \param test_data The data to run the test on
/// \param test_data: The data to run the test on
void require_is_static_initializer(const test_datat &test_data)
{
REQUIRE(

4
src/analyses/call_graph_helpers.h
View File

@ -55,7 +55,7 @@ std::set<irep_idt> get_reaching_functions(
/// \param start_functions: set of start functions
/// \param n: number of steps to consider
/// \return set of functions that can be reached from the start function
/// including the start function
/// including the start function
std::set<irep_idt> get_functions_reachable_within_n_steps(
const call_grapht::directed_grapht &graph,
const std::set<irep_idt> &start_functions,
@ -67,7 +67,7 @@ std::set<irep_idt> get_functions_reachable_within_n_steps(
/// \param start_function: single start function
/// \param n: number of steps to consider
/// \return set of functions that can be reached from the start function
/// including the start function
/// including the start function
std::set<irep_idt> get_functions_reachable_within_n_steps(
const call_grapht::directed_grapht &graph,
const irep_idt &start_function,

10
src/analyses/constant_propagator.cpp
View File

@ -638,8 +638,8 @@ bool constant_propagator_domaint::merge(
/// Attempt to evaluate expression using domain knowledge
/// This function changes the expression that is passed into it.
/// \param known_values: The constant values under which to evaluate \p expr
/// \param expr The expression to evaluate
/// \param ns The namespace for symbols in the expression
/// \param expr: The expression to evaluate
/// \param ns: The namespace for symbols in the expression
/// \return True if the expression is unchanged, false otherwise
bool constant_propagator_domaint::partial_evaluate(
const valuest &known_values,
@ -659,10 +659,10 @@ bool constant_propagator_domaint::partial_evaluate(
/// Attempt to evaluate an expression in all rounding modes.
///
/// \param known_values: The constant values under which to evaluate \p expr
/// \param expr The expression to evaluate
/// \param ns The namespace for symbols in the expression
/// \param expr: The expression to evaluate
/// \param ns: The namespace for symbols in the expression
/// \return If the result is the same for all rounding modes, change
/// expr to that result and return false. Otherwise, return true.
/// expr to that result and return false. Otherwise, return true.
bool constant_propagator_domaint::partial_evaluate_with_all_rounding_modes(
const valuest &known_values,
exprt &expr,

6
src/analyses/interval_analysis.cpp
View File

@ -24,8 +24,8 @@ Author: Daniel Kroening, kroening@kroening.com
/// conjunction.
/// Example: interval [5,10] (for variable "x") translates into conjunction
/// 5 <= x && x <= 10.
/// \param interval_analysis Interval domain to be used for variable evaluation.
/// \param goto_function [out] Goto function to be analysed and instrumented.
/// \param interval_analysis: Interval domain to be used for variable evaluation
/// \param [out] goto_function: Goto function to be analysed and instrumented.
void instrument_intervals(
const ait<interval_domaint> &interval_analysis,
goto_functionst::goto_functiont &goto_function)
@ -89,7 +89,7 @@ void instrument_intervals(
/// Initialises the abstract interpretation over interval domain and
/// instruments instructions using interval assumptions.
/// \param goto_model [out] Input code as goto_model.
/// \param [out] goto_model: Input code as goto_model.
void interval_analysis(goto_modelt &goto_model)
{
ait<interval_domaint> interval_analysis;

14
src/analyses/natural_loops.h
View File

@ -35,13 +35,13 @@ Author: Georg Weissenbacher, georg@weissenbacher.name
/// All instructions in a natural loop are stored into \ref loop_map, keyed by
/// their head - the target of the backwards goto jump.
///
/// \tparam P the program representation and needs:
/// [field] instruction which is an iterable of type T.
/// \tparam T iterator of the particular node type, ex: std::list<...>::iterator.
/// The object this iterator holds needs:
/// [function] is_backwards_goto() returning a bool.
/// [function] get_target() which returns an object that needs:
/// [field] location_number which returns an unsigned int.
/// \tparam P: the program representation and needs:
/// * [field] instruction which is an iterable of type T.
/// \tparam T: iterator of the particular node type, e.g.
/// std::list<...>::iterator. The object this iterator holds needs:
/// * [function] is_backwards_goto() returning a bool.
/// * [function] get_target() which returns an object that needs:
/// * [field] location_number which is an unsigned int.
template<class P, class T>
class natural_loops_templatet
{

2
src/ansi-c/ansi_c_entry_point.cpp
View File

@ -190,7 +190,7 @@ bool ansi_c_entry_point(
/// \param symbol_table: The symbol table for the program. The new _start
/// function symbol will be added to this table
/// \param message_handler: The message handler
/// \param object_factory_parameters configuration parameters for the object
/// \param object_factory_parameters: configuration parameters for the object
/// factory
/// \return Returns false if the _start method was generated correctly
bool generate_ansi_c_start_function(

6
src/ansi-c/c_nondet_symbol_factory.cpp
View File

@ -88,8 +88,8 @@ private:
/// \param assignments: The code block to add code to
/// \param expr: The expression which we are generating a non-determinate value
/// for
/// \param depth number of pointers followed so far during initialisation
/// \param recursion_set names of structs seen so far on current pointer chain
/// \param depth: number of pointers followed so far during initialisation
/// \param recursion_set: names of structs seen so far on current pointer chain
void symbol_factoryt::gen_nondet_init(
code_blockt &assignments,
const exprt &expr,
@ -218,7 +218,7 @@ void symbol_factoryt::gen_nondet_array_init(
/// \param base_name: The name to use for the symbol created
/// \param type: The type for the symbol created
/// \param loc: The location to assign to generated code
/// \param object_factory_parameters configuration parameters for the object
/// \param object_factory_parameters: configuration parameters for the object
/// factory
/// \return Returns the symbol_exprt for the symbol created
symbol_exprt c_nondet_symbol_factory(

4
src/ansi-c/c_object_factory_parameters.h
View File

@ -24,8 +24,8 @@ struct c_object_factory_parameterst final : public object_factory_parameterst
};
/// Parse the c object factory parameters from a given command line
/// \param cmdline Command line
/// \param [out] options The options object that will be updated
/// \param cmdline: Command line
/// \param [out] options: The options object that will be updated
void parse_c_object_factory_options(const cmdlinet &cmdline, optionst &options);
#endif

2
src/ansi-c/literals/convert_float_literal.cpp
View File

@ -25,7 +25,7 @@ Author: Daniel Kroening, kroening@kroening.com
#include "parse_float.h"
/// build an expression from a floating-point literal
/// \returns either a constant_exprt or a complex_exprt
/// \return either a constant_exprt or a complex_exprt
exprt convert_float_literal(const std::string &src)
{
parse_floatt parsed_float(src);

23
src/ansi-c/typedef_type.h
View File

@ -11,8 +11,7 @@ Author: Daniel Kroening, kroening@kroening.com
#include <util/type.h>
/*! \brief A typedef
*/
/// A typedef
class typedef_typet : public typet
{
public:
@ -32,25 +31,19 @@ public:
}
};
/*! \brief Cast a generic typet to a \ref typedef_typet
*
* This is an unchecked conversion. \a type must be known to be \ref
* typedef_typet.
*
* \param type Source type
* \return Object of type \ref typedef_typet
*
* \ingroup gr_std_types
*/
/// Cast a generic typet to a \ref typedef_typet. This is an unchecked
/// conversion. \a type must be known to be \ref typedef_typet.
/// \param type: Source type
/// \return Object of type \ref typedef_typet
/// \ingroup gr_std_types
inline const typedef_typet &to_typedef_type(const typet &type)
{
PRECONDITION(type.id() == ID_typedef_type);
return static_cast<const typedef_typet &>(type);
}
/*! \copydoc to_typedef_type(const typet &)
* \ingroup gr_std_types
*/
/// \copydoc to_typedef_type(const typet &)
/// \ingroup gr_std_types
inline typedef_typet &to_typedef_type(typet &type)
{
PRECONDITION(type.id() == ID_typedef_type);

2
src/cbmc/bmc.cpp
View File

@ -495,7 +495,7 @@ safety_checkert::resultt bmct::stop_on_fail(prop_convt &prop_conv)
/// large equation for the whole program or an equation per path
/// \param opts: command-line options affecting BMC
/// \param model: provides goto function bodies and the symbol table, perhaps
// creating those function bodies on demand.
/// creating those function bodies on demand.
/// \param ui: user-interface mode (plain text, XML output, JSON output, ...)
/// \param driver_configure_bmc: function provided by the driver program,
/// which applies driver-specific configuration to a bmct before running.

2
src/cpp/cpp_typecheck_destructor.cpp
View File

@ -49,8 +49,6 @@ void cpp_typecheckt::default_dtor(
}
/// produces destructor code for a class object
///
/// Note:
codet cpp_typecheckt::dtor(const symbolt &symbol)
{
assert(symbol.type.id()==ID_struct ||

2
src/goto-analyzer/static_simplifier.cpp
View File

@ -25,7 +25,7 @@ Author: Martin Brain, martin.brain@cs.ox.ac.uk
/// \param options: the parsed user options
/// \param message_handler: the system message handler
/// \param out: output stream for the simplified program
/// \return: false on success with the domain printed to out
/// \return false on success with the domain printed to out
bool static_simplifier(
goto_modelt &goto_model,
const ai_baset &ai,

2
src/goto-analyzer/static_verifier.cpp
View File

@ -230,7 +230,7 @@ static void static_verifier_console(
/// \param options: the parsed user options
/// \param message_handler: the system message handler
/// \param out: output stream for the printing
/// \return: false on success with the domain printed to out
/// \return false on success with the domain printed to out
bool static_verifier(
const goto_modelt &goto_model,
const ai_baset &ai,

4
src/goto-cc/compile.h
View File

@ -81,8 +81,8 @@ public:
/// \brief `__CPROVER_...` macros written to object files and their arities
///
/// \return A mapping from every `__CPROVER` macro that this compiler
/// wrote to one or more object files, to how many parameters that
/// `__CPROVER` macro has.
/// wrote to one or more object files, to how many parameters that
/// `__CPROVER` macro has.
void cprover_macro_arities(std::map<irep_idt,
std::size_t> &cprover_macros) const
{

9
src/goto-cc/hybrid_binary.h
View File

@ -19,11 +19,10 @@ Date: May 2018
#include <string>
/// \brief Merges a goto binary into an object file (e.g. ELF)
/// \param compiler_or_linker The name of the gcc or ld executable,
/// used to deduce the name of objcopy
/// \param goto_binary_file The file name of the goto binary
/// \param output_file The name of the object file; the result is
/// stored here.
/// \param compiler_or_linker: The name of the gcc or ld executable, used to
/// deduce the name of objcopy
/// \param goto_binary_file: The file name of the goto binary
/// \param output_file: The name of the object file; the result is stored here.
int hybrid_binary(
const std::string &compiler_or_linker,
const std::string &goto_binary_file,

23
src/goto-cc/linker_script_merge.h
View File

@ -157,11 +157,11 @@ protected:
/// converted to `foo` whose type is `char*`.
int pointerize_linker_defined_symbols(goto_modelt &, const linker_valuest &);
/// \param expr an expr whose subexpressions may need to be pointerized
/// \param to_pointerize The symbols that are contained in the subexpressions
/// that we will pointerize.
/// \param linker_values the names of symbols defined in linker scripts.
/// \param ns a namespace to look up types.
/// \param expr: an expr whose subexpressions may need to be pointerized
/// \param to_pointerize: The symbols that are contained in the subexpressions
/// that we will pointerize.
/// \param linker_values: the names of symbols defined in linker scripts.
/// \param ns: a namespace to look up types.
///
/// The subexpressions that we pointerize should be in one-to-one
/// correspondence with the symbols in `to_pointerize`. Every time we
@ -195,13 +195,12 @@ protected:
/// `linker_values` map. The error messages of this function describe what it
/// means for this constraint to be violated.
///
/// \param linker_defined_symbols the list of symbols that were extern with no
/// value in the goto-program)
/// \param linker_values map from the names of linker-defined symbols from
/// the object file, to synthesized values for those
/// linker symbols.
/// \return `1` if there is some mismatch between the list and map, `0`
/// if everything is OK.
/// \param linker_defined_symbols: the list of symbols that were extern with
/// no value in the goto-program
/// \param linker_values: map from the names of linker-defined symbols from
/// the object file, to synthesized values for those linker symbols.
/// \return `1` if there is some mismatch between the list and map, `0` if
/// everything is OK.
int goto_and_object_mismatch(
const std::list<irep_idt> &linker_defined_symbols,
const linker_valuest &linker_values);

6
src/goto-instrument/aggressive_slicer.h
View File

@ -56,8 +56,8 @@ public:
/// \brief Adds a list of functions to the set of functions for the aggressive
/// slicer to preserve
/// \param function_list: a list of functions in form
/// std::list<std::string>, as returned by get_cmdline_option.
/// \param function_list: a list of functions in form std::list<std::string>,
/// as returned by get_cmdline_option.
void preserve_functions(const std::list<std::string> &function_list)
{
for(const auto &f : function_list)
@ -86,7 +86,7 @@ private:
/// according to the configuration parameters set in the aggressive
/// slicer, i.e., shortest path between two functions, or all direct paths.
/// Inserts functions to preserve into the functions_to_keep set
/// \param destination_function name of destination function for slice
/// \param destination_function: name of destination function for slice
void note_functions_to_keep(const irep_idt &destination_function);
/// \brief Finds all functions that contain a property,

2
src/goto-instrument/cover.cpp
View File

@ -28,7 +28,7 @@ Date: May 2016
/// \param goto_program: the goto program
/// \param instrumenters: the instrumenters
/// \param mode: mode of the function to instrument (for instance ID_C or
/// ID_java)
/// ID_java)
/// \param message_handler: a message handler
void instrument_cover_goals(
goto_programt &goto_program,

38
src/goto-instrument/cover_basic_blocks.h
View File

@ -22,19 +22,19 @@ class cover_blocks_baset
{
public:
virtual ~cover_blocks_baset() = default;
/// \param t a goto instruction
/// \return the block number of the block
/// the given goto instruction is part of
/// \param t: a goto instruction
/// \return the block number of the block that the given goto instruction is
// part of
virtual std::size_t block_of(goto_programt::const_targett t) const = 0;
/// \param block_nr a block number
/// \return the instruction selected for
/// \param block_nr: a block number
/// \return the instruction selected for
/// instrumentation representative of the given block
virtual optionalt<goto_programt::const_targett>
instruction_of(std::size_t block_nr) const = 0;
/// \param block_nr a block number
/// \return the source location selected for
/// \param block_nr: a block number
/// \return the source location selected for
/// instrumentation representative of the given block
virtual const source_locationt &
source_location_of(std::size_t block_nr) const = 0;
@ -43,8 +43,8 @@ public:
virtual void output(std::ostream &out) const = 0;
/// Output warnings about ignored blocks
/// \param goto_program The goto program
/// \param message_handler The message handler
/// \param goto_program: The goto program
/// \param message_handler: The message handler
virtual void report_block_anomalies(
const goto_programt &goto_program,
message_handlert &message_handler)
@ -60,26 +60,26 @@ class cover_basic_blockst final : public cover_blocks_baset
public:
explicit cover_basic_blockst(const goto_programt &_goto_program);
/// \param t a goto instruction
/// \param t: a goto instruction
/// \return the block number of the block
/// the given goto instruction is part of
std::size_t block_of(goto_programt::const_targett t) const override;
/// \param block_nr a block number
/// \return the instruction selected for
/// \param block_nr: a block number
/// \return the instruction selected for
/// instrumentation representative of the given block
optionalt<goto_programt::const_targett>
instruction_of(std::size_t block_nr) const override;
/// \param block_nr a block number
/// \return the source location selected for
/// \param block_nr: a block number
/// \return the source location selected for
/// instrumentation representative of the given block
const source_locationt &
source_location_of(std::size_t block_nr) const override;
/// Output warnings about ignored blocks
/// \param goto_program The goto program
/// \param message_handler The message handler
/// \param goto_program: The goto program
/// \param message_handler: The message handler
void report_block_anomalies(
const goto_programt &goto_program,
message_handlert &message_handler) override;
@ -133,16 +133,16 @@ private:
public:
explicit cover_basic_blocks_javat(const goto_programt &_goto_program);
/// \param t a goto instruction
/// \param t: a goto instruction
/// \return block number the given goto instruction is part of
std::size_t block_of(goto_programt::const_targett t) const override;
/// \param block_number a block number
/// \param block_number: a block number
/// \return first instruction of the given block
optionalt<goto_programt::const_targett>
instruction_of(std::size_t block_number) const override;
/// \param block_number a block number
/// \param block_number: a block number
/// \return source location corresponding to the given block
const source_locationt &
source_location_of(std::size_t block_number) const override;

6
src/goto-instrument/cover_filter.cpp
View File

@ -16,7 +16,7 @@ Author: Peter Schrammel
/// Filter out functions that are not considered provided by the user
/// \param identifier: a function name
/// \param goto_function: a goto function
/// \return: returns true if function is considered user-provided
/// \return returns true if function is considered user-provided
bool internal_functions_filtert::operator()(
const irep_idt &identifier,
const goto_functionst::goto_functiont &goto_function) const
@ -46,7 +46,7 @@ bool internal_functions_filtert::operator()(
/// Filter functions whose name match the regex
/// \param identifier: a function name
/// \param goto_function: a goto function
/// \return: returns true if the function name matches
/// \return returns true if the function name matches
bool include_pattern_filtert::operator()(
const irep_idt &identifier,
const goto_functionst::goto_functiont &goto_function) const
@ -63,7 +63,7 @@ bool include_pattern_filtert::operator()(
/// These criteria are arbitrarily chosen.
/// \param identifier: a function name
/// \param goto_function: a goto function
/// \return: returns true if non-trivial
/// \return returns true if non-trivial
bool trivial_functions_filtert::operator()(
const irep_idt &identifier,
const goto_functionst::goto_functiont &goto_function) const

18
src/goto-instrument/nondet_static.cpp
View File

@ -24,10 +24,10 @@ Date: November 2011
#include <linking/static_lifetime_init.h>
/// See the return.
/// \param symbol_expr The symbol expression to analyze.
/// \param ns Namespace for resolving type information
/// \param symbol_expr: The symbol expression to analyze.
/// \param ns: Namespace for resolving type information
/// \return True if the symbol expression holds a static symbol which can be
/// nondeterministically initialized, false otherwise.
/// nondeterministically initialized, false otherwise.
bool is_nondet_initializable_static(
const symbol_exprt &symbol_expr,
const namespacet &ns)
@ -65,9 +65,9 @@ bool is_nondet_initializable_static(
/// Iterates over instructions in the specified function and replaces all values
/// assigned to nondet-initializable static variables with nondeterministic
/// values.
/// \param ns Namespace for resolving type information.
/// \param [out] goto_functions Existing goto-functions to be updated.
/// \param fct_name Name of the goto-function to be updated.
/// \param ns: Namespace for resolving type information.
/// \param [out] goto_functions: Existing goto-functions to be updated.
/// \param fct_name: Name of the goto-function to be updated.
void nondet_static(
const namespacet &ns,
goto_functionst &goto_functions,
@ -113,8 +113,8 @@ void nondet_static(
/// Nondeterministically initializes global scope variables in
/// CPROVER_initialize function.
/// \param ns Namespace for resolving type information.
/// \param [out] goto_functions Existing goto-functions to be updated.
/// \param ns: Namespace for resolving type information.
/// \param [out] goto_functions: Existing goto-functions to be updated.
void nondet_static(
const namespacet &ns,
goto_functionst &goto_functions)
@ -129,7 +129,7 @@ void nondet_static(
/// scope variables, except for constants (such as string literals, final
/// fields) and internal variables (such as CPROVER and symex variables,
/// language specific internal variables).
/// \param [out] goto_model Existing goto-model to be updated.
/// \param [out] goto_model: Existing goto-model to be updated.
void nondet_static(goto_modelt &goto_model)
{
const namespacet ns(goto_model.symbol_table);

48
src/goto-instrument/reachability_slicer.cpp
View File

@ -30,8 +30,8 @@ Author: Daniel Kroening, kroening@kroening.com
/// Get the set of nodes that correspond to the given criterion, or that can
/// appear in concurrent execution. None of these should be sliced away so
/// they are used as a basis for the search.
/// \param is_threaded Instructions that might be executed concurrently
/// \param criterion The criterion we care about
/// \param is_threaded: Instructions that might be executed concurrently
/// \param criterion: The criterion we care about
std::vector<reachability_slicert::cfgt::node_indext>
reachability_slicert::get_sources(
const is_threadedt &is_threaded,
@ -160,8 +160,8 @@ void reachability_slicert::backward_inwards_walk_from(
/// goto program, starting from the nodes corresponding to the criterion and
/// the instructions that might be executed concurrently. Set reaches_assertion
/// to true for every instruction visited.
/// \param is_threaded Instructions that might be executed concurrently
/// \param criterion the criterion we are trying to hit
/// \param is_threaded: Instructions that might be executed concurrently
/// \param criterion: the criterion we are trying to hit
void reachability_slicert::fixedpoint_to_assertions(
const is_threadedt &is_threaded,
const slicing_criteriont &criterion)
@ -298,8 +298,8 @@ void reachability_slicert::forward_inwards_walk_from(
/// goto program, starting from the nodes corresponding to the criterion and
/// the instructions that might be executed concurrently. Set reaches_assertion
/// to true for every instruction visited.
/// \param is_threaded Instructions that might be executed concurrently
/// \param criterion the criterion we are trying to hit
/// \param is_threaded: Instructions that might be executed concurrently
/// \param criterion: the criterion we are trying to hit
void reachability_slicert::fixedpoint_from_assertions(
const is_threadedt &is_threaded,
const slicing_criteriont &criterion)
@ -344,10 +344,10 @@ void reachability_slicert::slice(goto_functionst &goto_functions)
/// Perform reachability slicing on goto_model, with respect to the
/// criterion given by all properties.
/// \param goto_model Goto program to slice
/// \param include_forward_reachability Determines if only instructions
/// from which the criterion is reachable should be kept (false) or also
/// those reachable from the criterion (true)
/// \param goto_model: Goto program to slice
/// \param include_forward_reachability: Determines if only instructions
/// from which the criterion is reachable should be kept (false) or also
/// those reachable from the criterion (true)
void reachability_slicer(
goto_modelt &goto_model,
const bool include_forward_reachability)
@ -358,12 +358,12 @@ void reachability_slicer(
}
/// Perform reachability slicing on goto_model for selected properties.
/// \param goto_model Goto program to slice
/// \param properties The properties relevant for the slicing (i.e. starting
/// point for the search in the cfg)
/// \param include_forward_reachability Determines if only instructions
/// from which the criterion is reachable should be kept (false) or also
/// those reachable from the criterion (true)
/// \param goto_model: Goto program to slice
/// \param properties: The properties relevant for the slicing (i.e. starting
/// point for the search in the cfg)
/// \param include_forward_reachability: Determines if only instructions
/// from which the criterion is reachable should be kept (false) or also
/// those reachable from the criterion (true)
void reachability_slicer(
goto_modelt &goto_model,
const std::list<std::string> &properties,
@ -375,10 +375,10 @@ void reachability_slicer(
}
/// Perform reachability slicing on goto_model for selected functions.
/// \param goto_model Goto program to slice
/// \param functions_list The functions relevant for the slicing (i.e. starting
/// point for the search in the CFG). Anything that is reachable in the CFG
/// starting from these functions will be kept.
/// \param goto_model: Goto program to slice
/// \param functions_list: The functions relevant for the slicing (i.e. starting
/// point for the search in the CFG). Anything that is reachable in the CFG
/// starting from these functions will be kept.
void function_path_reachability_slicer(
goto_modelt &goto_model,
const std::list<std::string> &functions_list)
@ -400,7 +400,7 @@ void function_path_reachability_slicer(
/// Perform reachability slicing on goto_model, with respect to criterion
/// comprising all properties. Only instructions from which the criterion
/// is reachable will be kept.
/// \param goto_model Goto program to slice
/// \param goto_model: Goto program to slice
void reachability_slicer(goto_modelt &goto_model)
{
reachability_slicer(goto_model, false);
@ -408,9 +408,9 @@ void reachability_slicer(goto_modelt &goto_model)
/// Perform reachability slicing on goto_model for selected properties. Only
/// instructions from which the criterion is reachable will be kept.
/// \param goto_model Goto program to slice
/// \param properties The properties relevant for the slicing (i.e. starting
/// point for the search in the cfg)
/// \param goto_model: Goto program to slice
/// \param properties: The properties relevant for the slicing (i.e. starting
/// point for the search in the cfg)
void reachability_slicer(
goto_modelt &goto_model,
const std::list<std::string> &properties)

2
src/goto-instrument/splice_call.cpp
View File

@ -11,7 +11,7 @@ Date: July 2017
/// \file
/// Prepend a nullary call to another function
// useful for context/ environment setting in arbitrary nodes
/// useful for context/ environment setting in arbitrary nodes
#include "splice_call.h"

4
src/goto-programs/class_identifier.cpp
View File

@ -74,10 +74,10 @@ exprt get_class_identifier_field(
/// If expr has its components filled in then sets the `@class_identifier`
/// member of the struct
/// \remarks Follows through base class members until it gets to the object
/// type that contains the `@class_identifier` member
/// type that contains the `@class_identifier` member
/// \param expr: An expression that represents a struct
/// \param ns: The namespace used to resolve symbol references in the type of
/// the struct
/// the struct
/// \param class_type: A symbol whose identifier is the name of the class
void set_class_identifier(
struct_exprt &expr,

13
src/goto-programs/generate_function_bodies.cpp
View File

@ -330,8 +330,7 @@ public:
};
/// Create the type that actually generates the functions.
/// \see generate_function_bodies for the syntax of the options
/// parameter
/// \see generate_function_bodies for the syntax of the options parameter
std::unique_ptr<generate_function_bodiest> generate_function_bodies_factory(
const std::string &options,
const symbol_tablet &symbol_table,
@ -446,11 +445,11 @@ std::unique_ptr<generate_function_bodiest> generate_function_bodies_factory(
///
/// nondet-return: return nondet for non-void functions
///
/// \param functions_regex Specifies the functions whose body should
/// be generated
/// \param generate_function_body Specifies what kind of body to generate
/// \param model The goto-model in which to generate the function bodies
/// \param message_handler Destination for status/warning messages
/// \param functions_regex: Specifies the functions whose body should be
/// generated
/// \param generate_function_body: Specifies what kind of body to generate
/// \param model: The goto-model in which to generate the function bodies
/// \param message_handler: Destination for status/warning messages
void generate_function_bodies(
const std::regex &functions_regex,
const generate_function_bodiest &generate_function_body,

12
src/goto-programs/generate_function_bodies.h
View File

@ -26,9 +26,9 @@ protected:
/// Produce a body for the passed function
/// At this point the body of function is always empty,
/// and all function parameters have identifiers
/// \param function whose body to generate
/// \param symbol_table of the current goto program
/// \param function_name Identifier of function
/// \param function: whose body to generate
/// \param symbol_table: of the current goto program
/// \param function_name: Identifier of function
virtual void generate_function_body_impl(
goto_functiont &function,
const symbol_tablet &symbol_table,
@ -39,9 +39,9 @@ public:
/// Replace the function body with one based on the replace_function_body
/// class being used.
/// \param function whose body to replace
/// \param symbol_table of the current goto program
/// \param function_name Identifier of function
/// \param function: whose body to replace
/// \param symbol_table: of the current goto program
/// \param function_name: Identifier of function
void generate_function_body(
goto_functiont &function,
symbol_tablet &symbol_table,

8
src/goto-programs/goto_trace.cpp
View File

@ -351,10 +351,10 @@ bool is_index_member_symbol(const exprt &src)
}
/// \brief show a compact variant of the goto trace on the console
/// \param out the output stream
/// \param ns the namespace
/// \param goto_trace the trace to be shown
/// \param options any options, e.g., numerical representation
/// \param out: the output stream
/// \param ns: the namespace
/// \param goto_trace: the trace to be shown
/// \param options: any options, e.g., numerical representation
void show_compact_goto_trace(
messaget::mstreamt &out,
const namespacet &ns,

4
src/goto-programs/lazy_goto_model.h
View File

@ -146,7 +146,7 @@ public:
/// \param handler: An object that defines the handlers
/// \param options: The options passed to process_goto_functions
/// \param message_handler: The message_handler to use for logging
/// \tparam THandler a type that defines methods process_goto_function and
/// \tparam THandler: a type that defines methods process_goto_function and
/// process_goto_functions
template<typename THandler>
static lazy_goto_modelt from_handler_object(
@ -196,7 +196,7 @@ public:
/// load new functions, it has let it go.
/// Before freezing the functions all module-level passes are run
/// \param model: The lazy_goto_modelt to freeze
/// \returns The frozen goto_modelt or an empty optional if freezing fails
/// \return The frozen goto_modelt or an empty optional if freezing fails
static std::unique_ptr<goto_modelt> process_whole_model_and_freeze(
lazy_goto_modelt &&model)
{

14
src/goto-programs/link_to_library.cpp
View File

@ -15,11 +15,11 @@ Author: Daniel Kroening, kroening@kroening.com
#include "goto_convert_functions.h"
/// Complete missing function definitions using the \p library.
/// \param goto_model goto model that may contain function calls and symbols
/// \param goto_model: goto model that may contain function calls and symbols
/// with missing function bodies
/// \param message_handler message handler to report library processing
/// \param message_handler: message handler to report library processing
/// problems
/// \param library generator function that produces function definitions for a
/// \param library: generator function that produces function definitions for a
/// given set of symbol names that have no body.
void link_to_library(
goto_modelt &goto_model,
@ -36,13 +36,13 @@ void link_to_library(
}
/// Complete missing function definitions using the \p library.
/// \param symbol_table symbol table that may contain symbols with missing
/// \param symbol_table: symbol table that may contain symbols with missing
/// function bodies
/// \param goto_functions goto functions that may contain function calls with
/// \param goto_functions: goto functions that may contain function calls with
/// missing function bodies
/// \param message_handler message handler to report library processing
/// \param message_handler: message handler to report library processing
/// problems
/// \param library generator function that produces function definitions for a
/// \param library: generator function that produces function definitions for a
/// given set of symbol names that have no body.
void link_to_library(
symbol_tablet &symbol_table,

24
src/goto-programs/read_goto_binary.cpp
View File

@ -28,9 +28,9 @@ Author:
#include "osx_fat_reader.h"
/// \brief Read a goto binary from a file, but do not update \ref config
/// \param filename the file name of the goto binary
/// \param dest the goto model returned
/// \param message_handler for diagnostics
/// \param filename: the file name of the goto binary
/// \param dest: the goto model returned
/// \param message_handler: for diagnostics
/// \deprecated Use read_goto_binary(file, message_handler) instead
/// \return true on failure, false on success
bool read_goto_binary(
@ -43,8 +43,8 @@ bool read_goto_binary(
}
/// \brief Read a goto binary from a file, but do not update \ref config
/// \param filename the file name of the goto binary
/// \param message_handler for diagnostics
/// \param filename: the file name of the goto binary
/// \param message_handler: for diagnostics
/// \return goto model on success, {} on failure
optionalt<goto_modelt>
read_goto_binary(const std::string &filename, message_handlert &message_handler)
@ -61,10 +61,10 @@ read_goto_binary(const std::string &filename, message_handlert &message_handler)
}
/// \brief Read a goto binary from a file, but do not update \ref config
/// \param filename the file name of the goto binary
/// \param symbol_table the symbol table from the goto binary
/// \param goto_functions the goto functions from the goto binary
/// \param message_handler for diagnostics
/// \param filename: the file name of the goto binary
/// \param symbol_table: the symbol table from the goto binary
/// \param goto_functions: the goto functions from the goto binary
/// \param message_handler: for diagnostics
/// \return true on failure, false on success
bool read_goto_binary(
const std::string &filename,
@ -227,9 +227,9 @@ bool is_goto_binary(const std::string &filename)
}
/// \brief reads an object file, and also updates config
/// \param file_name file name of the goto binary
/// \param dest the goto model returned
/// \param message_handler for diagnostics
/// \param file_name: file name of the goto binary
/// \param dest: the goto model returned
/// \param message_handler: for diagnostics
/// \return true on error, false otherwise
bool read_object_and_link(
const std::string &file_name,

2
src/goto-programs/remove_const_function_pointers.cpp
View File

@ -47,7 +47,7 @@ remove_const_function_pointerst::remove_const_function_pointerst(
/// variations within.
/// \param base_expression: The function call through a function pointer
/// \param out_functions: The functions that (symbols of type ID_code) the base
/// expression could take.
/// expression could take.
/// \return Returns true if it was able to resolve the call, false if not. If it
/// returns true, out_functions will be populated by all the possible values
/// the function pointer could be.

10
src/goto-programs/remove_function_pointers.cpp
View File

@ -50,9 +50,9 @@ public:
/// Replace a call to a dynamic function at location
/// target in the given goto-program by a case-split
/// over a given set of functions
/// \param goto_program The goto program that contains target
/// \param target location with function call with function pointer
/// \param functions The set of functions to consider
/// \param goto_program: The goto program that contains target
/// \param target: location with function call with function pointer
/// \param functions: The set of functions to consider
void remove_function_pointer(
goto_programt &goto_program,
goto_programt::targett target,
@ -75,8 +75,8 @@ protected:
/// Replace a call to a dynamic function at location
/// target in the given goto-program by determining
/// functions that have a compatible signature
/// \param goto_program The goto program that contains target
/// \param target location with function call with function pointer
/// \param goto_program: The goto program that contains target
/// \param target: location with function call with function pointer
void remove_function_pointer(
goto_programt &goto_program,
goto_programt::targett target);

20
src/goto-programs/remove_skip.cpp
View File

@ -15,12 +15,12 @@ Author: Daniel Kroening, kroening@kroening.com
/// Determine whether the instruction is semantically equivalent to a skip
/// (no-op). This includes a skip, but also if(false) goto ..., goto next;
/// next: ..., and (void)0.
/// \param body goto program containing the instruction
/// \param it instruction iterator that is tested for being a skip (or
/// equivalent)
/// \param ignore_labels If the caller takes care of moving labels, then even
/// skip statements carrying labels can be treated as skips (even though they
/// may carry key information such as error labels).
/// \param body: goto program containing the instruction
/// \param it: instruction iterator that is tested for being a skip (or
/// equivalent)
/// \param ignore_labels: If the caller takes care of moving labels, then even
/// skip statements carrying labels can be treated as skips (even though they
/// may carry key information such as error labels).
/// \return True, iff it is equivalent to a skip.
bool is_skip(
const goto_programt &body,
@ -79,10 +79,10 @@ bool is_skip(
}
/// remove unnecessary skip statements
/// \param goto_program goto program containing the instructions to be cleaned
/// in the range [begin, end)
/// \param begin iterator pointing to first instruction to be considered
/// \param end iterator pointing beyond last instruction to be considered
/// \param goto_program: goto program containing the instructions to be cleaned
/// in the range [begin, end)
/// \param begin: iterator pointing to first instruction to be considered
/// \param end: iterator pointing beyond last instruction to be considered
void remove_skip(
goto_programt &goto_program,
goto_programt::targett begin,

40
src/goto-programs/remove_virtual_functions.cpp
View File

@ -74,11 +74,11 @@ remove_virtual_functionst::remove_virtual_functionst(
/// Replace specified virtual function call with a static call to its
/// most derived implementation
/// \param goto_program [in/out]: GOTO program to modify
/// \param target iterator: to a function in the supplied GOTO program
/// to replace. Must point to a virtual function call.
/// \param [in,out] goto_program: GOTO program to modify
/// \param target: iterator to a function in the supplied GOTO program
/// to replace. Must point to a virtual function call.
/// \return Returns a pointer to the statement in the supplied GOTO
/// program after replaced function call
/// program after replaced function call
goto_programt::targett remove_virtual_functionst::remove_virtual_function(
goto_programt &goto_program,
goto_programt::targett target)
@ -105,7 +105,7 @@ goto_programt::targett remove_virtual_functionst::remove_virtual_function(
}
/// Create a concrete function call to replace a virtual one
/// \param call [in,out]: the function call to update
/// \param [in,out] call: the function call to update
/// \param function_symbol: the function to be called
/// \param ns: namespace
static void create_static_function_call(
@ -131,16 +131,16 @@ static void create_static_function_call(
/// implementation. If there's a type mismatch between implementation
/// and the instance type or if fallback_action is set to
/// ASSUME_FALSE, then function is substituted with a call to ASSUME(false)
/// \param goto_program [in/out]: GOTO program to modify
/// \param [in,out] goto_program: GOTO program to modify
/// \param target: Iterator to the GOTO instruction in the supplied
/// GOTO program to be removed. Must point to a function call
/// GOTO program to be removed. Must point to a function call
/// \param functions: Dispatch table - all possible implementations of
/// this function sorted from the least to the most derived
/// this function sorted from the least to the most derived
/// \param fallback_action: - ASSUME_FALSE to replace virtual function
/// calls with ASSUME(false) or CALL_LAST_FUNCTION to replace them
/// with the most derived matching call
/// calls with ASSUME(false) or CALL_LAST_FUNCTION to replace them
/// with the most derived matching call
/// \return Returns a pointer to the statement in the supplied GOTO
/// program after replaced function call
/// program after replaced function call
goto_programt::targett remove_virtual_functionst::remove_virtual_function(
goto_programt &goto_program,
goto_programt::targett target,
@ -402,8 +402,8 @@ void remove_virtual_functionst::get_child_functions_rec(
/// Used to get dispatch entries to call for the given function
/// \param function: function that should be called
/// \param[out] functions: is assigned a list of dispatch entries, i.e., pairs
/// of class names and function symbol to call when encountering the class.
/// \param [out] functions: is assigned a list of dispatch entries, i.e., pairs
/// of class names and function symbol to call when encountering the class.
void remove_virtual_functionst::get_functions(
const exprt &function,
dispatch_table_entriest &functions)
@ -491,7 +491,7 @@ void remove_virtual_functionst::get_functions(
/// \param class_id: Class identifier to look up
/// \param component_name: Name of the function to look up
/// \return nil_exprt instance on error and a symbol_exprt pointing to
/// the method on success
/// the method on success
exprt remove_virtual_functionst::get_method(
const irep_idt &class_id,
const irep_idt &component_name) const
@ -597,16 +597,16 @@ void remove_virtual_functions(goto_model_functiont &function)
/// and the instance type or if fallback_action is set to
/// ASSUME_FALSE, then function is substituted with a call to ASSUME(false)
/// \param symbol_table: Symbol table
/// \param goto_program [in/out]: GOTO program to modify
/// \param [in,out] goto_program: GOTO program to modify
/// \param instruction: Iterator to the GOTO instruction in the supplied
/// GOTO program to be removed. Must point to a function call
/// GOTO program to be removed. Must point to a function call
/// \param dispatch_table: Dispatch table - all possible implementations of
/// this function sorted from the least to the most derived
/// this function sorted from the least to the most derived
/// \param fallback_action: - ASSUME_FALSE to replace virtual function
/// calls with ASSUME(false) or CALL_LAST_FUNCTION to replace them
/// with the most derived matching call
/// calls with ASSUME(false) or CALL_LAST_FUNCTION to replace them
/// with the most derived matching call
/// \return Returns a pointer to the statement in the supplied GOTO
/// program after replaced function call
/// program after replaced function call
goto_programt::targett remove_virtual_function(
symbol_tablet &symbol_table,
goto_programt &goto_program,

4
src/goto-programs/remove_virtual_functions.h
View File

@ -82,11 +82,11 @@ goto_programt::targett remove_virtual_function(
/// Given a function expression representing a virtual method of a class,
/// the function computes all overridden methods of that virtual method.
/// \param function: The virtual function expression for which the overridden
/// methods will be searched for.
/// methods will be searched for.
/// \param symbol_table: A symbol table.
/// \param class_hierarchy: A class hierarchy.
/// \param [out] overridden_functions: Output collection into which all
/// overridden functions will be stored.
/// overridden functions will be stored.
void collect_virtual_function_callees(
const exprt &function,
const symbol_tablet &symbol_table,

6
src/goto-programs/show_properties.h
View File

@ -43,11 +43,11 @@ void show_properties(
/// \brief Returns a source_locationt that corresponds
/// to the property given by an irep_idt.
/// \param property irep_idt that identifies property
/// \param goto_functions program in which to search for
/// \param property: irep_idt that identifies property
/// \param goto_functions: program in which to search for
/// the property
/// \return optional<source_locationt> the location of the
/// property, if found.
/// property, if found.
optionalt<source_locationt> find_property(
const irep_idt &property,
const goto_functionst &goto_functions);

19
src/goto-programs/wp.h
View File

@ -16,22 +16,19 @@ class codet;
class exprt;
class namespacet;
/*! \brief Compute the weakest precondition of the given program
* piece \a code with respect to the expression \a post.
* \param code Program
* \param post Postcondition
* \param ns Namespace
* \return Weakest precondition
*/
/// Compute the weakest precondition of the given program
/// piece \a code with respect to the expression \a post.
/// \param code: Program
/// \param post: Postcondition
/// \param ns: Namespace
/// \return Weakest precondition
exprt wp(
const codet &code,
const exprt &post,
const namespacet &ns);
/*! \brief approximate the non-deterministic choice
in a way cheaper than by (proper) quantification
*/
/// Approximate the non-deterministic choice in a way cheaper than by (proper)
/// quantification
void approximate_nondet(exprt &dest);
#endif // CPROVER_GOTO_PROGRAMS_WP_H

16
src/goto-symex/goto_symex.h
View File

@ -166,12 +166,12 @@ protected:
/// Initialise the symbolic execution and the given state with <code>pc</code>
/// as entry point.
/// \param state Symex state to initialise.
/// \param get_goto_function producer for GOTO functions
/// \param function_identifier The function in which the instructions are
/// \param pc first instruction to symex
/// \param limit final instruction, which itself will not
/// be symexed.
/// \param state: Symex state to initialise.
/// \param get_goto_function: producer for GOTO functions
/// \param function_identifier: The function in which the instructions are
/// \param pc: first instruction to symex
/// \param limit: final instruction, which itself will not
/// be symexed.
void initialize_entry_point(
statet &state,
const get_goto_functiont &get_goto_function,
@ -181,8 +181,8 @@ protected:
/// Invokes symex_step and verifies whether additional threads can be
/// executed.
/// \param state Current GOTO symex step.
/// \param get_goto_function function that retrieves function bodies
/// \param state: Current GOTO symex step.
/// \param get_goto_function: function that retrieves function bodies
void symex_threaded_step(
statet &, const get_goto_functiont &);

4
src/goto-symex/path_storage.h
View File

@ -64,8 +64,8 @@ public:
/// instruction with two successors. Thus, we always add a pair of paths to
/// the path storage.
///
/// \param next_instruction the instruction following the goto instruction
/// \param jump_target the target instruction of the goto instruction
/// \param next_instruction: the instruction following the goto instruction
/// \param jump_target: the target instruction of the goto instruction
virtual void
push(const patht &next_instruction, const patht &jump_target) = 0;

6
src/goto-symex/symex_goto.cpp
View File

@ -389,14 +389,14 @@ static void for_each2(
/// Helper function for \c phi_function which merges the names of an identifier
/// for two different states.
/// \param goto_state: first state
/// \param[in, out] dest_state: second state
/// \param [in, out] dest_state: second state
/// \param ns: namespace
/// \param diff_guard: difference between the guards of the two states
/// \param guard_identifier: prefix used for goto symex guards
/// \param[out] log: logger for debug messages
/// \param [out] log: logger for debug messages
/// \param do_simplify: should the right-hand-side of the assignment that is
/// added to the target be simplified
/// \param[out] target: equation that will receive the resulting assignment
/// \param [out] target: equation that will receive the resulting assignment
/// \param ssa: SSA expression to merge
/// \param goto_count: current level 2 count in \p goto_state of
/// \p l1_identifier

4
src/goto-symex/symex_target_equation.cpp
View File

@ -945,8 +945,8 @@ void symex_target_equationt::SSA_stept::output(std::ostream &out) const
}
/// Check that the SSA step is well-formed
/// \param ns namespace to lookup identifiers
/// \param vm validation mode to be used for reporting failures
/// \param ns: namespace to lookup identifiers
/// \param vm: validation mode to be used for reporting failures
void symex_target_equationt::SSA_stept::validate(
const namespacet &ns,
const validation_modet vm) const

6
src/json-symtab-language/json_symbol.cpp
View File

@ -17,7 +17,7 @@ Author: Chris Smowton, chris.smowton@diffblue.com
/// Return string value for a given key if present in the json object.
/// \param in: The json object that is getting fetched as a string.
/// \param key: The key for the json value to be fetched.
/// \return: A string value for the corresponding key.
/// \return A string value for the corresponding key.
static const std::string &
try_get_string(const jsont &in, const std::string &key)
{
@ -30,7 +30,7 @@ try_get_string(const jsont &in, const std::string &key)
/// Return boolean value for a given key if present in the json object.
/// \param in: The json object that is getting fetched as a boolean.
/// \param key: The key for the json value to be fetched.
/// \return: A boolean value for the corresponding key.
/// \return A boolean value for the corresponding key.
static bool try_get_bool(const jsont &in, const std::string &key)
{
if(!(in.is_true() || in.is_false()))
@ -41,7 +41,7 @@ static bool try_get_bool(const jsont &in, const std::string &key)
/// Deserialise a json object to a symbolt.
/// \param in: The json object that is getting fetched as an object.
/// \return: A symbolt representing the json object.
/// \return A symbolt representing the json object.
symbolt symbol_from_json(const jsont &in)
{
if(!in.is_object())

4
src/json-symtab-language/json_symtab_language.cpp
View File

@ -16,7 +16,7 @@ Author: Chris Smowton, chris.smowton@diffblue.com
/// Parse a goto program in json form.
/// \param instream: The input stream
/// \param path: A file path
/// \return: boolean signifying success or failure of the parsing
/// \return boolean signifying success or failure of the parsing
bool json_symtab_languaget::parse(
std::istream &instream,
const std::string &path)
@ -27,7 +27,7 @@ bool json_symtab_languaget::parse(
/// Typecheck a goto program in json form.
/// \param symbol_table: The symbol table containing symbols read from file.
/// \param module: A useless parameter, there for interface consistency.
/// \return: boolean signifying success or failure of the typechecking.
/// \return boolean signifying success or failure of the typechecking.
bool json_symtab_languaget::typecheck(
symbol_tablet &symbol_table,
const std::string &module)

2
src/langapi/mode.cpp
View File

@ -76,7 +76,7 @@ get_mode_from_identifier(const namespacet &ns, const irep_idt &identifier)
/// \param ns: a namespace
/// \param identifier: an identifier
/// \return the corresponding language if the mode is not `ID_unknown`, or
/// the default language otherwise;
/// the default language otherwise;
/// Note: It is assumed as an invariant that languages of symbols in the symbol
/// table have been registered.
std::unique_ptr<languaget>

4
src/pointer-analysis/goto_program_dereference.cpp
View File

@ -20,7 +20,7 @@ Author: Daniel Kroening, kroening@kroening.com
#include <util/options.h>
/// \param expr: expression to check
/// \param[out] symbol: symbol which gets assigned the value from the
/// \param [out] symbol: symbol which gets assigned the value from the
/// `failed_symbol` comment
/// \return true when `expr` is a symbol, whose type contains a `failed_symbol`
/// comment which exists in the namespace.
@ -233,7 +233,7 @@ void goto_program_dereferencet::dereference_rec(
/// Gets the value set corresponding to the current target and
/// expression `expr`.
/// \param expr: an expression
/// \param[out] dest: gets the value set
/// \param [out] dest: gets the value set
void goto_program_dereferencet::get_value_set(
const exprt &expr,
value_setst::valuest &dest)

4
src/pointer-analysis/value_set.h
View File

@ -457,8 +457,8 @@ protected:
/// Reads the set of objects pointed to by `expr`, including making
/// recursive lookups for dereference operations etc.
/// \param expr: query expression
/// \param dest [out]: overwritten by the set of object numbers pointed to
/// \param ns; global namespace
/// \param [out] dest: overwritten by the set of object numbers pointed to
/// \param ns: global namespace
/// \param is_simplified: if false, simplify `expr` before reading.
void get_value_set(
const exprt &expr,

25
src/pointer-analysis/value_set_dereference.h
View File

@ -27,14 +27,14 @@ class symbolt;
class value_set_dereferencet
{
public:
/// \param _ns Namespace
/// \param _new_symbol_table A symbol_table to store new symbols in
/// \param _dereference_callback Callback object for getting the set of
/// objects a given pointer may point to.
/// \param _language_mode Mode for any new symbols created to represent
/// a dereference failure
/// \param _exclude_null_derefs Ignore value-set entries that indicate a given
/// dereference may follow a null pointer
/// \param _ns: Namespace
/// \param _new_symbol_table: A symbol_table to store new symbols in
/// \param _dereference_callback: Callback object for getting the set of
/// objects a given pointer may point to.
/// \param _language_mode: Mode for any new symbols created to represent a
/// dereference failure
/// \param _exclude_null_derefs: Ignore value-set entries that indicate a
// given dereference may follow a null pointer
value_set_dereferencet(
const namespacet &_ns,
symbol_tablet &_new_symbol_table,
@ -54,12 +54,11 @@ public:
/// Dereference the given pointer-expression. Any errors are
/// reported to the callback method given in the constructor.
/// \param pointer A pointer-typed expression, to
/// \param pointer: A pointer-typed expression, to
/// be dereferenced.
/// \param guard A guard, which is assumed to hold when
/// dereferencing.
/// \param mode Indicates whether the dereferencing
/// is a load or store (unused).
/// \param guard: A guard, which is assumed to hold when dereferencing.
/// \param mode: Indicates whether the dereferencing is a load or store
// (unused).
virtual exprt dereference(
const exprt &pointer,
const guardt &guard,

3
src/solvers/flattening/bv_utils.cpp
View File

@ -991,11 +991,10 @@ void bv_utilst::equal_const_register(const bvt &var)
return;
}
/// The obvious recursive comparison, the interesting thing is that it is cached
/// so the literals are shared between constants.
/// \param Bit:vectors for a variable and a const to compare, note that
/// to avoid significant amounts of copying these are mutable and consumed.
/// to avoid significant amounts of copying these are mutable and consumed.
/// \return The literal that is true if and only if all the bits in var and
/// const are equal.
literalt bv_utilst::equal_const_rec(bvt &var, bvt &constant)

4
src/solvers/lowering/expr_lowering.h
View File

@ -22,8 +22,8 @@ exprt lower_byte_operators(const exprt &src, const namespacet &ns);
bool has_byte_operator(const exprt &src);
/// Lower a popcount_exprt to arithmetic and logic expressions
/// \param expr Input expression to be translated
/// \param ns Namespace for type lookups
/// \param expr: Input expression to be translated
/// \param ns: Namespace for type lookups
/// \return Semantically equivalent expression
exprt lower_popcount(const popcount_exprt &expr, const namespacet &ns);

20
src/solvers/prop/literal_expr.h
View File

@ -36,16 +36,11 @@ public:
}
};
/*! \brief Cast a generic exprt to a \ref literal_exprt
*
* This is an unchecked conversion. \a expr must be known to be \ref
* literal_exprt.
*
* \param expr Source expression
* \return Object of type \ref literal_exprt
*
* \ingroup gr_std_expr
*/
/// Cast a generic exprt to a \ref literal_exprt. This is an unchecked
/// conversion. \a expr must be known to be \ref literal_exprt.
/// \param expr: Source expression
/// \return Object of type \ref literal_exprt
/// \ingroup gr_std_expr
inline const literal_exprt &to_literal_expr(const exprt &expr)
{
PRECONDITION(expr.id() == ID_literal);
@ -54,9 +49,8 @@ inline const literal_exprt &to_literal_expr(const exprt &expr)
return static_cast<const literal_exprt &>(expr);
}
/*! \copydoc to_literal_expr(const exprt &)
* \ingroup gr_std_expr
*/
/// \copydoc to_literal_expr(const exprt &)
/// \ingroup gr_std_expr
inline literal_exprt &to_literal_expr(exprt &expr)
{
PRECONDITION(expr.id() == ID_literal);

2
src/solvers/refinement/string_builtin_function.h
View File

@ -431,7 +431,7 @@ public:
/// Functions that are not yet supported in this class but are supported by
/// string_constraint_generatort.
/// \note Ultimately this should be disappear, once all builtin function have
/// a corresponding string_builtin_functiont class.
/// a corresponding string_builtin_functiont class.
class string_builtin_function_with_no_evalt : public string_builtin_functiont
{
public:

2
src/solvers/refinement/string_constraint.cpp
View File

@ -12,7 +12,7 @@ Author: Diffblue Ltd.
#include <util/symbol_table.h>
/// Runs a solver instance to verify whether an expression can only be
// non-negative.
/// non-negative.
/// \param expr: the expression to check for negativity
/// \return true if `expr < 0` is unsatisfiable, false otherwise
static bool cannot_be_neg(const exprt &expr)

2
src/solvers/refinement/string_constraint_generator_code_points.cpp
View File

@ -186,7 +186,7 @@ std::pair<exprt, string_constraintst> add_axioms_for_code_point_before(
/// String.codePointCount java function
/// \param fresh_symbol: generator of fresh symbols
/// \param f: function application with three arguments string `str`, integer
/// `begin` and integer `end`.
/// `begin` and integer `end`.
/// \param array_pool: pool of arrays representing strings
/// \return an integer expression
std::pair<exprt, string_constraintst> add_axioms_for_code_point_count(

8
src/solvers/refinement/string_constraint_generator_comparison.cpp
View File

@ -25,7 +25,7 @@ Author: Romain Brenguier, romain.brenguier@diffblue.com
/// \lor (0 \le witness<|s_1| \land s_1[witness] \ne s_2[witness]) \f$
/// \param fresh_symbol: generator of fresh symbols
/// \param f: function application with arguments refined_string `s1` and
/// refined_string `s2`
/// refined_string `s2`
/// \param pool: pool of arrays representing strings
/// \return Boolean expression `eq`
std::pair<exprt, string_constraintst> add_axioms_for_equals(
@ -126,7 +126,7 @@ static exprt character_equals_ignore_case(
/// \land\lnot {\tt equal\_ignore\_case}(s_1[witness],s_2[witness]) \f$
/// \param fresh_symbol: generator of fresh symbols
/// \param f: function application with arguments refined_string `s1` and
/// refined_string `s2`
/// refined_string `s2`
/// \param pool: pool of arrays representing strings
/// \return Boolean expression `eq`
std::pair<exprt, string_constraintst> add_axioms_for_equals_ignore_case(
@ -234,8 +234,8 @@ string_constraint_generatort::add_axioms_for_hash_code(
/// \land res=|s1|-|s2|) \f$
/// * \f$ \forall i'<x. res\ne 0 \Rightarrow s1[i]=s2[i] \f$
/// \param fresh_symbol: generator of fresh symbols
/// \param f: function application with arguments refined_string `s1`
/// and refined_string `s2`
/// \param f: function application with arguments refined_string `s1` and
/// refined_string `s2`
/// \param pool: pool of arrays representing strings
/// \return integer expression `res`
std::pair<exprt, string_constraintst> add_axioms_for_compare_to(

8
src/solvers/refinement/string_constraint_generator_constants.cpp
View File

@ -57,7 +57,7 @@ std::pair<exprt, string_constraintst> add_axioms_for_constant(
/// Add axioms to say that the returned string expression is empty
/// \param f: function application with arguments integer `length` and character
/// pointer `ptr`.
/// pointer `ptr`.
/// \return integer expression equal to zero
std::pair<exprt, string_constraintst> add_axioms_for_empty_string(
const function_application_exprt &f)
@ -76,8 +76,8 @@ std::pair<exprt, string_constraintst> add_axioms_for_empty_string(
/// \param arg: expression of type string typet
/// \param guard: condition under which `res` should be equal to arg
/// \return 0 if constraints were added, 1 if expression could not be handled
/// and no constraint was added. Expression we can handle are of the
/// form \f$ e := "<string constant>" | (expr)? e : e \f$
/// and no constraint was added. Expression we can handle are of the form
/// \f$ e := "<string constant>" | (expr)? e : e \f$
std::pair<exprt, string_constraintst> add_axioms_for_cprover_string(
symbol_generatort &fresh_symbol,
const array_string_exprt &res,
@ -107,7 +107,7 @@ std::pair<exprt, string_constraintst> add_axioms_for_cprover_string(
/// \todo The name of the function should be changed to reflect what it does.
/// \param fresh_symbol: generator of fresh symbols
/// \param f: function application with an argument which is a string literal
/// that is a constant with a string value.
/// that is a constant with a string value.
/// \param array_pool: pool of arrays representing strings
/// \return string expression
std::pair<exprt, string_constraintst> add_axioms_from_literal(

10
src/solvers/refinement/string_constraint_generator_indexof.cpp
View File

@ -284,8 +284,8 @@ std::pair<exprt, string_constraintst> add_axioms_for_last_index_of_string(
/// \warning slow for string targets
/// \param fresh_symbol: generator of fresh symbols
/// \param f: function application with arguments refined_string `haystack`,
/// refined_string or character `needle`, and optional integer
/// `from_index` with default value `0`
/// refined_string or character `needle`, and optional integer `from_index`
/// with default value `0`
/// \param array_pool: pool of arrays representing strings
/// \return integer expression
std::pair<exprt, string_constraintst> add_axioms_for_index_of(
@ -342,7 +342,7 @@ std::pair<exprt, string_constraintst> add_axioms_for_index_of(
/// \param c: a character expression
/// \param from_index: an integer expression
/// \return integer expression `index` representing the last index of `needle`
/// in `haystack` before or at `from_index`, or `-1` if there is none
/// in `haystack` before or at `from_index`, or `-1` if there is none
std::pair<exprt, string_constraintst> add_axioms_for_last_index_of(
symbol_generatort &fresh_symbol,
const array_string_exprt &str,
@ -408,8 +408,8 @@ std::pair<exprt, string_constraintst> add_axioms_for_last_index_of(
/// \warning slow for string targets
/// \param fresh_symbol: generator of fresh symbols
/// \param f: function application with arguments refined_string `haystack`,
/// refined_string or character `needle`, and optional integer
/// `from_index` with default value `|haystack|-1`
/// refined_string or character `needle`, and optional integer
/// `from_index` with default value `|haystack|-1`
/// \param array_pool: pool of arrays representing strings
/// \return an integer expression
std::pair<exprt, string_constraintst> add_axioms_for_last_index_of(

11
src/solvers/refinement/string_constraint_generator_insert.cpp
View File

@ -29,7 +29,7 @@ Author: Romain Brenguier, romain.brenguier@diffblue.com
/// \param s2: array of characters expression
/// \param offset: integer expression
/// \return an expression expression which is different from zero if there is
/// an exception to signal
/// an exception to signal
std::pair<exprt, string_constraintst> add_axioms_for_insert(
symbol_generatort &fresh_symbol,
const array_string_exprt &res,
@ -97,12 +97,11 @@ exprt length_constraint_for_insert(
/// is considered instead of `s2`.
/// \param fresh_symbol: generator of fresh symbols
/// \param f: function application with arguments integer `|res|`, character
/// pointer `&res[0]`, refined_string `s1`, refined_string`s2`,
/// integer `offset`, optional integer `start` and optional integer
/// `end`
/// pointer `&res[0]`, refined_string `s1`, refined_string`s2`, integer
/// `offset`, optional integer `start` and optional integer `end`
/// \param pool: pool of arrays representing strings
/// \return an integer expression which is different from zero if there is
/// an exception to signal
/// \return an integer expression which is different from zero if there is an
/// exception to signal
std::pair<exprt, string_constraintst> add_axioms_for_insert(
symbol_generatort &fresh_symbol,
const function_application_exprt &f,

16
src/solvers/refinement/string_constraint_generator_main.cpp
View File

@ -167,7 +167,7 @@ const std::set<array_string_exprt> &array_poolt::created_strings() const
/// is infinite, a new integer symbol is created and stored in `array_pool`.
/// This also adds the default axioms for `arr`.
/// \param f: a function application with argument a character array `arr` and
/// a character pointer `ptr`.
/// a character pointer `ptr`.
exprt string_constraint_generatort::associate_array_to_pointer(
const function_application_exprt &f)
{
@ -188,7 +188,7 @@ exprt string_constraint_generatort::associate_array_to_pointer(
/// Associate an integer length to a char array.
/// This adds an axiom ensuring that `arr.length` and `length` are equal.
/// \param f: a function application with argument a character array `arr` and
/// a integer `length`.
/// an integer `length`.
/// \return integer expression equal to 0
exprt string_constraint_generatort::associate_length_to_array(
const function_application_exprt &f)
@ -247,8 +247,8 @@ void merge(string_constraintst &result, string_constraintst other)
/// \param start: index of the first character to constrain
/// \param end: index at which we stop adding constraints
/// \param char_set: a string of the form "<low_char>-<high_char>" where
/// `<low_char>` and `<high_char>` are two characters, which represents
/// the set of characters that are between `low_char` and `high_char`.
/// `<low_char>` and `<high_char>` are two characters, which represents the
/// set of characters that are between `low_char` and `high_char`.
/// \return a string expression that is linked to the argument through axioms
/// that are added to the list
string_constraintst add_constraint_on_characters(
@ -283,8 +283,8 @@ string_constraintst add_constraint_on_characters(
/// `char_set` if \f$low_char \le c \le high_char\f$.
/// \param fresh_symbol: generator of fresh symbols
/// \param f: a function application with arguments: integer `|s|`, character
/// pointer `&s[0]`, string `char_set_string`,
/// optional integers `start` and `end`
/// pointer `&s[0]`, string `char_set_string`, optional integers `start` and
/// `end`
/// \param array_pool: pool of arrays representing strings
/// \return integer expression whose value is zero
std::pair<exprt, string_constraintst> add_axioms_for_constrain_characters(
@ -483,7 +483,7 @@ string_constraint_generatort::add_axioms_for_function_application(
/// \deprecated should use substring instead
/// \param fresh_symbol: generator of fresh symbols
/// \param f: function application with one argument, which is a string,
/// or three arguments: string, integer offset and count
/// or three arguments: string, integer offset and count
/// \param array_pool: pool of arrays representing strings
/// \return a new string expression
DEPRECATED("should use substring instead")
@ -587,7 +587,7 @@ exprt maximum(const exprt &a, const exprt &b)
}
/// Returns a non-negative version of the argument.
/// \param expr: expression of which we want a non-negative version
/// \param expr: expression of which we want a non-negative version
/// \return `max(0, expr)`
exprt zero_if_negative(const exprt &expr)
{

10
src/solvers/refinement/string_constraint_generator_testing.cpp
View File

@ -90,10 +90,10 @@ std::pair<exprt, string_constraintst> add_axioms_for_is_prefix(
/// \todo Get rid of the boolean flag.
/// \param fresh_symbol: generator of fresh symbols
/// \param f: a function application with arguments refined_string `s0`,
/// refined string `s1` and optional integer argument `offset`
/// whose default value is 0
/// refined string `s1` and optional integer argument `offset`whose default
/// value is 0
/// \param swap_arguments: a Boolean telling whether the prefix is the second
/// argument or the first argument
/// argument or the first argument
/// \param array_pool: pool of arrays representing strings
/// \return boolean expression `isprefix`
std::pair<exprt, string_constraintst> add_axioms_for_is_prefix(
@ -159,9 +159,9 @@ std::pair<exprt, string_constraintst> add_axioms_for_is_empty(
/// \todo The primitive should be renamed `ends_with`.
/// \param fresh_symbol: generator of fresh symbols
/// \param f: a function application with arguments refined_string `s0`
/// and refined_string `s1`
/// and refined_string `s1`
/// \param swap_arguments: boolean flag telling whether the suffix is the second
/// argument or the first argument
/// argument or the first argument
/// \param array_pool: pool of arrays representing strings
/// \return Boolean expression `issuffix`
DEPRECATED("should use `strings_startwith(s0, s1, s1.length - s0.length)`")

23
src/solvers/refinement/string_constraint_generator_transformation.cpp
View File

@ -31,7 +31,7 @@ Author: Romain Brenguier, romain.brenguier@diffblue.com
/// \todo We can reduce the number of constraints by merging 2 and 3.
/// \param fresh_symbol: generator of fresh symbols
/// \param f: function application with arguments integer `|res|`, character
/// pointer `&res[0]`, refined_string `s1`, integer `k`
/// pointer `&res[0]`, refined_string `s1`, integer `k`
/// \param array_pool: pool of arrays representing strings
/// \return integer expression equal to `0`
std::pair<exprt, string_constraintst> add_axioms_for_set_length(
@ -86,11 +86,11 @@ std::pair<exprt, string_constraintst> add_axioms_for_set_length(
/// tan the end index.
/// \param fresh_symbol: generator of fresh symbols
/// \param f: function application with arguments integer `|res|`, character
/// pointer `&res[0]`, refined_string `str`, integer `start`,
/// optional integer `end` with default value `|str|`.
/// pointer `&res[0]`, refined_string `str`, integer `start`, optional integer
/// `end` with default value `|str|`.
/// \param array_pool: pool of arrays representing strings
/// \return integer expression which is different from 0 when there is an
/// exception to signal
/// exception to signal
std::pair<exprt, string_constraintst> add_axioms_for_substring(
symbol_generatort &fresh_symbol,
const function_application_exprt &f,
@ -176,10 +176,10 @@ std::pair<exprt, string_constraintst> add_axioms_for_substring(
/// \note Some of the constraints among 1, 2, 3, 4 and 5 seems to be redundant
/// \param fresh_symbol: generator of fresh symbols
/// \param f: function application with arguments integer `|res|`, character
/// pointer `&res[0]`, refined_string `str`.
/// pointer `&res[0]`, refined_string `str`.
/// \param array_pool: pool of arrays representing strings
/// \return integer expression which is different from 0 when there is an
/// exception to signal
/// exception to signal
std::pair<exprt, string_constraintst> add_axioms_for_trim(
symbol_generatort &fresh_symbol,
const function_application_exprt &f,
@ -248,8 +248,8 @@ std::pair<exprt, string_constraintst> add_axioms_for_trim(
/// If both expressions are characters, return pair of them
/// If both expressions are 1-length strings, return first character of each
/// Otherwise return empty optional
/// \param expr1 First expression
/// \param expr2 Second expression
/// \param expr1: First expression
/// \param expr2: Second expression
/// \param get_string_expr: Function that yields an array_string_exprt
/// corresponding to either `expr1` or `expr2`, for the case where they are
/// not primitive chars.
@ -290,8 +290,8 @@ static optionalt<std::pair<exprt, exprt>> to_char_pair(
/// be fixed in the future)
/// \param fresh_symbol: generator of fresh symbols
/// \param f: function application with arguments integer `|res|`, character
/// pointer `&res[0]`, refined_string `str`, character `old_char` and
/// character `new_char`
/// pointer `&res[0]`, refined_string `str`, character `old_char` and
/// character `new_char`
/// \param array_pool: pool of arrays representing strings
/// \return an integer expression equal to 0
std::pair<exprt, string_constraintst> add_axioms_for_replace(
@ -404,8 +404,7 @@ std::pair<exprt, string_constraintst> add_axioms_for_delete(
/// (More...) \endlink
/// \param fresh_symbol: generator of fresh symbols
/// \param f: function application with arguments integer `|res|`, character
/// pointer `&res[0]`, refined_string `str`, integer `start`
/// and integer `end`
/// pointer `&res[0]`, refined_string `str`, integer `start` and integer `end`
/// \param array_pool: pool of arrays representing strings
/// \return an integer expression whose value is different from 0 to signal
/// an exception

10
src/solvers/refinement/string_constraint_generator_valueof.cpp
View File

@ -286,9 +286,9 @@ std::pair<exprt, string_constraintst> add_axioms_from_int_hex(
/// \copybrief add_axioms_from_char(const array_string_exprt &res, const exprt &c)
// NOLINTNEXTLINE
/// \link add_axioms_from_char(const array_string_exprt &res, const exprt &c)
/// (More...) \endlink
/// (More...) \endlink
/// \param f: function application with arguments integer `|res|`, character
/// pointer `&res[0]` and character `c`
/// pointer `&res[0]` and character `c`
/// \param array_pool: pool of arrays representing strings
/// \return code 0 on success
std::pair<exprt, string_constraintst> add_axioms_from_char(
@ -408,7 +408,7 @@ string_constraintst add_axioms_for_correct_number_format(
/// \param input_int: the integer represented by str
/// \param type: the type for input_int
/// \param strict_formatting: if true, don't allow a leading plus, redundant
/// zeros or upper case letters
/// zeros or upper case letters
/// \param str: input string
/// \param max_string_length: the maximum length str can have
/// \param radix: the radix, with the same type as input_int
@ -502,7 +502,7 @@ string_constraintst add_axioms_for_characters_in_integer_string(
/// to the value represented by `str`
/// \param fresh_symbol: generator of fresh symbols
/// \param f: a function application with arguments refined_string `str` and
/// an optional integer for the radix
/// an optional integer for the radix
/// \param array_pool: pool of arrays representing strings
/// \param ns: namespace
/// \return integer expression equal to the value represented by `str`
@ -555,7 +555,7 @@ std::pair<exprt, string_constraintst> add_axioms_for_parse_int(
/// radix is 10 then check if the character is in the range 0-9.
/// \param chr: the character
/// \param strict_formatting: if true, don't allow upper case characters
/// \param radix_as_char: the radix as an expression of the same type as chr
/// \param radix_as_char: the radix as an expression of the same type as chr
/// \param radix_ul: the radix, which should be between 2 and 36, or 0, in
/// which case the return value will work for any radix
/// \return an expression for the condition

28
src/solvers/refinement/string_refinement.cpp
View File

@ -53,9 +53,9 @@ static optionalt<exprt> find_counter_example(
/// * we give lemma `b` to a fresh solver;
/// * if no counter-example to `b` is found, this means the constraint `a`
/// is satisfied by the valuation given by get.
/// \return `true` if the current model satisfies all the axioms,
/// `false` otherwise with a list of lemmas which are obtained by
/// instantiating constraints at indexes given by counter-examples.
/// \return `true` if the current model satisfies all the axioms, `false`
/// otherwise with a list of lemmas which are obtained by instantiating
/// constraints at indexes given by counter-examples.
static std::pair<bool, std::vector<exprt>> check_axioms(
const string_axiomst &axioms,
string_constraint_generatort &generator,
@ -308,7 +308,7 @@ void string_refinementt::set_to(const exprt &expr, bool value)
/// \param ns: namespace
/// \param stream: output stream
/// \return union_find_replacet where char pointer that have been set equal
/// by an equation are associated to the same element
/// by an equation are associated to the same element
static void add_equations_for_symbol_resolution(
union_find_replacet &symbol_solver,
const std::vector<equal_exprt> &equations,
@ -845,7 +845,7 @@ decision_proceduret::resultt string_refinementt::dec_solve()
/// Add the given lemma to the solver.
/// \param lemma: a Boolean expression
/// \param simplify_lemma: whether the lemma should be simplified before being
/// given to the underlying solver.
/// given to the underlying solver.
void string_refinementt::add_lemma(
const exprt &lemma,
const bool simplify_lemma)
@ -892,7 +892,7 @@ void string_refinementt::add_lemma(
/// Get a model of an array and put it in a certain form.
/// If the model is incomplete or if it is too big, return no value.
/// \param super_get: function returning the valuation of an expression
/// in a model
/// in a model
/// \param ns: namespace
/// \param stream: output stream for warning messages
/// \param arr: expression of type array representing a string
@ -1055,7 +1055,7 @@ void debug_model(
/// array valuations coming from the underlying solver are given.
/// \param index: An index with which to build the equality condition
/// \param left_propagate: If set to true, the expression will look like
/// `index<=0 ? 24 : index<=2 ? 42 : 12`
/// `index<=0 ? 24 : index<=2 ? 42 : 12`
/// \return An expression containing no 'with' expression
static exprt substitute_array_access(
const with_exprt &expr,
@ -1162,9 +1162,9 @@ static void substitute_array_access_in_place(
/// something like: `index <= 0 ? 24 : index <= 2 ? 42 : 12`
/// \param expr: an expression containing array accesses
/// \param symbol_generator: function which given a prefix and a type generates
/// a fresh symbol of the given type
/// a fresh symbol of the given type
/// \param left_propagate: should values be propagated to the left in with
/// expressions
/// expressions
/// \return an expression containing no array access
exprt substitute_array_access(
exprt expr,
@ -1185,7 +1185,7 @@ exprt substitute_array_access(
/// \param constraint: the not_contains constraint to add the negation of
/// \param univ_var: the universal variable for the negation of the axiom
/// \param get: valuation function, the result should have been simplified
/// \return: the negation of the axiom under the current evaluation
/// \return the negation of the axiom under the current evaluation
static exprt negation_of_not_contains_constraint(
const string_not_contains_constraintt &constraint,
const symbol_exprt &univ_var,
@ -1519,7 +1519,7 @@ exprt simplify_sum(const exprt &f)
/// \param qvar: a symbol representing a universally quantified variable
/// \param val: an expression
/// \param f: an expression containing `+` and `-`
/// operations in which `qvar` should appear exactly once.
/// operations in which `qvar` should appear exactly once.
/// \return an expression corresponding of $f^{-1}(val)$ where $f$ is seen as
/// a function of $qvar$, i.e. the value that is necessary for `qvar` for `f`
/// to be equal to `val`. For instance, if `f` corresponds to the expression
@ -1622,7 +1622,7 @@ static void update_index_set(
/// An expression representing an array of characters can be in the form of an
/// if expression for instance `cond?array1:(cond2:array2:array3)`.
/// We return all the array expressions contained in `array_expr`.
/// \param array_expr : an expression representing an array
/// \param array_expr: an expression representing an array
/// \param accu: a vector to which symbols and constant arrays contained in the
/// expression will be appended
static void get_sub_arrays(const exprt &array_expr, std::vector<exprt> &accu)
@ -2039,8 +2039,8 @@ exprt string_refinementt::get(const exprt &expr) const
/// \param ns: namespace
/// \param [in] axiom: the axiom to be checked
/// \param [in] var: the variable whose evaluation will be stored in witness
/// \return: the witness of the satisfying assignment if one
/// exists. If UNSAT, then behaviour is undefined.
/// \return the witness of the satisfying assignment if one
/// exists. If UNSAT, then behaviour is undefined.
static optionalt<exprt> find_counter_example(
const namespacet &ns,
const exprt &axiom,

7
src/solvers/refinement/string_refinement_util.h
View File

@ -39,10 +39,9 @@ bool is_char_pointer_type(const typet &type);
/// \param type: a type
/// \param ns: namespace
/// \return true if a subtype of `type` is an pointer of characters.
/// The meaning of "subtype" is in the algebraic datatype sense:
/// for example, the subtypes of a struct are the types of its
/// components, the subtype of a pointer is the type it points to,
/// etc...
/// The meaning of "subtype" is in the algebraic datatype sense: for example,
/// the subtypes of a struct are the types of its components, the subtype of
/// a pointer is the type it points to, etc...
bool has_char_pointer_subtype(const typet &type, const namespacet &ns);
/// \param expr: an expression

6
src/util/allocate_objects.cpp
View File

@ -235,7 +235,7 @@ exprt allocate_objectst::allocate_non_dynamic_object(
/// Add a pointer to a symbol to the list of pointers to symbols created so far
///
/// \param symbol_ptr pointer to a symbol in the symbol table
/// \param symbol_ptr: pointer to a symbol in the symbol table
void allocate_objectst::add_created_symbol(const symbolt *symbol_ptr)
{
symbols_created.push_back(symbol_ptr);
@ -243,7 +243,7 @@ void allocate_objectst::add_created_symbol(const symbolt *symbol_ptr)
/// Adds declarations for all non-static symbols created
///
/// \param init_code code block to which to add the declarations
/// \param init_code: code block to which to add the declarations
void allocate_objectst::declare_created_symbols(code_blockt &init_code)
{
// Add the following code to init_code for each symbol that's been created:
@ -261,7 +261,7 @@ void allocate_objectst::declare_created_symbols(code_blockt &init_code)
/// Adds code to mark the created symbols as input
///
/// \param init_code code block to which to add the generated code
/// \param init_code: code block to which to add the generated code
void allocate_objectst::mark_created_symbols_as_input(code_blockt &init_code)
{
// Add the following code to init_code for each symbol that's been created:

6
src/util/arith_tools.cpp
View File

@ -324,7 +324,7 @@ static char nibble2hex(unsigned char nibble)
/// construct a bit-vector representation from a functor
/// \param width: the width of the bit-vector
/// \param f: the functor -- the parameter is the bit index
/// \returns new bitvector representation
/// \return new bitvector representation
irep_idt
make_bvrep(const std::size_t width, const std::function<bool(std::size_t)> f)
{
@ -369,7 +369,7 @@ make_bvrep(const std::size_t width, const std::function<bool(std::size_t)> f)
/// \param b: the representation of the second bit vector
/// \param width: the width of the bit-vector
/// \param f: the functor
/// \returns new bitvector representation
/// \return new bitvector representation
irep_idt bvrep_bitwise_op(
const irep_idt &a,
const irep_idt &b,
@ -386,7 +386,7 @@ irep_idt bvrep_bitwise_op(
/// \param a: the bit-vector representation
/// \param width: the width of the bit-vector
/// \param f: the functor
/// \returns new bitvector representation
/// \return new bitvector representation
irep_idt bvrep_bitwise_op(
const irep_idt &a,
const std::size_t width,

4
src/util/arith_tools.h
View File

@ -117,8 +117,8 @@ public:
/// Converts an expression to any integral type
/// \tparam Target: type to convert to
/// \param arg: expression to convert
/// \return optional integer of type Target if conversion is possible,
/// empty optional otherwise.
/// \return optional integer of type Target if conversion is possible, empty
/// optional otherwise.
template <typename Target>
optionalt<Target> numeric_cast(const exprt &arg)
{

Some files were not shown because too many files have changed in this diff Show More