From b854fcdd5079024225e4da652f48001d07934f43 Mon Sep 17 00:00:00 2001 From: Thomas Spriggs Date: Tue, 12 Sep 2023 17:48:42 +0100 Subject: [PATCH 1/4] Fix spelling of arbitrary --- src/solvers/smt2_incremental/object_tracking.h | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/solvers/smt2_incremental/object_tracking.h b/src/solvers/smt2_incremental/object_tracking.h index 24563e7abd2..89bfba0af9c 100644 --- a/src/solvers/smt2_incremental/object_tracking.h +++ b/src/solvers/smt2_incremental/object_tracking.h @@ -57,7 +57,7 @@ struct decision_procedure_objectt /// assigned. exprt find_object_base_expression(const address_of_exprt &address_of); -/// Arbitary expressions passed to the decision procedure may have multiple +/// Arbitrary expressions passed to the decision procedure may have multiple /// address of operations as its sub expressions. This means the overall /// expression may contain multiple base objects which need to be assigned /// unique identifiers. From 1ac9052338ec36ac6b60101ea25e8bc70a78cbc9 Mon Sep 17 00:00:00 2001 From: Thomas Spriggs Date: Tue, 12 Sep 2023 20:22:31 +0100 Subject: [PATCH 2/4] Fix spelling of dereferencing --- src/solvers/smt2_incremental/object_tracking.h | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/solvers/smt2_incremental/object_tracking.h b/src/solvers/smt2_incremental/object_tracking.h index 89bfba0af9c..15403e50447 100644 --- a/src/solvers/smt2_incremental/object_tracking.h +++ b/src/solvers/smt2_incremental/object_tracking.h @@ -40,7 +40,7 @@ struct decision_procedure_objectt { /// The expression for the root of the object. This is expression equivalent - /// to deferencing a pointer to this object with a zero offset. + /// to dereferencing a pointer to this object with a zero offset. exprt base_expression; /// Number which uniquely identifies this particular object. std::size_t unique_id = 0; From 6c516b3bb99cf68245beea7dc43d1ccd5ef47b21 Mon Sep 17 00:00:00 2001 From: Thomas Spriggs Date: Wed, 13 Sep 2023 11:46:00 +0100 Subject: [PATCH 3/4] Document `get_problem_messages` --- .../smt2_incremental/smt2_incremental_decision_procedure.cpp | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp b/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp index 16b26ce3a3f..071b469f91c 100644 --- a/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp +++ b/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp @@ -40,6 +40,8 @@ static smt_responset get_response_to_command( return response; } +/// Returns a message string describing the problem in the case where the +/// response from the solver is an error status. Returns empty otherwise. static optionalt get_problem_messages(const smt_responset &response) { From d93d3a16a92dbcf99285364f2f6b52a6f059c1c6 Mon Sep 17 00:00:00 2001 From: Thomas Spriggs Date: Wed, 13 Sep 2023 17:44:47 +0100 Subject: [PATCH 4/4] Document `ensure_handle_for_expr_defined` --- .../smt2_incremental/smt2_incremental_decision_procedure.h | 3 +++ 1 file changed, 3 insertions(+) diff --git a/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.h b/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.h index 36eaba4da64..7dcc0278e95 100644 --- a/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.h +++ b/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.h @@ -94,6 +94,9 @@ class smt2_incremental_decision_proceduret final /// \brief Defines any functions which \p expr depends on, which have not yet /// been defined, along with their dependencies in turn. void define_dependent_functions(const exprt &expr); + /// If a function has not been defined for handling \p expr, then a new + /// function is defined. If the corresponding function exists already, then + /// no action is taken. void ensure_handle_for_expr_defined(const exprt &expr); /// \brief Add objects in \p expr to object_map if needed and convert to smt. /// \note This function is non-const because it mutates the object_map.