Merge pull request #4322 from diffblue/introduce_code_bodyt

introduce code_bodyt

Author: tautschnig

src/util/irep_ids.def

@@ -721,6 +721,7 @@ IREP_ID_TWO(C_quoted, #quoted)
 IREP_ID_ONE(to_member)
 IREP_ID_ONE(pointer_to_member)
 IREP_ID_ONE(tuple)
+IREP_ID_ONE(function_body)
 
 // Projects depending on this code base that wish to extend the list of
 // available ids should provide a file local_irep_ids.def in their source tree

src/util/std_code.cpp

@@ -145,3 +145,25 @@ code_blockt create_fatal_assertion(
 
   return result;
 }
+
+std::vector<irep_idt> code_function_bodyt::get_parameter_identifiers() const
+{
+  const auto &sub = find(ID_parameters).get_sub();
+  std::vector<irep_idt> result;
+  result.reserve(sub.size());
+  for(const auto &s : sub)
+    result.push_back(s.get(ID_identifier));
+  return result;
+}
+
+void code_function_bodyt::set_parameter_identifiers(
+  const std::vector<irep_idt> &parameter_identifiers)
+{
+  auto &sub = add(ID_parameters).get_sub();
+  sub.reserve(parameter_identifiers.size());
+  for(const auto &id : parameter_identifiers)
+  {
+    sub.push_back(irept(ID_parameter));
+    sub.back().set(ID_identifier, id);
+  }
+}

src/util/std_code.h

@@ -2490,4 +2490,54 @@ inline code_try_catcht &to_code_try_catch(codet &code)
   return static_cast<code_try_catcht &>(code);
 }
 
+/// This class is used to interface between a language frontend
+/// and goto-convert -- it communicates the identifiers of the parameters
+/// of a function or method
+class code_function_bodyt : public codet
+{
+public:
+  explicit code_function_bodyt(
+    const std::vector<irep_idt> &parameter_identifiers,
+    code_blockt _block)
+    : codet(ID_function_body, {std::move(_block)})
+  {
+    set_parameter_identifiers(parameter_identifiers);
+  }
+
+  code_blockt &block()
+  {
+    return to_code_block(to_code(op0()));
+  }
+
+  const code_blockt &block() const
+  {
+    return to_code_block(to_code(op0()));
+  }
+
+  std::vector<irep_idt> get_parameter_identifiers() const;
+  void set_parameter_identifiers(const std::vector<irep_idt> &);
+
+protected:
+  using codet::op0;
+  using codet::op1;
+  using codet::op2;
+  using codet::op3;
+};
+
+inline const code_function_bodyt &to_code_function_body(const codet &code)
+{
+  PRECONDITION(code.get_statement() == ID_function_body);
+  DATA_INVARIANT(
+    code.operands().size() == 1, "code_function_body must have one operand");
+  return static_cast<const code_function_bodyt &>(code);
+}
+
+inline code_function_bodyt &to_code_function_body(codet &code)
+{
+  PRECONDITION(code.get_statement() == ID_function_body);
+  DATA_INVARIANT(
+    code.operands().size() == 1, "code_function_body must have one operand");
+  return static_cast<code_function_bodyt &>(code);
+}
+
 #endif // CPROVER_UTIL_STD_CODE_H