Replace containment -> inclusion throughout

Author: SaswatPadhi

src/goto-instrument/contracts/contracts.cpp

@@ -637,7 +637,7 @@ void code_contractst::instrument_assign_statement(
     "The first instruction of instrument_assign_statement should always be"
     " an assignment");
 
-  add_containment_check(
+  add_inclusion_check(
     program, assigns_clause, instruction_it, instruction_it->assign_lhs());
 }
 
@@ -678,7 +678,7 @@ void code_contractst::instrument_call_statement(
   }
   else if(callee_name == "free")
   {
-    add_containment_check(
+    add_inclusion_check(
       body,
       assigns,
       instruction_it,
@@ -846,12 +846,12 @@ void code_contractst::check_frame_conditions(
     {
       const exprt &havoc_argument = dereference_exprt(
         to_typecast_expr(instruction_it->get_other().operands().front()).op());
-      add_containment_check(body, assigns, instruction_it, havoc_argument);
+      add_inclusion_check(body, assigns, instruction_it, havoc_argument);
     }
   }
 }
 
-void code_contractst::add_containment_check(
+void code_contractst::add_inclusion_check(
   goto_programt &program,
   const assigns_clauset &assigns,
   goto_programt::instructionst::iterator &instruction_it,

src/goto-instrument/contracts/contracts.h

@@ -134,7 +134,7 @@ class code_contractst
 
   /// Inserts an assertion into the goto program to ensure that
   /// an expression is within the assignable memory frame.
-  void add_containment_check(
+  void add_inclusion_check(
     goto_programt &,
     const assigns_clauset &,
     goto_programt::instructionst::iterator &,
@@ -144,19 +144,17 @@ class code_contractst
   /// a goto statement that jumps back.
   bool check_for_looped_mallocs(const goto_programt &program);
 
-  /// Inserts an assertion statement into program before the assignment
+  /// Inserts an assertion into program immediately before the assignment
   /// instruction_it, to ensure that the left-hand-side of the assignment
-  /// aliases some expression in original_references, unless it is contained
-  /// in freely assignable set.
+  /// is "included" in the (conditional address ranges in the) write set.
   void instrument_assign_statement(
     goto_programt::instructionst::iterator &,
     goto_programt &,
     assigns_clauset &);
 
-  /// Inserts an assertion statement into program before the function call at
-  /// ins_it, to ensure that any memory which may be written by the call is
-  /// aliased by some expression in assigns_references, unless it is contained
-  /// in freely assignable set.
+  /// Inserts an assertion into program immediately before the function call at
+  /// instruction_it, to ensure that all memory locations written to by the
+  // callee are "included" in the (conditional address ranges in the) write set.
   void instrument_call_statement(
     goto_programt::instructionst::iterator &,
     const irep_idt &,