source_lines.h

Go to the documentation of this file.

/*******************************************************************\
 
Module: Source Lines
 
Author: Mark R. Tuttle
 
\*******************************************************************/


 
#ifndef CPROVER_GOTO_INSTRUMENT_SOURCE_LINES_H
#define CPROVER_GOTO_INSTRUMENT_SOURCE_LINES_H
 
#include <util/irep.h>
#include <util/mp_arith.h>
 
#include <map>
#include <set>
#include <string>
 
class source_locationt;
 
class source_linest
{
public:
  source_linest() = default;
  explicit source_linest(const source_locationt &loc)
  {
    insert(loc);
  }

  void insert(const source_locationt &loc);

  std::string to_string() const;

  irept to_irep() const;
 
private:
  using linest = std::set<mp_integer>;
  using function_linest = std::map<std::string, linest>;
  using block_linest = std::map<std::string, function_linest>;
 
  block_linest block_lines;
};
 
#endif // CPROVER_GOTO_INSTRUMENT_SOURCE_LINES_H