Skip to content

Commit f8131c3

Browse files
Merge pull request #1102 from romainbrenguier/pull-request/remove-unused-function-in-string-preprocessing
Removing string literal function from string preprocess cpp
2 parents 836be74 + c33306a commit f8131c3

File tree

2 files changed

+0
-14
lines changed

2 files changed

+0
-14
lines changed

src/java_bytecode/java_string_library_preprocess.cpp

-12
Original file line numberDiff line numberDiff line change
@@ -868,18 +868,6 @@ codet java_string_library_preprocesst::make_equals_function_code(
868868
return code;
869869
}
870870

871-
/// construct a string_exprt from a constant string value
872-
/// \param s: a string
873-
/// \param symbol_table: a symbol table
874-
/// \return an expression representing a string expr with the given content
875-
exprt java_string_library_preprocesst::string_literal(
876-
const std::string &s, symbol_tablet &symbol_table)
877-
{
878-
constant_exprt expr(s, string_typet());
879-
return make_function_application(
880-
ID_cprover_string_literal_func, {expr}, refined_string_type, symbol_table);
881-
}
882-
883871
/// Provide code for the String.valueOf(F) function.
884872
/// \param type: type of the function call
885873
/// \param loc: location in the program_invocation_name

src/java_bytecode/java_string_library_preprocess.h

-2
Original file line numberDiff line numberDiff line change
@@ -286,8 +286,6 @@ class java_string_library_preprocesst:public messaget
286286
const std::string &s,
287287
symbol_tablet &symbol_table);
288288

289-
exprt string_literal(const std::string &s, symbol_tablet &symbol_table);
290-
291289
codet make_function_from_call(
292290
const irep_idt &function_name,
293291
const code_typet &type,

0 commit comments

Comments
 (0)