stack_depth takes a size_t as argument

Author: tautschnig

src/goto-instrument/goto_instrument_parse_options.cpp

@@ -1175,7 +1175,7 @@ void goto_instrument_parse_optionst::instrument_goto_program()
     status() << "Adding check for maximum call stack size" << eom;
     stack_depth(
       goto_model,
-      unsafe_string2unsigned(cmdline.get_value("stack-depth")));
+      safe_string2size_t(cmdline.get_value("stack-depth")));
   }
 
   // ignore default/user-specified initialization of variables with static

src/goto-instrument/stack_depth.cpp

@@ -22,7 +22,7 @@ Date: November 2011
 symbol_exprt add_stack_depth_symbol(symbol_tablet &symbol_table)
 {
   const irep_idt identifier="$stack_depth";
-  signedbv_typet type(sizeof(int)*8);
+  unsignedbv_typet type(sizeof(std::size_t)*8);
 
   symbolt new_symbol;
   new_symbol.name=identifier;
@@ -43,7 +43,7 @@ symbol_exprt add_stack_depth_symbol(symbol_tablet &symbol_table)
 void stack_depth(
   goto_programt &goto_program,
   const symbol_exprt &symbol,
-  const int i_depth,
+  const std::size_t i_depth,
   const exprt &max_depth)
 {
   assert(!goto_program.instructions.empty());
@@ -82,7 +82,7 @@ void stack_depth(
 
 void stack_depth(
   goto_modelt &goto_model,
-  const int depth)
+  const std::size_t depth)
 {
   const symbol_exprt sym=
     add_stack_depth_symbol(goto_model.symbol_table);

src/goto-instrument/stack_depth.h

@@ -14,10 +14,12 @@ Date: November 2011
 #ifndef CPROVER_GOTO_INSTRUMENT_STACK_DEPTH_H
 #define CPROVER_GOTO_INSTRUMENT_STACK_DEPTH_H
 
+#include <cstdint>
+
 class goto_modelt;
 
 void stack_depth(
   goto_modelt &,
-  const int depth);
+  const std::size_t depth);
 
 #endif // CPROVER_GOTO_INSTRUMENT_STACK_DEPTH_H