Extends ansi_c_declarationt to include accessors for assigns clauses

Author: feliperodri

src/ansi-c/ansi_c_declaration.h

@@ -244,6 +244,21 @@ class ansi_c_declarationt:public exprt
     assert(!declarators().empty());
     declarators().back().value().swap(value);
   }
+
+  const exprt &spec_assigns() const
+  {
+    return static_cast<const exprt &>(find(ID_C_spec_assigns));
+  }
+
+  const exprt &spec_requires() const
+  {
+    return static_cast<const exprt &>(find(ID_C_spec_requires));
+  }
+
+  const exprt &spec_ensures() const
+  {
+    return static_cast<const exprt &>(find(ID_C_spec_ensures));
+  }
 };
 
 inline ansi_c_declarationt &to_ansi_c_declaration(exprt &expr)

src/ansi-c/c_typecheck_base.cpp

@@ -645,17 +645,14 @@ void c_typecheck_baset::typecheck_declaration(
     irept contract;
 
     {
-      exprt spec_assigns=
-        static_cast<const exprt&>(declaration.find(ID_C_spec_assigns));
+      exprt spec_assigns = declaration.spec_assigns();
       contract.add(ID_C_spec_assigns).swap(spec_assigns);
 
-      exprt spec_requires=
-        static_cast<const exprt&>(declaration.find(ID_C_spec_requires));
-      contract.add(ID_C_spec_requires).swap(spec_requires);
-
-      exprt spec_ensures=
-        static_cast<const exprt&>(declaration.find(ID_C_spec_ensures));
+      exprt spec_ensures = declaration.spec_ensures();
       contract.add(ID_C_spec_ensures).swap(spec_ensures);
+
+      exprt spec_requires = declaration.spec_requires();
+      contract.add(ID_C_spec_requires).swap(spec_requires);
     }
 
     // Now do declarators, if any.