Added appropriate const modifiers to local_value_set_analysist

Author: NathanJPhillips

cbmc/src/pointer-analysis/value_set_analysis.h

@@ -73,7 +73,7 @@ class value_set_analysis_templatet:
   /// \param values: The set of expressions to check.
   /// \return true, if it contains only one expression and that expression is a
   ///   symbol, false, otherwise.
-  virtual bool is_singular(const std::set<exprt> &values)
+  virtual bool is_singular(const std::set<exprt> &values) const
   {
     return values.size()==1 && values.begin()->id()==ID_symbol;
   }

src/pointer-analysis/local_value_set_analysis.cpp

@@ -653,7 +653,7 @@ static void get_reachable_objects(
   }
 }
 
-bool local_value_set_analysist::is_singular(const std::set<exprt> &values)
+bool local_value_set_analysist::is_singular(const std::set<exprt> &values) const
 {
   if(values.size() != 1)
     return false;
@@ -980,7 +980,7 @@ void local_value_set_analysist::reconstruct_all_value_sets(
 }
 
 void local_value_set_analysist::get_values_reconstructed(
-  locationt l, const exprt &expr, value_setst::valuest &dest)
+  locationt l, const exprt &expr, value_setst::valuest &dest) const
 {
   optionalt<local_value_set_domaint> reconstructed_value_set =
     reconstruct_value_set(l);
@@ -994,7 +994,7 @@ void local_value_set_analysist::get_values_reconstructed(
 }
 
 void local_value_set_analysist::get_references_reconstructed(
-  locationt l, const exprt &expr, value_setst::valuest &dest)
+  locationt l, const exprt &expr, value_setst::valuest &dest) const
 {
   optionalt<local_value_set_domaint> reconstructed_value_set =
     reconstruct_value_set(l);
@@ -1008,7 +1008,7 @@ void local_value_set_analysist::get_references_reconstructed(
 }
 
 optionalt<local_value_set_domaint>
-local_value_set_analysist::reconstruct_value_set(locationt l)
+local_value_set_analysist::reconstruct_value_set(locationt l) const
 {
   locationt walk_instruction = l;
 

src/pointer-analysis/local_value_set_analysis.h

@@ -241,15 +241,15 @@ class local_value_set_analysist
   /// \return true, if the set contains only one element and that element is
   ///   either a most-recent-allocation dynamic-object or a symbol (treated in the
   ///   call to the base class). false, otherwise.
-  virtual bool is_singular(const std::set<exprt> &) override;
+  virtual bool is_singular(const std::set<exprt> &) const override;
 
-  optionalt<local_value_set_domaint> reconstruct_value_set(locationt l);
+  optionalt<local_value_set_domaint> reconstruct_value_set(locationt l) const;
 
   void get_values_reconstructed(
-    locationt l, const exprt &expr, value_setst::valuest &dest);
+    locationt l, const exprt &expr, value_setst::valuest &dest) const;
 
   void get_references_reconstructed(
-    locationt l, const exprt &expr, value_setst::valuest &dest);
+    locationt l, const exprt &expr, value_setst::valuest &dest) const;
 
   void reconstruct_all_value_sets(const goto_programt &);
 

src/taint-analysis/taint_summary.cpp

@@ -173,7 +173,7 @@ static exprt transform_external_objects(const exprt& e)
 static void collect_lvsa_access_paths(
   const exprt &query,
   const namespacet &ns,
-  local_value_set_analysist &lvsa,
+  const local_value_set_analysist &lvsa,
   const instruction_iteratort &instit,
   std::set<exprt> &result)
 {
@@ -246,7 +246,7 @@ static void collect_lvsa_access_paths(
 static void collect_lvsa_access_paths(
   const exprt &query_in,
   const namespacet &ns,
-  local_value_set_analysist& lvsa,
+  const local_value_set_analysist &lvsa,
   const instruction_iteratort &instit,
   object_numberingt& taint_object_numbering,
   lvalue_numbers_sett& result,
@@ -272,7 +272,7 @@ static void collect_lvsa_access_paths(
   const exprt &query_in,
   namespacet const& ns,
   lvalue_numbers_sett &result,
-  local_value_set_analysist& lvsa,
+  const local_value_set_analysist &lvsa,
   const instruction_iteratort &instit,
   object_numberingt& taint_object_numbering)
 {
@@ -291,7 +291,7 @@ static void collect_lvsa_access_paths(
 }
 
 static void populate_formals_to_actuals(
-  local_value_set_analysist& lvsa,
+  const local_value_set_analysist &lvsa,
   const irep_idt& fname,
   const goto_programt& prog,
   const namespacet& ns,
@@ -383,7 +383,7 @@ bool taint_algorithm_computing_summary_of_functiont::
   collect_lvsa_access_paths_extended(
     const exprt &expr,
     const instruction_iteratort &it,
-    local_value_set_analysist &lvsa,
+    const local_value_set_analysist &lvsa,
     lvalue_numbers_sett &result,
     const bool generate_fresh_evs)
 {
@@ -585,7 +585,7 @@ void  taint_algorithm_computing_summary_of_functiont::
     const std::shared_ptr<taint_summaryt> summary,
     const code_function_callt &fn_call,
     const code_typet &fn_type,
-    local_value_set_analysist &lvsa,
+    const local_value_set_analysist &lvsa,
     const instruction_iteratort &Iit,
     const irep_idt &caller_ident)
 {
@@ -663,7 +663,7 @@ void taint_algorithm_computing_summary_of_functiont::
     const code_function_callt &fn_call,
     const code_typet &fn_type,
     const instruction_iteratort &Iit,
-    local_value_set_analysist &lvsa)
+    const local_value_set_analysist &lvsa)
 {
   TMPROF_BLOCK();
 
@@ -716,7 +716,7 @@ void taint_algorithm_computing_summary_of_functiont::initialise_domain(
   taint_summaryt::dbt &database,
   taint_summaryt &caller_summary,
   written_expressionst &written,
-  local_value_set_analysist &lvsa,
+  const local_value_set_analysist &lvsa,
   const std::map<goto_programt::const_targett, goto_programt::const_targetst>
     &inst_predecessors)
 {
@@ -859,7 +859,7 @@ void taint_algorithm_computing_summary_of_functiont::handle_assignment(
   const taint_summary_inputt &input,
   numbered_lvalue_to_taint_mapt& result,
   const instruction_iteratort &Iit,
-  local_value_set_analysist &lvsa)
+  const local_value_set_analysist &lvsa)
 {
   TMPROF_BLOCK();
 
@@ -906,7 +906,7 @@ taint_sett taint_algorithm_computing_summary_of_functiont::
   compute_taint_of_aliased_numbers_of_lvalue(
     const taint_lvaluet &lvalue,
     const instruction_iteratort &Iit,
-    local_value_set_analysist &lvsa,
+    const local_value_set_analysist &lvsa,
     const taint_summary_inputt &input,
     const numbered_lvalue_to_taint_mapt &a)
 {
@@ -936,7 +936,7 @@ void taint_algorithm_computing_summary_of_functiont::
     const taint_sett &taint_from_rule,
     const bool is_allowed_pure_assignment,
     const instruction_iteratort &Iit,
-    local_value_set_analysist &lvsa,
+    const local_value_set_analysist &lvsa,
     numbered_lvalue_to_taint_mapt &result)
 {
   TMPROF_BLOCK();
@@ -967,7 +967,7 @@ numbered_lvalue_to_taint_mapt taint_algorithm_computing_summary_of_functiont::
     const irep_idt &caller_ident,
     const taint_summary_inputt &input,
     taint_summaryt::dbt &database,
-    local_value_set_analysist &lvsa,
+    const local_value_set_analysist &lvsa,
     taint_transition_propertiest &transition_properties)
 {
   TMPROF_BLOCK();
@@ -1446,7 +1446,7 @@ void taint_algorithm_computing_summary_of_functiont::
     const goto_functionst::goto_functiont &fn_to_summarise,
     taint_summaryt &summary,
     const written_expressionst &written,
-    local_value_set_analysist &lvsa)
+    const local_value_set_analysist &lvsa)
 {
   TMPROF_BLOCK();
 

src/taint-analysis/taint_summary.h

@@ -209,7 +209,7 @@ class taint_algorithm_computing_summary_of_functiont
   bool collect_lvsa_access_paths_extended(
     const exprt &expr,
     const instruction_iteratort &it,
-    local_value_set_analysist &lvsa,
+    const local_value_set_analysist &lvsa,
     lvalue_numbers_sett &result,
     const bool generate_fresh_evs = true);
 
@@ -245,7 +245,7 @@ class taint_algorithm_computing_summary_of_functiont
     const std::shared_ptr<taint_summaryt> summary,
     const code_function_callt &fn_call,
     const code_typet &fn_type,
-    local_value_set_analysist &lvsa,
+    const local_value_set_analysist &lvsa,
     const instruction_iteratort &Iit,
     const irep_idt &caller_ident);
 
@@ -257,15 +257,15 @@ class taint_algorithm_computing_summary_of_functiont
     const code_function_callt &fn_call,
     const code_typet &fn_type,
     const instruction_iteratort &Iit,
-    local_value_set_analysist &lvsa);
+    const local_value_set_analysist &lvsa);
 
   void initialise_domain(
     const irep_idt &function_id,
     const goto_functionst::goto_functiont &function,
     taint_summaryt::dbt &database,
     taint_summaryt &caller_summary,
     written_expressionst &written,
-    local_value_set_analysist &lvsa,
+    const local_value_set_analysist &lvsa,
     const std::map<goto_programt::const_targett, goto_programt::const_targetst>
       &inst_predecessors);
 
@@ -275,12 +275,12 @@ class taint_algorithm_computing_summary_of_functiont
     const taint_summary_inputt &input,
     numbered_lvalue_to_taint_mapt& result,
     instruction_iteratort const& Iit,
-    local_value_set_analysist &lvsa);
+    const local_value_set_analysist &lvsa);
 
   taint_sett compute_taint_of_aliased_numbers_of_lvalue(
     const taint_lvaluet &lvalue,
     const instruction_iteratort &Iit,
-    local_value_set_analysist &lvsa,
+    const local_value_set_analysist &lvsa,
     const taint_summary_inputt &input,
     const numbered_lvalue_to_taint_mapt &a);
 
@@ -289,7 +289,7 @@ class taint_algorithm_computing_summary_of_functiont
     const taint_sett &value_from_rule,
     const bool is_allowed_pure_assignment,
     const instruction_iteratort &Iit,
-    local_value_set_analysist &lvsa,
+    const local_value_set_analysist &lvsa,
     numbered_lvalue_to_taint_mapt &result);
 
   numbered_lvalue_to_taint_mapt  transform(
@@ -298,15 +298,15 @@ class taint_algorithm_computing_summary_of_functiont
     const irep_idt &caller_ident,
     const taint_summary_inputt &input,
     taint_summaryt::dbt &database,
-    local_value_set_analysist &lvsa,
+    const local_value_set_analysist &lvsa,
     taint_transition_propertiest &transition_properties);
 
   void build_summary_from_computed_domain(
     const irep_idt fn_id,
     const goto_functionst::goto_functiont &fn_to_summarise,
     taint_summaryt &summary,
     const written_expressionst &written,
-    local_value_set_analysist &lvsa);
+    const local_value_set_analysist &lvsa);
 
   const taint_programt *program;
   const taint_rulest *transition_rules;