Skip to content

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

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
tautschnig merged 2 commits into from
Nov 10, 2018
Merged

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

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
a96218e
Do not use arbitrarily bounded integer types
tautschnig Nov 9, 2018
c32a775
Add missing documentation for parameter mode
tautschnig Nov 10, 2018
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
8 changes: 0 additions & 8 deletions scripts/expected_doxygen_warnings.txt
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
6 changes: 4 additions & 2 deletions src/util/nondet.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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,
Expand Down Expand Up @@ -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
Expand Down
4 changes: 2 additions & 2 deletions src/util/nondet.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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,
Expand Down