From 6e36ead3c92200b3bd923108967807636d68de48 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Mon, 16 Jan 2017 08:03:29 -0500 Subject: [PATCH 1/7] Replace gen_zero/gen_one by from_integer where possible Also remove all (now) unnecessary #include Includes cleanup of string construction. --- src/aa-path-symex/path_symex.cpp | 5 +- src/aa-path-symex/path_symex_state.cpp | 1 - src/analyses/ai.cpp | 1 - src/analyses/flow_insensitive_analysis.cpp | 1 - src/analyses/goto_check.cpp | 16 ++-- src/analyses/invariant_propagation.cpp | 1 - src/analyses/invariant_set.cpp | 3 +- src/analyses/local_may_alias.cpp | 5 +- src/analyses/static_analysis.cpp | 1 - src/ansi-c/ansi_c_entry_point.cpp | 27 ++++--- src/ansi-c/ansi_c_language.cpp | 1 - src/ansi-c/c_typecast.cpp | 3 +- src/ansi-c/c_typecheck_argc_argv.cpp | 1 - src/ansi-c/c_typecheck_expr.cpp | 9 +-- src/ansi-c/c_typecheck_initializer.cpp | 1 - src/ansi-c/c_typecheck_type.cpp | 3 +- src/ansi-c/literals/convert_float_literal.cpp | 4 +- .../literals/convert_integer_literal.cpp | 3 +- src/ansi-c/parser_static.inc | 1 - src/cbmc/cbmc_parse_options.cpp | 1 - src/cbmc/counterexample_beautification.cpp | 1 - src/cbmc/fault_localization.cpp | 1 - .../symex/learn/danger_learn_config.cpp | 4 +- .../symex/verify/extract_counterexample.cpp | 5 +- .../symex/verify/insert_constraint.cpp | 1 - .../jsa/constraint/jsa_constraint_factory.cpp | 8 +- src/cegis/jsa/instrument/temps_helper.cpp | 5 +- src/cegis/jsa/learn/execute_jsa_programs.cpp | 12 ++- src/cegis/jsa/learn/insert_counterexample.cpp | 6 +- .../learn/insert_predicates_and_queries.cpp | 5 +- src/cegis/jsa/learn/instrument_pred_ops.cpp | 3 +- .../preprocessing/create_temp_variables.cpp | 4 +- .../jsa/verify/extract_counterexample.cpp | 1 - .../constraint/constraint_factory.cpp | 4 +- .../cegis_processor_body_factory.cpp | 5 +- .../instructionset/execute_cegis_program.cpp | 3 +- .../learn/instrument_counterexamples.cpp | 3 +- .../symex/learn/safety_learn_config.cpp | 4 +- src/cegis/seed/literals_seed.cpp | 5 +- src/cpp/cpp_typecheck.cpp | 1 - src/cpp/cpp_typecheck_code.cpp | 1 - src/cpp/cpp_typecheck_compound_type.cpp | 1 - src/cpp/cpp_typecheck_constructor.cpp | 1 - src/cpp/cpp_typecheck_conversions.cpp | 1 - src/cpp/cpp_typecheck_declaration.cpp | 2 - src/cpp/cpp_typecheck_expr.cpp | 1 - src/cpp/cpp_typecheck_function.cpp | 2 - src/cpp/cpp_typecheck_initializer.cpp | 3 +- src/cpp/cpp_typecheck_resolve.cpp | 1 - src/cpp/cpp_typecheck_template.cpp | 1 - src/cpp/cpp_typecheck_virtual_table.cpp | 1 - src/goto-diff/goto_diff_parse_options.cpp | 1 - src/goto-instrument/cover.cpp | 1 - src/goto-instrument/function.cpp | 7 +- .../goto_instrument_parse_options.cpp | 1 - src/goto-instrument/mmio.cpp | 1 - src/goto-programs/builtin_functions.cpp | 12 +-- src/goto-programs/goto_clean_expr.cpp | 1 - .../goto_convert_function_call.cpp | 1 - .../goto_convert_new_switch_case.cpp | 1 - .../goto_convert_side_effect.cpp | 26 +++++-- src/goto-programs/goto_inline.cpp | 1 - src/goto-programs/pointer_arithmetic.cpp | 4 +- src/goto-programs/remove_complex.cpp | 4 +- .../remove_function_pointers.cpp | 1 - src/goto-programs/string_abstraction.cpp | 14 +++- src/goto-programs/string_instrumentation.cpp | 28 ++++--- src/goto-symex/postcondition.cpp | 1 - src/goto-symex/rewrite_union.cpp | 6 +- src/goto-symex/symex_assign.cpp | 1 - src/goto-symex/symex_builtin_functions.cpp | 7 +- src/goto-symex/symex_clean_expr.cpp | 4 +- src/goto-symex/symex_dead.cpp | 1 - src/goto-symex/symex_decl.cpp | 1 - src/goto-symex/symex_dereference.cpp | 13 ++-- src/goto-symex/symex_function_call.cpp | 3 +- src/goto-symex/symex_goto.cpp | 1 - src/goto-symex/symex_other.cpp | 4 +- src/goto-symex/symex_target_equation.cpp | 1 - .../java_bytecode_convert_method.cpp | 6 +- src/java_bytecode/java_entry_point.cpp | 13 ++-- src/java_bytecode/java_object_factory.cpp | 3 +- src/jsil/jsil_entry_point.cpp | 4 +- src/linking/static_lifetime_init.cpp | 3 +- src/linking/zero_initializer.cpp | 2 +- src/musketeer/fence_shared.cpp | 1 - src/musketeer/fencer.cpp | 1 - src/musketeer/pensieve.cpp | 1 - src/path-symex/path_symex.cpp | 4 +- src/path-symex/path_symex_state.cpp | 1 - src/pointer-analysis/dereference.cpp | 4 +- src/pointer-analysis/value_set.cpp | 3 +- .../value_set_dereference.cpp | 8 +- src/pointer-analysis/value_set_fi.cpp | 3 +- src/pointer-analysis/value_set_fivr.cpp | 3 +- src/pointer-analysis/value_set_fivrns.cpp | 3 +- src/solvers/cvc/cvc_conv.cpp | 3 +- src/solvers/dplib/dplib_conv.cpp | 3 +- src/solvers/flattening/boolbv_member.cpp | 3 +- src/solvers/flattening/boolbv_update.cpp | 1 - src/solvers/flattening/boolbv_with.cpp | 1 - src/solvers/flattening/bv_pointers.cpp | 1 - src/solvers/floatbv/float_bv.cpp | 78 +++++++++++-------- src/solvers/smt1/smt1_conv.cpp | 3 +- src/solvers/smt2/smt2_conv.cpp | 2 +- src/util/arith_tools.cpp | 19 ++++- src/util/expr_util.cpp | 7 +- src/util/pointer_offset_size.cpp | 10 +-- src/util/pointer_predicates.cpp | 2 +- src/util/simplify_expr.cpp | 8 +- src/util/simplify_expr_int.cpp | 38 ++++----- src/util/simplify_expr_pointer.cpp | 4 +- 112 files changed, 288 insertions(+), 289 deletions(-) diff --git a/src/aa-path-symex/path_symex.cpp b/src/aa-path-symex/path_symex.cpp index 0ead6c840ba..0c18e34bb8e 100644 --- a/src/aa-path-symex/path_symex.cpp +++ b/src/aa-path-symex/path_symex.cpp @@ -11,7 +11,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include -#include #include #include @@ -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()); diff --git a/src/aa-path-symex/path_symex_state.cpp b/src/aa-path-symex/path_symex_state.cpp index 124b0e7fea9..f0f21b1b8b5 100644 --- a/src/aa-path-symex/path_symex_state.cpp +++ b/src/aa-path-symex/path_symex_state.cpp @@ -9,7 +9,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include #include #include diff --git a/src/analyses/ai.cpp b/src/analyses/ai.cpp index 4bc490a726b..06dd02af83f 100644 --- a/src/analyses/ai.cpp +++ b/src/analyses/ai.cpp @@ -11,7 +11,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include #include "is_threaded.h" diff --git a/src/analyses/flow_insensitive_analysis.cpp b/src/analyses/flow_insensitive_analysis.cpp index 0f9e15991f0..257e4b70890 100644 --- a/src/analyses/flow_insensitive_analysis.cpp +++ b/src/analyses/flow_insensitive_analysis.cpp @@ -11,7 +11,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include #include "flow_insensitive_analysis.h" diff --git a/src/analyses/goto_check.cpp b/src/analyses/goto_check.cpp index 131b7890de5..e5c1ec0290a 100644 --- a/src/analyses/goto_check.cpp +++ b/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 diff --git a/src/analyses/invariant_propagation.cpp b/src/analyses/invariant_propagation.cpp index c7ed805eddf..8e73d7e151b 100644 --- a/src/analyses/invariant_propagation.cpp +++ b/src/analyses/invariant_propagation.cpp @@ -6,7 +6,6 @@ Author: Daniel Kroening, kroening@kroening.com \*******************************************************************/ -#include #include #include #include diff --git a/src/analyses/invariant_set.cpp b/src/analyses/invariant_set.cpp index 171e6510233..725a0fbc648 100644 --- a/src/analyses/invariant_set.cpp +++ b/src/analyses/invariant_set.cpp @@ -10,7 +10,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include #include #include #include @@ -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); } diff --git a/src/analyses/local_may_alias.cpp b/src/analyses/local_may_alias.cpp index c69158aebd7..25e3c4d5211 100644 --- a/src/analyses/local_may_alias.cpp +++ b/src/analyses/local_may_alias.cpp @@ -9,6 +9,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include #include #include #include @@ -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); diff --git a/src/analyses/static_analysis.cpp b/src/analyses/static_analysis.cpp index 2888ac26ec5..266b0131580 100644 --- a/src/analyses/static_analysis.cpp +++ b/src/analyses/static_analysis.cpp @@ -11,7 +11,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include #include "is_threaded.h" diff --git a/src/ansi-c/ansi_c_entry_point.cpp b/src/ansi-c/ansi_c_entry_point.cpp index 995ccf6ba03..bfb3f8663b1 100644 --- a/src/ansi-c/ansi_c_entry_point.cpp +++ b/src/ansi-c/ansi_c_entry_point.cpp @@ -10,7 +10,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include #include #include #include @@ -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); diff --git a/src/ansi-c/ansi_c_language.cpp b/src/ansi-c/ansi_c_language.cpp index 26be3f18935..dc69515ede2 100644 --- a/src/ansi-c/ansi_c_language.cpp +++ b/src/ansi-c/ansi_c_language.cpp @@ -10,7 +10,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include #include #include diff --git a/src/ansi-c/c_typecast.cpp b/src/ansi-c/c_typecast.cpp index 8486a01b406..06698fbd564 100644 --- a/src/ansi-c/c_typecast.cpp +++ b/src/ansi-c/c_typecast.cpp @@ -10,6 +10,7 @@ Author: Daniel Kroening, kroening@kroening.com #include +#include #include #include #include @@ -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)) diff --git a/src/ansi-c/c_typecheck_argc_argv.cpp b/src/ansi-c/c_typecheck_argc_argv.cpp index 71ac609d4b3..a528a630042 100644 --- a/src/ansi-c/c_typecheck_argc_argv.cpp +++ b/src/ansi-c/c_typecheck_argc_argv.cpp @@ -7,7 +7,6 @@ Author: Daniel Kroening, kroening@kroening.com \*******************************************************************/ #include -#include #include "c_typecheck_base.h" diff --git a/src/ansi-c/c_typecheck_expr.cpp b/src/ansi-c/c_typecheck_expr.cpp index abe2b49a1d1..1b9e8edae81 100644 --- a/src/ansi-c/c_typecheck_expr.cpp +++ b/src/ansi-c/c_typecheck_expr.cpp @@ -11,7 +11,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include -#include #include #include #include @@ -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(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) diff --git a/src/ansi-c/c_typecheck_initializer.cpp b/src/ansi-c/c_typecheck_initializer.cpp index c700210149e..4448f8f8de0 100644 --- a/src/ansi-c/c_typecheck_initializer.cpp +++ b/src/ansi-c/c_typecheck_initializer.cpp @@ -10,7 +10,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include -#include #include #include #include diff --git a/src/ansi-c/c_typecheck_type.cpp b/src/ansi-c/c_typecheck_type.cpp index 879fbc34efc..f6af7da7a1a 100644 --- a/src/ansi-c/c_typecheck_type.cpp +++ b/src/ansi-c/c_typecheck_type.cpp @@ -12,7 +12,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include -#include #include #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())); } } } diff --git a/src/ansi-c/literals/convert_float_literal.cpp b/src/ansi-c/literals/convert_float_literal.cpp index a7e256bf869..6eeaecb0dd8 100644 --- a/src/ansi-c/literals/convert_float_literal.cpp +++ b/src/ansi-c/literals/convert_float_literal.cpp @@ -11,9 +11,9 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include +#include #include #include -#include #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; } diff --git a/src/ansi-c/literals/convert_integer_literal.cpp b/src/ansi-c/literals/convert_integer_literal.cpp index 81fa0da5ac3..705fa23c645 100644 --- a/src/ansi-c/literals/convert_integer_literal.cpp +++ b/src/ansi-c/literals/convert_integer_literal.cpp @@ -13,7 +13,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include -#include #include #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 diff --git a/src/ansi-c/parser_static.inc b/src/ansi-c/parser_static.inc index 791c91fc6b7..eb91ce52983 100644 --- a/src/ansi-c/parser_static.inc +++ b/src/ansi-c/parser_static.inc @@ -1,7 +1,6 @@ #include #include #include -#include #include #include "c_types.h" diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp index 35a5002572d..51fd717edb2 100644 --- a/src/cbmc/cbmc_parse_options.cpp +++ b/src/cbmc/cbmc_parse_options.cpp @@ -13,7 +13,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include #include #include #include diff --git a/src/cbmc/counterexample_beautification.cpp b/src/cbmc/counterexample_beautification.cpp index 8475f122040..c0e5d1ba230 100644 --- a/src/cbmc/counterexample_beautification.cpp +++ b/src/cbmc/counterexample_beautification.cpp @@ -7,7 +7,6 @@ Author: Daniel Kroening, kroening@kroening.com \*******************************************************************/ #include -#include #include #include #include diff --git a/src/cbmc/fault_localization.cpp b/src/cbmc/fault_localization.cpp index 1554efa4b13..d1d711fe274 100644 --- a/src/cbmc/fault_localization.cpp +++ b/src/cbmc/fault_localization.cpp @@ -7,7 +7,6 @@ Author: Peter Schrammel \*******************************************************************/ #include -#include #include #include #include diff --git a/src/cegis/danger/symex/learn/danger_learn_config.cpp b/src/cegis/danger/symex/learn/danger_learn_config.cpp index 159af723b91..7a085695713 100644 --- a/src/cegis/danger/symex/learn/danger_learn_config.cpp +++ b/src/cegis/danger/symex/learn/danger_learn_config.cpp @@ -9,7 +9,7 @@ Author: Daniel Kroening, kroening@kroening.com #include -#include +#include #include #include @@ -61,7 +61,7 @@ void danger_learn_configt::process(const size_t max_solution_size) get_invariant_constraint_vars(ce_vars, original_program); counterexamplet dummy_ce; const typet type(cegis_default_integer_type()); // XXX: Currently single data type - const exprt zero(gen_zero(type)); + const exprt zero(from_integer(0, type)); for (const symbol_exprt &var : ce_vars) dummy_ce.insert(std::make_pair(var.get_identifier(), zero)); counterexamplest empty(1, dummy_ce); diff --git a/src/cegis/invariant/symex/verify/extract_counterexample.cpp b/src/cegis/invariant/symex/verify/extract_counterexample.cpp index 4a2d9cf211f..b02412176a0 100644 --- a/src/cegis/invariant/symex/verify/extract_counterexample.cpp +++ b/src/cegis/invariant/symex/verify/extract_counterexample.cpp @@ -10,7 +10,8 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include +#include + #include #include @@ -63,7 +64,7 @@ class extract_counterexamplet for (const goto_programt::targett &pos : q) { const irep_idt &var=get_affected_variable(*pos); - const exprt value(gen_zero(get_affected_type(*pos))); + const exprt value(from_integer(0, get_affected_type(*pos))); result.insert(std::make_pair(var, value)); } q.clear(); diff --git a/src/cegis/invariant/symex/verify/insert_constraint.cpp b/src/cegis/invariant/symex/verify/insert_constraint.cpp index 0eb89c01e09..1e8b84fdfe3 100644 --- a/src/cegis/invariant/symex/verify/insert_constraint.cpp +++ b/src/cegis/invariant/symex/verify/insert_constraint.cpp @@ -10,7 +10,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include #include #include diff --git a/src/cegis/jsa/constraint/jsa_constraint_factory.cpp b/src/cegis/jsa/constraint/jsa_constraint_factory.cpp index 00b611f9d36..7db0d975c79 100644 --- a/src/cegis/jsa/constraint/jsa_constraint_factory.cpp +++ b/src/cegis/jsa/constraint/jsa_constraint_factory.cpp @@ -7,7 +7,7 @@ Author: Daniel Kroening, kroening@kroening.com \*******************************************************************/ -#include +#include #include #include @@ -30,7 +30,7 @@ const notequal_exprt get_base_case(const jsa_programt &prog) { const irep_idt &id=get_affected_variable(*prog.base_case); const symbol_exprt symbol(prog.st.lookup(id).symbol_expr()); - return notequal_exprt(symbol, gen_zero(symbol.type())); + return notequal_exprt(symbol, from_integer(0, symbol.type())); } void imply_true(const jsa_programt &prog, goto_programt &body, @@ -40,10 +40,10 @@ void imply_true(const jsa_programt &prog, goto_programt &body, const goto_programt::targett restriction=body.insert_after(pos); restriction->type=instr_type; const symbol_exprt smb(as_symbol(prog.st, get_affected_variable(*pos))); - const notequal_exprt consequent(smb, gen_zero(smb.type())); + const notequal_exprt consequent(smb, from_integer(0, smb.type())); const irep_idt &sid=get_affected_variable(*prog.inductive_assumption); const symbol_exprt si(as_symbol(prog.st, sid)); - const equal_exprt antecedent(si, gen_zero(si.type())); + const equal_exprt antecedent(si, from_integer(0, si.type())); const or_exprt safety_implication(antecedent, consequent); restriction->guard=and_exprt(get_base_case(prog), safety_implication); restriction->source_location=jsa_builtin_source_location(); diff --git a/src/cegis/jsa/instrument/temps_helper.cpp b/src/cegis/jsa/instrument/temps_helper.cpp index d70f9c5ef50..7bb7510c2f3 100644 --- a/src/cegis/jsa/instrument/temps_helper.cpp +++ b/src/cegis/jsa/instrument/temps_helper.cpp @@ -10,7 +10,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include #include #include @@ -39,7 +38,7 @@ goto_programt::targett zero_jsa_temps(jsa_programt &prog, { if (!is_tmp(symbol)) continue; const symbol_exprt lhs(symbol.second.symbol_expr()); - pos=jsa_assign(st, gf, pos, lhs, gen_zero(lhs.type())); + pos=jsa_assign(st, gf, pos, lhs, from_integer(0, lhs.type())); } return pos; } @@ -77,7 +76,7 @@ void add_zero_jsa_temps_to_pred_exec(jsa_programt &prog) const constant_exprt index(from_integer(i, signed_int_type())); const index_exprt elem(ops, index); const dereference_exprt lhs(elem, jsa_word_type()); - const exprt rhs(gen_zero(lhs.type())); + const exprt rhs(from_integer(0, lhs.type())); pos=cegis_assign(st, body, pos, lhs, rhs, loc); } move_labels(body, return_pos, pos); diff --git a/src/cegis/jsa/learn/execute_jsa_programs.cpp b/src/cegis/jsa/learn/execute_jsa_programs.cpp index 27fed92b3fc..5e1433c3e14 100644 --- a/src/cegis/jsa/learn/execute_jsa_programs.cpp +++ b/src/cegis/jsa/learn/execute_jsa_programs.cpp @@ -7,8 +7,9 @@ Author: Daniel Kroening, kroening@kroening.com \*******************************************************************/ +#include + #include -#include #include #include @@ -47,7 +48,8 @@ void make_constraint_call(const symbol_tablet &st, goto_functionst &gf, args.push_back(address_of_exprt(get_user_heap(gf))); args.push_back(address_of_exprt(get_queried_heap(st))); const symbol_exprt p(st.lookup(get_cegis_meta_name(JSA_INV)).symbol_expr()); - args.push_back(address_of_exprt(index_exprt(p, gen_zero(signed_int_type())))); + constant_exprt zero=from_integer(0, signed_int_type()); + args.push_back(address_of_exprt(index_exprt(p, zero))); args.push_back(st.lookup(get_cegis_meta_name(JSA_INV_SZ)).symbol_expr()); make_constraint_call(st, gf, pos, args); } @@ -73,7 +75,8 @@ void make_query_call(jsa_programt &prog, const symbol_tablet &st, code_function_callt::argumentst &args=call.arguments(); args.push_back(address_of_exprt(get_queried_heap(st))); const symbol_exprt p(st.lookup(get_cegis_meta_name(JSA_QUERY)).symbol_expr()); - args.push_back(address_of_exprt(index_exprt(p, gen_zero(signed_int_type())))); + constant_exprt zero=from_integer(0, signed_int_type()); + args.push_back(address_of_exprt(index_exprt(p, zero))); args.push_back(st.lookup(get_cegis_meta_name(JSA_QUERY_SZ)).symbol_expr()); pos->code=call; } @@ -91,7 +94,8 @@ void make_sync_call(const symbol_tablet &st, goto_functionst &gf, args.push_back(address_of_exprt(get_user_heap(gf))); args.push_back(address_of_exprt(get_queried_heap(st))); const symbol_exprt p(st.lookup(get_cegis_meta_name(JSA_QUERY)).symbol_expr()); - args.push_back(address_of_exprt(index_exprt(p, gen_zero(signed_int_type())))); + constant_exprt zero=from_integer(0, signed_int_type()); + args.push_back(address_of_exprt(index_exprt(p, zero))); args.push_back(st.lookup(get_cegis_meta_name(JSA_QUERY_SZ)).symbol_expr()); pos->code=call; } diff --git a/src/cegis/jsa/learn/insert_counterexample.cpp b/src/cegis/jsa/learn/insert_counterexample.cpp index 6d277d54e2a..531c60df191 100644 --- a/src/cegis/jsa/learn/insert_counterexample.cpp +++ b/src/cegis/jsa/learn/insert_counterexample.cpp @@ -9,7 +9,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include #include #include @@ -93,7 +92,8 @@ void add_array_index(jsa_programt &prog) pos=body.insert_after(pos); const typet type(signed_int_type()); declare_jsa_meta_variable(st, pos, CE_ARRAY_INDEX, type); - pos=assign_jsa_meta_variable(st, gf, pos, CE_ARRAY_INDEX, gen_zero(type)); + constant_exprt zero=from_integer(0, signed_int_type()); + pos=assign_jsa_meta_variable(st, gf, pos, CE_ARRAY_INDEX, zero); } symbol_exprt get_ce_array_index(const symbol_tablet &st) @@ -110,7 +110,7 @@ void add_ce_goto(jsa_programt &prog, const size_t ces_size) pos->type=goto_program_instruction_typet::ASSIGN; const symbol_exprt lhs(get_ce_array_index(prog.st)); const typet &type=lhs.type(); - const plus_exprt inc(lhs, gen_one(type), type); + const plus_exprt inc(lhs, from_integer(1, type), type); pos->code=code_assignt(lhs, inc); pos=body.insert_after(pos); pos->source_location=jsa_builtin_source_location(); diff --git a/src/cegis/jsa/learn/insert_predicates_and_queries.cpp b/src/cegis/jsa/learn/insert_predicates_and_queries.cpp index 4aaf9e38cb5..2727450b193 100644 --- a/src/cegis/jsa/learn/insert_predicates_and_queries.cpp +++ b/src/cegis/jsa/learn/insert_predicates_and_queries.cpp @@ -12,7 +12,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include -#include #include #include @@ -36,7 +35,7 @@ goto_programt::targett assume_less_than(goto_programt &body, pos->type=goto_program_instruction_typet::ASSUME; const constant_exprt max_expr(from_integer(max, jsa_internal_index_type())); const binary_relation_exprt size_limit(lhs, ID_le, max_expr); - const exprt min(gen_one(jsa_internal_index_type())); + const exprt min(from_integer(1, jsa_internal_index_type())); const binary_relation_exprt min_size(lhs, ID_ge, min); pos->guard=and_exprt(min_size, size_limit); return pos; @@ -72,7 +71,7 @@ void declare_jsa_predicates(jsa_programt &prog, const size_t max_sz) const bv_arithmetict bv(to_array_type(preds.type()).size()); const mp_integer::ullong_t num_preds=bv.to_integer().to_ulong(); const typet sz_type(signed_int_type()); - const exprt zero(gen_zero(sz_type)); + const exprt zero(from_integer(0, sz_type)); const size_t max_pred_size=get_max_pred_size(st); for (mp_integer::ullong_t i=0; i < num_preds; ++i) { diff --git a/src/cegis/jsa/learn/instrument_pred_ops.cpp b/src/cegis/jsa/learn/instrument_pred_ops.cpp index 9e001bdb34d..7f477b1cd2b 100644 --- a/src/cegis/jsa/learn/instrument_pred_ops.cpp +++ b/src/cegis/jsa/learn/instrument_pred_ops.cpp @@ -12,7 +12,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include -#include #include #include @@ -71,7 +70,7 @@ void mark_dead(goto_programt &body, goto_programt::targett pos, pos=body.insert_after(pos); pos->type=goto_program_instruction_typet::ASSIGN; pos->source_location=jsa_builtin_source_location(); - pos->code=code_assignt(op_elem, gen_zero(op_elem.type())); + pos->code=code_assignt(op_elem, from_integer(0, op_elem.type())); } } diff --git a/src/cegis/jsa/preprocessing/create_temp_variables.cpp b/src/cegis/jsa/preprocessing/create_temp_variables.cpp index 4f142e7210e..95f552f94b0 100644 --- a/src/cegis/jsa/preprocessing/create_temp_variables.cpp +++ b/src/cegis/jsa/preprocessing/create_temp_variables.cpp @@ -7,7 +7,7 @@ Author: Daniel Kroening, kroening@kroening.com \*******************************************************************/ -#include +#include #include @@ -30,7 +30,7 @@ void create_jsa_temp_variables(jsa_programt &prog, const size_t max_size) pos=body.insert_after(pos); const std::string base_name(tmp_prefix + std::to_string(i)); declare_jsa_meta_variable(st, pos, base_name, type); - pos=assign_jsa_meta_variable(st, gf, pos, base_name, gen_zero(type)); + pos=assign_jsa_meta_variable(st, gf, pos, base_name, from_integer(0, type)); } prog.synthetic_variables=pos; } diff --git a/src/cegis/jsa/verify/extract_counterexample.cpp b/src/cegis/jsa/verify/extract_counterexample.cpp index 662dacdb6c9..3fd5a2f2d2c 100644 --- a/src/cegis/jsa/verify/extract_counterexample.cpp +++ b/src/cegis/jsa/verify/extract_counterexample.cpp @@ -9,7 +9,6 @@ Author: Daniel Kroening, kroening@kroening.com #include -#include #include #include diff --git a/src/cegis/refactor/constraint/constraint_factory.cpp b/src/cegis/refactor/constraint/constraint_factory.cpp index 42a2c324f71..66f0dd9ab7c 100644 --- a/src/cegis/refactor/constraint/constraint_factory.cpp +++ b/src/cegis/refactor/constraint/constraint_factory.cpp @@ -9,8 +9,8 @@ Author: Daniel Kroening, kroening@kroening.com #include +#include #include -#include #include #include #include @@ -88,7 +88,7 @@ void create_constraint_function_caller(refactor_programt &prog) call.function()=symbol.symbol_expr(); code_function_callt::argumentst &args=call.arguments(); for (const code_typet::parametert ¶m : type.parameters()) - args.push_back(gen_zero(param.type())); + args.push_back(from_integer(0, param.type())); pos->code=call; } body.add_instruction(goto_program_instruction_typet::END_FUNCTION); diff --git a/src/cegis/refactor/instructionset/cegis_processor_body_factory.cpp b/src/cegis/refactor/instructionset/cegis_processor_body_factory.cpp index 567276dc536..a7ccb540296 100644 --- a/src/cegis/refactor/instructionset/cegis_processor_body_factory.cpp +++ b/src/cegis/refactor/instructionset/cegis_processor_body_factory.cpp @@ -11,7 +11,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include #include #include @@ -163,7 +162,7 @@ class body_factoryt void declare_instruction_loop_head() { - decl(CEGIS_PROC_INSTR_INDEX, gen_zero(cegis_size_type())); + decl(CEGIS_PROC_INSTR_INDEX, from_integer(0, cegis_size_type())); const member_exprt opcode(cegis_opcode(st, func_name)); const size_t size(num_instrs(ordered_instructions)); assume_less(pos=body.insert_after(pos), opcode, size); @@ -178,7 +177,7 @@ class body_factoryt const char * const base_idx_name=CEGIS_PROC_INSTR_INDEX; const std::string idx(meta_name(base_idx_name)); const symbol_exprt idx_expr(st.lookup(idx).symbol_expr()); - const plus_exprt rhs(idx_expr, gen_one(idx_expr.type())); + const plus_exprt rhs(idx_expr, from_integer(1, idx_expr.type())); cegis_assign_local_variable(st, body, pos, func_name, base_idx_name, rhs); pos=std::prev(body.instructions.end(), 2); const std::string index(meta_name(CEGIS_PROC_INSTR_INDEX)); diff --git a/src/cegis/refactor/instructionset/execute_cegis_program.cpp b/src/cegis/refactor/instructionset/execute_cegis_program.cpp index 347f550bde5..663ddcb8b20 100644 --- a/src/cegis/refactor/instructionset/execute_cegis_program.cpp +++ b/src/cegis/refactor/instructionset/execute_cegis_program.cpp @@ -9,7 +9,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include #include #include @@ -56,7 +55,7 @@ void call_processor(const symbol_tablet &st, goto_programt::instructiont &instr, code_function_callt::argumentst &args=call.arguments(); const symbolt &prog_symbol=st.lookup(program_name); const symbol_exprt prog(prog_symbol.symbol_expr()); - const index_exprt first_instr(prog, gen_zero(signed_int_type())); + const index_exprt first_instr(prog, from_integer(0, signed_int_type())); args.push_back(address_of_exprt(first_instr)); const bv_arithmetict bv(get_size(prog_symbol)); const mp_integer sz_val(bv.to_integer()); diff --git a/src/cegis/refactor/learn/instrument_counterexamples.cpp b/src/cegis/refactor/learn/instrument_counterexamples.cpp index 58af6e51c03..4e6051f8283 100644 --- a/src/cegis/refactor/learn/instrument_counterexamples.cpp +++ b/src/cegis/refactor/learn/instrument_counterexamples.cpp @@ -11,7 +11,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include #include #include @@ -73,7 +72,7 @@ void create_ce_arrays(symbol_tablet &st, goto_functionst &gf, void create_ce_array_indexes(const std::set &ce_keys, symbol_tablet &st, goto_functionst &gf) { - const exprt zero(gen_zero(signed_int_type())); + const exprt zero(from_integer(0, signed_int_type())); declare_global_meta_variable(st, gf, CE_ARRAY_INDEX, zero); goto_programt &body=get_body(gf, CONSTRAINT_CALLER_ID); goto_programt::targett pos=body.instructions.begin(); diff --git a/src/cegis/safety/symex/learn/safety_learn_config.cpp b/src/cegis/safety/symex/learn/safety_learn_config.cpp index da2331cbda3..ec8c97de57a 100644 --- a/src/cegis/safety/symex/learn/safety_learn_config.cpp +++ b/src/cegis/safety/symex/learn/safety_learn_config.cpp @@ -9,7 +9,7 @@ Author: Daniel Kroening, kroening@kroening.com #include -#include +#include #include @@ -65,7 +65,7 @@ void safety_learn_configt::process(const size_t max_solution_size) constraint_varst ce_vars; get_invariant_constraint_vars(ce_vars, original_program); const typet type(cegis_default_integer_type()); // XXX: Currently single data type - const exprt zero(gen_zero(type)); + const exprt zero(from_integer(0, type)); counterexamplet dummy_ce; dummy_ce.x.push_back(counterexamplet::assignmentst()); counterexamplet::assignmentst &x=dummy_ce.x.front(); diff --git a/src/cegis/seed/literals_seed.cpp b/src/cegis/seed/literals_seed.cpp index 7e7c7b63639..6cd402d5467 100644 --- a/src/cegis/seed/literals_seed.cpp +++ b/src/cegis/seed/literals_seed.cpp @@ -10,7 +10,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include +#include #include #include @@ -275,7 +275,8 @@ class value_poolt const size_t index) const { const valuest &values=operator[](id); - if (values.empty()) return to_constant_expr(gen_zero(type)); + if(values.empty()) + return from_integer(0, type); return values.at(index % values.size()); } diff --git a/src/cpp/cpp_typecheck.cpp b/src/cpp/cpp_typecheck.cpp index 6a53c0aa04d..5d0387840fe 100644 --- a/src/cpp/cpp_typecheck.cpp +++ b/src/cpp/cpp_typecheck.cpp @@ -8,7 +8,6 @@ Author: Daniel Kroening, kroening@cs.cmu.edu #include -#include #include #include #include diff --git a/src/cpp/cpp_typecheck_code.cpp b/src/cpp/cpp_typecheck_code.cpp index 05f5491dc9a..0914df233d1 100644 --- a/src/cpp/cpp_typecheck_code.cpp +++ b/src/cpp/cpp_typecheck_code.cpp @@ -6,7 +6,6 @@ Author: Daniel Kroening, kroening@cs.cmu.edu \*******************************************************************/ -#include #include #include "cpp_typecheck.h" diff --git a/src/cpp/cpp_typecheck_compound_type.cpp b/src/cpp/cpp_typecheck_compound_type.cpp index 83dea257569..f8057808f38 100644 --- a/src/cpp/cpp_typecheck_compound_type.cpp +++ b/src/cpp/cpp_typecheck_compound_type.cpp @@ -9,7 +9,6 @@ Author: Daniel Kroening, kroening@cs.cmu.edu #include #include -#include #include #include diff --git a/src/cpp/cpp_typecheck_constructor.cpp b/src/cpp/cpp_typecheck_constructor.cpp index d3ce33b2871..65e97dfd263 100644 --- a/src/cpp/cpp_typecheck_constructor.cpp +++ b/src/cpp/cpp_typecheck_constructor.cpp @@ -9,7 +9,6 @@ Author: Daniel Kroening, kroening@cs.cmu.edu #include #include #include -#include #include diff --git a/src/cpp/cpp_typecheck_conversions.cpp b/src/cpp/cpp_typecheck_conversions.cpp index 37017ec41d9..32878368f1f 100644 --- a/src/cpp/cpp_typecheck_conversions.cpp +++ b/src/cpp/cpp_typecheck_conversions.cpp @@ -10,7 +10,6 @@ Module: C++ Language Type Checking #include #include -#include #include #include #include diff --git a/src/cpp/cpp_typecheck_declaration.cpp b/src/cpp/cpp_typecheck_declaration.cpp index 2b73f05d39c..bef63d1eda1 100644 --- a/src/cpp/cpp_typecheck_declaration.cpp +++ b/src/cpp/cpp_typecheck_declaration.cpp @@ -6,8 +6,6 @@ Author: Daniel Kroening, kroening@cs.cmu.edu \********************************************************************/ -#include - #include "cpp_typecheck.h" #include "cpp_declarator_converter.h" diff --git a/src/cpp/cpp_typecheck_expr.cpp b/src/cpp/cpp_typecheck_expr.cpp index 1bc298665f3..a8e8fed5651 100644 --- a/src/cpp/cpp_typecheck_expr.cpp +++ b/src/cpp/cpp_typecheck_expr.cpp @@ -8,7 +8,6 @@ Author: Daniel Kroening, kroening@cs.cmu.edu #include -#include #include #include #include diff --git a/src/cpp/cpp_typecheck_function.cpp b/src/cpp/cpp_typecheck_function.cpp index e0e1c5bf822..ccbd2dd58b2 100644 --- a/src/cpp/cpp_typecheck_function.cpp +++ b/src/cpp/cpp_typecheck_function.cpp @@ -6,8 +6,6 @@ Author: Daniel Kroening, kroening@cs.cmu.edu \*******************************************************************/ -#include - #include #include "cpp_template_type.h" diff --git a/src/cpp/cpp_typecheck_initializer.cpp b/src/cpp/cpp_typecheck_initializer.cpp index a225902d543..225f6d5aa5c 100644 --- a/src/cpp/cpp_typecheck_initializer.cpp +++ b/src/cpp/cpp_typecheck_initializer.cpp @@ -6,7 +6,6 @@ Author: Daniel Kroening, kroening@cs.cmu.edu \*******************************************************************/ -#include #include #include @@ -296,7 +295,7 @@ void cpp_typecheckt::zero_initializer( typet enum_type(ID_unsignedbv); enum_type.add(ID_width)=final_type.find(ID_width); - exprt zero(gen_zero(enum_type)); + exprt zero(from_integer(0, enum_type)); zero.make_typecast(type); already_typechecked(zero); diff --git a/src/cpp/cpp_typecheck_resolve.cpp b/src/cpp/cpp_typecheck_resolve.cpp index e8502c1419a..6655eb258f6 100644 --- a/src/cpp/cpp_typecheck_resolve.cpp +++ b/src/cpp/cpp_typecheck_resolve.cpp @@ -9,7 +9,6 @@ Author: Daniel Kroening, kroening@cs.cmu.edu #include #include -#include #include #include #include diff --git a/src/cpp/cpp_typecheck_template.cpp b/src/cpp/cpp_typecheck_template.cpp index 73997bb5aff..61aa6504968 100644 --- a/src/cpp/cpp_typecheck_template.cpp +++ b/src/cpp/cpp_typecheck_template.cpp @@ -6,7 +6,6 @@ Author: Daniel Kroening, kroening@cs.cmu.edu \*******************************************************************/ -#include #include #include "cpp_type2name.h" diff --git a/src/cpp/cpp_typecheck_virtual_table.cpp b/src/cpp/cpp_typecheck_virtual_table.cpp index 151ea1034e2..74efcad31c9 100644 --- a/src/cpp/cpp_typecheck_virtual_table.cpp +++ b/src/cpp/cpp_typecheck_virtual_table.cpp @@ -12,7 +12,6 @@ Function: cpp_typecheckt::do_virtual_table #include #include -#include #include "cpp_typecheck.h" diff --git a/src/goto-diff/goto_diff_parse_options.cpp b/src/goto-diff/goto_diff_parse_options.cpp index c819d1537d0..c22766492bb 100644 --- a/src/goto-diff/goto_diff_parse_options.cpp +++ b/src/goto-diff/goto_diff_parse_options.cpp @@ -13,7 +13,6 @@ Author: Peter Schrammel #include #include -#include #include #include diff --git a/src/goto-instrument/cover.cpp b/src/goto-instrument/cover.cpp index f27bbd5f19c..b7c8381a224 100644 --- a/src/goto-instrument/cover.cpp +++ b/src/goto-instrument/cover.cpp @@ -12,7 +12,6 @@ Date: May 2016 #include #include -#include #include "cover.h" diff --git a/src/goto-instrument/function.cpp b/src/goto-instrument/function.cpp index e7a08a5c1c2..1ad749814bd 100644 --- a/src/goto-instrument/function.cpp +++ b/src/goto-instrument/function.cpp @@ -6,10 +6,10 @@ Author: Daniel Kroening, kroening@kroening.com \*******************************************************************/ +#include #include #include #include -#include #include #include @@ -79,8 +79,9 @@ code_function_callt function_to_call( call.arguments().resize(1); call.arguments()[0]= typecast_exprt( - address_of_exprt(index_exprt( - function_id_string, gen_zero(index_type()))), + address_of_exprt( + index_exprt( + function_id_string, from_integer(0, index_type()))), to_code_type(s_it->second.type).parameters()[0].type()); return call; diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp index 11c3ffc6620..45a5a964812 100644 --- a/src/goto-instrument/goto_instrument_parse_options.cpp +++ b/src/goto-instrument/goto_instrument_parse_options.cpp @@ -11,7 +11,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include #include #include #include diff --git a/src/goto-instrument/mmio.cpp b/src/goto-instrument/mmio.cpp index 098e8378e18..fbd2fc5989c 100644 --- a/src/goto-instrument/mmio.cpp +++ b/src/goto-instrument/mmio.cpp @@ -15,7 +15,6 @@ Date: September 2011 #if 0 #include -#include #include #include diff --git a/src/goto-programs/builtin_functions.cpp b/src/goto-programs/builtin_functions.cpp index 687b13a664a..d6a67946730 100644 --- a/src/goto-programs/builtin_functions.cpp +++ b/src/goto-programs/builtin_functions.cpp @@ -10,7 +10,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include #include #include #include @@ -316,8 +315,11 @@ void goto_convertt::do_scanf( const symbolt &tmp_symbol= new_tmp_symbol(type, "scanf_string", dest, function.source_location()); - exprt rhs=address_of_exprt( - index_exprt(tmp_symbol.symbol_expr(), gen_zero(index_type()))); + exprt rhs= + address_of_exprt( + index_exprt( + tmp_symbol.symbol_expr(), + from_integer(0, index_type()))); // now use array copy codet array_copy_statement; @@ -838,11 +840,11 @@ void goto_convertt::do_java_new_array( side_effect_exprt inc(ID_assign); inc.operands().resize(2); inc.op0()=tmp_i; - inc.op1()=plus_exprt(tmp_i, gen_one(tmp_i.type())); + inc.op1()=plus_exprt(tmp_i, from_integer(1, tmp_i.type())); dereference_exprt deref_expr(plus_exprt(data, tmp_i), data.type().subtype()); - for_loop.init()=code_assignt(tmp_i, gen_zero(tmp_i.type())); + for_loop.init()=code_assignt(tmp_i, from_integer(0, tmp_i.type())); for_loop.cond()=binary_relation_exprt(tmp_i, ID_lt, rhs.op0()); for_loop.iter()=inc; for_loop.body()=code_skipt(); diff --git a/src/goto-programs/goto_clean_expr.cpp b/src/goto-programs/goto_clean_expr.cpp index ff9a8068c34..45c37242883 100644 --- a/src/goto-programs/goto_clean_expr.cpp +++ b/src/goto-programs/goto_clean_expr.cpp @@ -7,7 +7,6 @@ Author: Daniel Kroening, kroening@kroening.com \*******************************************************************/ #include -#include #include #include #include diff --git a/src/goto-programs/goto_convert_function_call.cpp b/src/goto-programs/goto_convert_function_call.cpp index badeebc29fb..9735f994297 100644 --- a/src/goto-programs/goto_convert_function_call.cpp +++ b/src/goto-programs/goto_convert_function_call.cpp @@ -9,7 +9,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include #include #include #include diff --git a/src/goto-programs/goto_convert_new_switch_case.cpp b/src/goto-programs/goto_convert_new_switch_case.cpp index 83b82b034c8..063fc579ead 100644 --- a/src/goto-programs/goto_convert_new_switch_case.cpp +++ b/src/goto-programs/goto_convert_new_switch_case.cpp @@ -9,7 +9,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include #include #include #include diff --git a/src/goto-programs/goto_convert_side_effect.cpp b/src/goto-programs/goto_convert_side_effect.cpp index da2d8ca7cad..6312e38f04b 100644 --- a/src/goto-programs/goto_convert_side_effect.cpp +++ b/src/goto-programs/goto_convert_side_effect.cpp @@ -6,6 +6,7 @@ Author: Daniel Kroening, kroening@kroening.com \*******************************************************************/ +#include #include #include #include @@ -197,14 +198,14 @@ void goto_convertt::remove_pre( if(op_type.id()==ID_bool) { - rhs.copy_to_operands(expr.op0(), gen_one(signed_int_type())); + rhs.copy_to_operands(expr.op0(), from_integer(1, signed_int_type())); rhs.op0().make_typecast(signed_int_type()); rhs.type()=signed_int_type(); rhs=is_not_zero(rhs, ns); } else if(op_type.id()==ID_c_bool) { - rhs.copy_to_operands(expr.op0(), gen_one(signed_int_type())); + rhs.copy_to_operands(expr.op0(), from_integer(1, signed_int_type())); rhs.op0().make_typecast(signed_int_type()); rhs.type()=signed_int_type(); rhs=is_not_zero(rhs, ns); @@ -213,7 +214,7 @@ void goto_convertt::remove_pre( else if(op_type.id()==ID_c_enum || op_type.id()==ID_c_enum_tag) { - rhs.copy_to_operands(expr.op0(), gen_one(signed_int_type())); + rhs.copy_to_operands(expr.op0(), from_integer(1, signed_int_type())); rhs.op0().make_typecast(signed_int_type()); rhs.type()=signed_int_type(); rhs.make_typecast(op_type); @@ -233,7 +234,7 @@ void goto_convertt::remove_pre( throw 0; } - exprt constant=gen_one(constant_type); + exprt constant=from_integer(1, constant_type); rhs.copy_to_operands(expr.op0()); rhs.move_to_operands(constant); @@ -301,14 +302,14 @@ void goto_convertt::remove_post( if(op_type.id()==ID_bool) { - rhs.copy_to_operands(expr.op0(), gen_one(signed_int_type())); + rhs.copy_to_operands(expr.op0(), from_integer(1, signed_int_type())); rhs.op0().make_typecast(signed_int_type()); rhs.type()=signed_int_type(); rhs=is_not_zero(rhs, ns); } else if(op_type.id()==ID_c_bool) { - rhs.copy_to_operands(expr.op0(), gen_one(signed_int_type())); + rhs.copy_to_operands(expr.op0(), from_integer(1, signed_int_type())); rhs.op0().make_typecast(signed_int_type()); rhs.type()=signed_int_type(); rhs=is_not_zero(rhs, ns); @@ -317,7 +318,7 @@ void goto_convertt::remove_post( else if(op_type.id()==ID_c_enum || op_type.id()==ID_c_enum_tag) { - rhs.copy_to_operands(expr.op0(), gen_one(signed_int_type())); + rhs.copy_to_operands(expr.op0(), from_integer(1, signed_int_type())); rhs.op0().make_typecast(signed_int_type()); rhs.type()=signed_int_type(); rhs.make_typecast(op_type); @@ -337,7 +338,16 @@ void goto_convertt::remove_post( throw 0; } - exprt constant=gen_one(constant_type); + exprt constant; + + if(constant_type.id()==ID_complex) + { + exprt real=from_integer(1, constant_type.subtype()); + exprt imag=from_integer(0, constant_type.subtype()); + constant=complex_exprt(real, imag, to_complex_type(constant_type)); + } + else + constant=from_integer(1, constant_type); rhs.copy_to_operands(expr.op0()); rhs.move_to_operands(constant); diff --git a/src/goto-programs/goto_inline.cpp b/src/goto-programs/goto_inline.cpp index d392de25170..830798c289e 100644 --- a/src/goto-programs/goto_inline.cpp +++ b/src/goto-programs/goto_inline.cpp @@ -13,7 +13,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include -#include #include "remove_skip.h" #include "goto_inline.h" diff --git a/src/goto-programs/pointer_arithmetic.cpp b/src/goto-programs/pointer_arithmetic.cpp index c080329cb75..0639a0dbca4 100644 --- a/src/goto-programs/pointer_arithmetic.cpp +++ b/src/goto-programs/pointer_arithmetic.cpp @@ -6,8 +6,8 @@ Author: Daniel Kroening, kroening@kroening.com \*******************************************************************/ +#include #include -#include #include "pointer_arithmetic.h" @@ -76,7 +76,7 @@ void pointer_arithmetict::read(const exprt &src) add_to_offset(index_expr.index()); // produce &x[0] + i instead of &x[i] exprt new_src=src; - new_src.op0().op1()=gen_zero(index_expr.index().type()); + new_src.op0().op1()=from_integer(0, index_expr.index().type()); make_pointer(new_src); } } diff --git a/src/goto-programs/remove_complex.cpp b/src/goto-programs/remove_complex.cpp index 553a70dab50..4bb030299a2 100644 --- a/src/goto-programs/remove_complex.cpp +++ b/src/goto-programs/remove_complex.cpp @@ -8,7 +8,7 @@ Date: September 2014 \*******************************************************************/ -#include +#include #include "remove_complex.h" @@ -166,7 +166,7 @@ void remove_complex(exprt &expr) struct_expr.operands().resize(2); struct_expr.op0()=typecast_exprt(expr.op0(), subtype); - struct_expr.op1()=gen_zero(subtype); + struct_expr.op1()=from_integer(0, subtype); struct_expr.add_source_location()=expr.source_location(); expr=struct_expr; diff --git a/src/goto-programs/remove_function_pointers.cpp b/src/goto-programs/remove_function_pointers.cpp index 7a25def3823..1baca8d11d5 100644 --- a/src/goto-programs/remove_function_pointers.cpp +++ b/src/goto-programs/remove_function_pointers.cpp @@ -9,7 +9,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include #include #include #include diff --git a/src/goto-programs/string_abstraction.cpp b/src/goto-programs/string_abstraction.cpp index 114eddb2d3e..a12b766eb1e 100644 --- a/src/goto-programs/string_abstraction.cpp +++ b/src/goto-programs/string_abstraction.cpp @@ -10,7 +10,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include #include #include #include @@ -764,7 +763,7 @@ void string_abstractiont::abstract_function_call( assert(type_eq(str_args.back().type().subtype(), abstract_type.subtype(), ns)); - index_exprt idx(str_args.back(), gen_zero(index_type())); + index_exprt idx(str_args.back(), from_integer(0, index_type())); // disable bounds check on that one idx.set("bounds_check", false); @@ -1533,8 +1532,15 @@ goto_programt::targett string_abstractiont::abstract_char_assign( assert(i2.is_not_nil()); make_type(ptr.offset, build_type(LENGTH)); - return char_assign(dest, target, new_lhs, i2, - ptr.offset.is_nil()?gen_zero(build_type(LENGTH)):ptr.offset); + return + char_assign( + dest, + target, + new_lhs, + i2, + ptr.offset.is_nil()? + from_integer(0, build_type(LENGTH)): + ptr.offset); } } diff --git a/src/goto-programs/string_instrumentation.cpp b/src/goto-programs/string_instrumentation.cpp index d5a269a6018..67d8a430b57 100644 --- a/src/goto-programs/string_instrumentation.cpp +++ b/src/goto-programs/string_instrumentation.cpp @@ -10,7 +10,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include #include #include #include @@ -549,7 +548,7 @@ void string_instrumentationt::do_format_string_read( { index_exprt index; index.array()=temp; - index.index()=gen_zero(index_type()); + index.index()=from_integer(0, index_type()); index.type()=arg_type.subtype(); temp=address_of_exprt(index); } @@ -597,7 +596,7 @@ void string_instrumentationt::do_format_string_read( { index_exprt index; index.array()=temp; - index.index()=gen_zero(index_type()); + index.index()=from_integer(0, index_type()); index.type()=arg_type.subtype(); temp=address_of_exprt(index); } @@ -664,7 +663,7 @@ void string_instrumentationt::do_format_string_write( { exprt fwidth = from_integer(token.field_width, unsigned_int_type()); exprt fw_1(ID_plus, unsigned_int_type()); - exprt one = gen_one(unsigned_int_type()); + exprt one=from_integer(1, unsigned_int_type()); fw_1.move_to_operands(fwidth); fw_1.move_to_operands(one); // +1 for 0-char @@ -676,7 +675,7 @@ void string_instrumentationt::do_format_string_write( { index_exprt index; index.array()=argument; - index.index()=gen_zero(unsigned_int_type()); + index.index()=from_integer(0, unsigned_int_type()); address_of_exprt aof(index); fw_lt_bs=binary_relation_exprt(fw_1, ID_le, buffer_size(aof)); } @@ -1018,16 +1017,20 @@ void string_instrumentationt::do_strerror( goto_programt::targett assumption1=tmp.add_instruction(); - assumption1->make_assumption(binary_relation_exprt( - symbol_size.symbol_expr(), ID_notequal, - gen_zero(symbol_size.type))); + assumption1->make_assumption( + binary_relation_exprt( + symbol_size.symbol_expr(), + ID_notequal, + from_integer(0, symbol_size.type))); assumption1->source_location=it->source_location; } // return a pointer to some magic buffer exprt index=exprt(ID_index, char_type()); - index.copy_to_operands(symbol_buf.symbol_expr(), gen_zero(index_type())); + index.copy_to_operands( + symbol_buf.symbol_expr(), + from_integer(0, index_type())); exprt ptr=exprt(ID_address_of, pointer_typet()); ptr.type().subtype()=char_type(); @@ -1096,7 +1099,8 @@ void string_instrumentationt::invalidate_buffer( goto_programt::targett init=dest.add_instruction(ASSIGN); init->source_location=target->source_location; - init->code=code_assignt(cntr_sym.symbol_expr(), gen_zero(cntr_sym.type)); + init->code= + code_assignt(cntr_sym.symbol_expr(), from_integer(0, cntr_sym.type)); goto_programt::targett check=dest.add_instruction(); check->source_location=target->source_location; @@ -1109,7 +1113,7 @@ void string_instrumentationt::invalidate_buffer( exprt plus(ID_plus, unsigned_int_type()); plus.copy_to_operands(cntr_sym.symbol_expr()); - plus.copy_to_operands(gen_one(unsigned_int_type())); + plus.copy_to_operands(from_integer(1, unsigned_int_type())); increment->code=code_assignt(cntr_sym.symbol_expr(), plus); @@ -1130,7 +1134,7 @@ void string_instrumentationt::invalidate_buffer( { index_exprt index; index.array()=buffer; - index.index()=gen_zero(index_type()); + index.index()=from_integer(0, index_type()); index.type()=buf_type.subtype(); bufp = address_of_exprt(index); } diff --git a/src/goto-symex/postcondition.cpp b/src/goto-symex/postcondition.cpp index 003f0ac60a8..d290a6335b6 100644 --- a/src/goto-symex/postcondition.cpp +++ b/src/goto-symex/postcondition.cpp @@ -7,7 +7,6 @@ Author: Daniel Kroening, kroening@kroening.com \*******************************************************************/ #include -#include #include #include "goto_symex_state.h" diff --git a/src/goto-symex/rewrite_union.cpp b/src/goto-symex/rewrite_union.cpp index 26b9282dfdf..903ec267466 100644 --- a/src/goto-symex/rewrite_union.cpp +++ b/src/goto-symex/rewrite_union.cpp @@ -6,9 +6,9 @@ Author: Daniel Kroening, kroening@kroening.com \*******************************************************************/ +#include #include #include -#include #include #include @@ -42,7 +42,7 @@ void rewrite_union( if(op_type.id()==ID_union) { - exprt offset=gen_zero(index_type()); + exprt offset=from_integer(0, index_type()); byte_extract_exprt tmp(byte_extract_id(), op, offset, expr.type()); expr=tmp; } @@ -50,7 +50,7 @@ void rewrite_union( else if(expr.id()==ID_union) { const union_exprt &union_expr=to_union_expr(expr); - exprt offset=gen_zero(index_type()); + exprt offset=from_integer(0, index_type()); side_effect_expr_nondett nondet(expr.type()); byte_update_exprt tmp( byte_update_id(), nondet, offset, union_expr.op()); diff --git a/src/goto-symex/symex_assign.cpp b/src/goto-symex/symex_assign.cpp index f251a1884ac..b8200280648 100644 --- a/src/goto-symex/symex_assign.cpp +++ b/src/goto-symex/symex_assign.cpp @@ -6,7 +6,6 @@ Author: Daniel Kroening, kroening@kroening.com \*******************************************************************/ -#include #include #include diff --git a/src/goto-symex/symex_builtin_functions.cpp b/src/goto-symex/symex_builtin_functions.cpp index 19cfe1f7e5c..1eaf30353d3 100644 --- a/src/goto-symex/symex_builtin_functions.cpp +++ b/src/goto-symex/symex_builtin_functions.cpp @@ -8,7 +8,6 @@ Author: Daniel Kroening, kroening@kroening.com #include -#include #include #include #include @@ -176,7 +175,7 @@ void goto_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 @@ -498,7 +497,9 @@ void goto_symext::symex_cpp_new( if(do_array) { exprt index_expr(ID_index, code.type().subtype()); - index_expr.copy_to_operands(symbol.symbol_expr(), gen_zero(index_type())); + index_expr.copy_to_operands( + symbol.symbol_expr(), + from_integer(0, index_type())); rhs.move_to_operands(index_expr); } else diff --git a/src/goto-symex/symex_clean_expr.cpp b/src/goto-symex/symex_clean_expr.cpp index 338854922b3..a88075d4a62 100644 --- a/src/goto-symex/symex_clean_expr.cpp +++ b/src/goto-symex/symex_clean_expr.cpp @@ -6,8 +6,8 @@ Author: Daniel Kroening, kroening@kroening.com \*******************************************************************/ +#include #include -#include #include #include @@ -78,7 +78,7 @@ void goto_symext::process_array_expr_rec( byte_extract_exprt be(byte_extract_id()); be.type()=type; be.op()=expr; - be.offset()=gen_zero(index_type()); + be.offset()=from_integer(0, index_type()); expr.swap(be); } diff --git a/src/goto-symex/symex_dead.cpp b/src/goto-symex/symex_dead.cpp index cb954a6fad0..ec9440bc5e8 100644 --- a/src/goto-symex/symex_dead.cpp +++ b/src/goto-symex/symex_dead.cpp @@ -8,7 +8,6 @@ Author: Daniel Kroening, kroening@kroening.com #include -#include #include #include diff --git a/src/goto-symex/symex_decl.cpp b/src/goto-symex/symex_decl.cpp index 60a94a610de..d46c449c755 100644 --- a/src/goto-symex/symex_decl.cpp +++ b/src/goto-symex/symex_decl.cpp @@ -8,7 +8,6 @@ Author: Daniel Kroening, kroening@kroening.com #include -#include #include #include diff --git a/src/goto-symex/symex_dereference.cpp b/src/goto-symex/symex_dereference.cpp index dbe5e9aed3c..2234f7d8eaa 100644 --- a/src/goto-symex/symex_dereference.cpp +++ b/src/goto-symex/symex_dereference.cpp @@ -6,7 +6,6 @@ Author: Daniel Kroening, kroening@kroening.com \*******************************************************************/ -#include #include #include #include @@ -150,7 +149,7 @@ exprt goto_symext::address_arithmetic( for(const typet *t=&(ns.follow(a.type().subtype())); t->id()==ID_array && !base_type_eq(expr.type(), *t, ns); t=&(ns.follow(*t).subtype())) - a.object()=index_exprt(a.object(), gen_zero(index_type())); + a.object()=index_exprt(a.object(), from_integer(0, index_type())); } // do (expr.type() *)(((char *)op)+offset) @@ -224,7 +223,7 @@ exprt goto_symext::address_arithmetic( // turn &array into &array[0] if(ns.follow(result.type()).id()==ID_array && !keep_array) - result=index_exprt(result, gen_zero(index_type())); + result=index_exprt(result, from_integer(0, index_type())); // handle field-sensitive SSA symbol mp_integer offset=0; @@ -360,9 +359,11 @@ void goto_symext::dereference_rec( pointer_typet(to_address_of_expr(tc_op).object().type().subtype()), ns)) { - expr=address_of_exprt(index_exprt( - to_address_of_expr(tc_op).object(), - gen_zero(index_type())));; + expr= + address_of_exprt( + index_exprt( + to_address_of_expr(tc_op).object(), + from_integer(0, index_type()))); dereference_rec(expr, state, guard, write); } diff --git a/src/goto-symex/symex_function_call.cpp b/src/goto-symex/symex_function_call.cpp index 16574d5679f..b333ebbc3a1 100644 --- a/src/goto-symex/symex_function_call.cpp +++ b/src/goto-symex/symex_function_call.cpp @@ -10,7 +10,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include #include #include #include @@ -135,7 +134,7 @@ void goto_symext::parameter_assignments( byte_extract_exprt( byte_extract_id(), rhs, - gen_zero(index_type()), + from_integer(0, index_type()), parameter_type); } else diff --git a/src/goto-symex/symex_goto.cpp b/src/goto-symex/symex_goto.cpp index 17149677965..2c64e62b15e 100644 --- a/src/goto-symex/symex_goto.cpp +++ b/src/goto-symex/symex_goto.cpp @@ -9,7 +9,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include #include #include "goto_symex.h" diff --git a/src/goto-symex/symex_other.cpp b/src/goto-symex/symex_other.cpp index 87f5428fe68..315447093ea 100644 --- a/src/goto-symex/symex_other.cpp +++ b/src/goto-symex/symex_other.cpp @@ -8,7 +8,7 @@ Author: Daniel Kroening, kroening@kroening.com #include -#include +#include #include #include #include @@ -116,7 +116,7 @@ void goto_symext::symex_other( byte_extract_exprt be(byte_extract_id()); be.type()=clean_code.op0().type(); be.op()=clean_code.op1(); - be.offset()=gen_zero(index_type()); + be.offset()=from_integer(0, index_type()); clean_code.op1()=be; } diff --git a/src/goto-symex/symex_target_equation.cpp b/src/goto-symex/symex_target_equation.cpp index 8b2aecfbcaa..66b9a87e9af 100644 --- a/src/goto-symex/symex_target_equation.cpp +++ b/src/goto-symex/symex_target_equation.cpp @@ -9,7 +9,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include #include #include diff --git a/src/java_bytecode/java_bytecode_convert_method.cpp b/src/java_bytecode/java_bytecode_convert_method.cpp index a2ca21ef80d..5935fe8e321 100644 --- a/src/java_bytecode/java_bytecode_convert_method.cpp +++ b/src/java_bytecode/java_bytecode_convert_method.cpp @@ -16,7 +16,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include -#include + #include #include @@ -1353,7 +1353,7 @@ codet java_bytecode_convert_methodt::convert_instructions( code_ifthenelset code_branch; code_branch.cond()= - binary_relation_exprt(op[0], id, gen_zero(op[0].type())); + binary_relation_exprt(op[0], id, from_integer(0, op[0].type())); code_branch.cond().add_source_location()=i_it->source_location; code_branch.cond().add_source_location().set_function(method_id); code_branch.then_case()=code_gotot(label(number)); @@ -1524,7 +1524,7 @@ codet java_bytecode_convert_methodt::convert_instructions( nan_result, if_exprt( ieee_float_equal_exprt(op[0], op[1]), - gen_zero(result_type), + from_integer(0, result_type), if_exprt( binary_relation_exprt(op[0], ID_lt, op[1]), minus_one, diff --git a/src/java_bytecode/java_entry_point.cpp b/src/java_bytecode/java_entry_point.cpp index e2c71735fec..d4d40beff3b 100644 --- a/src/java_bytecode/java_entry_point.cpp +++ b/src/java_bytecode/java_entry_point.cpp @@ -15,7 +15,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include -#include #include #include #include @@ -63,7 +62,8 @@ static void create_initialize(symbol_tablet &symbol_table) symbol_exprt rounding_mode= ns.lookup(CPROVER_PREFIX "rounding_mode").symbol_expr(); - init_code.add(code_assignt(rounding_mode, gen_zero(rounding_mode.type()))); + init_code.add( + code_assignt(rounding_mode, from_integer(0, rounding_mode.type()))); initialize.value=init_code; @@ -241,10 +241,11 @@ exprt::operandst java_build_arguments( // record as an input codet input(ID_input); input.operands().resize(2); - input.op0()=address_of_exprt( - index_exprt( - string_constantt(p_symbol.base_name), - from_integer(0, index_type()))); + input.op0()= + address_of_exprt( + index_exprt( + string_constantt(p_symbol.base_name), + from_integer(0, index_type()))); input.op1()=main_arguments[param_number]; input.add_source_location()=function.location; diff --git a/src/java_bytecode/java_object_factory.cpp b/src/java_bytecode/java_object_factory.cpp index f8f3d98748f..e7ab2f1a658 100644 --- a/src/java_bytecode/java_object_factory.cpp +++ b/src/java_bytecode/java_object_factory.cpp @@ -17,7 +17,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include -#include #include @@ -302,7 +301,7 @@ void java_object_factoryt::gen_nondet_init( } else if(name=="@lock") { - code_assignt code(me, gen_zero(me.type())); + code_assignt code(me, from_integer(0, me.type())); code.add_source_location()=loc; init_code.copy_to_operands(code); } diff --git a/src/jsil/jsil_entry_point.cpp b/src/jsil/jsil_entry_point.cpp index 2963ebb514f..c6f9c26abe8 100644 --- a/src/jsil/jsil_entry_point.cpp +++ b/src/jsil/jsil_entry_point.cpp @@ -6,12 +6,12 @@ Author: Michael Tautschnig, tautschn@amazon.com \*******************************************************************/ +#include #include #include #include #include #include -#include #include @@ -49,7 +49,7 @@ static void create_initialize(symbol_tablet &symbol_table) symbol_exprt rounding_mode= ns.lookup(CPROVER_PREFIX "rounding_mode").symbol_expr(); - code_assignt a(rounding_mode, gen_zero(rounding_mode.type())); + code_assignt a(rounding_mode, from_integer(0, rounding_mode.type())); init_code.add(a); initialize.value=init_code; diff --git a/src/linking/static_lifetime_init.cpp b/src/linking/static_lifetime_init.cpp index e008d64c612..8e7d475766c 100644 --- a/src/linking/static_lifetime_init.cpp +++ b/src/linking/static_lifetime_init.cpp @@ -10,7 +10,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include #include #include #include @@ -118,7 +117,7 @@ bool static_lifetime_init( assert(it!=symbol_table.symbols.end()); it->second.type=type; - it->second.type.set(ID_size, gen_one(size_type())); + it->second.type.set(ID_size, from_integer(1, size_type())); } if(type.id()==ID_incomplete_struct || diff --git a/src/linking/zero_initializer.cpp b/src/linking/zero_initializer.cpp index 24d483cb4c9..d652427059d 100644 --- a/src/linking/zero_initializer.cpp +++ b/src/linking/zero_initializer.cpp @@ -110,7 +110,7 @@ exprt zero_initializert::zero_initializer_rec( array_exprt value(array_type); value.type().id(ID_array); - value.type().set(ID_size, gen_zero(size_type())); + value.type().set(ID_size, from_integer(0, size_type())); value.add_source_location()=source_location; return value; } diff --git a/src/musketeer/fence_shared.cpp b/src/musketeer/fence_shared.cpp index c3557d712af..9e3a3c580f1 100644 --- a/src/musketeer/fence_shared.cpp +++ b/src/musketeer/fence_shared.cpp @@ -14,7 +14,6 @@ Author: Vincent Nimal #include #include -#include #include #include #include diff --git a/src/musketeer/fencer.cpp b/src/musketeer/fencer.cpp index bbcb1db1d2d..71587267e8f 100644 --- a/src/musketeer/fencer.cpp +++ b/src/musketeer/fencer.cpp @@ -7,7 +7,6 @@ Author: Vincent Nimal \*******************************************************************/ #include -#include #include #include diff --git a/src/musketeer/pensieve.cpp b/src/musketeer/pensieve.cpp index 42ae7b61a49..bea0fab3525 100644 --- a/src/musketeer/pensieve.cpp +++ b/src/musketeer/pensieve.cpp @@ -7,7 +7,6 @@ Author: Vincent Nimal \*******************************************************************/ #include -#include #include #include diff --git a/src/path-symex/path_symex.cpp b/src/path-symex/path_symex.cpp index a646e45409c..f3cffd498bb 100644 --- a/src/path-symex/path_symex.cpp +++ b/src/path-symex/path_symex.cpp @@ -280,7 +280,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 @@ -510,7 +510,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()); diff --git a/src/path-symex/path_symex_state.cpp b/src/path-symex/path_symex_state.cpp index 3cd0cd0d269..4f422172374 100644 --- a/src/path-symex/path_symex_state.cpp +++ b/src/path-symex/path_symex_state.cpp @@ -8,7 +8,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include #include #include diff --git a/src/pointer-analysis/dereference.cpp b/src/pointer-analysis/dereference.cpp index ca648722b04..a256a5e39d9 100644 --- a/src/pointer-analysis/dereference.cpp +++ b/src/pointer-analysis/dereference.cpp @@ -52,7 +52,7 @@ exprt dereferencet::operator()(const exprt &pointer) return dereference_rec( pointer, - gen_zero(index_type()), // offset + from_integer(0, index_type()), // offset type); } @@ -225,7 +225,7 @@ exprt dereferencet::dereference_rec( if(to_constant_expr(address).get_value()==ID_NULL) // NULL { // we turn this into (type *)0 - exprt zero=gen_zero(index_type()); + exprt zero=from_integer(0, index_type()); return dereference_rec( typecast_exprt(zero, address.type()), offset, type); } diff --git a/src/pointer-analysis/value_set.cpp b/src/pointer-analysis/value_set.cpp index 500dbd23bcf..4a22fc40acb 100644 --- a/src/pointer-analysis/value_set.cpp +++ b/src/pointer-analysis/value_set.cpp @@ -11,7 +11,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include #include #include #include @@ -1136,7 +1135,7 @@ void value_sett::get_reference_set_rec( { index_exprt index_expr(expr.type()); index_expr.array()=object; - index_expr.index()=gen_zero(index_type()); + index_expr.index()=from_integer(0, index_type()); // adjust type? if(ns.follow(object.type())!=array_type) diff --git a/src/pointer-analysis/value_set_dereference.cpp b/src/pointer-analysis/value_set_dereference.cpp index d9e8af80fc2..c69e6feda73 100644 --- a/src/pointer-analysis/value_set_dereference.cpp +++ b/src/pointer-analysis/value_set_dereference.cpp @@ -723,7 +723,7 @@ void value_set_dereferencet::bounds_check( } else { - exprt zero=gen_zero(expr.index().type()); + exprt zero=from_integer(0, expr.index().type()); if(zero.is_nil()) throw "no zero constant of index type "+ @@ -878,7 +878,7 @@ bool value_set_dereferencet::memory_model_conversion( if(options.get_bool_option("pointer-check")) { - equal_exprt offset_not_zero(offset, gen_zero(offset.type())); + equal_exprt offset_not_zero(offset, from_integer(0, offset.type())); offset_not_zero.make_not(); guardt tmp_guard(guard); @@ -972,8 +972,8 @@ bool value_set_dereferencet::memory_model_bytes( if(!offset.is_zero()) { binary_relation_exprt - offset_lower_bound(offset, ID_lt, - gen_zero(offset.type())); + offset_lower_bound( + offset, ID_lt, from_integer(0, offset.type())); guardt tmp_guard(guard); tmp_guard.add(offset_lower_bound); diff --git a/src/pointer-analysis/value_set_fi.cpp b/src/pointer-analysis/value_set_fi.cpp index e1157b49324..ed1de7872ac 100644 --- a/src/pointer-analysis/value_set_fi.cpp +++ b/src/pointer-analysis/value_set_fi.cpp @@ -11,7 +11,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include #include #include #include @@ -1029,7 +1028,7 @@ void value_set_fit::get_reference_set_sharing_rec( exprt index_expr(ID_index, expr.type()); index_expr.operands().resize(2); index_expr.op0()=object; - index_expr.op1()=gen_zero(index_type()); + index_expr.op1()=from_integer(0, index_type()); // adjust type? if(object.type().id()!="#REF#" && diff --git a/src/pointer-analysis/value_set_fivr.cpp b/src/pointer-analysis/value_set_fivr.cpp index c6c5c8920d2..3f34d861d89 100644 --- a/src/pointer-analysis/value_set_fivr.cpp +++ b/src/pointer-analysis/value_set_fivr.cpp @@ -12,7 +12,6 @@ Author: Daniel Kroening, kroening@kroening.com, #include #include -#include #include #include #include @@ -1152,7 +1151,7 @@ void value_set_fivrt::get_reference_set_sharing_rec( exprt index_expr(ID_index, expr.type()); index_expr.operands().resize(2); index_expr.op0()=object; - index_expr.op1()=gen_zero(index_type()); + index_expr.op1()=from_integer(0, index_type()); // adjust type? if(object.type().id()!="#REF#" && diff --git a/src/pointer-analysis/value_set_fivrns.cpp b/src/pointer-analysis/value_set_fivrns.cpp index 10e7c94006a..574942a73d7 100644 --- a/src/pointer-analysis/value_set_fivrns.cpp +++ b/src/pointer-analysis/value_set_fivrns.cpp @@ -12,7 +12,6 @@ Author: Daniel Kroening, kroening@kroening.com, #include #include -#include #include #include #include @@ -817,7 +816,7 @@ void value_set_fivrnst::get_reference_set_rec( exprt index_expr(ID_index, expr.type()); index_expr.operands().resize(2); index_expr.op0()=object; - index_expr.op1()=gen_zero(index_type()); + index_expr.op1()=from_integer(0, index_type()); // adjust type? if(ns.follow(object.type())!=array_type) diff --git a/src/solvers/cvc/cvc_conv.cpp b/src/solvers/cvc/cvc_conv.cpp index 6e01448d5e2..55c1815b182 100644 --- a/src/solvers/cvc/cvc_conv.cpp +++ b/src/solvers/cvc/cvc_conv.cpp @@ -14,7 +14,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include -#include #include #include #include @@ -349,7 +348,7 @@ void cvc_convt::convert_typecast_expr(const exprt &expr) { convert_expr(op); out << "/="; - convert_expr(gen_zero(op.type())); + convert_expr(from_integer(0, op.type())); } else { diff --git a/src/solvers/dplib/dplib_conv.cpp b/src/solvers/dplib/dplib_conv.cpp index 58b7702f927..ae69746fc2e 100644 --- a/src/solvers/dplib/dplib_conv.cpp +++ b/src/solvers/dplib/dplib_conv.cpp @@ -13,7 +13,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include -#include #include #include #include @@ -393,7 +392,7 @@ void dplib_convt::convert_dplib_expr(const exprt &expr) { convert_dplib_expr(op); dplib_prop.out << "/="; - convert_dplib_expr(gen_zero(op.type())); + convert_dplib_expr(from_integer(0, op.type())); } else { diff --git a/src/solvers/flattening/boolbv_member.cpp b/src/solvers/flattening/boolbv_member.cpp index a5a09a4239a..c5c0a697e1e 100644 --- a/src/solvers/flattening/boolbv_member.cpp +++ b/src/solvers/flattening/boolbv_member.cpp @@ -7,7 +7,6 @@ Author: Daniel Kroening, kroening@kroening.com \*******************************************************************/ #include -#include #include #include @@ -37,7 +36,7 @@ bvt boolbvt::convert_member(const member_exprt &expr) return convert_bv( byte_extract_exprt(byte_extract_id(), struct_op, - gen_zero(integer_typet()), + from_integer(0, integer_typet()), expr.type())); } else if(struct_op_type.id()==ID_struct) diff --git a/src/solvers/flattening/boolbv_update.cpp b/src/solvers/flattening/boolbv_update.cpp index 0d75a0f3eb8..2b485781f6b 100644 --- a/src/solvers/flattening/boolbv_update.cpp +++ b/src/solvers/flattening/boolbv_update.cpp @@ -11,7 +11,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include -#include #include #include diff --git a/src/solvers/flattening/boolbv_with.cpp b/src/solvers/flattening/boolbv_with.cpp index 50ac35813f0..2c5a2f5e556 100644 --- a/src/solvers/flattening/boolbv_with.cpp +++ b/src/solvers/flattening/boolbv_with.cpp @@ -8,7 +8,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include #include #include #include diff --git a/src/solvers/flattening/bv_pointers.cpp b/src/solvers/flattening/bv_pointers.cpp index e23dccace5e..673a81f6e5a 100644 --- a/src/solvers/flattening/bv_pointers.cpp +++ b/src/solvers/flattening/bv_pointers.cpp @@ -10,7 +10,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include -#include #include #include diff --git a/src/solvers/floatbv/float_bv.cpp b/src/solvers/floatbv/float_bv.cpp index 33f46b51c0f..99bfc7af317 100644 --- a/src/solvers/floatbv/float_bv.cpp +++ b/src/solvers/floatbv/float_bv.cpp @@ -9,7 +9,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include #include #include @@ -131,8 +130,7 @@ Function: float_bvt::abs exprt float_bvt::abs(const exprt &op, const ieee_float_spect &spec) { // we mask away the sign bit, which is the most significand bit - std::string mask_str; - mask_str.resize(spec.width(), '1'); + std::string mask_str(spec.width(), '1'); mask_str[0]='0'; constant_exprt mask(mask_str, op.type()); @@ -155,8 +153,7 @@ Function: float_bvt::negation exprt float_bvt::negation(const exprt &op, const ieee_float_spect &spec) { // we flip the sign bit with an xor - std::string mask_str; - mask_str.resize(spec.width(), '0'); + std::string mask_str(spec.width(), '0'); mask_str[0]='1'; constant_exprt mask(mask_str, op.type()); @@ -218,15 +215,15 @@ exprt float_bvt::is_zero( const floatbv_typet &type=to_floatbv_type(src.type()); std::size_t width=type.get_width(); - std::string mask_str; - mask_str.resize(width, '1'); + std::string mask_str(width, '1'); mask_str[0]='0'; constant_exprt mask(mask_str, src.type()); - return equal_exprt( - bitand_exprt(src, mask), - gen_zero(src.type())); + ieee_floatt z(type); + z.make_zero(); + + return equal_exprt(bitand_exprt(src, mask), z.to_expr()); } /*******************************************************************\ @@ -485,7 +482,7 @@ exprt float_bvt::to_integer( exprt exponent_sign=sign_exprt(unpacked.exponent); result= - if_exprt(exponent_sign, gen_zero(result.type()), result); + if_exprt(exponent_sign, from_integer(0, result.type()), result); // chop out the right number of bits from the result typet result_type= @@ -750,9 +747,12 @@ exprt float_bvt::add_sub( // 2. Subnormals mean that addition or subtraction can't round to 0, // thus we can perform this test now // 3. The rules for sign are different for zero - result.zero = and_exprt( + result.zero= + and_exprt( not_exprt(or_exprt(result.infinity, result.NaN)), - equal_exprt(result.fraction, gen_zero(result.fraction.type()))); + equal_exprt( + result.fraction, + from_integer(0, result.fraction.type()))); // sign exprt add_sub_sign= @@ -811,7 +811,8 @@ exprt float_bvt::limit_distance( exprt upper_bits= extractbits_exprt(dist, dist_width-1, nb_bits, unsignedbv_typet(dist_width-nb_bits)); - exprt upper_bits_zero=equal_exprt(upper_bits, gen_zero(upper_bits.type())); + exprt upper_bits_zero= + equal_exprt(upper_bits, from_integer(0, upper_bits.type())); exprt lower_bits= extractbits_exprt(dist, nb_bits-1, 0, @@ -864,7 +865,8 @@ exprt float_bvt::mul( // Adjust exponent; we are thowing in an extra fraction bit, // it has been extended above. - result.exponent=plus_exprt(added_exponent, gen_one(new_exponent_type)); + result.exponent= + plus_exprt(added_exponent, from_integer(1, new_exponent_type)); // new sign result.sign=notequal_exprt(unpacked1.sign, unpacked2.sign); @@ -935,7 +937,7 @@ exprt float_bvt::div( rem=mod_exprt(fraction1, fraction2); // is there a remainder? - exprt have_remainder=notequal_exprt(rem, gen_zero(rem.type())); + exprt have_remainder=notequal_exprt(rem, from_integer(0, rem.type())); // we throw this into the result, as least-significand bit, // to get the right rounding decision @@ -981,8 +983,11 @@ exprt float_bvt::div( exprt force_zero= and_exprt(not_exprt(unpacked1.NaN), unpacked2.infinity); - result.fraction=if_exprt(force_zero, - gen_zero(result.fraction.type()), result.fraction); + result.fraction= + if_exprt( + force_zero, + from_integer(0, result.fraction.type()), + result.fraction); return rounder(result, rm, spec); } @@ -1221,7 +1226,7 @@ void float_bvt::normalization_shift( if(exponent_bits=0; d--) { @@ -1232,7 +1237,7 @@ void float_bvt::normalization_shift( const exprt prefix= extractbits_exprt(fraction, fraction_bits-1, fraction_bits-distance, unsignedbv_typet(distance)); - exprt prefix_is_zero=equal_exprt(prefix, gen_zero(prefix.type())); + exprt prefix_is_zero=equal_exprt(prefix, from_integer(0, prefix.type())); // If so, shift the zeros out left by 'distance'. // Otherwise, leave as is. @@ -1296,9 +1301,10 @@ void float_bvt::denormalization_shift( from_integer(-bias+1, exponent.type()), exponent); // use sign bit - exprt denormal=and_exprt( - not_exprt(sign_exprt(distance)), - notequal_exprt(distance, gen_zero(distance.type()))); + exprt denormal= + and_exprt( + not_exprt(sign_exprt(distance)), + notequal_exprt(distance, from_integer(0, distance.type()))); #if 1 // Care must be taken to not loose information required for the @@ -1438,7 +1444,7 @@ exprt float_bvt::fraction_rounding_decision( exprt tail= extractbits_exprt(fraction, extra_bits-2, 0, unsignedbv_typet(extra_bits-2+1)); - sticky_bit=notequal_exprt(tail, gen_zero(tail.type())); + sticky_bit=notequal_exprt(tail, from_integer(0, tail.type())); } // the rounding bit is the last extra bit @@ -1578,10 +1584,12 @@ void float_bvt::round_fraction( // In case of an overflow or subnormal to normal conversion, // the exponent has to be incremented. result.exponent= - plus_exprt(result.exponent, - if_exprt(or_exprt(overflow, subnormal_to_normal), - gen_one(result.exponent.type()), - gen_zero(result.exponent.type()))); + plus_exprt( + result.exponent, + if_exprt( + or_exprt(overflow, subnormal_to_normal), + from_integer(1, result.exponent.type()), + from_integer(0, result.exponent.type()))); // post normalization of the fraction // In the case of overflow, set the MSB to 1 @@ -1590,7 +1598,7 @@ void float_bvt::round_fraction( result.fraction, if_exprt(overflow, from_integer(1<<(fraction_size-1), result.fraction.type()), - gen_zero(result.fraction.type()))); + from_integer(0, result.fraction.type()))); #endif } } @@ -1642,7 +1650,9 @@ void float_bvt::round_exponent( exprt exponent_too_large= and_exprt( binary_relation_exprt(old_exponent, ID_ge, max_exponent), - notequal_exprt(result.fraction, gen_zero(result.fraction.type()))); + notequal_exprt( + result.fraction, + from_integer(0, result.fraction.type()))); #if 1 // Directed rounding modes round overflow to the maximum normal @@ -1897,9 +1907,11 @@ exprt float_bvt::sticky_right_shift( exprt dist_bit= extractbit_exprt(dist, stage); - sticky=or_exprt( - and_exprt(dist_bit, - notequal_exprt(lost_bits, gen_zero(lost_bits.type()))), + sticky= + or_exprt( + and_exprt( + dist_bit, + notequal_exprt(lost_bits, from_integer(0, lost_bits.type()))), sticky); result=if_exprt(dist_bit, tmp, result); diff --git a/src/solvers/smt1/smt1_conv.cpp b/src/solvers/smt1/smt1_conv.cpp index b769d3b052e..e9127b15e77 100644 --- a/src/solvers/smt1/smt1_conv.cpp +++ b/src/solvers/smt1/smt1_conv.cpp @@ -9,7 +9,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include #include #include #include @@ -392,7 +391,7 @@ void smt1_convt::convert_address_of_rec( { // this is really pointer arithmetic exprt new_index_expr=expr; - new_index_expr.op1()=gen_zero(index.type()); + new_index_expr.op1()=from_integer(0, index.type()); exprt address_of_expr(ID_address_of, pointer_typet()); address_of_expr.type().subtype()=array.type().subtype(); diff --git a/src/solvers/smt2/smt2_conv.cpp b/src/solvers/smt2/smt2_conv.cpp index 870e3c5052f..b98cf9a9da5 100644 --- a/src/solvers/smt2/smt2_conv.cpp +++ b/src/solvers/smt2/smt2_conv.cpp @@ -648,7 +648,7 @@ void smt2_convt::convert_address_of_rec( { // this is really pointer arithmetic exprt new_index_expr=expr; - new_index_expr.op1()=gen_zero(index.type()); + new_index_expr.op1()=from_integer(0, index.type()); exprt address_of_expr(ID_address_of, pointer_typet()); address_of_expr.type().subtype()=array.type().subtype(); diff --git a/src/util/arith_tools.cpp b/src/util/arith_tools.cpp index 3334be4dcb4..7a99d385570 100644 --- a/src/util/arith_tools.cpp +++ b/src/util/arith_tools.cpp @@ -8,10 +8,13 @@ Author: Daniel Kroening, kroening@kroening.com #include -#include "arith_tools.h" +#include "fixedbv.h" +#include "ieee_float.h" #include "std_types.h" #include "std_expr.h" +#include "arith_tools.h" + /*******************************************************************\ Function: to_integer @@ -198,6 +201,20 @@ constant_exprt from_integer( result.set_value(integer2binary(int_value, width)); return result; } + else if(type_id==ID_fixedbv) + { + fixedbvt fixedbv; + fixedbv.spec=to_fixedbv_type(type); + fixedbv.from_integer(int_value); + return fixedbv.to_expr(); + } + else if(type_id==ID_floatbv) + { + ieee_floatt ieee_float; + ieee_float.spec=to_floatbv_type(type); + ieee_float.from_integer(int_value); + return ieee_float.to_expr(); + } { constant_exprt r; diff --git a/src/util/expr_util.cpp b/src/util/expr_util.cpp index b7034bda43c..577f59610d7 100644 --- a/src/util/expr_util.cpp +++ b/src/util/expr_util.cpp @@ -316,7 +316,10 @@ exprt is_not_zero( // Note that this returns a proper bool_typet(), not a C/C++ boolean. // To get a C/C++ boolean, add a further typecast. - const typet &src_type=ns.follow(src.type()); + const typet &src_type= + src.type().id()==ID_c_enum_tag? + ns.follow_tag(to_c_enum_tag_type(src.type())): + ns.follow(src.type()); if(src_type.id()==ID_bool) // already there return src; // do nothing @@ -324,7 +327,7 @@ exprt is_not_zero( irep_idt id= src_type.id()==ID_floatbv?ID_ieee_float_notequal:ID_notequal; - exprt zero=gen_zero(src_type); + exprt zero=from_integer(0, src_type); assert(zero.is_not_nil()); binary_exprt comparison(src, id, zero, bool_typet()); diff --git a/src/util/pointer_offset_size.cpp b/src/util/pointer_offset_size.cpp index a8dab9ab98e..370cc534ac7 100644 --- a/src/util/pointer_offset_size.cpp +++ b/src/util/pointer_offset_size.cpp @@ -268,7 +268,7 @@ exprt member_offset_expr( return member_offset_expr( to_struct_type(type), member_expr.get_component_name(), ns); else if(type.id()==ID_union) - return gen_zero(signedbv_typet(config.ansi_c.pointer_width)); + return from_integer(0, signedbv_typet(config.ansi_c.pointer_width)); else return nil_exprt(); } @@ -292,7 +292,7 @@ exprt member_offset_expr( { const struct_typet::componentst &components=type.components(); - exprt result=gen_zero(signedbv_typet(config.ansi_c.pointer_width)); + exprt result=from_integer(0, signedbv_typet(config.ansi_c.pointer_width)); std::size_t bit_field_bits=0; for(struct_typet::componentst::const_iterator @@ -395,7 +395,7 @@ exprt size_of_expr( const struct_typet::componentst &components= struct_type.components(); - exprt result=gen_zero(signedbv_typet(config.ansi_c.pointer_width)); + exprt result=from_integer(0, signedbv_typet(config.ansi_c.pointer_width)); std::size_t bit_field_bits=0; for(struct_typet::componentst::const_iterator @@ -482,7 +482,7 @@ exprt size_of_expr( } else if(type.id()==ID_bool) { - return gen_one(signedbv_typet(config.ansi_c.pointer_width)); + return from_integer(1, signedbv_typet(config.ansi_c.pointer_width)); } else if(type.id()==ID_pointer) { @@ -497,7 +497,7 @@ exprt size_of_expr( } else if(type.id()==ID_code) { - return gen_zero(signedbv_typet(config.ansi_c.pointer_width)); + return from_integer(0, signedbv_typet(config.ansi_c.pointer_width)); } else if(type.id()==ID_string) { diff --git a/src/util/pointer_predicates.cpp b/src/util/pointer_predicates.cpp index 732781878a2..1e1e285e01c 100644 --- a/src/util/pointer_predicates.cpp +++ b/src/util/pointer_predicates.cpp @@ -450,7 +450,7 @@ exprt object_lower_bound(const exprt &pointer) { exprt offset=pointer_offset(pointer); - exprt zero=gen_zero(offset.type()); + exprt zero=from_integer(0, offset.type()); assert(zero.is_not_nil()); return binary_relation_exprt(offset, ID_lt, zero); diff --git a/src/util/simplify_expr.cpp b/src/util/simplify_expr.cpp index 483c214855d..0bf81ed283d 100644 --- a/src/util/simplify_expr.cpp +++ b/src/util/simplify_expr.cpp @@ -236,7 +236,7 @@ bool simplify_exprt::simplify_typecast(exprt &expr) (expr_type.id()==ID_unsignedbv || expr_type.id()==ID_signedbv) && config.ansi_c.NULL_is_zero) { - exprt tmp=gen_zero(expr_type); + exprt tmp=from_integer(0, expr_type); expr.swap(tmp); return false; } @@ -516,13 +516,13 @@ bool simplify_exprt::simplify_typecast(exprt &expr) { if(operand.is_true()) { - expr=gen_one(expr_type); + expr=from_integer(1, expr_type); assert(expr.is_not_nil()); return false; } else if(operand.is_false()) { - expr=gen_zero(expr_type); + expr=from_integer(0, expr_type); assert(expr.is_not_nil()); return false; } @@ -1916,7 +1916,7 @@ bool simplify_exprt::simplify_byte_extract(byte_extract_exprt &expr) el_size<=pointer_offset_bits(expr.op().op2().type(), ns)) { expr.op()=expr.op().op2(); - expr.offset()=gen_zero(expr.offset().type()); + expr.offset()=from_integer(0, expr.offset().type()); simplify_byte_extract(expr); diff --git a/src/util/simplify_expr_int.cpp b/src/util/simplify_expr_int.cpp index acc1c0453a7..ffb51d7a328 100644 --- a/src/util/simplify_expr_int.cpp +++ b/src/util/simplify_expr_int.cpp @@ -110,7 +110,7 @@ bool simplify_exprt::simplify_mult(exprt &expr) if(it->is_zero() && it->type().id()!=ID_floatbv) { - expr=gen_zero(expr.type()); + expr=from_integer(0, expr.type()); return false; } @@ -353,7 +353,7 @@ bool simplify_exprt::simplify_mod(exprt &expr) if((ok1 && int_value1==1) || (ok0 && int_value0==0)) { - expr=gen_zero(expr.type()); + expr=from_integer(0, expr.type()); return false; } @@ -469,7 +469,8 @@ bool simplify_exprt::simplify_plus(exprt &expr) { if(!const_sum->sum(*it)) { - *it=gen_zero(it->type()); + *it=from_integer(0, it->type()); + assert(it->is_not_nil()); result=false; } } @@ -498,8 +499,9 @@ bool simplify_exprt::simplify_plus(exprt &expr) if(itm!=expr_map.end()) { - *(itm->second)=gen_zero(expr.type()); - *it=gen_zero(expr.type()); + *(itm->second)=from_integer(0, expr.type()); + *it=from_integer(0, expr.type()); + assert(it->is_not_nil()); expr_map.erase(itm); result=false; } @@ -525,7 +527,8 @@ bool simplify_exprt::simplify_plus(exprt &expr) if(operands.empty()) { - expr=gen_zero(expr.type()); + expr=from_integer(0, expr.type()); + assert(expr.is_not_nil()); return false; } else if(operands.size()==1) @@ -599,12 +602,10 @@ bool simplify_exprt::simplify_minus(exprt &expr) if(operands[0]==operands[1]) { - exprt zero=gen_zero(expr.type()); - if(zero.is_not_nil()) - { - expr=zero; - return false; - } + exprt zero=from_integer(0, expr.type()); + assert(zero.is_not_nil()); + expr=zero; + return false; } } @@ -985,7 +986,7 @@ bool simplify_exprt::simplify_shifts(exprt &expr) // this is to guard against large values of distance if(distance>=width) { - expr=gen_zero(expr.type()); + expr=from_integer(0, expr.type()); return false; } else if(distance>=0) @@ -1010,7 +1011,7 @@ bool simplify_exprt::simplify_shifts(exprt &expr) // this is to guard against large values of distance if(distance>=width) { - expr=gen_zero(expr.type()); + expr=from_integer(0, expr.type()); return false; } else if(distance>=0) @@ -1589,8 +1590,8 @@ bool simplify_exprt::eliminate_common_addends( op0.type().id()!=ID_complex) { // elimination! - op0=gen_zero(op0.type()); - op1=gen_zero(op1.type()); + op0=from_integer(0, op0.type()); + op1=from_integer(0, op1.type()); return false; } } @@ -1823,7 +1824,7 @@ bool simplify_exprt::simplify_inequality_constant(exprt &expr) exprt op=expr.op0().op0(); expr.op0().swap(op); if(expr.op0().type().id()!=ID_pointer) - expr.op1()=gen_zero(expr.op0().type()); + expr.op1()=from_integer(0, expr.op0().type()); else expr.op1().type()=expr.op0().type(); simplify_inequality(expr); // do again! @@ -1854,7 +1855,8 @@ bool simplify_exprt::simplify_inequality_constant(exprt &expr) if(!to_integer(*it, i)) { constant+=i; - *it=gen_zero(it->type()); + *it=from_integer(0, it->type()); + assert(it->is_not_nil()); changed=true; } } diff --git a/src/util/simplify_expr_pointer.cpp b/src/util/simplify_expr_pointer.cpp index ae5a0f60fd7..5e0d7a502fb 100644 --- a/src/util/simplify_expr_pointer.cpp +++ b/src/util/simplify_expr_pointer.cpp @@ -217,7 +217,7 @@ bool simplify_exprt::simplify_address_of(exprt &expr) // we normalize &a[i] to (&a[0])+i exprt offset; offset.swap(index_expr.op1()); - index_expr.op1()=gen_zero(offset.type()); + index_expr.op1()=from_integer(0, offset.type()); exprt addition(ID_plus, expr.type()); addition.move_to_operands(expr, offset); @@ -412,7 +412,7 @@ bool simplify_exprt::simplify_pointer_offset(exprt &expr) else if(ptr.id()==ID_constant && ptr.get(ID_value)==ID_NULL) { - expr=gen_zero(expr.type()); + expr=from_integer(0, expr.type()); simplify_node(expr); From a22a54a3a80faf09566410c43f0253c91c6edb0d Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Mon, 16 Jan 2017 08:04:35 -0500 Subject: [PATCH 2/7] Use null_pointer_exprt instead of gen_zero --- src/analyses/goto_check.cpp | 17 ++++++++++++----- src/cpp/cpp_typecheck_virtual_table.cpp | 3 +-- .../java_bytecode_convert_method.cpp | 6 +++--- src/java_bytecode/java_types.cpp | 2 +- src/java_bytecode/java_types.h | 2 +- src/util/arith_tools.cpp | 6 +----- src/util/simplify_expr.cpp | 3 +-- 7 files changed, 20 insertions(+), 19 deletions(-) diff --git a/src/analyses/goto_check.cpp b/src/analyses/goto_check.cpp index e5c1ec0290a..aa22aa72563 100644 --- a/src/analyses/goto_check.cpp +++ b/src/analyses/goto_check.cpp @@ -972,7 +972,8 @@ void goto_checkt::pointer_validity_check( return; const exprt &pointer=expr.op0(); - const typet &pointer_type=to_pointer_type(ns.follow(pointer.type())); + const pointer_typet &pointer_type= + to_pointer_type(ns.follow(pointer.type())); assert(base_type_eq(pointer_type.subtype(), expr.type(), ns)); @@ -986,7 +987,7 @@ void goto_checkt::pointer_validity_check( { if(flags.is_unknown() || flags.is_null()) { - notequal_exprt not_eq_null(pointer, gen_zero(pointer.type())); + notequal_exprt not_eq_null(pointer, null_pointer_exprt(pointer_type)); add_guarded_claim( not_eq_null, @@ -1612,7 +1613,9 @@ void goto_checkt::goto_check(goto_functiont &goto_function) if(flags.is_unknown() || flags.is_null()) { - notequal_exprt not_eq_null(pointer, gen_zero(pointer.type())); + notequal_exprt not_eq_null( + pointer, + null_pointer_exprt(to_pointer_type(pointer.type()))); add_guarded_claim( not_eq_null, @@ -1651,7 +1654,9 @@ void goto_checkt::goto_check(goto_functiont &goto_function) if(pointer.type().subtype().get(ID_identifier)!="java::java.lang.AssertionError") { - notequal_exprt not_eq_null(pointer, gen_zero(pointer.type())); + notequal_exprt not_eq_null( + pointer, + null_pointer_exprt(to_pointer_type(pointer.type()))); add_guarded_claim( not_eq_null, @@ -1718,7 +1723,9 @@ void goto_checkt::goto_check(goto_functiont &goto_function) source_locationt source_location; source_location.set_function(i.function); - equal_exprt eq(leak_expr, gen_zero(ns.follow(leak.type))); + equal_exprt eq( + leak_expr, + null_pointer_exprt(to_pointer_type(leak.type))); add_guarded_claim( eq, "dynamically allocated memory never freed", diff --git a/src/cpp/cpp_typecheck_virtual_table.cpp b/src/cpp/cpp_typecheck_virtual_table.cpp index 74efcad31c9..b2c18974613 100644 --- a/src/cpp/cpp_typecheck_virtual_table.cpp +++ b/src/cpp/cpp_typecheck_virtual_table.cpp @@ -47,8 +47,7 @@ void cpp_typecheckt::do_virtual_table(const symbolt &symbol) if(compo.get_bool("is_pure_virtual")) { pointer_typet pointer_type(code_type); - e = gen_zero(pointer_type); - assert(e.is_not_nil()); + e=null_pointer_exprt(pointer_type); value_map[compo.get("virtual_name")] = e; } else diff --git a/src/java_bytecode/java_bytecode_convert_method.cpp b/src/java_bytecode/java_bytecode_convert_method.cpp index 5935fe8e321..7d22cda295b 100644 --- a/src/java_bytecode/java_bytecode_convert_method.cpp +++ b/src/java_bytecode/java_bytecode_convert_method.cpp @@ -906,7 +906,7 @@ codet java_bytecode_convert_methodt::convert_instructions( if(statement=="aconst_null") { assert(results.size()==1); - results[0]=gen_zero(java_reference_type(void_typet())); + results[0]=null_pointer_exprt(java_reference_type(void_typet())); } else if(statement=="athrow") { @@ -1370,7 +1370,7 @@ codet java_bytecode_convert_methodt::convert_instructions( assert(op.size()==1 && results.empty()); code_ifthenelset code_branch; const typecast_exprt lhs(op[0], pointer_typet(empty_typet())); - const exprt rhs(gen_zero(lhs.type())); + const exprt rhs(null_pointer_exprt(to_pointer_type(lhs.type()))); code_branch.cond()=binary_relation_exprt(lhs, ID_notequal, rhs); code_branch.then_case()=code_gotot(label(number)); code_branch.then_case().add_source_location()=i_it->source_location; @@ -1384,7 +1384,7 @@ codet java_bytecode_convert_methodt::convert_instructions( irep_idt number=to_constant_expr(arg0).get_value(); code_ifthenelset code_branch; const typecast_exprt lhs(op[0], pointer_typet(empty_typet())); - const exprt rhs(gen_zero(lhs.type())); + const exprt rhs(null_pointer_exprt(to_pointer_type(lhs.type()))); code_branch.cond()=binary_relation_exprt(lhs, ID_equal, rhs); code_branch.then_case()=code_gotot(label(number)); code_branch.then_case().add_source_location()=i_it->source_location; diff --git a/src/java_bytecode/java_types.cpp b/src/java_bytecode/java_types.cpp index cd3d23b22bd..de89fc0e209 100644 --- a/src/java_bytecode/java_types.cpp +++ b/src/java_bytecode/java_types.cpp @@ -183,7 +183,7 @@ Function: java_reference_type \*******************************************************************/ -typet java_reference_type(const typet &subtype) +reference_typet java_reference_type(const typet &subtype) { return reference_typet(subtype); } diff --git a/src/java_bytecode/java_types.h b/src/java_bytecode/java_types.h index 41f68bdda01..e283a5acf23 100644 --- a/src/java_bytecode/java_types.h +++ b/src/java_bytecode/java_types.h @@ -20,7 +20,7 @@ typet java_char_type(); typet java_float_type(); typet java_double_type(); typet java_boolean_type(); -typet java_reference_type(const typet &subtype); +reference_typet java_reference_type(const typet &subtype); symbol_typet java_classname(const std::string &); pointer_typet java_array_type(const char subtype); diff --git a/src/util/arith_tools.cpp b/src/util/arith_tools.cpp index 7a99d385570..0957cf41ab5 100644 --- a/src/util/arith_tools.cpp +++ b/src/util/arith_tools.cpp @@ -188,11 +188,7 @@ constant_exprt from_integer( else if(type_id==ID_pointer) { if(int_value==0) - { - constant_exprt result(type); - result.set_value(ID_NULL); - return result; - } + return null_pointer_exprt(to_pointer_type(type)); } else if(type_id==ID_c_bit_field) { diff --git a/src/util/simplify_expr.cpp b/src/util/simplify_expr.cpp index 0bf81ed283d..b827edc3972 100644 --- a/src/util/simplify_expr.cpp +++ b/src/util/simplify_expr.cpp @@ -543,8 +543,7 @@ bool simplify_exprt::simplify_typecast(exprt &expr) operand.is_false() && config.ansi_c.NULL_is_zero) { - expr=gen_zero(expr_type); - assert(expr.is_not_nil()); + expr=null_pointer_exprt(to_pointer_type(expr_type)); return false; } } From 0f9541816a8c5cdb8eb2716e07f0f360b51035b5 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Mon, 16 Jan 2017 08:06:32 -0500 Subject: [PATCH 3/7] zero_initializer without message_handlert Throws a string instead of 0. --- src/cegis/control/facade/control_runner.cpp | 2 -- src/cegis/control/verify/insert_solution.cpp | 4 +-- src/cegis/control/verify/zero_solutions.cpp | 6 ++-- src/cegis/jsa/learn/jsa_symex_learn.cpp | 3 +- .../preprocessing/add_synthesis_library.cpp | 3 +- src/cegis/learn/insert_counterexample.cpp | 6 ++-- .../instructionset/create_cegis_processor.cpp | 6 ++-- .../refactor/verify/refactor_symex_verify.cpp | 3 +- src/goto-symex/symex_start_thread.cpp | 7 +--- .../java_bytecode_convert_method.cpp | 1 + src/linking/zero_initializer.cpp | 35 ++++++++++++++++++- src/linking/zero_initializer.h | 12 +++++-- 12 files changed, 57 insertions(+), 31 deletions(-) diff --git a/src/cegis/control/facade/control_runner.cpp b/src/cegis/control/facade/control_runner.cpp index 8e6a2070dc6..140f1ef3908 100644 --- a/src/cegis/control/facade/control_runner.cpp +++ b/src/cegis/control/facade/control_runner.cpp @@ -7,8 +7,6 @@ Author: Daniel Kroening, kroening@kroening.com \*******************************************************************/ -#include - #include #include #include diff --git a/src/cegis/control/verify/insert_solution.cpp b/src/cegis/control/verify/insert_solution.cpp index 9c1fbe27642..ca5decd1ac7 100644 --- a/src/cegis/control/verify/insert_solution.cpp +++ b/src/cegis/control/verify/insert_solution.cpp @@ -10,7 +10,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include #include #include @@ -56,8 +55,7 @@ struct_exprt to_struct_expr(const symbol_tablet &st, const symbol_typet &type=control_solution_type(st); const namespacet ns(st); const struct_typet &struct_type=to_struct_type(ns.follow(type)); - null_message_handlert msg; - const exprt zero(zero_initializer(type, loc, ns, msg)); + const exprt zero(zero_initializer(type, loc, ns)); struct_exprt result(to_struct_expr(zero)); struct_exprt::operandst &ops=result.operands(); set_array(ops, st, struct_type, solution.a, CEGIS_CONTROL_A_MEMBER_NAME); diff --git a/src/cegis/control/verify/zero_solutions.cpp b/src/cegis/control/verify/zero_solutions.cpp index 59468253271..22249c9b7e4 100644 --- a/src/cegis/control/verify/zero_solutions.cpp +++ b/src/cegis/control/verify/zero_solutions.cpp @@ -32,8 +32,7 @@ namespace struct_exprt make_zero(const namespacet &ns, const symbol_typet &type) { const source_locationt loc(default_cegis_source_location()); - null_message_handlert msg; - return to_struct_expr(zero_initializer(type, loc, ns, msg)); + return to_struct_expr(zero_initializer(type, loc, ns)); } } @@ -59,6 +58,5 @@ void zero_vector_solutiont::operator ()( const namespacet ns(st); const array_typet &type=control_vector_solution_type(st); const source_locationt loc(default_cegis_source_location()); - null_message_handlert msg; - solution.K=to_array_expr(zero_initializer(type, loc, ns, msg)); + solution.K=to_array_expr(zero_initializer(type, loc, ns)); } diff --git a/src/cegis/jsa/learn/jsa_symex_learn.cpp b/src/cegis/jsa/learn/jsa_symex_learn.cpp index d44640e5006..eb1fffecb3b 100644 --- a/src/cegis/jsa/learn/jsa_symex_learn.cpp +++ b/src/cegis/jsa/learn/jsa_symex_learn.cpp @@ -45,7 +45,6 @@ void jsa_symex_learnt::process(const counterexamplest &counterexamples, void jsa_symex_learnt::process(const size_t max_solution_size) { - null_message_handlert msg; const namespacet ns(original_program.st); counterexamplest counterexamples(1); counterexamplet &counterexample=counterexamples.front(); @@ -55,7 +54,7 @@ void jsa_symex_learnt::process(const size_t max_solution_size) const irep_idt &key=pos->labels.front(); const typet &type=get_affected_type(*pos); const source_locationt &loc=pos->source_location; - const exprt value(zero_initializer(type, loc, ns, msg)); + const exprt value(zero_initializer(type, loc, ns)); counterexample.insert(std::make_pair(key, value)); } process(counterexamples, max_solution_size); diff --git a/src/cegis/jsa/preprocessing/add_synthesis_library.cpp b/src/cegis/jsa/preprocessing/add_synthesis_library.cpp index f2e394c51ed..20d8edb420a 100644 --- a/src/cegis/jsa/preprocessing/add_synthesis_library.cpp +++ b/src/cegis/jsa/preprocessing/add_synthesis_library.cpp @@ -93,7 +93,6 @@ void zero_new_global_vars(const symbol_tablet &st, goto_functionst &gf) assert(init.body_available()); goto_programt &body=init.body; goto_programt::targett pos=std::prev(body.instructions.end(), 2); - null_message_handlert msg; const source_locationt loc(jsa_builtin_source_location()); const namespacet ns(st); for (const symbol_tablet::symbolst::value_type &symbol : st.symbols) @@ -103,7 +102,7 @@ void zero_new_global_vars(const symbol_tablet &st, goto_functionst &gf) pos->type=goto_program_instruction_typet::ASSIGN; pos->source_location=loc; const symbol_exprt lhs(ns.lookup(symbol.first).symbol_expr()); - const exprt rhs(zero_initializer(lhs.type(), loc, ns, msg)); + const exprt rhs(zero_initializer(lhs.type(), loc, ns)); pos->code=code_assignt(lhs, rhs); } } diff --git a/src/cegis/learn/insert_counterexample.cpp b/src/cegis/learn/insert_counterexample.cpp index 7c321db9128..9a54bd750ed 100644 --- a/src/cegis/learn/insert_counterexample.cpp +++ b/src/cegis/learn/insert_counterexample.cpp @@ -31,12 +31,11 @@ zero_valuest get_zero_values(const symbol_tablet &st, std::map zero_values; const source_locationt loc(default_cegis_source_location()); const namespacet ns(st); - null_message_handlert msg; for (const goto_programt::const_targett pos : ce_locs) { const irep_idt &marker=get_counterexample_marker(pos); const typet &type=get_affected_type(*pos); - const exprt value(zero_initializer(type, loc, ns, msg)); + const exprt value(zero_initializer(type, loc, ns)); zero_values.insert(std::make_pair(marker, value)); } return zero_values; @@ -172,8 +171,7 @@ void add_array_indexes(const std::set &ce_keys, symbol_tablet &st, pos=declare_cegis_meta_variable(st, gf, std::prev(pos), CE_ARRAY_INDEX, type); const source_locationt loc(default_cegis_source_location()); const namespacet ns(st); - null_message_handlert msg; - const exprt zero(zero_initializer(type, loc, ns, msg)); + const exprt zero(zero_initializer(type, loc, ns)); assign_cegis_meta_variable(st, gf, pos, CE_ARRAY_INDEX, zero); pos=cprover_init; for (const irep_idt &key : ce_keys) diff --git a/src/cegis/refactor/instructionset/create_cegis_processor.cpp b/src/cegis/refactor/instructionset/create_cegis_processor.cpp index 0a5871aef54..0d2d3cb54c1 100644 --- a/src/cegis/refactor/instructionset/create_cegis_processor.cpp +++ b/src/cegis/refactor/instructionset/create_cegis_processor.cpp @@ -7,8 +7,9 @@ Author: Daniel Kroening, kroening@kroening.com \*******************************************************************/ -#include #include + +#include #include #include @@ -83,8 +84,7 @@ void create_variable_array(symbol_tablet &st, goto_functionst &gf, pos->source_location=new_symbol.location; const symbol_exprt lhs(st.lookup(name).symbol_expr()); const namespacet ns(st); - null_message_handlert msg; - const exprt rhs(zero_initializer(array_type, new_symbol.location, ns, msg)); + const exprt rhs(zero_initializer(array_type, new_symbol.location, ns)); pos->code=code_assignt(lhs, rhs); body.update(); } diff --git a/src/cegis/refactor/verify/refactor_symex_verify.cpp b/src/cegis/refactor/verify/refactor_symex_verify.cpp index a65fba9f684..4586b00acaf 100644 --- a/src/cegis/refactor/verify/refactor_symex_verify.cpp +++ b/src/cegis/refactor/verify/refactor_symex_verify.cpp @@ -28,14 +28,13 @@ void refactor_symex_verifyt::process(const candidatet &candidate) symbol_tablet &st=current_program.st; goto_functionst &gf=current_program.gf; const namespacet ns(st); - null_message_handlert msg; for (const irep_idt &program : current_program.programs) { symbolt &symbol=st.lookup(program); const candidatet::const_iterator it=candidate.find(program); if (candidate.end() == it) { - const exprt zero(zero_initializer(symbol.type, symbol.location, ns, msg)); + const exprt zero(zero_initializer(symbol.type, symbol.location, ns)); assign_in_cprover_init(gf, symbol, zero); } else assign_in_cprover_init(gf, symbol, it->second); } diff --git a/src/goto-symex/symex_start_thread.cpp b/src/goto-symex/symex_start_thread.cpp index 72b1acdb840..959034733d7 100644 --- a/src/goto-symex/symex_start_thread.cpp +++ b/src/goto-symex/symex_start_thread.cpp @@ -6,8 +6,6 @@ Author: Daniel Kroening, kroening@kroening.com \*******************************************************************/ -#include - #include #include "goto_symex.h" @@ -116,10 +114,7 @@ void goto_symext::symex_start_thread(statet &state) exprt rhs=symbol.value; if(rhs.is_nil()) - { - null_message_handlert null_message; - rhs=zero_initializer(symbol.type, symbol.location, ns, null_message); - } + rhs=zero_initializer(symbol.type, symbol.location, ns); guardt guard; symex_assign_symbol(state, lhs, nil_exprt(), rhs, guard, symex_targett::HIDDEN); diff --git a/src/java_bytecode/java_bytecode_convert_method.cpp b/src/java_bytecode/java_bytecode_convert_method.cpp index 7d22cda295b..d455f07e432 100644 --- a/src/java_bytecode/java_bytecode_convert_method.cpp +++ b/src/java_bytecode/java_bytecode_convert_method.cpp @@ -10,6 +10,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #endif +#include #include #include #include diff --git a/src/linking/zero_initializer.cpp b/src/linking/zero_initializer.cpp index d652427059d..616920ca0bc 100644 --- a/src/linking/zero_initializer.cpp +++ b/src/linking/zero_initializer.cpp @@ -6,9 +6,11 @@ Author: Daniel Kroening, kroening@kroening.com \*******************************************************************/ +#include + +#include #include #include -#include #include #include #include @@ -298,3 +300,34 @@ exprt zero_initializer( zero_initializert z_i(ns, message_handler); return z_i(type, source_location); } + +/*******************************************************************\ + +Function: zero_initializer + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +exprt zero_initializer( + const typet &type, + const source_locationt &source_location, + const namespacet &ns) +{ + std::ostringstream oss; + stream_message_handlert mh(oss); + + try + { + zero_initializert z_i(ns, mh); + return z_i(type, source_location); + } + catch(int) + { + throw oss.str(); + } +} diff --git a/src/linking/zero_initializer.h b/src/linking/zero_initializer.h index 0768a15056d..766fdf26784 100644 --- a/src/linking/zero_initializer.h +++ b/src/linking/zero_initializer.h @@ -10,8 +10,10 @@ Author: Daniel Kroening, kroening@kroening.com #define CPROVER_LINKING_ZERO_INITIALIZER_H #include -#include -#include + +class message_handlert; +class namespacet; +class source_locationt; exprt zero_initializer( const typet &, @@ -19,4 +21,10 @@ exprt zero_initializer( const namespacet &, message_handlert &); +// throws a char* in case of failure +exprt zero_initializer( + const typet &, + const source_locationt &, + const namespacet &); + #endif // CPROVER_LINKING_ZERO_INITIALIZER_H From f5ef5318bcad7201d30ddbefe5563f826676b8c0 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Mon, 16 Jan 2017 08:05:54 -0500 Subject: [PATCH 4/7] Use zero_initializer instead of gen_zero gen_zero/gen_one can now safely be removed. --- src/cegis/instrument/cegis_library.cpp | 10 +- src/cpp/cpp_typecheck_expr.cpp | 17 +- src/goto-programs/builtin_functions.cpp | 15 +- src/goto-symex/symex_builtin_functions.cpp | 4 +- .../java_bytecode_convert_class.cpp | 12 +- src/linking/zero_initializer.cpp | 66 +++++-- src/memory-models/Makefile | 2 + src/path-symex/path_symex.cpp | 9 +- src/solvers/smt1/smt1_conv.cpp | 10 +- src/solvers/smt2/smt2_conv.cpp | 8 +- src/util/expr_util.cpp | 180 ------------------ src/util/expr_util.h | 7 +- src/util/simplify_expr.cpp | 8 +- 13 files changed, 123 insertions(+), 225 deletions(-) diff --git a/src/cegis/instrument/cegis_library.cpp b/src/cegis/instrument/cegis_library.cpp index 251849164a3..920f620f74a 100644 --- a/src/cegis/instrument/cegis_library.cpp +++ b/src/cegis/instrument/cegis_library.cpp @@ -7,13 +7,13 @@ Author: Daniel Kroening, kroening@kroening.com \*******************************************************************/ -#include - #include #include #include +#include + #include #include #include @@ -78,7 +78,11 @@ goto_programt::targett init_array(const symbol_tablet &st, goto_programt &body, pos->source_location=default_cegis_source_location(); const symbol_exprt array(st.lookup(name).symbol_expr()); const array_typet &type=to_array_type(array.type()); - pos->code=code_assignt(array, array_of_exprt(gen_zero(type.subtype()), type)); + const namespacet ns(st); + pos->code= + code_assignt( + array, + zero_initializer(type, pos->source_location, ns)); return pos; } diff --git a/src/cpp/cpp_typecheck_expr.cpp b/src/cpp/cpp_typecheck_expr.cpp index a8e8fed5651..935d174a23e 100644 --- a/src/cpp/cpp_typecheck_expr.cpp +++ b/src/cpp/cpp_typecheck_expr.cpp @@ -19,6 +19,8 @@ Author: Daniel Kroening, kroening@cs.cmu.edu #include #include +#include + #include "cpp_type2name.h" #include "cpp_typecheck.h" #include "cpp_convert_type.h" @@ -1035,15 +1037,12 @@ void cpp_typecheckt::typecheck_expr_explicit_typecast(exprt &expr) { // Default value, e.g., int() typecheck_type(expr.type()); - exprt new_expr=gen_zero(expr.type()); - - if(new_expr.is_nil()) - { - error().source_location=expr.find_source_location(); - error() << "no default value for `" << to_string(expr.type()) - << "'" << eom; - throw 0; - } + exprt new_expr= + ::zero_initializer( + expr.type(), + expr.find_source_location(), + *this, + get_message_handler()); new_expr.add_source_location()=expr.source_location(); expr=new_expr; diff --git a/src/goto-programs/builtin_functions.cpp b/src/goto-programs/builtin_functions.cpp index d6a67946730..2ee615aa4b4 100644 --- a/src/goto-programs/builtin_functions.cpp +++ b/src/goto-programs/builtin_functions.cpp @@ -814,7 +814,12 @@ void goto_convertt::do_java_new_array( t_p->source_location=location; // zero-initialize the data - exprt zero_element=gen_zero(data.type().subtype()); + exprt zero_element= + zero_initializer( + data.type().subtype(), + location, + ns, + get_message_handler()); codet array_set(ID_array_set); array_set.copy_to_operands(data, zero_element); goto_programt::targett t_d=dest.add_instruction(OTHER); @@ -1646,7 +1651,13 @@ void goto_convertt::do_function_call_symbol( { goto_programt::targett t=dest.add_instruction(ASSIGN); t->source_location=function.source_location(); - t->code=code_assignt(dest_expr, gen_zero(dest_expr.type())); + exprt zero= + zero_initializer( + dest_expr.type(), + function.source_location(), + ns, + get_message_handler()); + t->code=code_assignt(dest_expr, zero); } } else if(identifier=="__sync_fetch_and_add" || diff --git a/src/goto-symex/symex_builtin_functions.cpp b/src/goto-symex/symex_builtin_functions.cpp index 1eaf30353d3..92b269f9405 100644 --- a/src/goto-symex/symex_builtin_functions.cpp +++ b/src/goto-symex/symex_builtin_functions.cpp @@ -21,6 +21,8 @@ Author: Daniel Kroening, kroening@kroening.com #include +#include + #include "goto_symex.h" #include "goto_symex_state.h" @@ -235,7 +237,7 @@ void goto_symext::symex_gcc_builtin_va_arg_next( do_simplify(tmp); irep_idt id=get_symbol(tmp); - exprt rhs=gen_zero(lhs.type()); + exprt rhs=zero_initializer(lhs.type(), code.source_location(), ns); if(id!=irep_idt()) { diff --git a/src/java_bytecode/java_bytecode_convert_class.cpp b/src/java_bytecode/java_bytecode_convert_class.cpp index 113a8b9422d..6f292ee5985 100644 --- a/src/java_bytecode/java_bytecode_convert_class.cpp +++ b/src/java_bytecode/java_bytecode_convert_class.cpp @@ -15,8 +15,10 @@ Author: Daniel Kroening, kroening@kroening.com #include "java_types.h" #include "java_bytecode_convert_method.h" +#include #include -#include + +#include class java_bytecode_convert_classt:public messaget { @@ -215,7 +217,13 @@ void java_bytecode_convert_classt::convert( "."+id2string(f.name); new_symbol.mode=ID_java; new_symbol.is_type=false; - new_symbol.value=gen_zero(field_type); + const namespacet ns(symbol_table); + new_symbol.value= + zero_initializer( + field_type, + class_symbol.location, + ns, + get_message_handler()); // Do we have the static field symbol already? const auto s_it=symbol_table.symbols.find(new_symbol.name); diff --git a/src/linking/zero_initializer.cpp b/src/linking/zero_initializer.cpp index 616920ca0bc..071cb34aa27 100644 --- a/src/linking/zero_initializer.cpp +++ b/src/linking/zero_initializer.cpp @@ -74,25 +74,42 @@ exprt zero_initializert::zero_initializer_rec( { const irep_idt &type_id=type.id(); - if(type_id==ID_bool) + if(type_id==ID_unsignedbv || + type_id==ID_signedbv || + type_id==ID_pointer || + type_id==ID_c_enum || + type_id==ID_incomplete_c_enum || + type_id==ID_c_bit_field || + type_id==ID_bool || + type_id==ID_c_bool || + type_id==ID_floatbv || + type_id==ID_fixedbv) { - exprt result=false_exprt(); + exprt result=from_integer(0, type); result.add_source_location()=source_location; return result; } - else if(type_id==ID_unsignedbv || - type_id==ID_signedbv || - type_id==ID_floatbv || - type_id==ID_fixedbv || - type_id==ID_pointer || - type_id==ID_complex || - type_id==ID_c_enum || - type_id==ID_incomplete_c_enum || - type_id==ID_c_enum_tag || - type_id==ID_c_bit_field || - type_id==ID_c_bool) + else if(type_id==ID_rational || + type_id==ID_real) { - exprt result=gen_zero(type); + constant_exprt result(ID_0, type); + result.add_source_location()=source_location; + return result; + } + else if(type_id==ID_verilog_signedbv || + type_id==ID_verilog_unsignedbv) + { + std::size_t width=to_bitvector_type(type).get_width(); + std::string value(width, '0'); + + constant_exprt result(value, type); + result.add_source_location()=source_location; + return result; + } + else if(type_id==ID_complex) + { + exprt sub_zero=zero_initializer_rec(type.subtype(), source_location); + complex_exprt result(sub_zero, sub_zero, to_complex_type(type)); result.add_source_location()=source_location; return result; } @@ -266,6 +283,27 @@ exprt zero_initializert::zero_initializer_rec( return result; } + else if(type_id==ID_c_enum_tag) + { + return + zero_initializer_rec( + ns.follow_tag(to_c_enum_tag_type(type)), + source_location); + } + else if(type_id==ID_struct_tag) + { + return + zero_initializer_rec( + ns.follow_tag(to_struct_tag_type(type)), + source_location); + } + else if(type_id==ID_union_tag) + { + return + zero_initializer_rec( + ns.follow_tag(to_union_tag_type(type)), + source_location); + } else if(type_id==ID_string) { return constant_exprt(irep_idt(), type); diff --git a/src/memory-models/Makefile b/src/memory-models/Makefile index c4c7b403b13..a1127d05821 100644 --- a/src/memory-models/Makefile +++ b/src/memory-models/Makefile @@ -2,6 +2,8 @@ SRC = mm_y.tab.cpp mm_lex.yy.cpp mmcc_main.cpp mm_parser.cpp \ mmcc_parse_options.cpp mm2cpp.cpp OBJ += ../big-int/big-int$(LIBEXT) \ + ../ansi-c/ansi-c$(LIBEXT) \ + ../linking/linking$(LIBEXT) \ ../util/util$(LIBEXT) INCLUDES= -I .. diff --git a/src/path-symex/path_symex.cpp b/src/path-symex/path_symex.cpp index f3cffd498bb..8455bec3392 100644 --- a/src/path-symex/path_symex.cpp +++ b/src/path-symex/path_symex.cpp @@ -11,11 +11,12 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include -#include #include #include #include +#include + #include #include "path_symex_class.h" @@ -352,7 +353,11 @@ void path_symext::symex_va_arg_next( // Get old symbol of va_arg and modify it to generate a new one. irep_idt id=get_old_va_symbol(state, tmp); - exprt rhs=gen_zero(lhs.type()); + exprt rhs= + zero_initializer( + lhs.type(), + code.source_location(), + state.var_map.ns); if(!id.empty()) { diff --git a/src/solvers/smt1/smt1_conv.cpp b/src/solvers/smt1/smt1_conv.cpp index e9127b15e77..0a403f6dd76 100644 --- a/src/solvers/smt1/smt1_conv.cpp +++ b/src/solvers/smt1/smt1_conv.cpp @@ -21,6 +21,8 @@ Author: Daniel Kroening, kroening@kroening.com #include +#include + #include #include #include @@ -1540,7 +1542,9 @@ void smt1_convt::convert_typecast( out << "(not (= "; convert_expr(src, true); out << " "; - convert_expr(gen_zero(src_type), true); + convert_expr( + zero_initializer(src_type, expr.source_location(), ns), + true); out << "))"; } else @@ -1566,7 +1570,9 @@ void smt1_convt::convert_typecast( out << "(not (= "; convert_expr(src, true); out << " "; - convert_expr(gen_zero(src_type), true); + convert_expr( + zero_initializer(src_type, expr.source_location(), ns), + true); out << ")) "; // not, = out << " bv1[" << to_width << "]"; out << " bv0[" << to_width << "]"; diff --git a/src/solvers/smt2/smt2_conv.cpp b/src/solvers/smt2/smt2_conv.cpp index b98cf9a9da5..32df575ff84 100644 --- a/src/solvers/smt2/smt2_conv.cpp +++ b/src/solvers/smt2/smt2_conv.cpp @@ -22,6 +22,8 @@ Author: Daniel Kroening, kroening@kroening.com #include +#include + #include #include #include @@ -2062,7 +2064,8 @@ void smt2_convt::convert_typecast(const typecast_exprt &expr) out << "(not (= "; convert_expr(src); out << " "; - convert_expr(gen_zero(src_type)); + convert_expr( + zero_initializer(src_type, expr.source_location(), ns)); out << "))"; } else if(src_type.id()==ID_floatbv) @@ -2088,7 +2091,8 @@ void smt2_convt::convert_typecast(const typecast_exprt &expr) out << "(not (= "; convert_expr(src); out << " "; - convert_expr(gen_zero(src_type)); + convert_expr( + zero_initializer(src_type, expr.source_location(), ns)); out << ")) "; // not, = out << " (_ bv1 " << to_width << ")"; out << " (_ bv0 " << to_width << ")"; diff --git a/src/util/expr_util.cpp b/src/util/expr_util.cpp index 577f59610d7..09f3ef2a7c6 100644 --- a/src/util/expr_util.cpp +++ b/src/util/expr_util.cpp @@ -17,186 +17,6 @@ Author: Daniel Kroening, kroening@kroening.com /*******************************************************************\ -Function: gen_zero - - Inputs: - - Outputs: - - Purpose: - -\*******************************************************************/ - -exprt gen_zero(const typet &type) -{ - const irep_idt type_id=type.id(); - - if(type_id==ID_rational || - type_id==ID_real || - type_id==ID_integer || - type_id==ID_natural) - { - return constant_exprt(ID_0, type); - } - else if(type_id==ID_c_enum) - { - exprt tmp=gen_zero(type.subtype()); - tmp.type()=type; - return tmp; - } - else if(type_id==ID_c_enum_tag) - { - // Ha! We generate a typecast. - exprt tmp=gen_zero(unsignedbv_typet(1)); - return typecast_exprt(tmp, type); - } - else if(type_id==ID_unsignedbv || - type_id==ID_signedbv || - type_id==ID_verilog_signedbv || - type_id==ID_verilog_unsignedbv || - type_id==ID_floatbv || - type_id==ID_fixedbv || - type_id==ID_c_bit_field || - type_id==ID_c_bool) - { - std::string value; - std::size_t width=to_bitvector_type(type).get_width(); - - for(std::size_t i=0; i=3 operands into nested binary expressions */ +/*! splits an expression with >=3 operands into nested binary expressions */ exprt make_binary(const exprt &); /*! converts an udpate expr into a (possibly nested) with expression */ diff --git a/src/util/simplify_expr.cpp b/src/util/simplify_expr.cpp index b827edc3972..1c8dfd226c2 100644 --- a/src/util/simplify_expr.cpp +++ b/src/util/simplify_expr.cpp @@ -32,6 +32,8 @@ Author: Daniel Kroening, kroening@kroening.com #include "endianness_map.h" #include "simplify_utils.h" +#include + //#define DEBUGX #ifdef DEBUGX @@ -273,7 +275,8 @@ bool simplify_exprt::simplify_typecast(exprt &expr) inequality.id(op_type.id()==ID_floatbv?ID_ieee_float_notequal:ID_notequal); inequality.add_source_location()=expr.source_location(); inequality.lhs()=expr.op0(); - inequality.rhs()=gen_zero(ns.follow(expr.op0().type())); + inequality.rhs()= + zero_initializer(expr.op0().type(), expr.source_location(), ns); assert(inequality.rhs().is_not_nil()); simplify_node(inequality); expr.swap(inequality); @@ -289,7 +292,8 @@ bool simplify_exprt::simplify_typecast(exprt &expr) inequality.id(op_type.id()==ID_floatbv?ID_ieee_float_notequal:ID_notequal); inequality.add_source_location()=expr.source_location(); inequality.lhs()=expr.op0(); - inequality.rhs()=gen_zero(ns.follow(expr.op0().type())); + inequality.rhs()= + zero_initializer(expr.op0().type(), expr.source_location(), ns); assert(inequality.rhs().is_not_nil()); simplify_node(inequality); expr.op0()=inequality; From 7eae44cfba493bac523e6e0951810729468d763a Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Sat, 21 Jan 2017 21:42:20 +0000 Subject: [PATCH 5/7] Added file copyright header as noted by linter --- src/cpp/cpp_typecheck_virtual_table.cpp | 18 +++++++++++++----- 1 file changed, 13 insertions(+), 5 deletions(-) diff --git a/src/cpp/cpp_typecheck_virtual_table.cpp b/src/cpp/cpp_typecheck_virtual_table.cpp index b2c18974613..1d8cca10b84 100644 --- a/src/cpp/cpp_typecheck_virtual_table.cpp +++ b/src/cpp/cpp_typecheck_virtual_table.cpp @@ -1,5 +1,18 @@ /*******************************************************************\ +Module: C++ Language Type Checking + +Author: Daniel Kroening, kroening@cs.cmu.edu + +\*******************************************************************/ + +#include +#include + +#include "cpp_typecheck.h" + +/*******************************************************************\ + Function: cpp_typecheckt::do_virtual_table Inputs: @@ -10,11 +23,6 @@ Function: cpp_typecheckt::do_virtual_table \*******************************************************************/ -#include -#include - -#include "cpp_typecheck.h" - void cpp_typecheckt::do_virtual_table(const symbolt &symbol) { assert(symbol.type.id()==ID_struct); From cf06f353d10e16263b11534957d7f308c29adc80 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 27 Jan 2017 08:10:33 +0000 Subject: [PATCH 6/7] cbmc-java: Print details of errors in regression tests This is the same as various other directories already do. --- regression/cbmc-java/Makefile | 10 ++++++++-- 1 file changed, 8 insertions(+), 2 deletions(-) diff --git a/regression/cbmc-java/Makefile b/regression/cbmc-java/Makefile index 5ac5a21995e..cee83cba67a 100644 --- a/regression/cbmc-java/Makefile +++ b/regression/cbmc-java/Makefile @@ -1,10 +1,16 @@ default: tests.log test: - @../test.pl -c ../../../src/cbmc/cbmc + @if ! ../test.pl -c ../../../src/cbmc/cbmc ; then \ + ../failed-tests-printer.pl ; \ + exit 1 ; \ + fi tests.log: ../test.pl - @../test.pl -c ../../../src/cbmc/cbmc + @if ! ../test.pl -c ../../../src/cbmc/cbmc ; then \ + ../failed-tests-printer.pl ; \ + exit 1 ; \ + fi show: @for dir in *; do \ From 31ce11f2073278c383eb569e74a043a156afa32e Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 27 Jan 2017 09:23:22 +0000 Subject: [PATCH 7/7] Make from_integer fail an assertion for unsupported types Prompts a fix in java bytecode conversion. --- .../java_bytecode_convert_method.cpp | 16 ++++++++++------ src/util/arith_tools.cpp | 1 + src/util/arith_tools.h | 2 +- 3 files changed, 12 insertions(+), 7 deletions(-) diff --git a/src/java_bytecode/java_bytecode_convert_method.cpp b/src/java_bytecode/java_bytecode_convert_method.cpp index d455f07e432..5f22c135e06 100644 --- a/src/java_bytecode/java_bytecode_convert_method.cpp +++ b/src/java_bytecode/java_bytecode_convert_method.cpp @@ -1240,9 +1240,11 @@ codet java_bytecode_convert_methodt::convert_instructions( irep_idt number=to_constant_expr(arg0).get_value(); code_gotot code_goto(label(number)); c=code_goto; - results[0]=from_integer( - std::next(i_it)->address, - pointer_typet(void_typet(), 64)); + results[0]= + from_integer( + std::next(i_it)->address, + unsignedbv_typet(64)); + results[0].type()=pointer_typet(void_typet(), 64); } else if(statement=="ret") { @@ -1263,9 +1265,11 @@ codet java_bytecode_convert_methodt::convert_instructions( else { code_ifthenelset branch; - auto address_ptr=from_integer( - jsr_ret_targets[idx], - pointer_typet(void_typet(), 64)); + auto address_ptr= + from_integer( + jsr_ret_targets[idx], + unsignedbv_typet(64)); + address_ptr.type()=pointer_typet(void_typet(), 64); branch.cond()=equal_exprt(retvar, address_ptr); branch.cond().add_source_location()=i_it->source_location; branch.then_case()=g; diff --git a/src/util/arith_tools.cpp b/src/util/arith_tools.cpp index 0957cf41ab5..6acac029673 100644 --- a/src/util/arith_tools.cpp +++ b/src/util/arith_tools.cpp @@ -213,6 +213,7 @@ constant_exprt from_integer( } { + assert(false); constant_exprt r; r.make_nil(); return r; diff --git a/src/util/arith_tools.h b/src/util/arith_tools.h index 227910b0674..2dbef68b7a3 100644 --- a/src/util/arith_tools.h +++ b/src/util/arith_tools.h @@ -22,7 +22,7 @@ bool to_integer(const exprt &expr, mp_integer &int_value); // returns 'true' on error bool to_integer(const constant_exprt &expr, mp_integer &int_value); -// returns 'nil' on error +// assert(false) in case of unsupported type constant_exprt from_integer(const mp_integer &int_value, const typet &type); // ceil(log2(size))