add next_symbol_exprt

Author: Daniel Kroening

src/ansi-c/expr2c.cpp

@@ -1660,7 +1660,7 @@ std::string expr2ct::convert_norep(
 }
 
 std::string expr2ct::convert_symbol(
-  const exprt &src,
+  const symbol_exprt &src,
   unsigned &precedence)
 {
   const irep_idt &id=src.get(ID_identifier);
@@ -1701,6 +1701,14 @@ std::string expr2ct::convert_symbol(
   return dest;
 }
 
+std::string expr2ct::convert_next_symbol(
+  const next_symbol_exprt &src,
+  unsigned &precedence)
+{
+  const irep_idt id=src.get_identifier();
+  return "NEXT("+id2string(id)+")";
+}
+
 std::string expr2ct::convert_nondet_symbol(
   const nondet_symbol_exprt &src,
   unsigned &precedence)
@@ -3844,10 +3852,10 @@ std::string expr2ct::convert_with_precedence(
     return precedence=16, convert_index_designator(src);
 
   else if(src.id()==ID_symbol)
-    return convert_symbol(src, precedence);
+    return convert_symbol(to_symbol_expr(src), precedence);
 
   else if(src.id()==ID_next_symbol)
-    return convert_symbol(src, precedence);
+    return convert_next_symbol(to_next_symbol_expr(src), precedence);
 
   else if(src.id()==ID_nondet_symbol)
     return convert_nondet_symbol(to_nondet_symbol_expr(src), precedence);

src/ansi-c/expr2c_class.h

@@ -223,7 +223,8 @@ class expr2ct
   // NOLINTNEXTLINE(whitespace/line_length)
   std::string convert_statement_expression(const exprt &src, unsigned &precendence);
 
-  virtual std::string convert_symbol(const exprt &src, unsigned &precedence);
+  virtual std::string convert_symbol(const symbol_exprt &src, unsigned &precedence);
+  virtual std::string convert_next_symbol(const next_symbol_exprt &src, unsigned &precedence);
   std::string convert_predicate_symbol(const exprt &src, unsigned &precedence);
   // NOLINTNEXTLINE(whitespace/line_length)
   std::string convert_predicate_next_symbol(const exprt &src, unsigned &precedence);

src/util/std_expr.h

@@ -131,6 +131,95 @@ class symbol_exprt:public exprt
   }
 };
 
+/*! \brief Cast a generic exprt to a \ref symbol_exprt
+ *
+ * This is an unchecked conversion. \a expr must be known to be \ref
+ * symbol_exprt.
+ *
+ * \param expr Source expression
+ * \return Object of type \ref symbol_exprt
+ *
+ * \ingroup gr_std_expr
+*/
+inline const symbol_exprt &to_symbol_expr(const exprt &expr)
+{
+  PRECONDITION(expr.id()==ID_symbol);
+  DATA_INVARIANT(!expr.has_operands(), "Symbols must not have operands");
+  return static_cast<const symbol_exprt &>(expr);
+}
+
+/*! \copydoc to_symbol_expr(const exprt &)
+ * \ingroup gr_std_expr
+*/
+inline symbol_exprt &to_symbol_expr(exprt &expr)
+{
+  PRECONDITION(expr.id()==ID_symbol);
+  DATA_INVARIANT(!expr.has_operands(), "Symbols must not have operands");
+  return static_cast<symbol_exprt &>(expr);
+}
+
+template<> inline bool can_cast_expr<symbol_exprt>(const exprt &base)
+{
+  return base.id()==ID_symbol;
+}
+inline void validate_expr(const symbol_exprt &value)
+{
+  validate_operands(value, 0, "Symbols must not have operands");
+}
+
+/*! \brief Expression to hold a "next state" symbol (variable)
+*/
+class next_symbol_exprt:public symbol_exprt
+{
+public:
+  /*! \brief Constructor
+   * \param identifier Name of symbol
+   * \param  type Type of symbol
+  */
+  next_symbol_exprt(
+    const irep_idt &identifier,
+    const typet &type):symbol_exprt(identifier, type)
+  {
+    id(ID_next_symbol);
+  }
+};
+
+/*! \brief Cast a generic exprt to a \ref next_symbol_exprt
+ *
+ * This is an unchecked conversion. \a expr must be known to be \ref
+ * next_symbol_exprt.
+ *
+ * \param expr Source expression
+ * \return Object of type \ref next_symbol_exprt
+ *
+ * \ingroup gr_std_expr
+*/
+inline const next_symbol_exprt &to_next_symbol_expr(const exprt &expr)
+{
+  PRECONDITION(expr.id()==ID_next_symbol);
+  DATA_INVARIANT(!expr.has_operands(), "Symbols must not have operands");
+  return static_cast<const next_symbol_exprt &>(expr);
+}
+
+/*! \copydoc to_next_symbol_expr(const exprt &)
+ * \ingroup gr_std_expr
+*/
+inline next_symbol_exprt &to_next_symbol_expr(exprt &expr)
+{
+  PRECONDITION(expr.id()==ID_next_symbol);
+  DATA_INVARIANT(!expr.has_operands(), "Symbols must not have operands");
+  return static_cast<next_symbol_exprt &>(expr);
+}
+
+template<> inline bool can_cast_expr<next_symbol_exprt>(const exprt &base)
+{
+  return base.id()==ID_next_symbol;
+}
+inline void validate_expr(const next_symbol_exprt &value)
+{
+  validate_operands(value, 0, "Symbols must not have operands");
+}
+
 /*! \brief Expression to hold a symbol (variable)
 */
 class decorated_symbol_exprt:public symbol_exprt
@@ -197,41 +286,6 @@ class decorated_symbol_exprt:public symbol_exprt
   }
 };
 
-/*! \brief Cast a generic exprt to a \ref symbol_exprt
- *
- * This is an unchecked conversion. \a expr must be known to be \ref
- * symbol_exprt.
- *
- * \param expr Source expression
- * \return Object of type \ref symbol_exprt
- *
- * \ingroup gr_std_expr
-*/
-inline const symbol_exprt &to_symbol_expr(const exprt &expr)
-{
-  PRECONDITION(expr.id()==ID_symbol);
-  DATA_INVARIANT(!expr.has_operands(), "Symbols must not have operands");
-  return static_cast<const symbol_exprt &>(expr);
-}
-
-/*! \copydoc to_symbol_expr(const exprt &)
- * \ingroup gr_std_expr
-*/
-inline symbol_exprt &to_symbol_expr(exprt &expr)
-{
-  PRECONDITION(expr.id()==ID_symbol);
-  DATA_INVARIANT(!expr.has_operands(), "Symbols must not have operands");
-  return static_cast<symbol_exprt &>(expr);
-}
-
-template<> inline bool can_cast_expr<symbol_exprt>(const exprt &base)
-{
-  return base.id()==ID_symbol;
-}
-inline void validate_expr(const symbol_exprt &value)
-{
-  validate_operands(value, 0, "Symbols must not have operands");
-}
 
 
 /*! \brief Expression to hold a nondeterministic choice