File tree Expand file tree Collapse file tree 1 file changed +9
-6
lines changed Expand file tree Collapse file tree 1 file changed +9
-6
lines changed Original file line number Diff line number Diff line change @@ -429,6 +429,14 @@ array_string_exprt array_poolt::of_argument(const exprt &arg)
429
429
return find (string_argument.op1 (), string_argument.op0 ());
430
430
}
431
431
432
+ static irep_idt get_function_name (const function_application_exprt &expr)
433
+ {
434
+ const exprt &name = expr.function ();
435
+ PRECONDITION (name.id () == ID_symbol);
436
+ return is_ssa_expr (name) ? to_ssa_expr (name).get_object_name ()
437
+ : to_symbol_expr (name).get_identifier ();
438
+ }
439
+
432
440
// / strings contained in this call are converted to objects of type
433
441
// / `string_exprt`, through adding axioms. Axioms are then added to enforce that
434
442
// / the result corresponds to the function application.
@@ -437,12 +445,7 @@ array_string_exprt array_poolt::of_argument(const exprt &arg)
437
445
exprt string_constraint_generatort::add_axioms_for_function_application (
438
446
const function_application_exprt &expr)
439
447
{
440
- const exprt &name=expr.function ();
441
- PRECONDITION (name.id ()==ID_symbol);
442
-
443
- const irep_idt &id=is_ssa_expr (name)?to_ssa_expr (name).get_object_name ():
444
- to_symbol_expr (name).get_identifier ();
445
-
448
+ const irep_idt &id = get_function_name (expr);
446
449
exprt res;
447
450
448
451
if (id==ID_cprover_char_literal_func)
You can’t perform that action at this time.
0 commit comments