diff --git a/jbmc/src/java_bytecode/java_bytecode_language.cpp b/jbmc/src/java_bytecode/java_bytecode_language.cpp index 5c15f43abee..ecf8cc2f4e6 100644 --- a/jbmc/src/java_bytecode/java_bytecode_language.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_language.cpp @@ -53,20 +53,21 @@ void java_bytecode_languaget::get_language_options(const cmdlinet &cmd) if(cmd.isset("java-max-input-array-length")) object_factory_parameters.max_nondet_array_length= - std::stoi(cmd.get_value("java-max-input-array-length")); + safe_string2size_t(cmd.get_value("java-max-input-array-length")); if(cmd.isset("java-max-input-tree-depth")) object_factory_parameters.max_nondet_tree_depth= - std::stoi(cmd.get_value("java-max-input-tree-depth")); + safe_string2size_t(cmd.get_value("java-max-input-tree-depth")); if(cmd.isset("string-max-input-length")) object_factory_parameters.max_nondet_string_length= - std::stoi(cmd.get_value("string-max-input-length")); + safe_string2size_t(cmd.get_value("string-max-input-length")); else if(cmd.isset("string-max-length")) object_factory_parameters.max_nondet_string_length = - std::stoi(cmd.get_value("string-max-length")); + safe_string2size_t(cmd.get_value("string-max-length")); object_factory_parameters.string_printable = cmd.isset("string-printable"); if(cmd.isset("java-max-vla-length")) - max_user_array_length=std::stoi(cmd.get_value("java-max-vla-length")); + max_user_array_length = + safe_string2size_t(cmd.get_value("java-max-vla-length")); if(cmd.isset("symex-driven-lazy-loading")) lazy_methods_mode=LAZY_METHODS_MODE_EXTERNAL_DRIVER; else if(cmd.isset("lazy-methods")) diff --git a/src/ansi-c/literals/convert_integer_literal.cpp b/src/ansi-c/literals/convert_integer_literal.cpp index 7123f2dddd8..573602966ab 100644 --- a/src/ansi-c/literals/convert_integer_literal.cpp +++ b/src/ansi-c/literals/convert_integer_literal.cpp @@ -41,7 +41,7 @@ exprt convert_integer_literal(const std::string &src) // and "10i" (imaginary) for GCC. // If it's followed by a number, we do MS mode. if((i+1) #include +#include +#include #include +#include +#include #include +#include #include #include -#include -#include -#include -#include + #include #include "interpreter_class.h" @@ -207,7 +209,7 @@ void interpretert::command() stack_depth=call_stack.size()+1; else { - num_steps=atoi(command+1); + num_steps=safe_string2size_t(command+1); if(num_steps==0) num_steps=1; } diff --git a/src/goto-symex/slice_by_trace.cpp b/src/goto-symex/slice_by_trace.cpp index 3a5800f19b3..d02b54ed3e7 100644 --- a/src/goto-symex/slice_by_trace.cpp +++ b/src/goto-symex/slice_by_trace.cpp @@ -547,7 +547,7 @@ std::set symex_slice_by_tracet::implied_guards(exprt e) } else { - int i=unsafe_string2int(id_string.substr(merge_loc+6)); + const std::size_t i = unsafe_string2size_t(id_string.substr(merge_loc+6)); if(merge_impl_cache_back[i].first) { return merge_impl_cache_back[i].second; diff --git a/src/solvers/flattening/boolbv.cpp b/src/solvers/flattening/boolbv.cpp index 219e372afcf..3c5cb3856d8 100644 --- a/src/solvers/flattening/boolbv.cpp +++ b/src/solvers/flattening/boolbv.cpp @@ -380,7 +380,7 @@ bvt boolbvt::convert_bv_literals(const exprt &expr) throw "bv_literals with wrong size"; for(std::size_t i=0; i