You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
gets the refuted goals and paths to it as a path object.
Path objects are just maps from tids to bools (branches and the paths they take), which are useful, but hard to read in an output. As a result, Constr.print_refuted_goals and Constr.refuted_goal_to_string discard the path.
However, when stepping trough the counter-example with gdb, it's useful to be able to assess whether we're going down the right path with regards to the counter-model, so having a Constr.refuted_goal_path_to_string would be nice.
This function should include the concrete addresses of the branch, which Ivan tells me can be obtained using Term.get_attr address t. Unfortunately this means tracking terms in addition to their tids, or look up the terms each time using Term.find on the whole subroutine.
The text was updated successfully, but these errors were encountered:
Right now
cbat_tools/wp/lib/bap_wp/src/constraint.mli
Line 100 in 7a8d7c6
Path objects are just maps from
tid
s tobools
(branches and the paths they take), which are useful, but hard to read in an output. As a result,Constr.print_refuted_goals
andConstr.refuted_goal_to_string
discard the path.However, when stepping trough the counter-example with gdb, it's useful to be able to assess whether we're going down the right path with regards to the counter-model, so having a
Constr.refuted_goal_path_to_string
would be nice.This function should include the concrete addresses of the branch, which Ivan tells me can be obtained using
Term.get_attr address t
. Unfortunately this means tracking terms in addition to theirtid
s, or look up the terms each time usingTerm.find
on the whole subroutine.The text was updated successfully, but these errors were encountered: