Also prefix assigns, frees, and ensures.

Also adds the "c_" prefix to the assigns, frees, and ensures
for consistency.

Author: TGWDB

src/ansi-c/ansi_c_convert_type.cpp

@@ -326,13 +326,13 @@ void ansi_c_convert_typet::write(typet &type)
       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);
+      to_code_with_contract_type(type).c_assigns() = std::move(assigns);
 
     if(!frees.empty())
-      to_code_with_contract_type(type).frees() = std::move(frees);
+      to_code_with_contract_type(type).c_frees() = std::move(frees);
 
     if(!ensures.empty())
-      to_code_with_contract_type(type).ensures() = std::move(ensures);
+      to_code_with_contract_type(type).c_ensures() = std::move(ensures);
 
     if(constructor || destructor)
     {

src/ansi-c/c_typecheck_base.cpp

@@ -917,8 +917,8 @@ void c_typecheck_baset::typecheck_declaration(
           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

@@ -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.c_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.c_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");
@@ -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);
            }))
@@ -699,7 +701,7 @@ void code_contractst::apply_function_contract(
 
   // 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(
@@ -1327,7 +1329,7 @@ void code_contractst::add_contract_check(
 
   // 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

@@ -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();

src/linking/remove_internal_symbols.cpp

@@ -67,9 +67,9 @@ static void get_symbols(
         to_code_with_contract_type(code_type);
 
       find_symbols_sett new_symbols;
-      for(const exprt &a : maybe_contract.assigns())
+      for(const exprt &a : maybe_contract.c_assigns())
         find_type_and_expr_symbols(a, new_symbols);
-      for(const exprt &e : maybe_contract.ensures())
+      for(const exprt &e : maybe_contract.c_ensures())
         find_type_and_expr_symbols(e, new_symbols);
       for(const exprt &r : maybe_contract.c_requires())
         find_type_and_expr_symbols(r, new_symbols);

src/util/c_types.h

@@ -390,26 +390,26 @@ class code_with_contract_typet : public code_typet
 
   bool has_contract() const
   {
-    return !ensures().empty() || !c_requires().empty() || !assigns().empty() ||
-           !frees().empty();
+    return !c_ensures().empty() || !c_requires().empty() ||
+           !c_assigns().empty() || !c_frees().empty();
   }
 
-  const exprt::operandst &assigns() const
+  const exprt::operandst &c_assigns() const
   {
     return static_cast<const exprt &>(find(ID_C_spec_assigns)).operands();
   }
 
-  exprt::operandst &assigns()
+  exprt::operandst &c_assigns()
   {
     return static_cast<exprt &>(add(ID_C_spec_assigns)).operands();
   }
 
-  const exprt::operandst &frees() const
+  const exprt::operandst &c_frees() const
   {
     return static_cast<const exprt &>(find(ID_C_spec_frees)).operands();
   }
 
-  exprt::operandst &frees()
+  exprt::operandst &c_frees()
   {
     return static_cast<exprt &>(add(ID_C_spec_frees)).operands();
   }
@@ -424,12 +424,12 @@ class code_with_contract_typet : public code_typet
     return static_cast<exprt &>(add(ID_C_spec_requires)).operands();
   }
 
-  const exprt::operandst &ensures() const
+  const exprt::operandst &c_ensures() const
   {
     return static_cast<const exprt &>(find(ID_C_spec_ensures)).operands();
   }
 
-  exprt::operandst &ensures()
+  exprt::operandst &c_ensures()
   {
     return static_cast<exprt &>(add(ID_C_spec_ensures)).operands();
   }