CONTRACTS: use size_t for assigns clause size

Author: Remi Delmas

src/goto-instrument/contracts/dynamic-frames/dfcc.cpp

@@ -113,7 +113,7 @@ dfcct::dfcct(goto_modelt &goto_model, messaget &log)
       instrument,
       spec_functions,
       dsl_contract_handler),
-    max_assigns_clause_size(-1)
+    max_assigns_clause_size(0)
 {
 }
 
@@ -333,7 +333,7 @@ void dfcct::transform_goto_model(
       other_symbols.erase(wrapper_id);
 
     // upate max contract size
-    const int assigns_clause_size =
+    const std::size_t assigns_clause_size =
       dsl_contract_handler.get_assigns_clause_size(contract_id);
     if(assigns_clause_size > max_assigns_clause_size)
       max_assigns_clause_size = assigns_clause_size;

src/goto-instrument/contracts/dynamic-frames/dfcc.h

@@ -196,7 +196,7 @@ class dfcct
 
   /// Tracks the maximum number of targets in any assigns clause handled in the
   /// transformation (used to specialize/unwind loops in DFCC library functions)
-  int max_assigns_clause_size;
+  std::size_t max_assigns_clause_size;
 
   /// Checks preconditions on arguments of \ref transform_goto_model.
   ///

src/goto-instrument/contracts/dynamic-frames/dfcc_contract_handler.h

@@ -71,7 +71,8 @@ class dfcc_contract_handlert
 
   /// Returns the size of the assigns clause of the given contract_id
   /// in number of targets.
-  virtual const int get_assigns_clause_size(const irep_idt &contract_id) = 0;
+  virtual const std::size_t
+  get_assigns_clause_size(const irep_idt &contract_id) = 0;
 };
 
 #endif

src/goto-instrument/contracts/dynamic-frames/dfcc_dsl_contract_functions.cpp

@@ -83,12 +83,12 @@ dfcc_dsl_contract_functionst::get_spec_frees_function_symbol() const
   return ns.lookup(spec_frees_function_id);
 }
 
-const int dfcc_dsl_contract_functionst::get_nof_assigns_targets() const
+const std::size_t dfcc_dsl_contract_functionst::get_nof_assigns_targets() const
 {
   return nof_assigns_targets;
 }
 
-const int dfcc_dsl_contract_functionst::get_nof_frees_targets() const
+const std::size_t dfcc_dsl_contract_functionst::get_nof_frees_targets() const
 {
   return nof_frees_targets;
 }
@@ -118,10 +118,8 @@ void dfcc_dsl_contract_functionst::gen_spec_assigns_function()
   {
     // use a dummy symbol for __CPROVER_return_value
     // which does occur in the assigns clause anyway
-    symbolt dummy;
-    dummy.name = "dummy_return_value";
-    dummy.type = code_with_contract.return_type();
-    lambda_parameters.push_back(dummy.symbol_expr());
+    lambda_parameters.push_back(
+      symbol_exprt("dummy_return_value", code_with_contract.return_type()));
   }
 
   for(const auto &param_id : spec_code_type.parameter_identifiers())

src/goto-instrument/contracts/dynamic-frames/dfcc_dsl_contract_functions.h

@@ -87,10 +87,10 @@ class dfcc_dsl_contract_functionst
   const symbolt &get_spec_frees_function_symbol() const;
 
   /// Returns the maximum number of targets in the assigns clause
-  const int get_nof_assigns_targets() const;
+  const std::size_t get_nof_assigns_targets() const;
 
   /// Returns the maximum number of targets in the frees clause
-  const int get_nof_frees_targets() const;
+  const std::size_t get_nof_frees_targets() const;
 
   /// The function symbol carrying the contract
   const symbolt &pure_contract_symbol;

src/goto-instrument/contracts/dynamic-frames/dfcc_dsl_contract_handler.cpp

@@ -75,7 +75,7 @@ dfcc_dsl_contract_handlert::get_contract_functions(const irep_idt &contract_id)
   return dfcc_dsl_contract_handlert::contract_cache.at(contract_id);
 }
 
-const int
+const std::size_t
 dfcc_dsl_contract_handlert::get_assigns_clause_size(const irep_idt &contract_id)
 {
   return get_contract_functions(contract_id).get_nof_assigns_targets();

src/goto-instrument/contracts/dynamic-frames/dfcc_dsl_contract_handler.h

@@ -96,7 +96,7 @@ class dfcc_dsl_contract_handlert : public dfcc_contract_handlert
     std::set<irep_idt> &function_pointer_contracts) override;
 
   /// Returns the size assigns clause of the given contract in number of targets
-  const int get_assigns_clause_size(const irep_idt &contract_id) override;
+  const std::size_t get_assigns_clause_size(const irep_idt &contract_id) override;
 
   /// Searches for a symbol named "contract::contract_id" that has a type
   /// signature compatible with that of "contract_id", or creates an empty one

src/goto-instrument/contracts/dynamic-frames/dfcc_library.cpp

@@ -413,7 +413,7 @@ static const std::map<dfcc_funt, int> to_unwind = {
 
 bool dfcc_libraryt::specialized = false;
 
-void dfcc_libraryt::specialize(const int contract_assigns_size)
+void dfcc_libraryt::specialize(const std::size_t contract_assigns_size)
 {
   log.debug() << "->dfcc_libraryt::specialize(" << contract_assigns_size << ") "
               << messaget::eom;

src/goto-instrument/contracts/dynamic-frames/dfcc_library.h

@@ -204,7 +204,7 @@ class dfcc_libraryt
   /// Specializes the library by unwinding loops in library functions
   /// to the given assigns clause size.
   /// \param contract_assigns_size_hint size of the assigns clause being checked
-  void specialize(const int contract_assigns_size_hint);
+  void specialize(const std::size_t contract_assigns_size_hint);
 
   /// Adds an ASSERT(false) body to all front-end functions
   /// __CPROVER_object_whole