Split generate_nondet_int into two functions
We will be able to use the exprt version in other parts of the code.
This commit is contained in:
parent
0d32a43dc7
commit
6278e42e9d
|
@ -14,16 +14,16 @@ Author: Diffblue Ltd.
|
||||||
#include <util/symbol.h>
|
#include <util/symbol.h>
|
||||||
|
|
||||||
symbol_exprt generate_nondet_int(
|
symbol_exprt generate_nondet_int(
|
||||||
const mp_integer &min_value,
|
const exprt &min_value_expr,
|
||||||
const mp_integer &max_value,
|
const exprt &max_value_expr,
|
||||||
const std::string &name_prefix,
|
const std::string &name_prefix,
|
||||||
const typet &int_type,
|
|
||||||
const irep_idt &mode,
|
const irep_idt &mode,
|
||||||
const source_locationt &source_location,
|
const source_locationt &source_location,
|
||||||
symbol_table_baset &symbol_table,
|
symbol_table_baset &symbol_table,
|
||||||
code_blockt &instructions)
|
code_blockt &instructions)
|
||||||
{
|
{
|
||||||
PRECONDITION(min_value < max_value);
|
PRECONDITION(min_value_expr.type() == max_value_expr.type());
|
||||||
|
const typet &int_type = min_value_expr.type();
|
||||||
|
|
||||||
// Declare a symbol for the non deterministic integer.
|
// Declare a symbol for the non deterministic integer.
|
||||||
const symbol_exprt &nondet_symbol =
|
const symbol_exprt &nondet_symbol =
|
||||||
|
@ -40,20 +40,37 @@ symbol_exprt generate_nondet_int(
|
||||||
// Constrain the non deterministic integer with a lower bound of `min_value`.
|
// Constrain the non deterministic integer with a lower bound of `min_value`.
|
||||||
// ASSUME(name_prefix::nondet_int >= min_value)
|
// ASSUME(name_prefix::nondet_int >= min_value)
|
||||||
instructions.add(
|
instructions.add(
|
||||||
code_assumet(
|
code_assumet(binary_predicate_exprt(nondet_symbol, ID_ge, min_value_expr)));
|
||||||
binary_predicate_exprt(
|
|
||||||
nondet_symbol, ID_ge, from_integer(min_value, int_type))));
|
|
||||||
|
|
||||||
// Constrain the non deterministic integer with an upper bound of `max_value`.
|
// Constrain the non deterministic integer with an upper bound of `max_value`.
|
||||||
// ASSUME(name_prefix::nondet_int <= max_value)
|
// ASSUME(name_prefix::nondet_int <= max_value)
|
||||||
instructions.add(
|
instructions.add(
|
||||||
code_assumet(
|
code_assumet(binary_predicate_exprt(nondet_symbol, ID_le, max_value_expr)));
|
||||||
binary_predicate_exprt(
|
|
||||||
nondet_symbol, ID_le, from_integer(max_value, int_type))));
|
|
||||||
|
|
||||||
return nondet_symbol;
|
return nondet_symbol;
|
||||||
}
|
}
|
||||||
|
|
||||||
|
symbol_exprt generate_nondet_int(
|
||||||
|
const mp_integer &min_value,
|
||||||
|
const mp_integer &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)
|
||||||
|
{
|
||||||
|
PRECONDITION(min_value < max_value);
|
||||||
|
return generate_nondet_int(
|
||||||
|
from_integer(min_value, int_type),
|
||||||
|
from_integer(max_value, int_type),
|
||||||
|
name_prefix,
|
||||||
|
mode,
|
||||||
|
source_location,
|
||||||
|
symbol_table,
|
||||||
|
instructions);
|
||||||
|
}
|
||||||
|
|
||||||
code_blockt generate_nondet_switch(
|
code_blockt generate_nondet_switch(
|
||||||
const irep_idt &name_prefix,
|
const irep_idt &name_prefix,
|
||||||
const alternate_casest &switch_cases,
|
const alternate_casest &switch_cases,
|
||||||
|
|
|
@ -13,6 +13,25 @@ Author: Diffblue Ltd.
|
||||||
#include <util/std_expr.h>
|
#include <util/std_expr.h>
|
||||||
#include <util/symbol_table.h>
|
#include <util/symbol_table.h>
|
||||||
|
|
||||||
|
/// Same as \ref generate_nondet_int(
|
||||||
|
/// const mp_integer &min_value,
|
||||||
|
/// const mp_integer &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)
|
||||||
|
/// except the minimum and maximum values are represented as exprts.
|
||||||
|
symbol_exprt generate_nondet_int(
|
||||||
|
const exprt &min_value_expr,
|
||||||
|
const exprt &max_value_expr,
|
||||||
|
const std::string &name_prefix,
|
||||||
|
const irep_idt &mode,
|
||||||
|
const source_locationt &source_location,
|
||||||
|
symbol_table_baset &symbol_table,
|
||||||
|
code_blockt &instructions);
|
||||||
|
|
||||||
/// Gets a fresh nondet choice in range (min_value, max_value). GOTO generated
|
/// Gets a fresh nondet choice in range (min_value, max_value). GOTO generated
|
||||||
/// resembles:
|
/// resembles:
|
||||||
/// ```
|
/// ```
|
||||||
|
|
Loading…
Reference in New Issue