goto_symex_fault_localizer.h

Go to the documentation of this file.

/*******************************************************************\
 
Module: Fault Localization for Goto Symex
 
Author: Peter Schrammel
 
\*******************************************************************/

 
#ifndef CPROVER_GOTO_CHECKER_GOTO_SYMEX_FAULT_LOCALIZER_H
#define CPROVER_GOTO_CHECKER_GOTO_SYMEX_FAULT_LOCALIZER_H
 
#include <util/threeval.h>
 
#include "fault_localization_provider.h"
 
class optionst;
class stack_decision_proceduret;
class symex_target_equationt;
class SSA_stept;
class ui_message_handlert;
 
class goto_symex_fault_localizert
{
public:
  goto_symex_fault_localizert(
    const optionst &options,
    ui_message_handlert &ui_message_handler,
    const symex_target_equationt &equation,
    stack_decision_proceduret &solver);
 
  fault_location_infot operator()(const irep_idt &failed_property_id);
 
protected:
  const optionst &options;
  ui_message_handlert &ui_message_handler;
  const symex_target_equationt &equation;
  stack_decision_proceduret &solver;

  typedef std::map<exprt, fault_location_infot::score_mapt::iterator>
    localization_pointst;

  const SSA_stept &collect_guards(
    const irep_idt &failed_property_id,
    localization_pointst &localization_points,
    fault_location_infot &fault_location);
 
  // specify a localization point combination to check
  typedef std::vector<tvt> localization_points_valuet;
  bool check(
    const SSA_stept &failed_step,
    const localization_pointst &,
    const localization_points_valuet &);
 
  void update_scores(const localization_pointst &);
 
  // localization method: flip each point
  void
  localize_linear(const SSA_stept &failed_step, const localization_pointst &);
};
 
#endif // CPROVER_GOTO_CHECKER_GOTO_SYMEX_FAULT_LOCALIZER_H