user_func_spec sometimes picks the wrong input/output vars for the summary

[codyroux]

In WP, user_func_spec (

cbat_tools/wp/lib/bap_wp/src/precondition.ml

Line 1298 in 8891fde

let sub_inputs : Var.t list = vars_from_sub env sub |> Var.Set.to_list in

) uses the vars_from_sub heuristic to pick both the inputs and outputs of its arguments.

This is already a bit fishy: why should the inputs and outputs be the same?

Second of all: it's often the case that the user knows what the "actual" affected registers are.

Probably the right solution is to extract the variables init_R?? and R?? from the sub_pre and sub_post strings, and use them as the inputs and outputs, respectively.