@@ -275,13 +275,6 @@ bool variable_sensitivity_domaint::is_top() const
275
275
return abstract_state.is_top ();
276
276
}
277
277
278
- std::vector<irep_idt> variable_sensitivity_domaint::get_modified_symbols (
279
- const variable_sensitivity_domaint &other) const
280
- {
281
- return abstract_environmentt::modified_symbols (
282
- abstract_state, other.abstract_state );
283
- }
284
-
285
278
void variable_sensitivity_domaint::transform_function_call (
286
279
locationt from,
287
280
locationt to,
@@ -439,7 +432,8 @@ void variable_sensitivity_domaint::merge_three_way_function_return(
439
432
static_cast <const variable_sensitivity_domaint &>(function_end);
440
433
441
434
const std::vector<irep_idt> &modified_symbol_names =
442
- cast_function_start.get_modified_symbols (cast_function_end);
435
+ abstract_environmentt::modified_symbols (
436
+ cast_function_start.abstract_state , cast_function_end.abstract_state );
443
437
444
438
std::vector<symbol_exprt> modified_symbols;
445
439
modified_symbols.reserve (modified_symbol_names.size ());
@@ -450,21 +444,14 @@ void variable_sensitivity_domaint::merge_three_way_function_return(
450
444
[&ns](const irep_idt &id) { return ns.lookup (id).symbol_expr (); });
451
445
452
446
abstract_state = cast_function_call.abstract_state ;
453
- apply_domain (modified_symbols, cast_function_end, ns);
454
-
455
- return ;
456
- }
457
-
458
- void variable_sensitivity_domaint::apply_domain (
459
- std::vector<symbol_exprt> modified_symbols,
460
- const variable_sensitivity_domaint &source,
461
- const namespacet &ns)
462
- {
463
447
for (const auto &symbol : modified_symbols)
464
448
{
465
- abstract_object_pointert value = source.abstract_state .eval (symbol, ns);
449
+ abstract_object_pointert value =
450
+ cast_function_end.abstract_state .eval (symbol, ns);
466
451
abstract_state.assign (symbol, value, ns);
467
452
}
453
+
454
+ return ;
468
455
}
469
456
470
457
void variable_sensitivity_domaint::assume (exprt expr, namespacet ns)
0 commit comments