diff --git a/jbmc/lib/java-models-library b/jbmc/lib/java-models-library index c9d9226d346..3163b09a9f4 160000 --- a/jbmc/lib/java-models-library +++ b/jbmc/lib/java-models-library @@ -1 +1 @@ -Subproject commit c9d9226d34649c21f30bb99f92e0a3d6e5fb8977 +Subproject commit 3163b09a9f43ebe637caf508427b52e41e1993f2 diff --git a/jbmc/src/java_bytecode/java_string_library_preprocess.cpp b/jbmc/src/java_bytecode/java_string_library_preprocess.cpp index ff2dd7c23e3..bae9a3db4e3 100644 --- a/jbmc/src/java_bytecode/java_string_library_preprocess.cpp +++ b/jbmc/src/java_bytecode/java_string_library_preprocess.cpp @@ -168,18 +168,6 @@ bool java_string_library_preprocesst::is_java_char_array_pointer_type( return false; } -/// \param symbol_table: a symbol_table containing an entry for java Strings -/// \return the type of data fields in java Strings. -typet string_data_type(const symbol_tablet &symbol_table) -{ - symbolt sym=*symbol_table.lookup("java::java.lang.String"); - typet concrete_type=sym.type; - struct_typet struct_type=to_struct_type(concrete_type); - std::size_t index=struct_type.component_number("data"); - typet data_type=struct_type.components()[index].type(); - return data_type; -} - /// \return the type of the length field in java Strings. typet string_length_type() { @@ -589,26 +577,6 @@ exprt java_string_library_preprocesst::allocate_fresh_string( return str; } -/// declare a new character array and allocate it -/// \param type: a type for string -/// \param loc: a location in the program -/// \param symbol_table: symbol table -/// \param code: code block to which allocation instruction will be added -/// \return a new array -exprt java_string_library_preprocesst::allocate_fresh_array( - const typet &type, - const source_locationt &loc, - const irep_idt &function_id, - symbol_tablet &symbol_table, - code_blockt &code) -{ - exprt array=fresh_array(type, loc, symbol_table); - code.add(code_declt(array), loc); - allocate_dynamic_object_with_decl( - array, symbol_table, loc, function_id, code); - return array; -} - /// assign the result of a function call /// \param lhs: an expression /// \param function_name: the name of the function @@ -1719,55 +1687,6 @@ codet java_string_library_preprocesst::make_copy_constructor_code( return code; } -/// Used to provide code for constructor from a char array. -/// The implementation is similar to substring except the 3rd argument is a -/// count instead of end index -/// \param type: type of the function call -/// \param loc: location in the program_invocation_name -/// \param function_id: unused -/// \param symbol_table: symbol table -/// \return code implementing String intitialization from a char array and -/// arguments offset and end. -codet java_string_library_preprocesst::make_init_from_array_code( - const java_method_typet &type, - const source_locationt &loc, - const irep_idt &function_id, - symbol_table_baset &symbol_table) -{ - (void)function_id; - - // Code for the output - code_blockt code; - - java_method_typet::parameterst params = type.parameters(); - PRECONDITION(params.size() == 4); - exprt::operandst args = - process_parameters(type.parameters(), loc, symbol_table, code); - INVARIANT( - args.size() == 4, "process_parameters preserves number of arguments"); - - /// \todo this assumes the array to be constant between all calls to - /// string primitives, which may not be true in general. - refined_string_exprt string_arg = to_string_expr(args[1]); - - // The third argument is `count`, whereas the third argument of substring - // is `end` which corresponds to `offset+count` - refined_string_exprt string_expr = string_expr_of_function( - ID_cprover_string_substring_func, - {args[1], args[2], plus_exprt(args[2], args[3])}, - loc, - symbol_table, - code); - - // Assign string_expr to `this` object - symbol_exprt arg_this(params[0].get_identifier(), params[0].type()); - code.add( - code_assign_string_expr_to_java_string(arg_this, string_expr, symbol_table), - loc); - - return code; -} - /// Generates code for the String.length method /// \param type: type of the function /// \param loc: location in the source @@ -1922,13 +1841,6 @@ void java_string_library_preprocesst::initialize_conversion_table() std::placeholders::_2, std::placeholders::_3, std::placeholders::_4); - conversion_table["java::java.lang.String.:([CII)V"] = std::bind( - &java_string_library_preprocesst::make_init_from_array_code, - this, - std::placeholders::_1, - std::placeholders::_2, - std::placeholders::_3, - std::placeholders::_4); cprover_equivalent_to_java_constructor ["java::java.lang.String.:()V"]= ID_cprover_string_empty_string_func; @@ -1956,12 +1868,6 @@ void java_string_library_preprocesst::initialize_conversion_table() cprover_equivalent_to_java_function ["java::java.lang.String.contains:(Ljava/lang/CharSequence;)Z"]= ID_cprover_string_contains_func; - cprover_equivalent_to_java_string_returning_function - ["java::java.lang.String.copyValueOf:([CII)Ljava/lang/String;"]= - ID_cprover_string_copy_func; - cprover_equivalent_to_java_string_returning_function - ["java::java.lang.String.copyValueOf:([C)Ljava/lang/String;"]= - ID_cprover_string_copy_func; cprover_equivalent_to_java_function ["java::java.lang.String.endsWith:(Ljava/lang/String;)Z"]= ID_cprover_string_endswith_func; @@ -2108,9 +2014,6 @@ void java_string_library_preprocesst::initialize_conversion_table() cprover_equivalent_to_java_assign_and_return_function ["java::java.lang.StringBuilder.append:(C)Ljava/lang/StringBuilder;"]= ID_cprover_string_concat_char_func; - cprover_equivalent_to_java_assign_and_return_function - ["java::java.lang.StringBuilder.append:([C)Ljava/lang/StringBuilder;"] = - ID_cprover_string_concat_func; cprover_equivalent_to_java_assign_and_return_function ["java::java.lang.StringBuilder.append:(D)Ljava/lang/StringBuilder;"] = ID_cprover_string_concat_double_func; diff --git a/jbmc/src/java_bytecode/java_string_library_preprocess.h b/jbmc/src/java_bytecode/java_string_library_preprocess.h index dca4e97d2cd..f3b7ac829b0 100644 --- a/jbmc/src/java_bytecode/java_string_library_preprocess.h +++ b/jbmc/src/java_bytecode/java_string_library_preprocess.h @@ -43,7 +43,6 @@ class java_string_library_preprocesst:public messaget void initialize_known_type_table(); void initialize_conversion_table(); - void initialize_refined_string_type(); bool implements_function(const irep_idt &function_id) const; void get_all_function_names(std::unordered_set &methods) const; @@ -151,12 +150,6 @@ class java_string_library_preprocesst:public messaget const irep_idt &function_id, symbol_table_baset &symbol_table); - codet make_string_to_char_array_code( - const java_method_typet &type, - const source_locationt &loc, - const irep_idt &function_id, - symbol_tablet &symbol_table); - codet make_string_format_code( const java_method_typet &type, const source_locationt &loc, @@ -254,13 +247,6 @@ class java_string_library_preprocesst:public messaget symbol_table_baset &symbol_table, code_blockt &code); - exprt allocate_fresh_array( - const typet &type, - const source_locationt &loc, - const irep_idt &function_id, - symbol_tablet &symbol_table, - code_blockt &code); - codet code_return_function_application( const irep_idt &function_name, const exprt::operandst &arguments, @@ -346,12 +332,6 @@ class java_string_library_preprocesst:public messaget code_blockt &code); exprt get_object_at_index(const exprt &argv, std::size_t index); - - codet make_init_from_array_code( - const java_method_typet &type, - const source_locationt &loc, - const irep_idt &function_id, - symbol_table_baset &symbol_table); }; exprt make_nondet_infinite_char_array(