diff --git a/regression/goto-instrument/generate-function-body-existing-body/main.c b/regression/goto-instrument/generate-function-body-existing-body/main.c new file mode 100644 index 00000000000..81c7d4283af --- /dev/null +++ b/regression/goto-instrument/generate-function-body-existing-body/main.c @@ -0,0 +1,13 @@ +int generate_my_body(); + +int replace_my_body() +{ + return 1; +} + +int main(void) +{ + generate_my_body(); + replace_my_body(); + return 0; +} diff --git a/regression/goto-instrument/generate-function-body-existing-body/test.desc b/regression/goto-instrument/generate-function-body-existing-body/test.desc new file mode 100644 index 00000000000..4933822e059 --- /dev/null +++ b/regression/goto-instrument/generate-function-body-existing-body/test.desc @@ -0,0 +1,6 @@ +CORE +main.c +--generate-function-body replace_my_body --generate-function-body-options assert-false +^generate function bodies: Function\(s\) matched but already have bodies +^EXIT=10$ +^SIGNAL=0$ diff --git a/regression/goto-instrument/generate-function-body-mixed/main.c b/regression/goto-instrument/generate-function-body-mixed/main.c new file mode 100644 index 00000000000..ab46711eb0a --- /dev/null +++ b/regression/goto-instrument/generate-function-body-mixed/main.c @@ -0,0 +1,15 @@ +#include + +void generate_me(); + +void already_has_body() +{ + assert(0); +} + +int main(void) +{ + generate_me(); + already_has_body(); + return 0; +} diff --git a/regression/goto-instrument/generate-function-body-mixed/test.desc b/regression/goto-instrument/generate-function-body-mixed/test.desc new file mode 100644 index 00000000000..6d7785968d6 --- /dev/null +++ b/regression/goto-instrument/generate-function-body-mixed/test.desc @@ -0,0 +1,7 @@ +CORE +main.c +--generate-function-body '[ag].*' --generate-function-body-options assert-false +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +^\[generate_me.assertion.1\] .* undefined function should be unreachable: FAILURE$ diff --git a/regression/goto-instrument/generate-function-body-no-match/main.c b/regression/goto-instrument/generate-function-body-no-match/main.c new file mode 100644 index 00000000000..a9f4a190555 --- /dev/null +++ b/regression/goto-instrument/generate-function-body-no-match/main.c @@ -0,0 +1,10 @@ +int some_function() +{ + return 1; +} + +int main(void) +{ + some_function(); + return 0; +} diff --git a/regression/goto-instrument/generate-function-body-no-match/test.desc b/regression/goto-instrument/generate-function-body-no-match/test.desc new file mode 100644 index 00000000000..676e236f83f --- /dev/null +++ b/regression/goto-instrument/generate-function-body-no-match/test.desc @@ -0,0 +1,6 @@ +CORE +main.c +--generate-function-body nonexistent_function --generate-function-body-options assert-false +^generate function bodies: No function name matched regex +^EXIT=0$ +^SIGNAL=0$ diff --git a/src/goto-instrument/generate_function_bodies.cpp b/src/goto-instrument/generate_function_bodies.cpp index 7639ebe78e4..8212478f2a3 100644 --- a/src/goto-instrument/generate_function_bodies.cpp +++ b/src/goto-instrument/generate_function_bodies.cpp @@ -510,30 +510,46 @@ void generate_function_bodies( messaget messages(message_handler); const std::regex cprover_prefix = std::regex("__CPROVER.*"); bool did_generate_body = false; + bool matched_function_with_body = false; for(auto &function : model.goto_functions.function_map) { - if( - !function.second.body_available() && - std::regex_match(id2string(function.first), functions_regex)) + if(std::regex_match(id2string(function.first), functions_regex)) { - if(std::regex_match(id2string(function.first), cprover_prefix)) + if(!function.second.body_available()) { - messages.warning() << "generate function bodies: matched function '" - << id2string(function.first) - << "' begins with __CPROVER " - << "the generated body for this function " - << "may interfere with analysis" << messaget::eom; + if(std::regex_match(id2string(function.first), cprover_prefix)) + { + messages.warning() + << "generate function bodies: matched function '" + << id2string(function.first) << "' begins with __CPROVER " + << "the generated body for this function " + << "may interfere with analysis" << messaget::eom; + } + did_generate_body = true; + generate_function_body.generate_function_body( + function.second, model.symbol_table, function.first); + } + else + { + matched_function_with_body = true; } - did_generate_body = true; - generate_function_body.generate_function_body( - function.second, model.symbol_table, function.first); } } if(!did_generate_body && !ignore_no_match) { - messages.warning() - << "generate function bodies: No function name matched regex" - << messaget::eom; + if(matched_function_with_body) + { + messages.warning() + << "generate function bodies: Function(s) matched but already have " + << "bodies (body generation is only performed for functions without " + << "existing bodies)" << messaget::eom; + } + else + { + messages.warning() + << "generate function bodies: No function name matched regex" + << messaget::eom; + } } } diff --git a/src/goto-instrument/generate_function_bodies.h b/src/goto-instrument/generate_function_bodies.h index 7d1ed12266e..11014c7d06f 100644 --- a/src/goto-instrument/generate_function_bodies.h +++ b/src/goto-instrument/generate_function_bodies.h @@ -92,7 +92,8 @@ void generate_function_bodies( #define HELP_REPLACE_FUNCTION_BODY \ " {y--generate-function-body} {uregex} \t " \ - "generate bodies for functions matching {uregex}\n" \ + "generate bodies for functions matching {uregex} that do not already " \ + "have bodies\n" \ " {y--generate-havocing-body}