Skip to content

Use consistent types with function_application_exprt [blocks: #3766] #3872

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 2 commits into from
Jan 22, 2019
Merged

Use consistent types with function_application_exprt [blocks: #3766] #3872

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
df04b3d
Hide declare_function and set type in symbol_exprt
tautschnig Jan 21, 2019
b4a3c0c
Use consistent types with function_application_exprt
tautschnig Jan 21, 2019
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
14 changes: 7 additions & 7 deletions jbmc/src/java_bytecode/java_utils.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -247,8 +247,9 @@ void java_add_components_to_class(
/// \param function_name: a name
/// \param type: a type
/// \param symbol_table: symbol table
void declare_function(
irep_idt function_name,
/// \return newly created symbol
static auxiliary_symbolt declare_function(
const irep_idt &function_name,
const typet &type,
symbol_table_baset &symbol_table)
{
Expand All @@ -260,6 +261,8 @@ void declare_function(
func_symbol.name=function_name;
func_symbol.type=type;
symbol_table.add(func_symbol);

return func_symbol;
}

/// Create a function application expression.
Expand All @@ -275,14 +278,11 @@ exprt make_function_application(
const typet &type,
symbol_table_baset &symbol_table)
{
// Names of function to call
std::string fun_name=id2string(function_name);

// Declaring the function
declare_function(fun_name, type, symbol_table);
const auto symbol = declare_function(function_name, type, symbol_table);

// Function application
return function_application_exprt(symbol_exprt(fun_name), arguments, type);
return function_application_exprt(symbol.symbol_expr(), arguments, type);
}

/// Strip java:: prefix from given identifier
Expand Down
5 changes: 0 additions & 5 deletions jbmc/src/java_bytecode/java_utils.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -87,11 +87,6 @@ size_t find_closing_delimiter(
char open_char,
char close_char);

void declare_function(
irep_idt function_name,
const typet &type,
symbol_table_baset &symbol_table);

exprt make_function_application(
const irep_idt &function_name,
const exprt::operandst &arguments,
Expand Down
2 changes: 1 addition & 1 deletion jbmc/unit/solvers/strings/string_constraint_instantiation/instantiate_not_contains.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -194,7 +194,7 @@ SCENARIO(
{
// Creating "ab".lastIndexOf("b", 0)
const function_application_exprt func(
symbol_exprt(ID_cprover_string_last_index_of_func),
symbol_exprt(ID_cprover_string_last_index_of_func, t.length_type()),
{ab, b, from_integer(2)},
t.length_type());

Expand Down
6 changes: 3 additions & 3 deletions jbmc/unit/solvers/strings/string_refinement/dependency_graph.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -64,19 +64,19 @@ SCENARIO("dependency_graph", "[core][solvers][refinement][string_refinement]")

// fun1 is s3 = s1.concat(s2)
const function_application_exprt fun1(
symbol_exprt(ID_cprover_string_concat_func),
symbol_exprt(ID_cprover_string_concat_func, fun_type),
{string3.op0(), string3.op1(), string1, string2},
fun_type);

// fun2 is s5 = s3.concat(s4)
const function_application_exprt fun2(
symbol_exprt(ID_cprover_string_concat_func),
symbol_exprt(ID_cprover_string_concat_func, fun_type),
{string5.op0(), string5.op1(), string3, string4},
fun_type);

// fun3 is s6 = s5.concat(s2)
const function_application_exprt fun3(
symbol_exprt(ID_cprover_string_concat_func),
symbol_exprt(ID_cprover_string_concat_func, fun_type),
{string6.op0(), string6.op1(), string5, string2},
fun_type);

Expand Down