Replace gen_zero/gen_one by from_integer where possible

Also remove all (now) unnecessary #include <expr_util.h>
Includes cleanup of string construction.

Author: tautschnig

src/aa-path-symex/path_symex.cpp

@@ -11,7 +11,6 @@ Author: Daniel Kroening, [email protected]
 #include <util/simplify_expr.h>
 #include <util/byte_operators.h>
 #include <util/pointer_offset_size.h>
-#include <util/expr_util.h>
 #include <util/base_type.h>
 
 #include <ansi-c/c_types.h>
@@ -353,7 +352,7 @@ void path_symext::symex_malloc(
     rhs.type()=pointer_typet(value_symbol.type.subtype());
     index_exprt index_expr(value_symbol.type.subtype());
     index_expr.array()=value_symbol.symbol_expr();
-    index_expr.index()=gen_zero(index_type());
+    index_expr.index()=from_integer(0, index_type());
     rhs.op0()=index_expr;
   }
   else
@@ -486,7 +485,7 @@ void path_symext::assign_rec(
     else if(compound_type.id()==ID_union)
     {
       // rewrite into byte_extract, and do again
-      exprt offset=gen_zero(index_type());
+      exprt offset=from_integer(0, index_type());
 
       byte_extract_exprt
         new_lhs(byte_update_id(), struct_op, offset, ssa_rhs.type());

src/aa-path-symex/path_symex_state.cpp

@@ -9,7 +9,6 @@ Author: Daniel Kroening, [email protected]
 
 #include <util/simplify_expr.h>
 #include <util/arith_tools.h>
-#include <util/expr_util.h>
 #include <util/decision_procedure.h>
 
 #include <ansi-c/c_types.h>

src/analyses/ai.cpp

@@ -11,7 +11,6 @@ Author: Daniel Kroening, [email protected]
 
 #include <util/std_expr.h>
 #include <util/std_code.h>
-#include <util/expr_util.h>
 
 #include "is_threaded.h"
 

src/analyses/flow_insensitive_analysis.cpp

@@ -11,7 +11,6 @@ Author: Daniel Kroening, [email protected]
 
 #include <util/std_expr.h>
 #include <util/std_code.h>
-#include <util/expr_util.h>
 
 #include "flow_insensitive_analysis.h"
 

src/analyses/goto_check.cpp

@@ -188,7 +188,7 @@ void goto_checkt::div_by_zero_check(
 
   // add divison by zero subgoal
 
-  exprt zero=gen_zero(expr.op1().type());
+  exprt zero=from_integer(0, expr.op1().type());
 
   if(zero.is_nil())
     throw "no zero of argument type of operator "+expr.id_string();
@@ -233,7 +233,7 @@ void goto_checkt::undefined_shift_check(
   if(distance_type.id()==ID_signedbv)
   {
     binary_relation_exprt inequality(
-      expr.distance(), ID_ge, gen_zero(distance_type));
+      expr.distance(), ID_ge, from_integer(0, distance_type));
 
     add_guarded_claim(
       inequality,
@@ -289,7 +289,7 @@ void goto_checkt::mod_by_zero_check(
 
   // add divison by zero subgoal
 
-  exprt zero=gen_zero(expr.op1().type());
+  exprt zero=from_integer(0, expr.op1().type());
 
   if(zero.is_nil())
     throw "no zero of argument type of operator "+expr.id_string();
@@ -802,8 +802,8 @@ void goto_checkt::nan_check(
     // 0/0 = NaN and x/inf = NaN
     // (note that x/0 = +-inf for x!=0 and x!=inf)
     exprt zero_div_zero=and_exprt(
-      ieee_float_equal_exprt(expr.op0(), gen_zero(expr.op0().type())),
-      ieee_float_equal_exprt(expr.op1(), gen_zero(expr.op1().type())));
+      ieee_float_equal_exprt(expr.op0(), from_integer(0, expr.op0().type())),
+      ieee_float_equal_exprt(expr.op1(), from_integer(0, expr.op1().type())));
 
     exprt div_inf=unary_exprt(ID_isinf, expr.op1(), bool_typet());
 
@@ -819,10 +819,10 @@ void goto_checkt::nan_check(
     // Inf * 0 is NaN
     exprt inf_times_zero=and_exprt(
       unary_exprt(ID_isinf, expr.op0(), bool_typet()),
-      ieee_float_equal_exprt(expr.op1(), gen_zero(expr.op1().type())));
+      ieee_float_equal_exprt(expr.op1(), from_integer(0, expr.op1().type())));
 
     exprt zero_times_inf=and_exprt(
-      ieee_float_equal_exprt(expr.op1(), gen_zero(expr.op1().type())),
+      ieee_float_equal_exprt(expr.op1(), from_integer(0, expr.op1().type())),
       unary_exprt(ID_isinf, expr.op0(), bool_typet()));
 
     isnan=or_exprt(inf_times_zero, zero_times_inf);
@@ -1175,7 +1175,7 @@ void goto_checkt::bounds_check(
           effective_offset=plus_exprt(p_offset, effective_offset);
         }
 
-        exprt zero=gen_zero(ode.offset().type());
+        exprt zero=from_integer(0, ode.offset().type());
         assert(zero.is_not_nil());
 
         // the final offset must not be negative

src/analyses/invariant_propagation.cpp

@@ -6,7 +6,6 @@ Author: Daniel Kroening, [email protected]
 
 \*******************************************************************/
 
-#include <util/expr_util.h>
 #include <util/simplify_expr.h>
 #include <util/base_type.h>
 #include <util/symbol_table.h>

src/analyses/invariant_set.cpp

@@ -10,7 +10,6 @@ Author: Daniel Kroening, [email protected]
 
 #include <util/symbol_table.h>
 #include <util/namespace.h>
-#include <util/expr_util.h>
 #include <util/arith_tools.h>
 #include <util/std_expr.h>
 #include <util/simplify_expr.h>
@@ -992,7 +991,7 @@ void invariant_sett::nnf(exprt &expr, bool negate)
     {
       equal_exprt tmp;
       tmp.lhs()=expr.op0();
-      tmp.rhs()=gen_zero(expr.op0().type());
+      tmp.rhs()=from_integer(0, expr.op0().type());
       nnf(tmp, !negate);
       expr.swap(tmp);
     }

src/analyses/local_may_alias.cpp

@@ -9,6 +9,7 @@ Author: Daniel Kroening, [email protected]
 #include <iterator>
 #include <algorithm>
 
+#include <util/arith_tools.h>
 #include <util/std_expr.h>
 #include <util/std_code.h>
 #include <util/expr_util.h>
@@ -272,7 +273,7 @@ void local_may_aliast::get_rec(
       if(index_expr.array().id()==ID_symbol)
       {
         index_exprt tmp1=index_expr;
-        tmp1.index()=gen_zero(index_type());
+        tmp1.index()=from_integer(0, index_type());
         address_of_exprt tmp2(tmp1);
         unsigned object_nr=objects.number(tmp2);
         dest.insert(object_nr);
@@ -284,7 +285,7 @@ void local_may_aliast::get_rec(
       else if(index_expr.array().id()==ID_string_constant)
       {
         index_exprt tmp1=index_expr;
-        tmp1.index()=gen_zero(index_type());
+        tmp1.index()=from_integer(0, index_type());
         address_of_exprt tmp2(tmp1);
         unsigned object_nr=objects.number(tmp2);
         dest.insert(object_nr);

src/analyses/static_analysis.cpp

@@ -11,7 +11,6 @@ Author: Daniel Kroening, [email protected]
 
 #include <util/std_expr.h>
 #include <util/std_code.h>
-#include <util/expr_util.h>
 
 #include "is_threaded.h"
 

src/ansi-c/ansi_c_entry_point.cpp

@@ -10,7 +10,6 @@ Author: Daniel Kroening, [email protected]
 #include <cstdlib>
 
 #include <util/namespace.h>
-#include <util/expr_util.h>
 #include <util/std_expr.h>
 #include <util/arith_tools.h>
 #include <util/std_code.h>
@@ -90,7 +89,7 @@ exprt::operandst build_function_environment(
 
     // record as an input
     input.op0()=address_of_exprt(
-      index_exprt(string_constantt(base_name), gen_zero(index_type())));
+      index_exprt(string_constantt(base_name), from_integer(0, index_type())));
     input.op1()=symbol_expr;
     input.add_source_location()=p.source_location();
 
@@ -131,9 +130,11 @@ void record_function_outputs(
 
     const symbolt &return_symbol=symbol_table.lookup("return'");
 
-    output.op0()=address_of_exprt(
-      index_exprt(string_constantt(return_symbol.base_name),
-                  gen_zero(index_type())));
+    output.op0()=
+      address_of_exprt(
+        index_exprt(
+          string_constantt(return_symbol.base_name),
+          from_integer(0, index_type())));
 
     output.op1()=return_symbol.symbol_expr();
     output.add_source_location()=function.location;
@@ -158,9 +159,11 @@ void record_function_outputs(
       codet output(ID_output);
       output.operands().resize(2);
 
-      output.op0()=address_of_exprt(
-        index_exprt(string_constantt(symbol.base_name),
-                    gen_zero(index_type())));
+      output.op0()=
+        address_of_exprt(
+          index_exprt(
+            string_constantt(symbol.base_name),
+            from_integer(0, index_type())));
       output.op1()=symbol.symbol_expr();
       output.add_source_location()=p.source_location();
 
@@ -350,7 +353,7 @@ bool ansi_c_entry_point(
         codet input(ID_input);
         input.operands().resize(2);
         input.op0()=address_of_exprt(
-          index_exprt(string_constantt("argc"), gen_zero(index_type())));
+          index_exprt(string_constantt("argc"), from_integer(0, index_type())));
         input.op1()=argc_symbol.symbol_expr();
         init_code.move_to_operands(input);
       }
@@ -392,7 +395,7 @@ bool ansi_c_entry_point(
         zero_string.type().subtype()=char_type();
         zero_string.type().set(ID_size, "infinity");
         exprt index(ID_index, char_type());
-        index.copy_to_operands(zero_string, gen_zero(uint_type()));
+        index.copy_to_operands(zero_string, from_integer(0, uint_type()));
         exprt address_of("address_of", pointer_typet());
         address_of.type().subtype()=char_type();
         address_of.copy_to_operands(index);
@@ -470,7 +473,7 @@ bool ansi_c_entry_point(
           exprt index_expr(ID_index, arg1.type().subtype());
           index_expr.copy_to_operands(
             argv_symbol.symbol_expr(),
-            gen_zero(index_type()));
+            from_integer(0, index_type()));
 
           // disable bounds check on that one
           index_expr.set("bounds_check", false);
@@ -489,7 +492,7 @@ bool ansi_c_entry_point(
 
           exprt index_expr(ID_index, arg2.type().subtype());
           index_expr.copy_to_operands(
-            envp_symbol.symbol_expr(), gen_zero(index_type()));
+            envp_symbol.symbol_expr(), from_integer(0, index_type()));
 
           op2=exprt(ID_address_of, arg2.type());
           op2.move_to_operands(index_expr);

src/ansi-c/ansi_c_language.cpp

@@ -10,7 +10,6 @@ Author: Daniel Kroening, [email protected]
 #include <sstream>
 #include <fstream>
 
-#include <util/expr_util.h>
 #include <util/config.h>
 #include <util/get_base_name.h>
 

src/ansi-c/c_typecast.cpp

@@ -10,6 +10,7 @@ Author: Daniel Kroening, [email protected]
 
 #include <cassert>
 
+#include <util/arith_tools.h>
 #include <util/config.h>
 #include <util/expr_util.h>
 #include <util/std_expr.h>
@@ -853,7 +854,7 @@ void c_typecastt::do_typecast(exprt &expr, const typet &dest_type)
   {
     index_exprt index;
     index.array()=expr;
-    index.index()=gen_zero(index_type());
+    index.index()=from_integer(0, index_type());
     index.type()=src_type.subtype();
     expr=address_of_exprt(index);
     if(ns.follow(expr.type())!=ns.follow(dest_type))

src/ansi-c/c_typecheck_argc_argv.cpp

@@ -7,7 +7,6 @@ Author: Daniel Kroening, [email protected]
 \*******************************************************************/
 
 #include <util/arith_tools.h>
-#include <util/expr_util.h>
 
 #include "c_typecheck_base.h"
 

src/ansi-c/c_typecheck_expr.cpp

@@ -11,7 +11,6 @@ Author: Daniel Kroening, [email protected]
 #include <util/arith_tools.h>
 #include <util/config.h>
 #include <util/std_types.h>
-#include <util/expr_util.h>
 #include <util/prefix.h>
 #include <util/cprover_prefix.h>
 #include <util/simplify_expr.h>
@@ -100,7 +99,7 @@ void c_typecheck_baset::add_rounding_mode(exprt &expr)
       else
         assert(false);
 
-      expr.op2()=gen_zero(unsigned_int_type());
+      expr.op2()=from_integer(0, unsigned_int_type());
     }
   }
 }
@@ -604,7 +603,7 @@ void c_typecheck_baset::typecheck_expr_builtin_offsetof(exprt &expr)
 
   exprt &member=static_cast<exprt &>(expr.add(ID_designator));
 
-  exprt result=gen_zero(size_type());
+  exprt result=from_integer(0, size_type());
 
   forall_operands(m_it, member)
   {
@@ -1286,7 +1285,7 @@ void c_typecheck_baset::typecheck_expr_typecast(exprt &expr)
   {
     index_exprt index;
     index.array()=op;
-    index.index()=gen_zero(index_type());
+    index.index()=from_integer(0, index_type());
     index.type()=op_type.subtype();
     op=address_of_exprt(index);
   }
@@ -2031,7 +2030,7 @@ void c_typecheck_baset::typecheck_expr_dereference(exprt &expr)
     // *a is the same as a[0]
     expr.id(ID_index);
     expr.type()=op_type.subtype();
-    expr.copy_to_operands(gen_zero(index_type()));
+    expr.copy_to_operands(from_integer(0, index_type()));
     assert(expr.operands().size()==2);
   }
   else if(op_type.id()==ID_pointer)

src/ansi-c/c_typecheck_initializer.cpp

@@ -10,7 +10,6 @@ Author: Daniel Kroening, [email protected]
 #include <util/config.h>
 #include <util/type_eq.h>
 #include <util/std_types.h>
-#include <util/expr_util.h>
 #include <util/simplify_expr.h>
 #include <util/cprover_prefix.h>
 #include <util/prefix.h>

src/ansi-c/c_typecheck_type.cpp

@@ -12,7 +12,6 @@ Author: Daniel Kroening, [email protected]
 #include <util/simplify_expr.h>
 #include <util/arith_tools.h>
 #include <util/std_types.h>
-#include <util/expr_util.h>
 #include <util/pointer_offset_size.h>
 
 #include "c_typecheck_base.h"
@@ -949,7 +948,7 @@ void c_typecheck_baset::typecheck_compound_body(
 
         // make it zero-length
         c_type.id(ID_array);
-        c_type.set(ID_size, gen_zero(index_type()));
+        c_type.set(ID_size, from_integer(0, index_type()));
       }
     }
   }

src/ansi-c/literals/convert_float_literal.cpp

@@ -11,9 +11,9 @@ Author: Daniel Kroening, [email protected]
 #include <util/arith_tools.h>
 #include <util/config.h>
 #include <util/ieee_float.h>
+#include <util/std_expr.h>
 #include <util/std_types.h>
 #include <util/string2int.h>
-#include <util/expr_util.h>
 
 #include "../c_types.h"
 #include "parse_float.h"
@@ -142,7 +142,7 @@ exprt convert_float_literal(const std::string &src)
     complex_type.subtype()=result.type();
     exprt complex_expr(ID_complex, complex_type);
     complex_expr.operands().resize(2);
-    complex_expr.op0()=gen_zero(result.type());
+    complex_expr.op0()=from_integer(0, result.type());
     complex_expr.op1()=result;
     return complex_expr;
   }

src/ansi-c/literals/convert_integer_literal.cpp

@@ -13,7 +13,6 @@ Author: Daniel Kroening, [email protected]
 #include <util/config.h>
 #include <util/std_types.h>
 #include <util/std_expr.h>
-#include <util/expr_util.h>
 #include <util/string2int.h>
 
 #include "convert_integer_literal.h"
@@ -187,7 +186,7 @@ exprt convert_integer_literal(const std::string &src)
     complex_type.subtype()=type;
     result=exprt(ID_complex, complex_type);
     result.operands().resize(2);
-    result.op0()=gen_zero(type);
+    result.op0()=from_integer(0, type);
     result.op1()=from_integer(value, type);
   }
   else

src/ansi-c/parser_static.inc

@@ -1,7 +1,6 @@
 #include <util/std_code.h>
 #include <util/std_types.h>
 #include <util/std_expr.h>
-#include <util/expr_util.h>
 #include <util/string2int.h>
 
 #include "c_types.h"