symbol.h

Go to the documentation of this file.

/*******************************************************************\
 
Module:
 
Author: Daniel Kroening, kroening@kroening.com
 
\*******************************************************************/
 
 
#ifndef CPROVER_UTIL_SYMBOL_H
#define CPROVER_UTIL_SYMBOL_H

 
#include <iosfwd>
 
#include "expr.h"
#include "invariant.h"

class symbolt
{
public:
  typet type;

  exprt value;

  source_locationt location;

  irep_idt name;

  irep_idt module;

  irep_idt base_name;

  irep_idt mode;

  irep_idt pretty_name;

  const irep_idt &display_name() const
  {
    return pretty_name.empty()?name:pretty_name;
  }
 
  // global use
  bool is_type = false;
  bool is_macro = false;
  bool is_exported = false;
  bool is_input = false;
  bool is_output = false;
  bool is_state_var = false;
  bool is_property = false;
 
  // ANSI-C
  bool is_static_lifetime = false;
  bool is_thread_local = false;
  bool is_lvalue = false;
  bool is_file_local = false;
  bool is_extern = false;
  bool is_volatile = false;
  bool is_parameter = false;
  bool is_auxiliary = false;
  bool is_weak = false;
 
  symbolt()
    : type(static_cast<const typet &>(get_nil_irep())),
      value(static_cast<const exprt &>(get_nil_irep())),
      location(source_locationt::nil())
  {
  }
 
  symbolt(const irep_idt &_name, typet _type, const irep_idt &_mode)
    : type(std::move(_type)),
      value(static_cast<const exprt &>(get_nil_irep())),
      location(source_locationt::nil()),
      name(_name),
      mode(_mode)
  {
  }
 
  void swap(symbolt &b);
  void show(std::ostream &out) const;
 
  class symbol_exprt symbol_expr() const;
 
  bool is_shared() const
  {
    return !is_thread_local;
  }
 
  bool is_function() const
  {
    return !is_type && !is_macro && type.id()==ID_code;
  }

  bool is_compiled() const
  {
    return type.id() == ID_code && value == exprt(ID_compiled);
  }

  void set_compiled()
  {
    PRECONDITION(type.id() == ID_code);
    value = exprt(ID_compiled);
  }

  bool is_well_formed() const;
 
  bool operator==(const symbolt &other) const;
  bool operator!=(const symbolt &other) const;
};
 
std::ostream &operator<<(std::ostream &out, const symbolt &symbol);

class type_symbolt:public symbolt
{
public:
  type_symbolt(const irep_idt &_name, typet _type, const irep_idt &_mode)
    : symbolt(_name, _type, _mode)
  {
    is_type = true;
  }
};

class auxiliary_symbolt:public symbolt
{
public:
  auxiliary_symbolt()
  {
    is_lvalue=true;
    is_state_var=true;
    is_thread_local=true;
    is_file_local=true;
    is_auxiliary=true;
  }
 
  auxiliary_symbolt(const irep_idt &name, typet type, const irep_idt &mode)
    : symbolt(name, type, mode)
  {
    is_lvalue = true;
    is_state_var = true;
    is_thread_local = true;
    is_file_local = true;
    is_auxiliary = true;
  }
};

class parameter_symbolt:public symbolt
{
public:
  parameter_symbolt()
  {
    is_lvalue=true;
    is_state_var=true;
    is_thread_local=true;
    is_file_local=true;
    is_parameter=true;
  }
};
 
#endif // CPROVER_UTIL_SYMBOL_H