Merge pull request #3326 from tautschnig/vs-bounded

Do not use arbitrarily bounded integer types [blocks: #2310]

Author: tautschnig

scripts/expected_doxygen_warnings.txt

@@ -24,14 +24,6 @@
   parameter 'witnesses'
 /cbmc/src/solvers/refinement/string_refinement.cpp:1052: warning: The following parameters of substitute_array_access(const with_exprt &expr, const exprt &index, const bool left_propagate) are not documented:
   parameter 'left_propagate'
-/cbmc/src/util/nondet.cpp:35: warning: The following parameters of generate_nondet_int(const int64_t min_value, const int64_t max_value, const std::string &name_prefix, const typet &int_type, const irep_idt &mode, const source_locationt &source_location, symbol_table_baset &symbol_table, code_blockt &instructions) are not documented:
-  parameter 'mode'
-/cbmc/src/util/nondet.cpp:85: warning: The following parameters of generate_nondet_switch(const irep_idt &name_prefix, const alternate_casest &switch_cases, const typet &int_type, const irep_idt &mode, const source_locationt &source_location, symbol_table_baset &symbol_table) are not documented:
-  parameter 'mode'
-/cbmc/src/util/nondet.h:16: warning: The following parameters of generate_nondet_int(const int64_t min_value, const int64_t max_value, const std::string &name_prefix, const typet &int_type, const irep_idt &mode, const source_locationt &source_location, symbol_table_baset &symbol_table, code_blockt &instructions) are not documented:
-  parameter 'mode'
-/cbmc/src/util/nondet.h:28: warning: The following parameters of generate_nondet_switch(const irep_idt &name_prefix, const alternate_casest &switch_cases, const typet &int_type, const irep_idt &mode, const source_locationt &source_location, symbol_table_baset &symbol_table) are not documented:
-  parameter 'mode'
 /cbmc/doc/architectural/howto.md:260: warning: found </div> at different nesting level (6) than expected (3)
 /cbmc/doc/architectural/howto.md:261: warning: end of comment block while expecting command </div>
 /cbmc/src/solvers/README.md:4: warning: @copydetails or @copydoc target 'generate_instantiations(messaget::mstreamt &stream, const string_constraint_generatort &generator, const index_set_pairt &index_set, const string_axiomst &axioms, const std::map<string_not_contains_constraintt, symbol_exprt> &not_contain_witnesses).' not found

src/util/nondet.cpp

@@ -26,15 +26,16 @@ Module: Non-deterministic object init and choice for CBMC
 ///   function id)
 /// \param int_type: The type of the int used to non-deterministically choose
 ///   one of the switch cases.
+/// \param mode: Mode (language) of the symbol to be generated.
 /// \param source_location: The location to mark the generated int with.
 /// \param symbol_table: The global symbol table.
 /// \param instructions [out]: Output instructions are written to
 ///   'instructions'. These declare, nondet-initialise and range-constrain (with
 ///   assume statements) a fresh integer.
 /// \return Returns a symbol expression for the resulting integer.
 symbol_exprt generate_nondet_int(
-  const int64_t min_value,
-  const int64_t max_value,
+  const mp_integer &min_value,
+  const mp_integer &max_value,
   const std::string &name_prefix,
   const typet &int_type,
   const irep_idt &mode,
@@ -78,6 +79,7 @@ symbol_exprt generate_nondet_int(
 /// \param switch_cases: List of codet objects to execute in each switch case.
 /// \param int_type: The type of the int used to non-deterministically choose
 ///   one of the switch cases.
+/// \param mode: Mode (language) of the symbol to be generated.
 /// \param source_location: The location to mark the generated int with.
 /// \param symbol_table: The global symbol table.
 /// \return Returns a nondet-switch choosing between switch_cases. The resulting

src/util/nondet.h

@@ -14,8 +14,8 @@
 #include <util/symbol_table.h>
 
 symbol_exprt generate_nondet_int(
-  int64_t min_value,
-  int64_t max_value,
+  const mp_integer &min_value,
+  const mp_integer &max_value,
   const std::string &name_prefix,
   const typet &int_type,
   const irep_idt &mode,