havoc_assigns_clause_targets.h

Go to the documentation of this file.

/*******************************************************************\
 
Module: Havoc multiple and possibly dependent targets simultaneously
 
Author: Remi Delmas, delmasrd@amazon.com
 
\*******************************************************************/
 
 
#ifndef CPROVER_GOTO_INSTRUMENT_CONTRACTS_HAVOC_ASSIGNS_CLAUSE_TARGETS_H
#define CPROVER_GOTO_INSTRUMENT_CONTRACTS_HAVOC_ASSIGNS_CLAUSE_TARGETS_H
 
#include "instrument_spec_assigns.h"
#include <util/expr.h>
 
class namespacet;
class symbol_tablet;
class goto_programt;
class goto_functionst;
class message_handlert;
 
class havoc_assigns_clause_targetst : public instrument_spec_assignst
{
public:
  havoc_assigns_clause_targetst(
    const irep_idt &_function_id,
    const std::vector<exprt> &_targets,
    const goto_functionst &_functions,
    cfg_infot &_cfg_info,
    const source_locationt &_source_location,
    symbol_tablet &_st,
    message_handlert &_message_handler)
    : instrument_spec_assignst(
        _function_id,
        _functions,
        _cfg_info,
        _st,
        _message_handler),
      targets(_targets),
      source_location(_source_location)
  {
  }
 
  void get_instructions(goto_programt &dest);
 
private:
  void havoc_if_valid(car_exprt car, goto_programt &dest);
 
  void havoc_static_local(car_exprt car, goto_programt &dest);
 
  const std::vector<exprt> &targets;
  const source_locationt &source_location;
};
#endif // CPROVER_GOTO_INSTRUMENT_CONTRACTS_HAVOC_ASSIGNS_CLAUSE_TARGETS_H