CBMC: constant_exprt Class Reference

Public Member Functions

 constant_exprt (const irep_idt &_value, typet _type)   const irep_idtget_value () const   void set_value (const irep_idt &value)   bool is_null_pointer () const  Returns true if expr has a pointer type and a value NULL; it also returns true when expr has value zero and NULL_is_zero is true; returns false in all other cases.
  bool operator== (bool rhs) const  Return whether the expression lhs is a constant of Boolean type that is representing the Boolean value rhs.
  bool operator!= (bool rhs) const  Return whether the expression lhs is not a constant of Boolean type or is not representing the Boolean value rhs.
  bool operator== (int rhs) const  Return whether the expression lhs is a constant of Boolean type that is representing the Boolean value rhs.
  bool operator!= (int rhs) const  Return whether the expression lhs is not a constant of Boolean type or is not representing the Boolean value rhs.
  bool operator== (std::nullptr_t) const  Return whether the expression lhs is a constant representing the NULL pointer.
  bool operator!= (std::nullptr_t) const  Returns the negation of operator==(const exprt &, std::nullptr_t).
  bool operator== (const irept &other) const   bool operator!= (const irept &other) const   - Public Member Functions inherited from nullary_exprt  nullary_exprt (const irep_idt &_id, typet _type)   operandstoperands ()=delete  remove all operand methods
  const operandstoperands () const =delete   const exprtop0 () const =delete   exprtop0 ()=delete   const exprtop1 () const =delete   exprtop1 ()=delete   const exprtop2 () const =delete   exprtop2 ()=delete   const exprtop3 () const =delete   exprtop3 ()=delete   void copy_to_operands (const exprt &expr)=delete   void copy_to_operands (const exprt &, const exprt &)=delete   void copy_to_operands (const exprt &, const exprt &, const exprt &)=delete   - Public Member Functions inherited from exprt  exprt ()    exprt (const irep_idt &_id)    exprt (irep_idt _id, typet _type)    exprt (irep_idt _id, typet _type, operandst &&_operands)    exprt (const irep_idt &id, typet type, source_locationt loc)   typettype ()  Return the type of the expression.
  const typettype () const   bool has_operands () const  Return true if there is at least one operand.
  operandstoperands ()   const operandstoperands () const   exprtwith_source_location (source_locationt location) &  Add the source location from location, if it is non-nil.
  exprt && with_source_location (source_locationt location) &&  Add the source location from location, if it is non-nil.
  exprtwith_source_location (const exprt &other) &  Add the source location from other, if it has any.
  exprt && with_source_location (const exprt &other) &&  Add the source location from other, if it has any.
  void reserve_operands (operandst::size_type n)   void copy_to_operands (const exprt &expr)  Copy the given argument to the end of exprt's operands.
  void add_to_operands (const exprt &expr)  Add the given argument to the end of exprt's operands.
  void add_to_operands (exprt &&expr)  Add the given argument to the end of exprt's operands.
  void add_to_operands (exprt &&e1, exprt &&e2)  Add the given arguments to the end of exprt's operands.
  void add_to_operands (exprt &&e1, exprt &&e2, exprt &&e3)  Add the given arguments to the end of exprt's operands.
  bool is_constant () const  Return whether the expression is a constant.
  bool is_true () const  Return whether the expression is a constant representing true.
  bool is_false () const  Return whether the expression is a constant representing false.
  bool is_zero () const  Return whether the expression is a constant representing 0.
  bool is_one () const  Return whether the expression is a constant representing 1.
  bool is_boolean () const  Return whether the expression represents a Boolean.
  const source_locationtfind_source_location () const  Get a source_locationt from the expression or from its operands (non-recursively).
  const source_locationtsource_location () const   source_locationtadd_source_location ()   void drop_source_location ()   void visit (class expr_visitort &visitor)  These are pre-order traversal visitors, i.e., the visitor is executed on a node before its children have been visited.
  void visit (class const_expr_visitort &visitor) const   void visit_pre (std::function< void(exprt &)>)   void visit_pre (std::function< void(const exprt &)>) const   void visit_post (std::function< void(exprt &)>)  These are post-order traversal visitors, i.e., the visitor is executed on a node after its children have been visited.
  void visit_post (std::function< void(const exprt &)>) const   depth_iteratort depth_begin ()   depth_iteratort depth_end ()   const_depth_iteratort depth_begin () const   const_depth_iteratort depth_end () const   const_depth_iteratort depth_cbegin () const   const_depth_iteratort depth_cend () const   depth_iteratort depth_begin (std::function< exprt &()> mutate_root) const   const_unique_depth_iteratort unique_depth_begin () const   const_unique_depth_iteratort unique_depth_end () const   const_unique_depth_iteratort unique_depth_cbegin () const   const_unique_depth_iteratort unique_depth_cend () const   - Public Member Functions inherited from irept bool is_nil () const   bool is_not_nil () const    irept (const irep_idt &_id)    irept (const irep_idt &_id, const named_subt &_named_sub, const subt &_sub)    irept ()=default   const irep_idtid () const   const std::string & id_string () const   void id (const irep_idt &_data)   const ireptfind (const irep_idt &name) const   ireptadd (const irep_idt &name)   ireptadd (const irep_idt &name, irept irep)   const std::string & get_string (const irep_idt &name) const   const irep_idtget (const irep_idt &name) const   bool get_bool (const irep_idt &name) const   signed int get_int (const irep_idt &name) const   std::size_t get_size_t (const irep_idt &name) const   long long get_long_long (const irep_idt &name) const   void set (const irep_idt &name, const irep_idt &value)   void set (const irep_idt &name, irept irep)   void set (const irep_idt &name, const long long value)   void set_size_t (const irep_idt &name, const std::size_t value)   void remove (const irep_idt &name)   void move_to_sub (irept &irep)   void move_to_named_sub (const irep_idt &name, irept &irep)   bool operator== (const irept &other) const   bool operator!= (const irept &other) const   void swap (irept &irep)   bool operator< (const irept &other) const  defines ordering on the internal representation
  bool ordering (const irept &other) const  defines ordering on the internal representation
  int compare (const irept &i) const  defines ordering on the internal representation comments are ignored
  void clear ()   void make_nil ()   subtget_sub ()   const subtget_sub () const   named_subtget_named_sub ()   const named_subtget_named_sub () const   std::size_t hash () const   std::size_t full_hash () const   bool full_eq (const irept &other) const   std::string pretty (unsigned indent=0, unsigned max_indent=0) const   - Public Member Functions inherited from sharing_treet< irept, forward_list_as_mapt< irep_idt, irept > >  sharing_treet (irep_idt _id)    sharing_treet (irep_idt _id, named_subt _named_sub, subt _sub)    sharing_treet ()    sharing_treet (const sharing_treet &irep)    sharing_treet (sharing_treet &&irep)   sharing_treetoperator= (const sharing_treet &irep)   sharing_treetoperator= (sharing_treet &&irep)    ~sharing_treet ()   const dtread () const   dtwrite ()  

Static Public Member Functions

static void check (const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)   static void validate (const exprt &expr, const namespacet &, const validation_modet vm=validation_modet::INVARIANT)   - Static Public Member Functions inherited from nullary_exprt static void check (const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)   static void validate (const exprt &expr, const namespacet &, const validation_modet vm=validation_modet::INVARIANT)   - Static Public Member Functions inherited from exprt static void check (const exprt &, const validation_modet=validation_modet::INVARIANT)  Check that the expression is well-formed (shallow checks only, i.e., subexpressions and its type are not checked).
  static void validate (const exprt &expr, const namespacet &, const validation_modet vm=validation_modet::INVARIANT)  Check that the expression is well-formed, assuming that its subexpressions and type have all ready been checked for well-formedness.
  static void validate_full (const exprt &expr, const namespacet &ns, const validation_modet vm=validation_modet::INVARIANT)  Check that the expression is well-formed (full check, including checks of all subexpressions and the type)
  - Static Public Member Functions inherited from irept static bool is_comment (const irep_idt &name)   static std::size_t number_of_non_comments (const named_subt &)  count the number of named_sub elements that are not comments
 

Additional Inherited Members

- Public Types inherited from exprt typedef std::vector< exprtoperandst   - Public Types inherited from irept using baset = tree_implementationt   - Public Types inherited from sharing_treet< irept, forward_list_as_mapt< irep_idt, irept > > using dt = tree_nodet< irept, forward_list_as_mapt< irep_idt, irept >, true >   using subt = typename dt::subt   using named_subt = typename dt::named_subt   using tree_implementationt = sharing_treet  Used to refer to this class from derived classes.
  - Static Protected Member Functions inherited from sharing_treet< irept, forward_list_as_mapt< irep_idt, irept > > static void remove_ref (dt *old_data)   static void nonrecursive_destructor (dt *old_data)  Does the same as remove_ref, but using an explicit stack instead of recursion.
  - Protected Attributes inherited from sharing_treet< irept, forward_list_as_mapt< irep_idt, irept > > dtdata   - Static Protected Attributes inherited from sharing_treet< irept, forward_list_as_mapt< irep_idt, irept > > static dt empty_d  

A constant literal expression.

Definition at line 2996 of file std_expr.h.