This PR extends the function name map to work with function calls.
At a function call site in the modified binary, looks up the mapped function name in the environment. If no name is found, we assume that the function has the same name as the original. (Rewrites modified names to original names.)
Renames the field in the environment from consts to call_preds. At a call site, we add the predicate to this field. When Z3 prints out the model, we can see the results of each function predicate. This does not print predicates of the array sort.
This PR extends the function name map to work with function calls.
consts
tocall_preds
. At a call site, we add the predicate to this field. When Z3 prints out the model, we can see the results of each function predicate. This does not print predicates of thearray
sort.