From 6278e42e9dcaa740090a4d31210a2dc2a08c6a21 Mon Sep 17 00:00:00 2001
From: Antonia Lechner <antonia.lechner@diffblue.com>
Date: Thu, 21 Mar 2019 17:11:06 +0000
Subject: [PATCH] Split generate_nondet_int into two functions

We will be able to use the exprt version in other parts of the code.
---
 src/util/nondet.cpp | 37 +++++++++++++++++++++++++++----------
 src/util/nondet.h   | 19 +++++++++++++++++++
 2 files changed, 46 insertions(+), 10 deletions(-)

diff --git a/src/util/nondet.cpp b/src/util/nondet.cpp
index f8dd8b7b15..08c374d37e 100644
--- a/src/util/nondet.cpp
+++ b/src/util/nondet.cpp
@@ -14,16 +14,16 @@ Author: Diffblue Ltd.
 #include <util/symbol.h>
 
 symbol_exprt generate_nondet_int(
-  const mp_integer &min_value,
-  const mp_integer &max_value,
+  const exprt &min_value_expr,
+  const exprt &max_value_expr,
   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);
+  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.
   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`.
   //   ASSUME(name_prefix::nondet_int >= min_value)
   instructions.add(
-    code_assumet(
-      binary_predicate_exprt(
-        nondet_symbol, ID_ge, from_integer(min_value, int_type))));
+    code_assumet(binary_predicate_exprt(nondet_symbol, ID_ge, min_value_expr)));
 
   // Constrain the non deterministic integer with an upper bound of `max_value`.
   //   ASSUME(name_prefix::nondet_int <= max_value)
   instructions.add(
-    code_assumet(
-      binary_predicate_exprt(
-        nondet_symbol, ID_le, from_integer(max_value, int_type))));
+    code_assumet(binary_predicate_exprt(nondet_symbol, ID_le, max_value_expr)));
 
   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(
   const irep_idt &name_prefix,
   const alternate_casest &switch_cases,
diff --git a/src/util/nondet.h b/src/util/nondet.h
index f221758fcf..c1529fba30 100644
--- a/src/util/nondet.h
+++ b/src/util/nondet.h
@@ -13,6 +13,25 @@ Author: Diffblue Ltd.
 #include <util/std_expr.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
 /// resembles:
 /// ```