Merge pull request #2418 from tautschnig/vs-stack-depth

stack_depth takes a signed int as argument

Author: tautschnig

regression/goto-instrument/stack-depth1/fails.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--stack-depth 1
+^EXIT=10$
+^SIGNAL=0$
+VERIFICATION FAILED
+--
+^warning: ignoring

regression/goto-instrument/stack-depth1/main.c

@@ -0,0 +1,14 @@
+int bar(int x)
+{
+  return 42;
+}
+
+int foo(int x)
+{
+  return bar(x);
+}
+
+int main(int argc, char* argv[])
+{
+  return foo(argc);
+}

regression/goto-instrument/stack-depth1/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--stack-depth 2
+^EXIT=0$
+^SIGNAL=0$
+VERIFICATION SUCCESSFUL
+--
+^warning: ignoring

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 <cstddef>
+
 class goto_modelt;
 
 void stack_depth(
   goto_modelt &,
-  const int depth);
+  const std::size_t depth);
 
 #endif // CPROVER_GOTO_INSTRUMENT_STACK_DEPTH_H