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, is_macro, is_exported,
       is_input, is_output, is_state_var, is_property;
 
  // ANSI-C
  bool is_static_lifetime, is_thread_local;
  bool is_lvalue, is_file_local, is_extern, is_volatile,
       is_parameter, is_auxiliary, is_weak;
 
  symbolt()
  {
    clear();
  }
 
  void clear()
  {
    type.make_nil();
    value.make_nil();
    location.make_nil();
 
    name=module=base_name=mode=pretty_name=irep_idt();
 
    is_type=is_macro=is_exported=
    is_input=is_output=is_state_var=is_property=
    is_static_lifetime=is_thread_local=
    is_lvalue=is_file_local=is_extern=is_volatile=
    is_parameter=is_auxiliary=is_weak=false;
  }
 
  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:
  explicit type_symbolt(const typet &_type)
  {
    type=_type;
    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, const typet &type):
    auxiliary_symbolt()
  {
    this->name=name;
    this->base_name=name;
    this->type=type;
  }
};
 
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