diff --git a/jbmc/regression/jbmc/NondetEnumArg/Color.class b/jbmc/regression/jbmc/NondetEnumArg/Color.class new file mode 100644 index 00000000000..5fc329a12dd Binary files /dev/null and b/jbmc/regression/jbmc/NondetEnumArg/Color.class differ diff --git a/jbmc/regression/jbmc/NondetEnumArg/Color.java b/jbmc/regression/jbmc/NondetEnumArg/Color.java new file mode 100644 index 00000000000..0fd41d395d0 --- /dev/null +++ b/jbmc/regression/jbmc/NondetEnumArg/Color.java @@ -0,0 +1,5 @@ +public enum Color { + RED, + GREEN, + BLUE +} diff --git a/jbmc/regression/jbmc/NondetEnumArg/NondetEnumArg.class b/jbmc/regression/jbmc/NondetEnumArg/NondetEnumArg.class new file mode 100644 index 00000000000..b4af0ffd3c8 Binary files /dev/null and b/jbmc/regression/jbmc/NondetEnumArg/NondetEnumArg.class differ diff --git a/jbmc/regression/jbmc/NondetEnumArg/NondetEnumArg.java b/jbmc/regression/jbmc/NondetEnumArg/NondetEnumArg.java new file mode 100644 index 00000000000..399fcd53033 --- /dev/null +++ b/jbmc/regression/jbmc/NondetEnumArg/NondetEnumArg.java @@ -0,0 +1,46 @@ +public class NondetEnumArg { + + public static void canChooseSomeConstant(Color c) { + if (c == null) + return; + assert c != null; + boolean isRed = c.name().startsWith("RED") && c.name().length() == 3 + && c.ordinal() == 0; + boolean isGreen = c.name().startsWith("GREEN") && c.name().length() == 5 + && c.ordinal() == 1; + boolean isBlue = c.name().startsWith("BLUE") && c.name().length() == 4 + && c.ordinal() == 2; + assert (isRed || isGreen || isBlue); + } + + public static void canChooseRed(Color c) { + if (c == null) + return; + boolean isGreen = c.name().startsWith("GREEN") && c.name().length() == 5 + && c.ordinal() == 1; + boolean isBlue = c.name().startsWith("BLUE") && c.name().length() == 4 + && c.ordinal() == 2; + assert (isGreen || isBlue); + } + + public static void canChooseGreen(Color c) { + if (c == null) + return; + boolean isRed = c.name().startsWith("RED") && c.name().length() == 3 + && c.ordinal() == 0; + boolean isBlue = c.name().startsWith("BLUE") && c.name().length() == 4 + && c.ordinal() == 2; + assert (isRed || isBlue); + } + + public static void canChooseBlue(Color c) { + if (c == null) + return; + boolean isRed = c.name().startsWith("RED") && c.name().length() == 3 + && c.ordinal() == 0; + boolean isGreen = c.name().startsWith("GREEN") && c.name().length() == 5 + && c.ordinal() == 1; + assert (isRed || isGreen); + } + +} diff --git a/jbmc/regression/jbmc/NondetEnumArg/test_some_constant.desc b/jbmc/regression/jbmc/NondetEnumArg/test_some_constant.desc new file mode 100644 index 00000000000..2e88221ea60 --- /dev/null +++ b/jbmc/regression/jbmc/NondetEnumArg/test_some_constant.desc @@ -0,0 +1,10 @@ +CORE +NondetEnumArg.class +--function NondetEnumArg.canChooseSomeConstant --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` +^VERIFICATION SUCCESSFUL$ +^EXIT=0$ +^SIGNAL=0$ +-- +-- +The test checks that the name and ordinal fields of nondet-initialized enums +correspond to those of an enum constant of the same type. diff --git a/jbmc/regression/jbmc/NondetEnumArg/test_specific_constant1.desc b/jbmc/regression/jbmc/NondetEnumArg/test_specific_constant1.desc new file mode 100644 index 00000000000..4f4d5c34208 --- /dev/null +++ b/jbmc/regression/jbmc/NondetEnumArg/test_specific_constant1.desc @@ -0,0 +1,7 @@ +CORE +NondetEnumArg.class +--function NondetEnumArg.canChooseRed --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` +^VERIFICATION FAILED$ +-- +-- +Test 1 of 3 to check that any of the enum constants can be chosen. diff --git a/jbmc/regression/jbmc/NondetEnumArg/test_specific_constant2.desc b/jbmc/regression/jbmc/NondetEnumArg/test_specific_constant2.desc new file mode 100644 index 00000000000..52b06d65b1c --- /dev/null +++ b/jbmc/regression/jbmc/NondetEnumArg/test_specific_constant2.desc @@ -0,0 +1,7 @@ +CORE +NondetEnumArg.class +--function NondetEnumArg.canChooseGreen --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` +^VERIFICATION FAILED$ +-- +-- +Test 2 of 3 to check that any of the enum constants can be chosen. diff --git a/jbmc/regression/jbmc/NondetEnumArg/test_specific_constant3.desc b/jbmc/regression/jbmc/NondetEnumArg/test_specific_constant3.desc new file mode 100644 index 00000000000..3913535c8c4 --- /dev/null +++ b/jbmc/regression/jbmc/NondetEnumArg/test_specific_constant3.desc @@ -0,0 +1,7 @@ +CORE +NondetEnumArg.class +--function NondetEnumArg.canChooseBlue --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` +^VERIFICATION FAILED$ +-- +-- +Test 3 of 3 to check that any of the enum constants can be chosen. diff --git a/jbmc/src/java_bytecode/ci_lazy_methods.cpp b/jbmc/src/java_bytecode/ci_lazy_methods.cpp index dd7a161e303..414b2a51ad0 100644 --- a/jbmc/src/java_bytecode/ci_lazy_methods.cpp +++ b/jbmc/src/java_bytecode/ci_lazy_methods.cpp @@ -381,7 +381,17 @@ void ci_lazy_methodst::initialize_instantiated_classes( { if(param.type().id()==ID_pointer) { - const pointer_typet &original_pointer=to_pointer_type(param.type()); + const pointer_typet &original_pointer = to_pointer_type(param.type()); + const auto &original_type = ns.follow(original_pointer.subtype()); + // Special case for enums. We may want to generalise this, see TG-4689 + // and the comment in java_object_factoryt::gen_nondet_pointer_init. + if( + can_cast_type(original_type) && + to_java_class_type(original_type).get_base("java::java.lang.Enum")) + { + add_clinit_call_for_pointer_type( + original_pointer, ns.get_symbol_table(), needed_lazy_methods); + } needed_lazy_methods.add_all_needed_classes(original_pointer); } } @@ -399,6 +409,29 @@ void ci_lazy_methodst::initialize_instantiated_classes( needed_lazy_methods.add_needed_class("java::" + id2string(id)); } +/// Helper function for `initialize_instantiated_classes`. +/// For a given pointer_typet that is being noted as needed in +/// `needed_lazy_methods`, notes that its static initializer is also needed. +/// This applies the same logic to the class of `pointer_type` that +/// `java_bytecode_convert_methodt::get_clinit_call` applies e.g. to classes +/// whose constructor we call in a method body. This duplication is unavoidable +/// due to the fact that ci_lazy_methods essentially has to go through the same +/// logic as __CPROVER_start in its initial setup. +/// \param pointer_type: The given pointer_typet +/// \param symbol_table: Used to look up occurrences of static initializers +/// \param [out] needed_lazy_methods: Gets notified of any static initializers +/// that need to be loaded +void ci_lazy_methodst::add_clinit_call_for_pointer_type( + const pointer_typet &pointer_type, + const symbol_tablet &symbol_table, + ci_lazy_methods_neededt &needed_lazy_methods) +{ + const irep_idt &pointer_id = + to_symbol_type(pointer_type.subtype()).get_identifier(); + const irep_idt &clinit_wrapper = clinit_wrapper_name(pointer_id); + if(symbol_table.symbols.count(clinit_wrapper)) + needed_lazy_methods.add_needed_method(clinit_wrapper); +} /// Get places where virtual functions are called. /// \param e: expression tree to search diff --git a/jbmc/src/java_bytecode/ci_lazy_methods.h b/jbmc/src/java_bytecode/ci_lazy_methods.h index f90d2186a8e..905258f1c4d 100644 --- a/jbmc/src/java_bytecode/ci_lazy_methods.h +++ b/jbmc/src/java_bytecode/ci_lazy_methods.h @@ -120,6 +120,11 @@ class ci_lazy_methodst:public messaget const namespacet &ns, ci_lazy_methods_neededt &needed_lazy_methods); + void add_clinit_call_for_pointer_type( + const pointer_typet &pointer_type, + const symbol_tablet &symbol_table, + ci_lazy_methods_neededt &needed_lazy_methods); + void gather_virtual_callsites( const exprt &e, std::unordered_set &result); diff --git a/jbmc/src/java_bytecode/java_object_factory.cpp b/jbmc/src/java_bytecode/java_object_factory.cpp index 2760a9936bb..e29b5d5832c 100644 --- a/jbmc/src/java_bytecode/java_object_factory.cpp +++ b/jbmc/src/java_bytecode/java_object_factory.cpp @@ -107,6 +107,12 @@ class java_object_factoryt update_in_placet, const source_locationt &location); + void gen_nondet_enum_init( + code_blockt &assignments, + const exprt &expr, + const java_class_typet &java_class_type, + const source_locationt &location); + void gen_nondet_init( code_blockt &assignments, const exprt &expr, @@ -148,6 +154,18 @@ class java_object_factoryt const pointer_typet &substitute_pointer_type, size_t depth, const source_locationt &location); + + const symbol_exprt gen_nondet_int_init( + code_blockt &assignments, + const std::string &basename_prefix, + const exprt &min_length_expr, + const exprt &max_length_expr, + const source_locationt &location); + + void gen_method_call_if_present( + code_blockt &assignments, + const exprt &instance_expr, + const irep_idt &method_name); }; /// Generates code for allocating a dynamic object. This is used in @@ -382,65 +400,64 @@ void java_object_factoryt::gen_pointer_target_init( update_in_placet update_in_place, const source_locationt &location) { - PRECONDITION(expr.type().id()==ID_pointer); - PRECONDITION(update_in_place!=update_in_placet::MAY_UPDATE_IN_PLACE); + PRECONDITION(expr.type().id() == ID_pointer); + PRECONDITION(update_in_place != update_in_placet::MAY_UPDATE_IN_PLACE); - if(target_type.id()==ID_struct && - has_prefix( - id2string(to_struct_type(target_type).get_tag()), - "java::array[")) - { - gen_nondet_array_init( - assignments, expr, depth + 1, update_in_place, location); - } - else + if(target_type.id() == ID_struct) { - // obtain a target pointer to initialize; if in MUST_UPDATE_IN_PLACE mode we - // initialize the fields of the object pointed by `expr`; if in - // NO_UPDATE_IN_PLACE then we allocate a new object, get a pointer to it - // (return value of `allocate_object`), emit a statement of the form - // ` := address-of()` and recursively initialize such new - // object. - exprt target; - if(update_in_place==update_in_placet::NO_UPDATE_IN_PLACE) + const auto &target_class_type = to_java_class_type(target_type); + if(has_prefix(id2string(target_class_type.get_tag()), "java::array[")) { - target=allocate_object( - assignments, - expr, - target_type, - alloc_type); - INVARIANT( - target.type().id()==ID_pointer, - "Pointer-typed expression expected"); + gen_nondet_array_init( + assignments, expr, depth + 1, update_in_place, location); + return; } - else + if(target_class_type.get_base("java::java.lang.Enum")) { - target=expr; + gen_nondet_enum_init(assignments, expr, target_class_type, location); + return; } + } - // we dereference the pointer and initialize the resulting object using a - // recursive call - exprt init_expr; - if(target.id()==ID_address_of) - init_expr=target.op0(); - else - { - init_expr= - dereference_exprt(target, target.type().subtype()); - } - gen_nondet_init( - assignments, - init_expr, - false, // is_sub - "", // class_identifier - false, // skip_classid - alloc_type, - false, - typet(), - depth + 1, - update_in_place, - location); + // obtain a target pointer to initialize; if in MUST_UPDATE_IN_PLACE mode we + // initialize the fields of the object pointed by `expr`; if in + // NO_UPDATE_IN_PLACE then we allocate a new object, get a pointer to it + // (return value of `allocate_object`), emit a statement of the form + // ` := address-of()` and recursively initialize such new + // object. + exprt target; + if(update_in_place == update_in_placet::NO_UPDATE_IN_PLACE) + { + target = allocate_object(assignments, expr, target_type, alloc_type); + INVARIANT( + target.type().id() == ID_pointer, "Pointer-typed expression expected"); } + else + { + target = expr; + } + + // we dereference the pointer and initialize the resulting object using a + // recursive call + exprt init_expr; + if(target.id() == ID_address_of) + init_expr = target.op0(); + else + { + init_expr = dereference_exprt(target, target.type().subtype()); + } + gen_nondet_init( + assignments, + init_expr, + false, // is_sub + "", // class_identifier + false, // skip_classid + alloc_type, + false, // override + typet(), // override type immaterial + depth + 1, + update_in_place, + location); } /// Recursion-set entry owner class. If a recursion-set entry is added @@ -764,6 +781,35 @@ void java_object_factoryt::gen_nondet_pointer_init( } } + // If this is a void* we *must* initialise with null: + // (This can currently happen for some cases of #exception_value) + bool must_be_null = subtype == empty_typet(); + + // If we may be about to initialize a non-null enum type, always run the + // clinit_wrapper of its class first. + // TODO: TG-4689 we may want to do this for all types, not just enums, as + // described in the Java language specification: + // https://docs.oracle.com/javase/specs/jls/se8/html/jls-8.html#jls-8.7 + // https://docs.oracle.com/javase/specs/jls/se8/html/jls-12.html#jls-12.4.1 + // But we would have to put this behavior behind an option as it would have an + // impact on running times. + // Note that it would be more consistent with the behaviour of the JVM to only + // run clinit_wrapper if we are about to initialize an object of which we know + // for sure that it is not null on any following branch. However, adding this + // case in gen_nondet_struct_init would slow symex down too much, so if we + // decide to do this for all types, we should do it here. + // Note also that this logic is mirrored in + // ci_lazy_methodst::initialize_instantiated_classes. + if(const auto class_type = type_try_dynamic_cast(subtype)) + { + if(class_type->get_base("java::java.lang.Enum") && !must_be_null) + { + const irep_idt &class_name = class_type->get_name(); + const irep_idt class_clinit = clinit_wrapper_name(class_name); + gen_method_call_if_present(assignments, expr, class_clinit); + } + } + code_blockt new_object_assignments; code_blockt update_in_place_assignments; @@ -810,10 +856,6 @@ void java_object_factoryt::gen_nondet_pointer_init( const bool allow_null = depth > object_factory_parameters.max_nonnull_tree_depth; - // Alternatively, if this is a void* we *must* initialise with null: - // (This can currently happen for some cases of #exception_value) - bool must_be_null = subtype == empty_typet(); - if(must_be_null) { // Add the following code to assignments: @@ -974,7 +1016,7 @@ void java_object_factoryt::gen_nondet_struct_init( // Should we write the whole object? // * Not if this is a sub-structure (a superclass object), as our caller will // have done this already - // * Not if the object has already been initialised by our caller, in whic + // * Not if the object has already been initialised by our caller, in which // case they will set `skip_classid` // * Not if we're re-initializing an existing object (i.e. update_in_place) @@ -1081,20 +1123,10 @@ void java_object_factoryt::gen_nondet_struct_init( const irep_idt init_method_name = "java::" + id2string(struct_tag) + ".cproverNondetInitialize:()V"; - - if(const auto func = symbol_table.lookup(init_method_name)) - { - const java_method_typet &type = to_java_method_type(func->type); - code_function_callt fun_call; - fun_call.function() = func->symbol_expr(); - if(type.has_this()) - fun_call.arguments().push_back(address_of_exprt(expr)); - - assignments.add(fun_call); - } + gen_method_call_if_present(assignments, expr, init_method_name); } -/// Initializes a primitive-typed or referece-typed object tree rooted at +/// Initializes a primitive-typed or reference-typed object tree rooted at /// `expr`, allocating child objects as necessary and nondet-initializing their /// members, or if MUST_UPDATE_IN_PLACE is set, re-initializing /// already-allocated objects. @@ -1209,6 +1241,60 @@ void java_object_factoryt::gen_nondet_init( } } +/// Nondeterministically initializes an int i in the range min <= i <= max, +/// where min is the integer represented by `min_value_expr` and max is the +/// integer represented by `max_value_expr`. +/// \param [out] assignments: A code block that the initializing assignments +/// will be appended to. +/// \param basename_prefix: Used for naming the newly created symbol. +/// \param min_value_expr: Represents the minimum value for the integer. +/// \param max_value_expr: Represents the maximum value for the integer. +/// \param location: Source location associated with nondet-initialization. +/// \return A symbol expression for the resulting integer. +const symbol_exprt java_object_factoryt::gen_nondet_int_init( + code_blockt &assignments, + const std::string &basename_prefix, + const exprt &min_value_expr, + const exprt &max_value_expr, + const source_locationt &location) +{ + PRECONDITION(min_value_expr.type() == max_value_expr.type()); + // Allocate a new symbol for the int + const symbolt &int_symbol = get_fresh_aux_symbol( + min_value_expr.type(), + id2string(object_factory_parameters.function_id), + basename_prefix, + loc, + ID_java, + symbol_table); + symbols_created.push_back(&int_symbol); + const auto &int_symbol_expr = int_symbol.symbol_expr(); + + // Nondet-initialize it + gen_nondet_init( + assignments, + int_symbol_expr, + false, // is_sub + irep_idt(), + false, // skip_classid + allocation_typet::LOCAL, // immaterial, type is primitive + false, // override + typet(), // override type is immaterial + 0, // depth is immaterial, always non-null + update_in_placet::NO_UPDATE_IN_PLACE, + location); + + // Insert assumptions to bound its value + const auto min_assume_expr = + binary_relation_exprt(int_symbol_expr, ID_ge, min_value_expr); + const auto max_assume_expr = + binary_relation_exprt(int_symbol_expr, ID_le, max_value_expr); + assignments.add(code_assumet(min_assume_expr)); + assignments.add(code_assumet(max_assume_expr)); + + return int_symbol_expr; +} + /// Allocates a fresh array and emits an assignment writing to \p lhs the /// address of the new array. Single-use at the moment, but useful to keep as a /// separate function for downstream branches. @@ -1229,46 +1315,19 @@ void java_object_factoryt::allocate_nondet_length_array( const typet &element_type, const source_locationt &location) { - symbolt &length_sym = get_fresh_aux_symbol( - java_int_type(), - id2string(object_factory_parameters.function_id), - "nondet_array_length", - loc, - ID_java, - symbol_table); - symbols_created.push_back(&length_sym); - const auto &length_sym_expr=length_sym.symbol_expr(); - - // Initialize array with some undetermined length: - gen_nondet_init( + const auto &length_sym_expr = gen_nondet_int_init( assignments, - length_sym_expr, - false, // is_sub - irep_idt(), - false, // skip_classid - allocation_typet::LOCAL, // immaterial, type is primitive - false, // override - typet(), // override type is immaterial - 0, // depth is immaterial, always non-null - update_in_placet::NO_UPDATE_IN_PLACE, + "nondet_array_length", + from_integer(0, java_int_type()), + max_length_expr, location); - // Insert assumptions to bound its length: - binary_relation_exprt - assume1(length_sym_expr, ID_ge, from_integer(0, java_int_type())); - binary_relation_exprt - assume2(length_sym_expr, ID_le, max_length_expr); - code_assumet assume_inst1(assume1); - code_assumet assume_inst2(assume2); - assignments.move_to_operands(assume_inst1); - assignments.move_to_operands(assume_inst2); - side_effect_exprt java_new_array(ID_java_new_array, lhs.type(), loc); java_new_array.copy_to_operands(length_sym_expr); java_new_array.set(ID_length_upper_bound, max_length_expr); java_new_array.type().subtype().set(ID_element_type, element_type); code_assignt assign(lhs, java_new_array); - assign.add_source_location()=loc; + assign.add_source_location() = loc; assignments.copy_to_operands(assign); } @@ -1411,6 +1470,51 @@ void java_object_factoryt::gen_nondet_array_init( assignments.move_to_operands(init_done_label); } +/// We nondet-initialize enums to be equal to one of the constants defined +/// for their type: +/// int i = nondet(int); +/// assume(0 < = i < $VALUES.length); +/// expr = $VALUES[i]; +/// where $VALUES is a variable generated by the Java compiler that stores +/// the array that is returned by Enum.values(). +void java_object_factoryt::gen_nondet_enum_init( + code_blockt &assignments, + const exprt &expr, + const java_class_typet &java_class_type, + const source_locationt &location) +{ + const irep_idt &class_name = java_class_type.get_name(); + const irep_idt values_name = id2string(class_name) + ".$VALUES"; + INVARIANT( + ns.get_symbol_table().has_symbol(values_name), + "The $VALUES array (populated by clinit_wrapper) should be in the " + "symbol table"); + const symbolt &values = ns.lookup(values_name); + + // Access members (length and data) of $VALUES array + dereference_exprt deref_expr(values.symbol_expr()); + const auto &deref_struct_type = to_struct_type(ns.follow(deref_expr.type())); + PRECONDITION(is_valid_java_array(deref_struct_type)); + const auto &comps = deref_struct_type.components(); + const member_exprt length_expr(deref_expr, "length", comps[1].type()); + const member_exprt enum_array_expr = + member_exprt(deref_expr, "data", comps[2].type()); + + const symbol_exprt &index_expr = gen_nondet_int_init( + assignments, + "enum_index_init", + from_integer(0, java_int_type()), + minus_exprt(length_expr, from_integer(1, java_int_type())), + location); + + // Generate statement using pointer arithmetic to access array element: + // expr = (expr.type())*(enum_array_expr + index_expr); + plus_exprt plus(enum_array_expr, index_expr); + const dereference_exprt arraycellref(plus); + code_assignt enum_assign(expr, typecast_exprt(arraycellref, expr.type())); + assignments.add(enum_assign); +} + /// Add code_declt instructions to `init_code` for every non-static symbol /// in `symbols_created` /// \param symbols_created: list of symbols @@ -1619,3 +1723,25 @@ void gen_nondet_init( pointer_type_selector, update_in_place); } + +/// Adds a call for the given method to the end of `assignments` if the method +/// exists in the symbol table. Does nothing if the method does not exist. +/// \param assignments: A code block that the method call will be appended to. +/// \param instance_expr: The instance to call the method on. This argument is +/// ignored if the method is static. +/// \param method_name: The name of the method to be called. +void java_object_factoryt::gen_method_call_if_present( + code_blockt &assignments, + const exprt &instance_expr, + const irep_idt &method_name) +{ + if(const auto func = symbol_table.lookup(method_name)) + { + const java_method_typet &type = to_java_method_type(func->type); + code_function_callt fun_call; + fun_call.function() = func->symbol_expr(); + if(type.has_this()) + fun_call.arguments().push_back(address_of_exprt(instance_expr)); + assignments.add(fun_call); + } +} diff --git a/jbmc/src/java_bytecode/java_object_factory.h b/jbmc/src/java_bytecode/java_object_factory.h index d174d4e4ae2..acde2f165fe 100644 --- a/jbmc/src/java_bytecode/java_object_factory.h +++ b/jbmc/src/java_bytecode/java_object_factory.h @@ -19,8 +19,9 @@ Author: Daniel Kroening, kroening@kroening.com /// that are called but for which we don't have a body (overapproximating the /// return value and possibly side effects). /// -/// The two main APIs are \ref gen_nondet_init() and \ref object_factory(), at -/// the bottom of the file. Their purpose is very similar. A call to +/// The two main APIs are \ref gen_nondet_init() and \ref object_factory() +/// (which calls gen_nondet_init()), at the bottom of the file. +/// A call to /// /// gen_nondet_init(expr, code, ..., update_in_place) /// @@ -28,7 +29,9 @@ Author: Daniel Kroening, kroening@kroening.com /// non-deterministically initialize the `expr` (which is expected to be an /// l-value exprt) with a primitive or reference value of type equal to or /// compatible with `expr.type()` -- see documentation for the argument -/// `pointer_type_selector` for additional details. +/// `pointer_type_selector` for additional details. gen_nondet_init() is the +/// starting point of a recursive algorithm, and most other functions in this +/// file are different (recursive or base) cases depending on the type of expr. /// /// The code generated mainly depends on the parameter `update_in_place`. Assume /// that `expr` is a reference to an object (in our IR, that means a pointer to diff --git a/src/goto-symex/symex_builtin_functions.cpp b/src/goto-symex/symex_builtin_functions.cpp index 07104728643..f23726cd88a 100644 --- a/src/goto-symex/symex_builtin_functions.cpp +++ b/src/goto-symex/symex_builtin_functions.cpp @@ -505,7 +505,8 @@ void goto_symext::symex_fkt( statet &, const code_function_callt &) { - UNREACHABLE; + // TODO: uncomment this line when TG-4667 is done + // UNREACHABLE; #if 0 exprt new_fc(ID_function, fc.type()); diff --git a/src/goto-symex/symex_catch.cpp b/src/goto-symex/symex_catch.cpp index a5440bb3c90..33b0317f61e 100644 --- a/src/goto-symex/symex_catch.cpp +++ b/src/goto-symex/symex_catch.cpp @@ -13,7 +13,8 @@ Author: Daniel Kroening, kroening@kroening.com void goto_symext::symex_catch(statet &) { - UNREACHABLE; + // TODO: uncomment this line when TG-4667 is done + // UNREACHABLE; // there are two variants: 'push' and 'pop' #if 0