From 54e80da8391068a3353dde1731fde744891f9a1e Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Fri, 1 Sep 2017 11:31:33 +0100 Subject: [PATCH 1/9] added __CPROVER_precondtion(c, d) --- src/ansi-c/ansi_c_internal_additions.cpp | 2 ++ src/ansi-c/library/cprover.h | 1 + src/goto-programs/builtin_functions.cpp | 23 ++++++++++++++++++----- src/util/irep_ids.def | 1 + 4 files changed, 22 insertions(+), 5 deletions(-) diff --git a/src/ansi-c/ansi_c_internal_additions.cpp b/src/ansi-c/ansi_c_internal_additions.cpp index aa1d82e0102..6cfe07b0e2c 100644 --- a/src/ansi-c/ansi_c_internal_additions.cpp +++ b/src/ansi-c/ansi_c_internal_additions.cpp @@ -112,6 +112,8 @@ void ansi_c_internal_additions(std::string &code) "void __VERIFIER_assume(__CPROVER_bool assumption);\n" // NOLINTNEXTLINE(whitespace/line_length) "void __CPROVER_assert(__CPROVER_bool assertion, const char *description);\n" + // NOLINTNEXTLINE(whitespace/line_length) + "void __CPROVER_precondition(__CPROVER_bool precondition, const char *description);\n" "__CPROVER_bool __CPROVER_equal();\n" "__CPROVER_bool __CPROVER_same_object(const void *, const void *);\n" "__CPROVER_bool __CPROVER_invalid_pointer(const void *);\n" diff --git a/src/ansi-c/library/cprover.h b/src/ansi-c/library/cprover.h index 251bb828b6f..94da717f33d 100644 --- a/src/ansi-c/library/cprover.h +++ b/src/ansi-c/library/cprover.h @@ -19,6 +19,7 @@ extern const void *__CPROVER_memory_leak; void __CPROVER_assume(__CPROVER_bool assumption) __attribute__((__noreturn__)); void __CPROVER_assert(__CPROVER_bool assertion, const char *description); +void __CPROVER_precondition(__CPROVER_bool assertion, const char *description); __CPROVER_bool __CPROVER_is_zero_string(const void *); __CPROVER_size_t __CPROVER_zero_string_length(const void *); diff --git a/src/goto-programs/builtin_functions.cpp b/src/goto-programs/builtin_functions.cpp index f1a103e2428..fbf77309efe 100644 --- a/src/goto-programs/builtin_functions.cpp +++ b/src/goto-programs/builtin_functions.cpp @@ -1113,7 +1113,8 @@ void goto_convertt::do_function_call_symbol( throw 0; } } - else if(identifier==CPROVER_PREFIX "assert") + else if(identifier==CPROVER_PREFIX "assert" || + identifier==CPROVER_PREFIX "precondition") { if(arguments.size()!=2) { @@ -1123,16 +1124,28 @@ void goto_convertt::do_function_call_symbol( throw 0; } + bool is_precondition= + identifier==CPROVER_PREFIX "precondition"; + const irep_idt description= get_string_constant(arguments[1]); goto_programt::targett t=dest.add_instruction(ASSERT); t->guard=arguments[0]; t->source_location=function.source_location(); - t->source_location.set( - "user-provided", - !function.source_location().is_built_in()); - t->source_location.set_property_class(ID_assertion); + + if(is_precondition) + { + t->source_location.set_property_class(ID_precondition); + } + else + { + t->source_location.set( + "user-provided", + !function.source_location().is_built_in()); + t->source_location.set_property_class(ID_assertion); + } + t->source_location.set_comment(description); // let's double-check the type of the argument diff --git a/src/util/irep_ids.def b/src/util/irep_ids.def index 92457c747f3..92afdfd3e4a 100644 --- a/src/util/irep_ids.def +++ b/src/util/irep_ids.def @@ -90,6 +90,7 @@ IREP_ID_ONE(assign_bitor) IREP_ID_ONE(assume) IREP_ID_ONE(assert) IREP_ID_ONE(assertion) +IREP_ID_ONE(precondition) IREP_ID_ONE(goto) IREP_ID_ONE(gcc_computed_goto) IREP_ID_ONE(ifthenelse) From 5624b153a8cdca31412ad5e1d652f81c0d0d54b0 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Fri, 1 Sep 2017 16:47:55 +0100 Subject: [PATCH 2/9] instrumentation for preconditions --- src/cbmc/cbmc_parse_options.cpp | 4 + src/goto-programs/Makefile | 1 + .../instrument_preconditions.cpp | 148 ++++++++++++++++++ src/goto-programs/instrument_preconditions.h | 19 +++ src/util/irep_ids.def | 1 + 5 files changed, 173 insertions(+) create mode 100644 src/goto-programs/instrument_preconditions.cpp create mode 100644 src/goto-programs/instrument_preconditions.h diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp index 265759fc698..224d71b658e 100644 --- a/src/cbmc/cbmc_parse_options.cpp +++ b/src/cbmc/cbmc_parse_options.cpp @@ -27,6 +27,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include #include #include #include @@ -780,6 +781,9 @@ bool cbmc_parse_optionst::process_goto_program( mm_io(goto_model); + // instrument library preconditions + instrument_preconditions(goto_model); + // do partial inlining status() << "Partial Inlining" << eom; goto_partial_inline(goto_model, get_message_handler()); diff --git a/src/goto-programs/Makefile b/src/goto-programs/Makefile index 4da25537292..2474a7d7e8b 100644 --- a/src/goto-programs/Makefile +++ b/src/goto-programs/Makefile @@ -23,6 +23,7 @@ SRC = basic_blocks.cpp \ goto_program_template.cpp \ goto_trace.cpp \ graphml_witness.cpp \ + instrument_preconditions.cpp \ interpreter.cpp \ interpreter_evaluate.cpp \ json_goto_trace.cpp \ diff --git a/src/goto-programs/instrument_preconditions.cpp b/src/goto-programs/instrument_preconditions.cpp new file mode 100644 index 00000000000..f3d020ddad9 --- /dev/null +++ b/src/goto-programs/instrument_preconditions.cpp @@ -0,0 +1,148 @@ +/*******************************************************************\ + +Module: Move preconditions of a function + to the call-site of the function + +Author: Daniel Kroening + +Date: September 2017 + +\*******************************************************************/ + +#include "instrument_preconditions.h" + +#include + +std::vector get_preconditions( + const symbol_exprt &function, + const goto_functionst &goto_functions) +{ + const irep_idt &identifier=function.get_identifier(); + + auto f_it=goto_functions.function_map.find(identifier); + if(f_it==goto_functions.function_map.end()) + return {}; + + const auto &body=f_it->second.body; + + std::vector result; + + for(auto i_it=body.instructions.begin(); + i_it!=body.instructions.end(); + i_it++) + { + if(i_it->is_location() || + i_it->is_skip()) + continue; // ignore + + if(i_it->is_assert() && + i_it->source_location.get_property_class()==ID_precondition) + result.push_back(i_it); + else + break; // preconditions must be at the front + } + + return result; +} + +void remove_preconditions(goto_programt &goto_program) +{ + for(auto &instruction : goto_program.instructions) + { + if(instruction.is_location() || + instruction.is_skip()) + continue; // ignore + + if(instruction.is_assert() && + instruction.source_location.get_property_class()==ID_precondition) + instruction.type=LOCATION; + else + break; // preconditions must be at the front + } +} + +replace_symbolt actuals_replace_map( + const code_function_callt &call, + const namespacet &ns) +{ + PRECONDITION(call.function().id()==ID_symbol); + const symbolt &s=ns.lookup(to_symbol_expr(call.function())); + const auto &code_type=to_code_type(s.type); + const auto ¶meters=code_type.parameters(); + const auto &arguments=call.arguments(); + + replace_symbolt result; + std::size_t count=0; + for(const auto &p : parameters) + { + if(p.get_identifier()!=irep_idt() && + arguments.size()>count) + { + exprt a=arguments[count]; + if(a.type()!=p.type()) + a=typecast_exprt(a, p.type()); + symbol_exprt s(p.get_identifier(), p.type()); + result.insert(s, a); + } + count++; + } + + return result; +} + +void instrument_preconditions( + const goto_modelt &goto_model, + goto_programt &goto_program) +{ + const namespacet ns(goto_model.symbol_table); + + for(auto it=goto_program.instructions.begin(); + it!=goto_program.instructions.end(); + it++) + { + if(it->is_function_call()) + { + // does the function we call have preconditions? + const auto &call=to_code_function_call(it->code); + + if(call.function().id()==ID_symbol) + { + auto preconditions= + get_preconditions(to_symbol_expr(call.function()), + goto_model.goto_functions); + + source_locationt source_location=it->source_location; + irep_idt function=it->function; + + replace_symbolt r=actuals_replace_map(call, ns); + + // add before the call, with location of the call + for(const auto &p : preconditions) + { + goto_program.insert_before_swap(it); + exprt instance=p->guard; + r(instance); + it->make_assertion(instance); + it->function=function; + it->source_location=source_location; + it->source_location.set_property_class(ID_precondition_instance); + it->source_location.set_comment(p->source_location.get_comment()); + it++; + } + } + } + } +} + +void instrument_preconditions(goto_modelt &goto_model) +{ + // add at call site + for(auto &f_it : goto_model.goto_functions.function_map) + instrument_preconditions( + goto_model, + f_it.second.body); + + // now remove the preconditions + for(auto &f_it : goto_model.goto_functions.function_map) + remove_preconditions(f_it.second.body); +} diff --git a/src/goto-programs/instrument_preconditions.h b/src/goto-programs/instrument_preconditions.h new file mode 100644 index 00000000000..b73d10965e2 --- /dev/null +++ b/src/goto-programs/instrument_preconditions.h @@ -0,0 +1,19 @@ +/*******************************************************************\ + +Module: Move preconditions of a function + to the call-site of the function + +Author: Daniel Kroening + +Date: September 2017 + +\*******************************************************************/ + +#ifndef CPROVER_GOTO_PROGRAMS_INSTRUMENT_PRECONDITIONS_H +#define CPROVER_GOTO_PROGRAMS_INSTRUMENT_PRECONDITIONS_H + +#include + +void instrument_preconditions(goto_modelt &); + +#endif // CPROVER_GOTO_PROGRAMS_INSTRUMENT_PRECONDITIONS_H diff --git a/src/util/irep_ids.def b/src/util/irep_ids.def index 92afdfd3e4a..cb8e1c89dd3 100644 --- a/src/util/irep_ids.def +++ b/src/util/irep_ids.def @@ -91,6 +91,7 @@ IREP_ID_ONE(assume) IREP_ID_ONE(assert) IREP_ID_ONE(assertion) IREP_ID_ONE(precondition) +IREP_ID_ONE(precondition_instance) IREP_ID_ONE(goto) IREP_ID_ONE(gcc_computed_goto) IREP_ID_ONE(ifthenelse) From f443b1815e34bbec2b51fe14d732ba41d92010b7 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Thu, 7 Sep 2017 14:40:21 +0100 Subject: [PATCH 3/9] partial inlining is no longer needed --- src/cbmc/cbmc_parse_options.cpp | 4 ---- src/goto-programs/set_properties.cpp | 3 +-- 2 files changed, 1 insertion(+), 6 deletions(-) diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp index 224d71b658e..aa2736cb862 100644 --- a/src/cbmc/cbmc_parse_options.cpp +++ b/src/cbmc/cbmc_parse_options.cpp @@ -784,10 +784,6 @@ bool cbmc_parse_optionst::process_goto_program( // instrument library preconditions instrument_preconditions(goto_model); - // do partial inlining - status() << "Partial Inlining" << eom; - goto_partial_inline(goto_model, get_message_handler()); - // remove returns, gcc vectors, complex remove_returns(goto_model); remove_vector(goto_model); diff --git a/src/goto-programs/set_properties.cpp b/src/goto-programs/set_properties.cpp index 5861d8d2fda..43c9ea9107c 100644 --- a/src/goto-programs/set_properties.cpp +++ b/src/goto-programs/set_properties.cpp @@ -122,8 +122,7 @@ void label_properties(goto_functionst &goto_functions) it=goto_functions.function_map.begin(); it!=goto_functions.function_map.end(); it++) - if(!it->second.is_inlined()) - label_properties(it->second.body, property_counters); + label_properties(it->second.body, property_counters); } void make_assertions_false(goto_modelt &goto_model) From 3a4ebebdf20999178eb45c10c89a78a39cced98e Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Thu, 7 Sep 2017 14:50:40 +0100 Subject: [PATCH 4/9] use preconditions in the library --- src/ansi-c/library/stdlib.c | 11 +++++------ 1 file changed, 5 insertions(+), 6 deletions(-) diff --git a/src/ansi-c/library/stdlib.c b/src/ansi-c/library/stdlib.c index 493c9a74ef8..b0c9c1f3e6c 100644 --- a/src/ansi-c/library/stdlib.c +++ b/src/ansi-c/library/stdlib.c @@ -145,14 +145,13 @@ inline void free(void *ptr) { __CPROVER_HIDE:; // If ptr is NULL, no operation is performed. + __CPROVER_precondition(ptr==0 || __CPROVER_DYNAMIC_OBJECT(ptr), + "free argument must be dynamic object"); + __CPROVER_precondition(ptr==0 || __CPROVER_POINTER_OFFSET(ptr)==0, + "free argument has offset zero"); + if(ptr!=0) { - // is it dynamic? - __CPROVER_assert(__CPROVER_DYNAMIC_OBJECT(ptr), - "free argument is dynamic object"); - __CPROVER_assert(__CPROVER_POINTER_OFFSET(ptr)==0, - "free argument has offset zero"); - // catch double free if(__CPROVER_deallocated==ptr) __CPROVER_assert(0, "double free"); From 4cb72b3d3e568f30920c7809c334bc18f1fe6421 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Thu, 7 Sep 2017 16:39:54 +0100 Subject: [PATCH 5/9] check error message in test --- regression/cbmc/Free2/test.desc | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/regression/cbmc/Free2/test.desc b/regression/cbmc/Free2/test.desc index 950f6791fef..caab5ef644d 100644 --- a/regression/cbmc/Free2/test.desc +++ b/regression/cbmc/Free2/test.desc @@ -1,8 +1,10 @@ CORE main.c ---pointer-check + ^EXIT=10$ ^SIGNAL=0$ +^.*free argument must be dynamic object: FAILURE$ +^.*free argument has offset zero: SUCCESS$ ^VERIFICATION FAILED$ -- ^warning: ignoring From ac022e27ba02aa3b76621d1193397adc16055c9b Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Sat, 9 Sep 2017 18:27:04 +0100 Subject: [PATCH 6/9] inlined functions are no longer ignored when doing coverage --- regression/cbmc-cover/inlining1/main.c | 2 ++ regression/cbmc-cover/inlining1/test.desc | 8 ++++---- src/cbmc/bmc_cover.cpp | 2 -- 3 files changed, 6 insertions(+), 6 deletions(-) diff --git a/regression/cbmc-cover/inlining1/main.c b/regression/cbmc-cover/inlining1/main.c index c15b715bc76..ac37bc65f27 100644 --- a/regression/cbmc-cover/inlining1/main.c +++ b/regression/cbmc-cover/inlining1/main.c @@ -1,3 +1,5 @@ +// Discussion point: is the branch below one goal or two? + inline void my_func(int x) { if(x) diff --git a/regression/cbmc-cover/inlining1/test.desc b/regression/cbmc-cover/inlining1/test.desc index 1c2f5cff9fb..f9f0e95caa0 100644 --- a/regression/cbmc-cover/inlining1/test.desc +++ b/regression/cbmc-cover/inlining1/test.desc @@ -3,9 +3,9 @@ main.c --cover branch ^EXIT=0$ ^SIGNAL=0$ -^\[my_func.coverage.1\] file main.c line 3 function my_func block 1 branch false: SATISFIED$ -^\[my_func.coverage.2\] file main.c line 3 function my_func block 1 branch true: FAILED$ -^\[my_func.coverage.3\] file main.c line 3 function my_func block 2 branch false: FAILED$ -^\[my_func.coverage.4\] file main.c line 3 function my_func block 2 branch true: SATISFIED$ +^\[main.coverage.1\] file main.c line 13 function main entry point: SATISFIED$ +^\[my_func.coverage.1\] file main.c line 5 function my_func entry point: SATISFIED$ +^\[my_func.coverage.2\] file main.c line 5 function my_func block 1 branch false: SATISFIED$ +^\[my_func.coverage.3\] file main.c line 5 function my_func block 1 branch true: SATISFIED$ -- ^warning: ignoring diff --git a/src/cbmc/bmc_cover.cpp b/src/cbmc/bmc_cover.cpp index c0ad5465c6a..bc772e59608 100644 --- a/src/cbmc/bmc_cover.cpp +++ b/src/cbmc/bmc_cover.cpp @@ -204,8 +204,6 @@ bool bmc_covert::operator()() // This maps property IDs to 'goalt' forall_goto_functions(f_it, goto_functions) { - // Functions are already inlined. - if(f_it->second.is_inlined()) continue; forall_goto_program_instructions(i_it, f_it->second.body) { if(i_it->is_assert()) From 1ff6bf25228e63677be3f24e2dda82736c5c898c Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Sat, 9 Sep 2017 18:28:30 +0100 Subject: [PATCH 7/9] missing include --- regression/cbmc-cover/built-ins1/main.c | 5 ++++- regression/cbmc-cover/built-ins4/main.c | 2 ++ regression/cbmc-cover/built-ins5/main.c | 2 ++ regression/cbmc-cover/built-ins6/main.c | 2 ++ regression/cbmc-cover/built-ins7/main.c | 2 ++ 5 files changed, 12 insertions(+), 1 deletion(-) diff --git a/regression/cbmc-cover/built-ins1/main.c b/regression/cbmc-cover/built-ins1/main.c index 2822ea8e7b2..dceca3a443b 100644 --- a/regression/cbmc-cover/built-ins1/main.c +++ b/regression/cbmc-cover/built-ins1/main.c @@ -1,9 +1,11 @@ +#include + int main() { char a[10]; __CPROVER_input("a[3]", a[3]); - int len = strlen(a); + int len=strlen(a); if(len==3) { @@ -13,5 +15,6 @@ int main() { return -1; } + return 1; } diff --git a/regression/cbmc-cover/built-ins4/main.c b/regression/cbmc-cover/built-ins4/main.c index 2822ea8e7b2..06ea031a2e4 100644 --- a/regression/cbmc-cover/built-ins4/main.c +++ b/regression/cbmc-cover/built-ins4/main.c @@ -1,3 +1,5 @@ +#include + int main() { char a[10]; diff --git a/regression/cbmc-cover/built-ins5/main.c b/regression/cbmc-cover/built-ins5/main.c index 2822ea8e7b2..06ea031a2e4 100644 --- a/regression/cbmc-cover/built-ins5/main.c +++ b/regression/cbmc-cover/built-ins5/main.c @@ -1,3 +1,5 @@ +#include + int main() { char a[10]; diff --git a/regression/cbmc-cover/built-ins6/main.c b/regression/cbmc-cover/built-ins6/main.c index 2822ea8e7b2..06ea031a2e4 100644 --- a/regression/cbmc-cover/built-ins6/main.c +++ b/regression/cbmc-cover/built-ins6/main.c @@ -1,3 +1,5 @@ +#include + int main() { char a[10]; diff --git a/regression/cbmc-cover/built-ins7/main.c b/regression/cbmc-cover/built-ins7/main.c index 2822ea8e7b2..06ea031a2e4 100644 --- a/regression/cbmc-cover/built-ins7/main.c +++ b/regression/cbmc-cover/built-ins7/main.c @@ -1,3 +1,5 @@ +#include + int main() { char a[10]; From e3f75d3147bb1687fa47338d70a72a9a394af4b9 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Sat, 9 Sep 2017 18:28:47 +0100 Subject: [PATCH 8/9] fixup coverage tests --- regression/cbmc-cover/branch3/test.desc | 3 ++- regression/cbmc-cover/built-ins1/test.desc | 2 +- regression/cbmc-cover/built-ins3/main.c | 2 ++ regression/cbmc-cover/built-ins3/test.desc | 2 +- regression/cbmc-cover/inlining1/test.desc | 2 +- 5 files changed, 7 insertions(+), 4 deletions(-) diff --git a/regression/cbmc-cover/branch3/test.desc b/regression/cbmc-cover/branch3/test.desc index 057b9d56a31..9226cc75866 100644 --- a/regression/cbmc-cover/branch3/test.desc +++ b/regression/cbmc-cover/branch3/test.desc @@ -3,6 +3,7 @@ main.c --cover branch --unwind 6 ^EXIT=0$ ^SIGNAL=0$ -^\*\* .* of .* covered \(100.0%\)$ +^\*\* .* of .* covered \(.*\)$ -- ^warning: ignoring +^\[main.coverage.*\] file main.c line .* function main block .* branch .*: FAILED$ diff --git a/regression/cbmc-cover/built-ins1/test.desc b/regression/cbmc-cover/built-ins1/test.desc index 49b517629f3..d80a20e49ef 100644 --- a/regression/cbmc-cover/built-ins1/test.desc +++ b/regression/cbmc-cover/built-ins1/test.desc @@ -3,7 +3,7 @@ main.c --cover location --unwind 1 ^EXIT=0$ ^SIGNAL=0$ -^\*\* 4 of 7 covered +^\*\* 5 of 8 covered -- ^warning: ignoring ^\[.* Date: Tue, 12 Sep 2017 15:23:37 +0100 Subject: [PATCH 9/9] goto-instrument no longer needs partial inlining by default --- .../goto_instrument_parse_options.cpp | 18 +----------------- 1 file changed, 1 insertion(+), 17 deletions(-) diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp index 397dfc10536..90dc6240b77 100644 --- a/src/goto-instrument/goto_instrument_parse_options.cpp +++ b/src/goto-instrument/goto_instrument_parse_options.cpp @@ -259,7 +259,6 @@ int goto_instrument_parse_optionst::doit() if(cmdline.isset("show-value-sets")) { do_indirect_call_and_rtti_removal(); - do_partial_inlining(); // recalculate numbers, etc. goto_model.goto_functions.update(); @@ -275,7 +274,6 @@ int goto_instrument_parse_optionst::doit() if(cmdline.isset("show-global-may-alias")) { do_indirect_call_and_rtti_removal(); - do_partial_inlining(); do_remove_returns(); parameter_assignments(goto_model); @@ -292,7 +290,6 @@ int goto_instrument_parse_optionst::doit() if(cmdline.isset("show-local-bitvector-analysis")) { do_indirect_call_and_rtti_removal(); - do_partial_inlining(); parameter_assignments(goto_model); // recalculate numbers, etc. @@ -316,7 +313,6 @@ int goto_instrument_parse_optionst::doit() if(cmdline.isset("show-custom-bitvector-analysis")) { do_indirect_call_and_rtti_removal(); - do_partial_inlining(); do_remove_returns(); parameter_assignments(goto_model); @@ -341,7 +337,6 @@ int goto_instrument_parse_optionst::doit() if(cmdline.isset("show-escape-analysis")) { do_indirect_call_and_rtti_removal(); - do_partial_inlining(); do_remove_returns(); parameter_assignments(goto_model); @@ -358,7 +353,6 @@ int goto_instrument_parse_optionst::doit() if(cmdline.isset("custom-bitvector-analysis")) { do_indirect_call_and_rtti_removal(); - do_partial_inlining(); do_remove_returns(); parameter_assignments(goto_model); @@ -388,7 +382,6 @@ int goto_instrument_parse_optionst::doit() if(cmdline.isset("show-points-to")) { do_indirect_call_and_rtti_removal(); - do_partial_inlining(); // recalculate numbers, etc. goto_model.goto_functions.update(); @@ -405,7 +398,6 @@ int goto_instrument_parse_optionst::doit() if(cmdline.isset("show-intervals")) { do_indirect_call_and_rtti_removal(); - do_partial_inlining(); // recalculate numbers, etc. goto_model.goto_functions.update(); @@ -434,7 +426,6 @@ int goto_instrument_parse_optionst::doit() if(cmdline.isset("list-calls-args")) { do_indirect_call_and_rtti_removal(); - do_partial_inlining(); list_calls_and_arguments(goto_model); @@ -448,7 +439,6 @@ int goto_instrument_parse_optionst::doit() if(!cmdline.isset("inline")) { do_indirect_call_and_rtti_removal(); - do_partial_inlining(); // recalculate numbers, etc. goto_model.goto_functions.update(); @@ -977,8 +967,6 @@ void goto_instrument_parse_optionst::instrument_goto_program() if(cmdline.isset("show-custom-bitvector-analysis") || cmdline.isset("custom-bitvector-analysis")) { - do_partial_inlining(); - status() << "Propagating Constants" << eom; constant_propagator_ait constant_propagator_ai(goto_model); remove_skip(goto_model); @@ -987,7 +975,6 @@ void goto_instrument_parse_optionst::instrument_goto_program() if(cmdline.isset("escape-analysis")) { do_indirect_call_and_rtti_removal(); - do_partial_inlining(); do_remove_returns(); parameter_assignments(goto_model); @@ -1082,9 +1069,7 @@ void goto_instrument_parse_optionst::instrument_goto_program() if(cmdline.isset("partial-inline")) { do_indirect_call_and_rtti_removal(); - - status() << "Partial inlining" << eom; - goto_partial_inline(goto_model, get_message_handler(), true); + do_partial_inlining(); goto_model.goto_functions.update(); goto_model.goto_functions.compute_loop_numbers(); @@ -1172,7 +1157,6 @@ void goto_instrument_parse_optionst::instrument_goto_program() cmdline.isset("concurrency")) { do_indirect_call_and_rtti_removal(); - do_partial_inlining(); status() << "Pointer Analysis" << eom; value_set_analysist value_set_analysis(ns);