Replace requires with c_requires

src/ansi-c/ansi_c_convert_type.cpp

@@ -250,29 +250,29 @@ void ansi_c_convert_typet::read_rec(const typet &type)
   {
     const exprt &as_expr =
       static_cast<const exprt &>(static_cast<const irept &>(type));
-    requires.push_back(to_unary_expr(as_expr).op());
+    c_requires.push_back(to_unary_expr(as_expr).op());
   }
   else if(type.id() == ID_C_spec_assigns)
   {
     const exprt &as_expr =
       static_cast<const exprt &>(static_cast<const irept &>(type));
 
     for(const exprt &target : to_unary_expr(as_expr).op().operands())
-      assigns.push_back(target);
+      c_assigns.push_back(target);
   }
   else if(type.id() == ID_C_spec_frees)
   {
     const exprt &as_expr =
       static_cast<const exprt &>(static_cast<const irept &>(type));
 
     for(const exprt &target : to_unary_expr(as_expr).op().operands())
-      frees.push_back(target);
+      c_frees.push_back(target);
   }
   else if(type.id() == ID_C_spec_ensures)
   {
     const exprt &as_expr =
       static_cast<const exprt &>(static_cast<const irept &>(type));
-    ensures.push_back(to_unary_expr(as_expr).op());
+    c_ensures.push_back(to_unary_expr(as_expr).op());
   }
   else
     other.push_back(type);
@@ -322,17 +322,17 @@ void ansi_c_convert_typet::write(typet &type)
     type.swap(other.front());
 
     // the contract expressions are meant for function types only
-    if(!requires.empty())
-      to_code_with_contract_type(type).requires() = std::move(requires);
+    if(!c_requires.empty())
+      to_code_with_contract_type(type).c_requires() = std::move(c_requires);
 
-    if(!assigns.empty())
-      to_code_with_contract_type(type).assigns() = std::move(assigns);
+    if(!c_assigns.empty())
+      to_code_with_contract_type(type).c_assigns() = std::move(c_assigns);
 
-    if(!frees.empty())
-      to_code_with_contract_type(type).frees() = std::move(frees);
+    if(!c_frees.empty())
+      to_code_with_contract_type(type).c_frees() = std::move(c_frees);
 
-    if(!ensures.empty())
-      to_code_with_contract_type(type).ensures() = std::move(ensures);
+    if(!c_ensures.empty())
+      to_code_with_contract_type(type).c_ensures() = std::move(c_ensures);
 
     if(constructor || destructor)
     {

src/ansi-c/ansi_c_convert_type.h

@@ -48,7 +48,7 @@ class ansi_c_convert_typet
   bool constructor, destructor;
 
   // contracts
-  exprt::operandst assigns, frees, ensures, requires;
+  exprt::operandst c_assigns, c_frees, c_ensures, c_requires;
 
   // storage spec
   c_storage_spect c_storage_spec;

src/ansi-c/c_typecheck_base.cpp

@@ -905,20 +905,20 @@ void c_typecheck_baset::typecheck_declaration(
             parameter_identifier, p.type());
         }
 
-        for(auto &requires : code_type.requires())
+        for(auto &c_requires : code_type.c_requires())
         {
-          typecheck_expr(requires);
-          implicit_typecast_bool(requires);
+          typecheck_expr(c_requires);
+          implicit_typecast_bool(c_requires);
           std::string clause_type = "preconditions";
-          check_history_expr_return_value(requires, clause_type);
-          check_was_freed(requires, clause_type);
-          lambda_exprt lambda{temporary_parameter_symbols, requires};
-          lambda.add_source_location() = requires.source_location();
-          requires.swap(lambda);
+          check_history_expr_return_value(c_requires, clause_type);
+          check_was_freed(c_requires, clause_type);
+          lambda_exprt lambda{temporary_parameter_symbols, c_requires};
+          lambda.add_source_location() = c_requires.source_location();
+          c_requires.swap(lambda);
         }
 
-        typecheck_spec_assigns(code_type.assigns());
-        for(auto &assigns : code_type.assigns())
+        typecheck_spec_assigns(code_type.c_assigns());
+        for(auto &assigns : code_type.c_assigns())
         {
           std::string clause_type = "assigns clauses";
           check_history_expr_return_value(assigns, clause_type);
@@ -927,15 +927,15 @@ void c_typecheck_baset::typecheck_declaration(
           assigns.swap(lambda);
         }
 
-        typecheck_spec_frees(code_type.frees());
-        for(auto &frees : code_type.frees())
+        typecheck_spec_frees(code_type.c_frees());
+        for(auto &frees : code_type.c_frees())
         {
           lambda_exprt lambda{temporary_parameter_symbols, frees};
           lambda.add_source_location() = frees.source_location();
           frees.swap(lambda);
         }
 
-        for(auto &ensures : code_type.ensures())
+        for(auto &ensures : code_type.c_ensures())
         {
           typecheck_expr(ensures);
           implicit_typecast_bool(ensures);

src/cprover/instrument_contracts.cpp

@@ -286,11 +286,11 @@ void instrument_contract_checks(
   goto_programt add_at_beginning;
 
   // precondition?
-  if(!contract.requires().empty())
+  if(!contract.c_requires().empty())
   {
     // stick these in as assumptions, preserving the ordering
     goto_programt dest;
-    for(auto &assumption : contract.requires())
+    for(auto &assumption : contract.c_requires())
     {
       exprt assumption_instance = instantiate_contract_lambda(assumption);
       auto fixed_assumption = add_function(f.first, assumption_instance);
@@ -304,19 +304,19 @@ void instrument_contract_checks(
   const auto old_prefix = "old::" + id2string(f.first);
 
   // postcondition?
-  if(!contract.ensures().empty())
+  if(!contract.c_ensures().empty())
   {
     // Stick the postconditions in as assertions at the end
     auto last = body.instructions.end();
     if(std::prev(last)->is_end_function())
       last = std::prev(last);
 
-    for(auto &assertion : contract.ensures())
+    for(auto &assertion : contract.c_ensures())
     {
       exprt assertion_instance = instantiate_contract_lambda(assertion);
 
       std::string comment = "postcondition";
-      if(contract.ensures().size() >= 2)
+      if(contract.c_ensures().size() >= 2)
         comment += " " + expr2text(assertion_instance, ns);
 
       auto location = assertion.source_location();
@@ -338,8 +338,8 @@ void instrument_contract_checks(
 
   // do 'old' in the body
   if(
-    !contract.assigns().empty() || !contract.requires().empty() ||
-    !contract.ensures().empty())
+    !contract.c_assigns().empty() || !contract.c_requires().empty() ||
+    !contract.c_ensures().empty())
   {
     for(auto &instruction : body.instructions)
       instruction.transform(
@@ -359,8 +359,8 @@ void instrument_contract_checks(
 
   // assigns?
   if(
-    !contract.assigns().empty() || !contract.requires().empty() ||
-    !contract.ensures().empty())
+    !contract.c_assigns().empty() || !contract.c_requires().empty() ||
+    !contract.c_ensures().empty())
   {
     for(auto it = body.instructions.begin(); it != body.instructions.end();
         it++)
@@ -378,7 +378,7 @@ void instrument_contract_checks(
 
         // maybe not ok
         auto assigns_assertion =
-          make_assigns_assertion(f.first, contract.assigns(), lhs);
+          make_assigns_assertion(f.first, contract.c_assigns(), lhs);
         auto location = it->source_location();
         location.set_property_class("assigns");
         location.set_comment("assigns clause");
@@ -449,7 +449,7 @@ void replace_function_calls_by_contracts(
         goto_programt dest;
 
         // assert the preconditions
-        for(auto &precondition : contract.requires())
+        for(auto &precondition : contract.c_requires())
         {
           auto instantiated_precondition =
             instantiate_contract_lambda(precondition);
@@ -468,7 +468,7 @@ void replace_function_calls_by_contracts(
         }
 
         // havoc the 'assigned' variables
-        for(auto &assigns_clause_lambda : contract.assigns())
+        for(auto &assigns_clause_lambda : contract.c_assigns())
         {
           auto location = it->source_location();
 
@@ -519,7 +519,7 @@ void replace_function_calls_by_contracts(
         }
 
         // assume the postconditions
-        for(auto &postcondition : contract.ensures())
+        for(auto &postcondition : contract.c_ensures())
         {
           auto &location = it->source_location();
 

src/goto-instrument/contracts/contracts.cpp

@@ -629,7 +629,9 @@ void code_contractst::apply_function_contract(
       // If the function does return a value, but the return value is
       // disregarded, check if the postcondition includes the return value.
       if(std::any_of(
-           type.ensures().begin(), type.ensures().end(), [](const exprt &e) {
+           type.c_ensures().begin(),
+           type.c_ensures().end(),
+           [](const exprt &e) {
              return has_symbol_expr(
                to_lambda_expr(e).where(), CPROVER_PREFIX "return_value", true);
            }))
@@ -674,7 +676,7 @@ void code_contractst::apply_function_contract(
   is_fresh.add_memory_map_decl(new_program);
 
   // Generate: assert(requires)
-  for(const auto &clause : type.requires())
+  for(const auto &clause : type.c_requires())
   {
     auto instantiated_clause =
       to_lambda_expr(clause).application(instantiation_values);
@@ -690,16 +692,16 @@ void code_contractst::apply_function_contract(
       converter,
       instantiated_clause,
       mode,
-      [&is_fresh](goto_programt &requires) {
-        is_fresh.update_requires(requires);
+      [&is_fresh](goto_programt &c_requires) {
+        is_fresh.update_requires(c_requires);
       },
       new_program,
       _location);
   }
 
   // Generate all the instructions required to initialize history variables
   exprt::operandst instantiated_ensures_clauses;
-  for(auto clause : type.ensures())
+  for(auto clause : type.c_ensures())
   {
     auto instantiated_clause =
       to_lambda_expr(clause).application(instantiation_values);
@@ -712,7 +714,7 @@ void code_contractst::apply_function_contract(
   // ASSIGNS clause should not refer to any quantified variables,
   // and only refer to the common symbols to be replaced.
   exprt::operandst targets;
-  for(auto &target : type.assigns())
+  for(auto &target : type.c_assigns())
     targets.push_back(to_lambda_expr(target).application(instantiation_values));
 
   // Create a sequence of non-deterministic assignments ...
@@ -1138,7 +1140,7 @@ void code_contractst::check_frame_conditions_function(const irep_idt &function)
     instantiation_values.push_back(
       ns.lookup(param.get_identifier()).symbol_expr());
   }
-  for(auto &target : get_contract(function, ns).assigns())
+  for(auto &target : get_contract(function, ns).c_assigns())
   {
     goto_programt payload;
     instrument_spec_assigns.track_spec_target(
@@ -1299,7 +1301,7 @@ void code_contractst::add_contract_check(
   visitor.add_memory_map_decl(check);
 
   // Generate: assume(requires)
-  for(const auto &clause : code_type.requires())
+  for(const auto &clause : code_type.c_requires())
   {
     auto instantiated_clause =
       to_lambda_expr(clause).application(instantiation_values);
@@ -1318,16 +1320,16 @@ void code_contractst::add_contract_check(
       converter,
       instantiated_clause,
       function_symbol.mode,
-      [&visitor](goto_programt &requires) {
-        visitor.update_requires(requires);
+      [&visitor](goto_programt &c_requires) {
+        visitor.update_requires(c_requires);
       },
       check,
       _location);
   }
 
   // Generate all the instructions required to initialize history variables
   exprt::operandst instantiated_ensures_clauses;
-  for(auto clause : code_type.ensures())
+  for(auto clause : code_type.c_ensures())
   {
     auto instantiated_clause =
       to_lambda_expr(clause).application(instantiation_values);

src/goto-instrument/contracts/dynamic-frames/dfcc_contract_functions.cpp

@@ -150,7 +150,7 @@ void dfcc_contract_functionst::gen_spec_assigns_function()
 
   exprt::operandst targets;
 
-  for(const exprt &target : code_with_contract.assigns())
+  for(const exprt &target : code_with_contract.c_assigns())
   {
     auto new_target = to_lambda_expr(target).application(lambda_parameters);
     new_target.add_source_location() = target.source_location();
@@ -201,7 +201,7 @@ void dfcc_contract_functionst::gen_spec_frees_function()
 
   exprt::operandst targets;
 
-  for(const exprt &target : code_with_contract.frees())
+  for(const exprt &target : code_with_contract.c_frees())
   {
     auto new_target = to_lambda_expr(target).application(lambda_parameters);
     new_target.add_source_location() = target.source_location();

src/goto-instrument/contracts/dynamic-frames/dfcc_contract_functions.h

@@ -42,16 +42,16 @@ class conditional_target_group_exprt;
 /// ```c
 /// // Populates write_set_to_fill with targets of the assigns clause
 /// // checks its own body against write_set_to_check:
-/// void contract_id::assigns(
+/// void contract_id::c_assigns(
 ///     function-params,
 ///     write_set_to_fill,
 ///     write_set_to_check);
 /// ```
 ///
 /// ```c
 /// // Havocs the targets specified in the assigns clause, assuming
-/// // write_set_to_havoc is a snapshot created using contract_id::assigns
-/// void contract_id::assigns::havoc(write_set_to_havoc);
+/// // write_set_to_havoc is a snapshot created using contract_id::c_assigns
+/// void contract_id::c_assigns::havoc(write_set_to_havoc);
 /// ```
 ///
 /// ```c
@@ -89,10 +89,10 @@ class dfcc_contract_functionst
   void instrument_without_loop_contracts_check_no_pointer_contracts(
     const irep_idt &spec_function_id);
 
-  /// Returns the contract::assigns function symbol
+  /// Returns the contract::c_assigns function symbol
   const symbolt &get_spec_assigns_function_symbol() const;
 
-  /// Returns the contract::assigns::havoc function symbol
+  /// Returns the contract::c_assigns::havoc function symbol
   const symbolt &get_spec_assigns_havoc_function_symbol() const;
 
   /// Returns the contract::frees function symbol
@@ -110,10 +110,10 @@ class dfcc_contract_functionst
   /// The code_with_contract_type carrying the contract clauses
   const code_with_contract_typet &code_with_contract;
 
-  /// Identifier of the contract::assigns function
+  /// Identifier of the contract::c_assigns function
   const irep_idt spec_assigns_function_id;
 
-  /// Identifier of the contract::assigns::havoc function
+  /// Identifier of the contract::c_assigns::havoc function
   const irep_idt spec_assigns_havoc_function_id;
 
   /// Identifier of the contract::frees function

src/goto-instrument/contracts/dynamic-frames/dfcc_wrapper_program.cpp

@@ -577,7 +577,7 @@ void dfcc_wrapper_programt::encode_requires_clauses()
   goto_programt requires_program;
 
   // translate each requires clause
-  for(const auto &r : contract_code_type.requires())
+  for(const auto &r : contract_code_type.c_requires())
   {
     exprt requires = to_lambda_expr(r).application(contract_lambda_parameters);
     requires.add_source_location() = r.source_location();
@@ -621,7 +621,7 @@ void dfcc_wrapper_programt::encode_ensures_clauses()
   goto_programt ensures_program;
 
   // translate each ensures clause
-  for(const auto &e : contract_code_type.ensures())
+  for(const auto &e : contract_code_type.c_ensures())
   {
     exprt ensures = to_lambda_expr(e)
                       .application(contract_lambda_parameters)

src/goto-instrument/contracts/dynamic-frames/dfcc_wrapper_program.h

@@ -224,7 +224,7 @@ class dfcc_wrapper_programt
   /// (populated by calling functions provided in contract_functions)
   /// - Adds declaration of write set and pointer to write set to \ref preamble
   /// - Adds initialisation function call in \ref write_set_checks
-  /// - Adds contract::assigns and contract::frees function call
+  /// - Adds contract::c_assigns and contract::frees function call
   /// in \ref write_set_checks
   /// - Adds release function call in \ref postamble
   void encode_contract_write_set();