Skip to content

Commit 1c79841

Browse files
smowtonpeterschrammel
authored andcommitted
Add static analysis hook for unavailable functions
This enables a subclass to supply behaviour when a function isn't loaded (i.e. its value is nil), rather than always ignore such callsites.
1 parent 09937e4 commit 1c79841

File tree

2 files changed

+9
-2
lines changed

2 files changed

+9
-2
lines changed

src/analyses/static_analysis.cpp

+6-2
Original file line numberDiff line numberDiff line change
@@ -422,8 +422,12 @@ void static_analysis_baset::do_function_call(
422422
{
423423
const goto_functionst::goto_functiont &goto_function=f_it->second;
424424

425-
if(!goto_function.body_available())
426-
return; // do nothing
425+
if((!goto_function.body_available()) || !should_enter_function(f_it->first))
426+
{
427+
// Per default do nothing, but a subclass might transform across the stubbed callsite.
428+
transform_function_stub(f_it->first,new_state,l_call,l_return);
429+
return;
430+
}
427431

428432
assert(!goto_function.body.instructions.empty());
429433

src/analyses/static_analysis.h

+3
Original file line numberDiff line numberDiff line change
@@ -244,6 +244,9 @@ class static_analysis_baset
244244
const exprt::operandst &arguments,
245245
statet &new_state);
246246

247+
virtual bool should_enter_function(const irep_idt&) { return true; }
248+
virtual void transform_function_stub(const irep_idt&, statet& state, locationt l_call, locationt l_return) {}
249+
247250
// abstract methods
248251

249252
virtual void generate_state(locationt l)=0;

0 commit comments

Comments
 (0)