Flag that lists functions to inline #60
Labels
enhancement
New feature or request
good first issue
Good for newcomers
WP
Involves the Weakest Precondition computation
Currently, the inline flag (
--wp-inline
) will inline all of the function calls. We should have a flag that lists which functions we want to inline, ex:--wp-inline-funcs=food,bar,baz
.When the
inline
flag is set, thewp
plugin creates aninline_env
which passes inspec_inline
as the default function spec: https://github.com/draperlaboratory/cbat_tools/blob/master/wp/lib/bap_wp/src/precondition.ml#L464-L475When the environment is created, it initializes a handler for each sub in the program. If the subroutine doesn't match the prerequisites for
spec_verifier_error
,spec_verifier_assume
, orspec_verifier_nondet
, it will be mapped tospec_inline
as seen in https://github.com/draperlaboratory/cbat_tools/blob/master/wp/lib/bap_wp/src/environment.ml#L114-L122At this point, we can specify exactly which functions we want to be inlined and map other specs to the remaining functions.
BAP flags can be set in the
wp.ml
plugin file: https://github.com/draperlaboratory/cbat_tools/blob/master/wp/plugin/wp.ml#L142-L161The text was updated successfully, but these errors were encountered: