Introduce ansi-c/c_expr.h

This introduces a new header file, ansi-c/c_expr.h, which is to collect
expressions that are specific to and internal to the C frontend.

Author: kroening

src/ansi-c/c_expr.h

@@ -0,0 +1,157 @@
+/*******************************************************************\
+
+Module: API to expression classes that are internal to the C frontend
+
+Author: Daniel Kroening, [email protected]
+
+\*******************************************************************/
+
+#ifndef CPROVER_ANSI_C_C_EXPR_H
+#define CPROVER_ANSI_C_C_EXPR_H
+
+/// \file ansi-c/c_expr.h
+/// API to expression classes that are internal to the C frontend
+
+#include <util/std_code.h>
+
+/// \ref codet representation of an inline assembler statement.
+class code_asmt:public codet
+{
+public:
+  code_asmt():codet(ID_asm)
+  {
+  }
+
+  explicit code_asmt(exprt expr) : codet(ID_asm, {std::move(expr)})
+  {
+  }
+
+  const irep_idt &get_flavor() const
+  {
+    return get(ID_flavor);
+  }
+
+  void set_flavor(const irep_idt &f)
+  {
+    set(ID_flavor, f);
+  }
+};
+
+template<> inline bool can_cast_expr<code_asmt>(const exprt &base)
+{
+  return detail::can_cast_code_impl(base, ID_asm);
+}
+
+// to_code_asm only checks the code statement, so no validate_expr is
+// provided for code_asmt
+
+inline code_asmt &to_code_asm(codet &code)
+{
+  PRECONDITION(code.get_statement() == ID_asm);
+  return static_cast<code_asmt &>(code);
+}
+
+inline const code_asmt &to_code_asm(const codet &code)
+{
+  PRECONDITION(code.get_statement() == ID_asm);
+  return static_cast<const code_asmt &>(code);
+}
+
+/// \ref codet representation of an inline assembler statement,
+/// for the gcc flavor.
+class code_asm_gcct : public code_asmt
+{
+public:
+  code_asm_gcct()
+  {
+    set_flavor(ID_gcc);
+    operands().resize(5);
+  }
+
+  exprt &asm_text()
+  {
+    return op0();
+  }
+
+  const exprt &asm_text() const
+  {
+    return op0();
+  }
+
+  exprt &outputs()
+  {
+    return op1();
+  }
+
+  const exprt &outputs() const
+  {
+    return op1();
+  }
+
+  exprt &inputs()
+  {
+    return op2();
+  }
+
+  const exprt &inputs() const
+  {
+    return op2();
+  }
+
+  exprt &clobbers()
+  {
+    return op3();
+  }
+
+  const exprt &clobbers() const
+  {
+    return op3();
+  }
+
+  exprt &labels()
+  {
+    return operands()[4];
+  }
+
+  const exprt &labels() const
+  {
+    return operands()[4];
+  }
+
+protected:
+  using code_asmt::op0;
+  using code_asmt::op1;
+  using code_asmt::op2;
+  using code_asmt::op3;
+};
+
+template <>
+inline bool can_cast_expr<code_asm_gcct>(const exprt &base)
+{
+  return detail::can_cast_code_impl(base, ID_asm);
+}
+
+inline void validate_expr(const code_asm_gcct &x)
+{
+  validate_operands(x, 5, "code_asm_gcc must have five operands");
+}
+
+inline code_asm_gcct &to_code_asm_gcc(codet &code)
+{
+  PRECONDITION(code.get_statement() == ID_asm);
+  PRECONDITION(to_code_asm(code).get_flavor() == ID_gcc);
+  code_asm_gcct &ret = static_cast<code_asm_gcct &>(code);
+  validate_expr(ret);
+  return ret;
+}
+
+inline const code_asm_gcct &to_code_asm_gcc(const codet &code)
+{
+  PRECONDITION(code.get_statement() == ID_asm);
+  PRECONDITION(to_code_asm(code).get_flavor() == ID_gcc);
+  const code_asm_gcct &ret = static_cast<const code_asm_gcct &>(code);
+  validate_expr(ret);
+  return ret;
+}
+
+#endif // CPROVER_ANSI_C_C_EXPR_H

src/ansi-c/c_typecheck_base.h

@@ -21,6 +21,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/typecheck.h>
 
 #include "ansi_c_declaration.h"
+#include "c_expr.h"
 #include "designator.h"
 
 class c_typecheck_baset:

src/ansi-c/expr2c.cpp

@@ -32,6 +32,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/suffix.h>
 #include <util/symbol.h>
 
+#include "c_expr.h"
 #include "c_misc.h"
 #include "c_qualifiers.h"
 #include "expr2c_class.h"

src/ansi-c/expr2c_class.h

@@ -22,8 +22,9 @@ Author: Daniel Kroening, [email protected]
 #include <util/std_code.h>
 #include <util/std_expr.h>
 
-class qualifierst;
+class code_asmt;
 class namespacet;
+class qualifierst;
 
 class expr2ct
 {

src/assembler/remove_asm.cpp

@@ -15,6 +15,8 @@ Date:   December 2014
 
 #include "remove_asm.h"
 
+#include <ansi-c/c_expr.h>
+
 #include <util/c_types.h>
 #include <util/pointer_expr.h>
 #include <util/string_constant.h>

src/cpp/parse.cpp

@@ -20,6 +20,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/std_types.h>
 
 #include <ansi-c/ansi_c_y.tab.h>
+#include <ansi-c/c_expr.h>
 #include <ansi-c/merged_type.h>
 
 #include "cpp_token_buffer.h"

src/goto-programs/goto_convert_class.h

@@ -22,6 +22,8 @@ Author: Daniel Kroening, [email protected]
 #include <util/replace_expr.h>
 #include <util/std_code.h>
 
+#include <ansi-c/c_expr.h>
+
 #include "goto_program.h"
 #include "destructor_tree.h"
 

src/util/std_code.h

@@ -1696,146 +1696,6 @@ inline code_continuet &to_code_continue(codet &code)
   return static_cast<code_continuet &>(code);
 }
 
-/// \ref codet representation of an inline assembler statement.
-class code_asmt:public codet
-{
-public:
-  code_asmt():codet(ID_asm)
-  {
-  }
-
-  explicit code_asmt(exprt expr) : codet(ID_asm, {std::move(expr)})
-  {
-  }
-
-  const irep_idt &get_flavor() const
-  {
-    return get(ID_flavor);
-  }
-
-  void set_flavor(const irep_idt &f)
-  {
-    set(ID_flavor, f);
-  }
-};
-
-template<> inline bool can_cast_expr<code_asmt>(const exprt &base)
-{
-  return detail::can_cast_code_impl(base, ID_asm);
-}
-
-// to_code_asm only checks the code statement, so no validate_expr is
-// provided for code_asmt
-
-inline code_asmt &to_code_asm(codet &code)
-{
-  PRECONDITION(code.get_statement() == ID_asm);
-  return static_cast<code_asmt &>(code);
-}
-
-inline const code_asmt &to_code_asm(const codet &code)
-{
-  PRECONDITION(code.get_statement() == ID_asm);
-  return static_cast<const code_asmt &>(code);
-}
-
-/// \ref codet representation of an inline assembler statement,
-/// for the gcc flavor.
-class code_asm_gcct : public code_asmt
-{
-public:
-  code_asm_gcct()
-  {
-    set_flavor(ID_gcc);
-    operands().resize(5);
-  }
-
-  exprt &asm_text()
-  {
-    return op0();
-  }
-
-  const exprt &asm_text() const
-  {
-    return op0();
-  }
-
-  exprt &outputs()
-  {
-    return op1();
-  }
-
-  const exprt &outputs() const
-  {
-    return op1();
-  }
-
-  exprt &inputs()
-  {
-    return op2();
-  }
-
-  const exprt &inputs() const
-  {
-    return op2();
-  }
-
-  exprt &clobbers()
-  {
-    return op3();
-  }
-
-  const exprt &clobbers() const
-  {
-    return op3();
-  }
-
-  exprt &labels()
-  {
-    return operands()[4];
-  }
-
-  const exprt &labels() const
-  {
-    return operands()[4];
-  }
-
-protected:
-  using code_asmt::op0;
-  using code_asmt::op1;
-  using code_asmt::op2;
-  using code_asmt::op3;
-};
-
-template <>
-inline bool can_cast_expr<code_asm_gcct>(const exprt &base)
-{
-  return detail::can_cast_code_impl(base, ID_asm);
-}
-
-inline void validate_expr(const code_asm_gcct &x)
-{
-  validate_operands(x, 5, "code_asm_gcc must have five operands");
-}
-
-inline code_asm_gcct &to_code_asm_gcc(codet &code)
-{
-  PRECONDITION(code.get_statement() == ID_asm);
-  PRECONDITION(to_code_asm(code).get_flavor() == ID_gcc);
-  code_asm_gcct &ret = static_cast<code_asm_gcct &>(code);
-  validate_expr(ret);
-  return ret;
-}
-
-inline const code_asm_gcct &to_code_asm_gcc(const codet &code)
-{
-  PRECONDITION(code.get_statement() == ID_asm);
-  PRECONDITION(to_code_asm(code).get_flavor() == ID_gcc);
-  const code_asm_gcct &ret = static_cast<const code_asm_gcct &>(code);
-  validate_expr(ret);
-  return ret;
-}
-
 /// \ref codet representation of an expression statement.
 /// It has one operand, which is the expression it stores.
 class code_expressiont:public codet