Convert assertions to invariants.

martin · martin · commit 8960b8a63412 · 2018-03-13T18:27:06.000Z
diff --git a/src/analyses/variable-sensitivity/abstract_enviroment.cpp b/src/analyses/variable-sensitivity/abstract_enviroment.cpp
@@ -159,7 +159,7 @@ Function: abstract_environmentt::assign
 bool abstract_environmentt::assign(
   const exprt &expr, const abstract_object_pointert value, const namespacet &ns)
 {
-  assert(value);
+  PRECONDITION(value);
 
   if(value->is_bottom())
   {
@@ -189,7 +189,7 @@ bool abstract_environmentt::assign(
 
   if(!lhs_value)
   {
-    assert(s.id()==ID_symbol);
+    INVARIANT(s.id()==ID_symbol, "Have a symbol or a stack");
     const symbol_exprt &symbol_expr(to_symbol_expr(s));
     if(map.find(symbol_expr)==map.end())
     {
@@ -230,7 +230,7 @@ bool abstract_environmentt::assign(
   const typet &rhs_type=ns.follow(final_value->type());
 
   // Write the value for the root symbol back into the map
-  assert(lhs_type==rhs_type);
+  INVARIANT(lhs_type==rhs_type, "Assignment types must match");
   // If LHS was directly the symbol
   if(s.id()==ID_symbol)
   {
@@ -276,7 +276,7 @@ abstract_object_pointert abstract_environmentt::write(
   const namespacet &ns,
   bool merge_write)
 {
-  assert(!remaining_stack.empty());
+  PRECONDITION(!remaining_stack.empty());
   const exprt & next_expr=remaining_stack.top();
   remaining_stack.pop();
 
@@ -305,7 +305,7 @@ abstract_object_pointert abstract_environmentt::write(
   }
   else
   {
-    assert(0);
+    UNREACHABLE;
     return nullptr;
   }
 }
@@ -332,7 +332,7 @@ bool abstract_environmentt::assume(const exprt &expr, const namespacet &ns)
   // This should be enforced by the well-structured-ness of the
   // goto-program and the way assume is used.
 
-  assert(expr.type().id()==ID_bool);
+  PRECONDITION(expr.type().id()==ID_bool);
 
   // Evaluate the expression
   abstract_object_pointert res = eval(expr, ns);
@@ -342,7 +342,7 @@ bool abstract_environmentt::assume(const exprt &expr, const namespacet &ns)
   if(possibly_constant.id()!=ID_nil)  // I.E. actually a value
   {
     // Should be of the right type
-    assert(possibly_constant.type().id()==ID_bool);
+    INVARIANT(possibly_constant.type().id()==ID_bool, "simplication preserves type");
 
     if(possibly_constant.is_false())
     {
diff --git a/src/analyses/variable-sensitivity/abstract_object.cpp b/src/analyses/variable-sensitivity/abstract_object.cpp
@@ -54,7 +54,7 @@ Function: abstract_objectt::abstract_objectt
 abstract_objectt::abstract_objectt(const typet &type, bool top, bool bottom):
   t(type), bottom(bottom), top(top)
 {
-  assert(!(top && bottom));
+  PRECONDITION(!(top && bottom));
 }
 
 /*******************************************************************\
diff --git a/src/analyses/variable-sensitivity/array_abstract_object.cpp b/src/analyses/variable-sensitivity/array_abstract_object.cpp
@@ -28,7 +28,7 @@ Function: array_abstract_objectt::array_abstract_objectt
 array_abstract_objectt::array_abstract_objectt(const typet &t):
   abstract_objectt(t)
 {
-  assert(t.id()==ID_array);
+  PRECONDITION(t.id()==ID_array);
 }
 
 /*******************************************************************\
@@ -51,7 +51,7 @@ array_abstract_objectt::array_abstract_objectt(
   const typet &t, bool tp, bool bttm):
     abstract_objectt(t, tp, bttm)
 {
-  assert(t.id()==ID_array);
+  PRECONDITION(t.id()==ID_array);
 }
 
 /*******************************************************************\
@@ -75,7 +75,7 @@ array_abstract_objectt::array_abstract_objectt(
   const namespacet &ns):
     abstract_objectt(e, environment, ns)
 {
-  assert(e.type().id()==ID_array);
+  PRECONDITION(e.type().id()==ID_array);
 }
 
 /**
diff --git a/src/analyses/variable-sensitivity/constant_array_abstract_object.cpp b/src/analyses/variable-sensitivity/constant_array_abstract_object.cpp
@@ -154,8 +154,8 @@ abstract_object_pointert constant_array_abstract_objectt::constant_array_merge(
 
       result->map=merged_map;
 
-      assert(!result->is_top());
-      assert(!result->is_bottom());
+      INVARIANT(!result->is_top(), "merge of maps doesn't generate top");
+      INVARIANT(!result->is_bottom(), "merge of maps doesn't generate bottom");
       return result;
     }
   }
@@ -277,7 +277,7 @@ abstract_object_pointert constant_array_abstract_objectt::read_index(
   }
   else
   {
-    assert(!is_bottom());
+    PRECONDITION(!is_bottom());
     mp_integer index_value;
     if(eval_index(index, env, ns, index_value))
     {
diff --git a/src/analyses/variable-sensitivity/constant_pointer_abstract_object.cpp b/src/analyses/variable-sensitivity/constant_pointer_abstract_object.cpp
@@ -31,7 +31,7 @@ constant_pointer_abstract_objectt::constant_pointer_abstract_objectt(
   const typet &t):
     pointer_abstract_objectt(t)
 {
-  assert(t.id()==ID_pointer);
+  PRECONDITION(t.id()==ID_pointer);
 }
 
 /*******************************************************************\
@@ -54,7 +54,7 @@ constant_pointer_abstract_objectt::constant_pointer_abstract_objectt(
   const typet &t, bool tp, bool bttm):
     pointer_abstract_objectt(t, tp, bttm)
 {
-  assert(t.id()==ID_pointer);
+  PRECONDITION(t.id()==ID_pointer);
 }
 
 /*******************************************************************\
@@ -95,7 +95,7 @@ constant_pointer_abstract_objectt::constant_pointer_abstract_objectt(
     pointer_abstract_objectt(e, environment, ns),
     value_stack(e, environment, ns)
 {
-  assert(e.type().id()==ID_pointer);
+  PRECONDITION(e.type().id()==ID_pointer);
   if(value_stack.is_top_value())
   {
     make_top();
@@ -328,7 +328,7 @@ sharing_ptrt<pointer_abstract_objectt>
     if(stack.empty())
     {
       // We should not be changing the type of an abstract object
-      assert(new_value->type()==type().subtype());
+      PRECONDITION(new_value->type()==type().subtype());
 
       // Get an expression that we can assign to
       exprt value=value_stack.to_expression().op0();
diff --git a/src/analyses/variable-sensitivity/full_struct_abstract_object.cpp b/src/analyses/variable-sensitivity/full_struct_abstract_object.cpp
@@ -36,8 +36,8 @@ Function: full_struct_abstract_objectt::struct_abstract_objectt
 full_struct_abstract_objectt::full_struct_abstract_objectt(const typet &t):
   struct_abstract_objectt(t)
 {
-  assert(t.id()==ID_struct);
-  assert(verify());
+  PRECONDITION(t.id()==ID_struct);
+  DATA_INVARIANT(verify(), "Structural invariants maintained");
 }
 
 /*******************************************************************\
@@ -60,8 +60,8 @@ full_struct_abstract_objectt::full_struct_abstract_objectt(
   const typet &t, bool top, bool bottom):
     struct_abstract_objectt(t, top, bottom)
 {
-  assert(t.id()==ID_struct);
-  assert(verify());
+  PRECONDITION(t.id()==ID_struct);
+  DATA_INVARIANT(verify(), "Structural invariants maintained");
 }
 
 /*******************************************************************\
@@ -84,7 +84,7 @@ full_struct_abstract_objectt::full_struct_abstract_objectt(
   const namespacet &ns):
     struct_abstract_objectt(e, environment, ns)
 {
-  assert(verify());
+  DATA_INVARIANT(verify(), "Structural invariants maintained");
 }
 
 /*******************************************************************\
@@ -122,7 +122,7 @@ abstract_object_pointert full_struct_abstract_objectt::read_component(
   }
   else
   {
-    assert(!is_bottom());
+    PRECONDITION(!is_bottom());
 
     irep_idt c=member_expr.get_component_name();
 
@@ -203,7 +203,7 @@ sharing_ptrt<struct_abstract_objectt>
     copy->map[c]=
       environment.write(starting_value, value, stack, ns, merging_write);
     copy->clear_top();
-    assert(copy->verify());
+    DATA_INVARIANT(copy->verify(), "Structural invariants maintained");;
     return copy;
   }
   else
@@ -219,19 +219,19 @@ sharing_ptrt<struct_abstract_objectt>
     {
       if(is_top()) // struct is top
       {
-        assert(copy->verify());
+        DATA_INVARIANT(copy->verify(), "Structural invariants maintained");;
         return copy;
       }
 
-      assert(!copy->map.empty());
+      INVARIANT(!copy->map.empty(), "If not top, map cannot be empty");
 
       struct_mapt &m=copy->map;
 
       struct_mapt::iterator it=m.find(c);
 
       if(it==m.end()) // component is top
       {
-        assert(copy->verify());
+        DATA_INVARIANT(copy->verify(), "Structural invariants maintained");;
         return copy;
       }
 
@@ -243,10 +243,10 @@ sharing_ptrt<struct_abstract_objectt>
     {
       copy->map[c]=value;
       copy->clear_top();
-      assert(!copy->is_bottom());
+      INVARIANT(!copy->is_bottom(), "top != bottom");
     }
 
-    assert(copy->verify());
+    DATA_INVARIANT(copy->verify(), "Structural invariants maintained");;
     return copy;
   }
 }
@@ -367,7 +367,7 @@ abstract_object_pointert full_struct_abstract_objectt::merge_constant_structs(
       abstract_objectt::merge_maps<irep_idt>(map, other->map, merged_map);
     if(!modified)
     {
-      assert(verify());
+      DATA_INVARIANT(verify(), "Structural invariants maintained");
       return shared_from_this();
     }
     else
@@ -378,9 +378,9 @@ abstract_object_pointert full_struct_abstract_objectt::merge_constant_structs(
 
       result->map=merged_map;
 
-      assert(!result->is_top());
-      assert(!result->is_bottom());
-      assert(result->verify());
+      INVARIANT(!result->is_top(), "Merge of maps will not generate top");
+      INVARIANT(!result->is_bottom(), "Merge of maps will not generate bottom");
+      DATA_INVARIANT(result->verify(), "Structural invariants maintained");
       return result;
     }
   }
diff --git a/src/analyses/variable-sensitivity/pointer_abstract_object.cpp b/src/analyses/variable-sensitivity/pointer_abstract_object.cpp
@@ -29,7 +29,7 @@ Function: pointer_abstract_objectt::pointer_abstract_objectt
 pointer_abstract_objectt::pointer_abstract_objectt(const typet &t):
   abstract_objectt(t)
 {
-  assert(t.id()==ID_pointer);
+  PRECONDITION(t.id()==ID_pointer);
 }
 
 /*******************************************************************\
@@ -52,7 +52,7 @@ pointer_abstract_objectt::pointer_abstract_objectt(
   const typet &t, bool tp, bool bttm):
     abstract_objectt(t, tp, bttm)
 {
-  assert(t.id()==ID_pointer);
+  PRECONDITION(t.id()==ID_pointer);
 }
 
 /*******************************************************************\
@@ -74,7 +74,7 @@ pointer_abstract_objectt::pointer_abstract_objectt(
   const namespacet &ns):
     abstract_objectt(e, environment, ns)
 {
-  assert(e.type().id()==ID_pointer);
+  PRECONDITION(e.type().id()==ID_pointer);
 }
 
 /**
diff --git a/src/analyses/variable-sensitivity/struct_abstract_object.cpp b/src/analyses/variable-sensitivity/struct_abstract_object.cpp
@@ -30,7 +30,7 @@ Function: struct_abstract_objectt::struct_abstract_objectt
 struct_abstract_objectt::struct_abstract_objectt(const typet &t):
   abstract_objectt(t)
 {
-  assert(t.id()==ID_struct);
+  PRECONDITION(t.id()==ID_struct);
 }
 
 /*******************************************************************\
@@ -53,7 +53,7 @@ struct_abstract_objectt::struct_abstract_objectt(
   const typet &t, bool tp, bool bttm):
     abstract_objectt(t, tp, bttm)
 {
-  assert(t.id()==ID_struct);
+  PRECONDITION(t.id()==ID_struct);
 }
 
 /*******************************************************************\
@@ -75,7 +75,7 @@ struct_abstract_objectt::struct_abstract_objectt(
   const namespacet &ns):
   abstract_objectt(e, environment, ns)
 {
-  assert(ns.follow(e.type()).id()==ID_struct);
+  PRECONDITION(ns.follow(e.type()).id()==ID_struct);
 }
 
 /**
diff --git a/src/analyses/variable-sensitivity/union_abstract_object.cpp b/src/analyses/variable-sensitivity/union_abstract_object.cpp
@@ -29,7 +29,7 @@ Function: union_abstract_objectt::union_abstract_objectt
 union_abstract_objectt::union_abstract_objectt(const typet &type):
   abstract_objectt(type)
 {
-  assert(type.id()==ID_union);
+  PRECONDITION(type.id()==ID_union);
 }
 
 /*******************************************************************\
@@ -52,7 +52,7 @@ union_abstract_objectt::union_abstract_objectt(
   const typet &type, bool top, bool bottom):
     abstract_objectt(type, top, bottom)
 {
-  assert(type.id()==ID_union);
+  PRECONDITION(type.id()==ID_union);
 }
 
 /*******************************************************************\
@@ -74,7 +74,7 @@ union_abstract_objectt::union_abstract_objectt(
   const namespacet &ns):
     abstract_objectt(expr, environment, ns)
 {
-  assert(ns.follow(expr.type()).id()==ID_union);
+  PRECONDITION(ns.follow(expr.type()).id()==ID_union);
 }
 
 /**
diff --git a/src/analyses/variable-sensitivity/variable_sensitivity_domain.cpp b/src/analyses/variable-sensitivity/variable_sensitivity_domain.cpp
diff --git a/src/analyses/variable-sensitivity/variable_sensitivity_object_factory.h b/src/analyses/variable-sensitivity/variable_sensitivity_object_factory.h

Original file line number	Diff line number	Diff line change
`@@ -159,7 +159,7 @@ Function: abstract_environmentt::assign`
`159`	`159`	`bool abstract_environmentt::assign(`
`160`	`160`	`const exprt &expr, const abstract_object_pointert value, const namespacet &ns)`
`161`	`161`	`{`
`162`		`- assert(value);`
	`162`	`+ PRECONDITION(value);`
`163`	`163`
`164`	`164`	`if(value->is_bottom())`
`165`	`165`	`{`
`@@ -189,7 +189,7 @@ bool abstract_environmentt::assign(`
`189`	`189`
`190`	`190`	`if(!lhs_value)`
`191`	`191`	`{`
`192`		`- assert(s.id()==ID_symbol);`
	`192`	`+ INVARIANT(s.id()==ID_symbol, "Have a symbol or a stack");`
`193`	`193`	`const symbol_exprt &symbol_expr(to_symbol_expr(s));`
`194`	`194`	`if(map.find(symbol_expr)==map.end())`
`195`	`195`	`{`
`@@ -230,7 +230,7 @@ bool abstract_environmentt::assign(`
`230`	`230`	`const typet &rhs_type=ns.follow(final_value->type());`
`231`	`231`
`232`	`232`	`// Write the value for the root symbol back into the map`
`233`		`- assert(lhs_type==rhs_type);`
	`233`	`+ INVARIANT(lhs_type==rhs_type, "Assignment types must match");`
`234`	`234`	`// If LHS was directly the symbol`
`235`	`235`	`if(s.id()==ID_symbol)`
`236`	`236`	`{`
`@@ -276,7 +276,7 @@ abstract_object_pointert abstract_environmentt::write(`
`276`	`276`	`const namespacet &ns,`
`277`	`277`	`bool merge_write)`
`278`	`278`	`{`
`279`		`- assert(!remaining_stack.empty());`
	`279`	`+ PRECONDITION(!remaining_stack.empty());`
`280`	`280`	`const exprt & next_expr=remaining_stack.top();`
`281`	`281`	`remaining_stack.pop();`
`282`	`282`
`@@ -305,7 +305,7 @@ abstract_object_pointert abstract_environmentt::write(`
`305`	`305`	`}`
`306`	`306`	`else`
`307`	`307`	`{`
`308`		`- assert(0);`
	`308`	`+ UNREACHABLE;`
`309`	`309`	`return nullptr;`
`310`	`310`	`}`
`311`	`311`	`}`
`@@ -332,7 +332,7 @@ bool abstract_environmentt::assume(const exprt &expr, const namespacet &ns)`
`332`	`332`	`// This should be enforced by the well-structured-ness of the`
`333`	`333`	`// goto-program and the way assume is used.`
`334`	`334`
`335`		`- assert(expr.type().id()==ID_bool);`
	`335`	`+ PRECONDITION(expr.type().id()==ID_bool);`
`336`	`336`
`337`	`337`	`// Evaluate the expression`
`338`	`338`	`abstract_object_pointert res = eval(expr, ns);`
`@@ -342,7 +342,7 @@ bool abstract_environmentt::assume(const exprt &expr, const namespacet &ns)`
`342`	`342`	`if(possibly_constant.id()!=ID_nil) // I.E. actually a value`
`343`	`343`	`{`
`344`	`344`	`// Should be of the right type`
`345`		`- assert(possibly_constant.type().id()==ID_bool);`
	`345`	`+ INVARIANT(possibly_constant.type().id()==ID_bool, "simplication preserves type");`
`346`	`346`
`347`	`347`	`if(possibly_constant.is_false())`
`348`	`348`	`{`
Original file line number	Diff line number	Diff line change
`@@ -54,7 +54,7 @@ Function: abstract_objectt::abstract_objectt`
`54`	`54`	`abstract_objectt::abstract_objectt(const typet &type, bool top, bool bottom):`
`55`	`55`	`t(type), bottom(bottom), top(top)`
`56`	`56`	`{`
`57`		`- assert(!(top && bottom));`
	`57`	`+ PRECONDITION(!(top && bottom));`
`58`	`58`	`}`
`59`	`59`
`60`	`60`	`/*******************************************************************\`
Original file line number	Diff line number	Diff line change
`@@ -28,7 +28,7 @@ Function: array_abstract_objectt::array_abstract_objectt`
`28`	`28`	`array_abstract_objectt::array_abstract_objectt(const typet &t):`
`29`	`29`	`abstract_objectt(t)`
`30`	`30`	`{`
`31`		`- assert(t.id()==ID_array);`
	`31`	`+ PRECONDITION(t.id()==ID_array);`
`32`	`32`	`}`
`33`	`33`
`34`	`34`	`/*******************************************************************\`
`@@ -51,7 +51,7 @@ array_abstract_objectt::array_abstract_objectt(`
`51`	`51`	`const typet &t, bool tp, bool bttm):`
`52`	`52`	`abstract_objectt(t, tp, bttm)`
`53`	`53`	`{`
`54`		`- assert(t.id()==ID_array);`
	`54`	`+ PRECONDITION(t.id()==ID_array);`
`55`	`55`	`}`
`56`	`56`
`57`	`57`	`/*******************************************************************\`
`@@ -75,7 +75,7 @@ array_abstract_objectt::array_abstract_objectt(`
`75`	`75`	`const namespacet &ns):`
`76`	`76`	`abstract_objectt(e, environment, ns)`
`77`	`77`	`{`
`78`		`- assert(e.type().id()==ID_array);`
	`78`	`+ PRECONDITION(e.type().id()==ID_array);`
`79`	`79`	`}`
`80`	`80`
`81`	`81`	`/**`
Original file line number	Diff line number	Diff line change
`@@ -154,8 +154,8 @@ abstract_object_pointert constant_array_abstract_objectt::constant_array_merge(`
`154`	`154`
`155`	`155`	`result->map=merged_map;`
`156`	`156`
`157`		`- assert(!result->is_top());`
`158`		`- assert(!result->is_bottom());`
	`157`	`+ INVARIANT(!result->is_top(), "merge of maps doesn't generate top");`
	`158`	`+ INVARIANT(!result->is_bottom(), "merge of maps doesn't generate bottom");`
`159`	`159`	`return result;`
`160`	`160`	`}`
`161`	`161`	`}`
`@@ -277,7 +277,7 @@ abstract_object_pointert constant_array_abstract_objectt::read_index(`
`277`	`277`	`}`
`278`	`278`	`else`
`279`	`279`	`{`
`280`		`- assert(!is_bottom());`
	`280`	`+ PRECONDITION(!is_bottom());`
`281`	`281`	`mp_integer index_value;`
`282`	`282`	`if(eval_index(index, env, ns, index_value))`
`283`	`283`	`{`
Original file line number	Diff line number	Diff line change
`@@ -31,7 +31,7 @@ constant_pointer_abstract_objectt::constant_pointer_abstract_objectt(`
`31`	`31`	`const typet &t):`
`32`	`32`	`pointer_abstract_objectt(t)`
`33`	`33`	`{`
`34`		`- assert(t.id()==ID_pointer);`
	`34`	`+ PRECONDITION(t.id()==ID_pointer);`
`35`	`35`	`}`
`36`	`36`
`37`	`37`	`/*******************************************************************\`
`@@ -54,7 +54,7 @@ constant_pointer_abstract_objectt::constant_pointer_abstract_objectt(`
`54`	`54`	`const typet &t, bool tp, bool bttm):`
`55`	`55`	`pointer_abstract_objectt(t, tp, bttm)`
`56`	`56`	`{`
`57`		`- assert(t.id()==ID_pointer);`
	`57`	`+ PRECONDITION(t.id()==ID_pointer);`
`58`	`58`	`}`
`59`	`59`
`60`	`60`	`/*******************************************************************\`
`@@ -95,7 +95,7 @@ constant_pointer_abstract_objectt::constant_pointer_abstract_objectt(`
`95`	`95`	`pointer_abstract_objectt(e, environment, ns),`
`96`	`96`	`value_stack(e, environment, ns)`
`97`	`97`	`{`
`98`		`- assert(e.type().id()==ID_pointer);`
	`98`	`+ PRECONDITION(e.type().id()==ID_pointer);`
`99`	`99`	`if(value_stack.is_top_value())`
`100`	`100`	`{`
`101`	`101`	`make_top();`
`@@ -328,7 +328,7 @@ sharing_ptrt<pointer_abstract_objectt>`
`328`	`328`	`if(stack.empty())`
`329`	`329`	`{`
`330`	`330`	`// We should not be changing the type of an abstract object`
`331`		`- assert(new_value->type()==type().subtype());`
	`331`	`+ PRECONDITION(new_value->type()==type().subtype());`
`332`	`332`
`333`	`333`	`// Get an expression that we can assign to`
`334`	`334`	`exprt value=value_stack.to_expression().op0();`
Original file line number	Diff line number	Diff line change
`@@ -36,8 +36,8 @@ Function: full_struct_abstract_objectt::struct_abstract_objectt`
`36`	`36`	`full_struct_abstract_objectt::full_struct_abstract_objectt(const typet &t):`
`37`	`37`	`struct_abstract_objectt(t)`
`38`	`38`	`{`
`39`		`- assert(t.id()==ID_struct);`
`40`		`- assert(verify());`
	`39`	`+ PRECONDITION(t.id()==ID_struct);`
	`40`	`+ DATA_INVARIANT(verify(), "Structural invariants maintained");`
`41`	`41`	`}`
`42`	`42`
`43`	`43`	`/*******************************************************************\`
`@@ -60,8 +60,8 @@ full_struct_abstract_objectt::full_struct_abstract_objectt(`
`60`	`60`	`const typet &t, bool top, bool bottom):`
`61`	`61`	`struct_abstract_objectt(t, top, bottom)`
`62`	`62`	`{`
`63`		`- assert(t.id()==ID_struct);`
`64`		`- assert(verify());`
	`63`	`+ PRECONDITION(t.id()==ID_struct);`
	`64`	`+ DATA_INVARIANT(verify(), "Structural invariants maintained");`
`65`	`65`	`}`
`66`	`66`
`67`	`67`	`/*******************************************************************\`
`@@ -84,7 +84,7 @@ full_struct_abstract_objectt::full_struct_abstract_objectt(`
`84`	`84`	`const namespacet &ns):`
`85`	`85`	`struct_abstract_objectt(e, environment, ns)`
`86`	`86`	`{`
`87`		`- assert(verify());`
	`87`	`+ DATA_INVARIANT(verify(), "Structural invariants maintained");`
`88`	`88`	`}`
`89`	`89`
`90`	`90`	`/*******************************************************************\`
`@@ -122,7 +122,7 @@ abstract_object_pointert full_struct_abstract_objectt::read_component(`
`122`	`122`	`}`
`123`	`123`	`else`
`124`	`124`	`{`
`125`		`- assert(!is_bottom());`
	`125`	`+ PRECONDITION(!is_bottom());`
`126`	`126`
`127`	`127`	`irep_idt c=member_expr.get_component_name();`
`128`	`128`
`@@ -203,7 +203,7 @@ sharing_ptrt<struct_abstract_objectt>`
`203`	`203`	`copy->map[c]=`
`204`	`204`	`environment.write(starting_value, value, stack, ns, merging_write);`
`205`	`205`	`copy->clear_top();`
`206`		`- assert(copy->verify());`
	`206`	`+ DATA_INVARIANT(copy->verify(), "Structural invariants maintained");;`
`207`	`207`	`return copy;`
`208`	`208`	`}`
`209`	`209`	`else`
`@@ -219,19 +219,19 @@ sharing_ptrt<struct_abstract_objectt>`
`219`	`219`	`{`
`220`	`220`	`if(is_top()) // struct is top`
`221`	`221`	`{`
`222`		`- assert(copy->verify());`
	`222`	`+ DATA_INVARIANT(copy->verify(), "Structural invariants maintained");;`
`223`	`223`	`return copy;`
`224`	`224`	`}`
`225`	`225`
`226`		`- assert(!copy->map.empty());`
	`226`	`+ INVARIANT(!copy->map.empty(), "If not top, map cannot be empty");`
`227`	`227`
`228`	`228`	`struct_mapt &m=copy->map;`
`229`	`229`
`230`	`230`	`struct_mapt::iterator it=m.find(c);`
`231`	`231`
`232`	`232`	`if(it==m.end()) // component is top`
`233`	`233`	`{`
`234`		`- assert(copy->verify());`
	`234`	`+ DATA_INVARIANT(copy->verify(), "Structural invariants maintained");;`
`235`	`235`	`return copy;`
`236`	`236`	`}`
`237`	`237`
`@@ -243,10 +243,10 @@ sharing_ptrt<struct_abstract_objectt>`
`243`	`243`	`{`
`244`	`244`	`copy->map[c]=value;`
`245`	`245`	`copy->clear_top();`
`246`		`- assert(!copy->is_bottom());`
	`246`	`+ INVARIANT(!copy->is_bottom(), "top != bottom");`
`247`	`247`	`}`
`248`	`248`
`249`		`- assert(copy->verify());`
	`249`	`+ DATA_INVARIANT(copy->verify(), "Structural invariants maintained");;`
`250`	`250`	`return copy;`
`251`	`251`	`}`
`252`	`252`	`}`
`@@ -367,7 +367,7 @@ abstract_object_pointert full_struct_abstract_objectt::merge_constant_structs(`
`367`	`367`	`abstract_objectt::merge_maps<irep_idt>(map, other->map, merged_map);`
`368`	`368`	`if(!modified)`
`369`	`369`	`{`
`370`		`- assert(verify());`
	`370`	`+ DATA_INVARIANT(verify(), "Structural invariants maintained");`
`371`	`371`	`return shared_from_this();`
`372`	`372`	`}`
`373`	`373`	`else`
`@@ -378,9 +378,9 @@ abstract_object_pointert full_struct_abstract_objectt::merge_constant_structs(`
`378`	`378`
`379`	`379`	`result->map=merged_map;`
`380`	`380`
`381`		`- assert(!result->is_top());`
`382`		`- assert(!result->is_bottom());`
`383`		`- assert(result->verify());`
	`381`	`+ INVARIANT(!result->is_top(), "Merge of maps will not generate top");`
	`382`	`+ INVARIANT(!result->is_bottom(), "Merge of maps will not generate bottom");`
	`383`	`+ DATA_INVARIANT(result->verify(), "Structural invariants maintained");`
`384`	`384`	`return result;`
`385`	`385`	`}`
`386`	`386`	`}`
Original file line number	Diff line number	Diff line change
`@@ -29,7 +29,7 @@ Function: pointer_abstract_objectt::pointer_abstract_objectt`
`29`	`29`	`pointer_abstract_objectt::pointer_abstract_objectt(const typet &t):`
`30`	`30`	`abstract_objectt(t)`
`31`	`31`	`{`
`32`		`- assert(t.id()==ID_pointer);`
	`32`	`+ PRECONDITION(t.id()==ID_pointer);`
`33`	`33`	`}`
`34`	`34`
`35`	`35`	`/*******************************************************************\`
`@@ -52,7 +52,7 @@ pointer_abstract_objectt::pointer_abstract_objectt(`
`52`	`52`	`const typet &t, bool tp, bool bttm):`
`53`	`53`	`abstract_objectt(t, tp, bttm)`
`54`	`54`	`{`
`55`		`- assert(t.id()==ID_pointer);`
	`55`	`+ PRECONDITION(t.id()==ID_pointer);`
`56`	`56`	`}`
`57`	`57`
`58`	`58`	`/*******************************************************************\`
`@@ -74,7 +74,7 @@ pointer_abstract_objectt::pointer_abstract_objectt(`
`74`	`74`	`const namespacet &ns):`
`75`	`75`	`abstract_objectt(e, environment, ns)`
`76`	`76`	`{`
`77`		`- assert(e.type().id()==ID_pointer);`
	`77`	`+ PRECONDITION(e.type().id()==ID_pointer);`
`78`	`78`	`}`
`79`	`79`
`80`	`80`	`/**`
Original file line number	Diff line number	Diff line change
`@@ -30,7 +30,7 @@ Function: struct_abstract_objectt::struct_abstract_objectt`
`30`	`30`	`struct_abstract_objectt::struct_abstract_objectt(const typet &t):`
`31`	`31`	`abstract_objectt(t)`
`32`	`32`	`{`
`33`		`- assert(t.id()==ID_struct);`
	`33`	`+ PRECONDITION(t.id()==ID_struct);`
`34`	`34`	`}`
`35`	`35`
`36`	`36`	`/*******************************************************************\`
`@@ -53,7 +53,7 @@ struct_abstract_objectt::struct_abstract_objectt(`
`53`	`53`	`const typet &t, bool tp, bool bttm):`
`54`	`54`	`abstract_objectt(t, tp, bttm)`
`55`	`55`	`{`
`56`		`- assert(t.id()==ID_struct);`
	`56`	`+ PRECONDITION(t.id()==ID_struct);`
`57`	`57`	`}`
`58`	`58`
`59`	`59`	`/*******************************************************************\`
`@@ -75,7 +75,7 @@ struct_abstract_objectt::struct_abstract_objectt(`
`75`	`75`	`const namespacet &ns):`
`76`	`76`	`abstract_objectt(e, environment, ns)`
`77`	`77`	`{`
`78`		`- assert(ns.follow(e.type()).id()==ID_struct);`
	`78`	`+ PRECONDITION(ns.follow(e.type()).id()==ID_struct);`
`79`	`79`	`}`
`80`	`80`
`81`	`81`	`/**`
Original file line number	Diff line number	Diff line change
`@@ -29,7 +29,7 @@ Function: union_abstract_objectt::union_abstract_objectt`
`29`	`29`	`union_abstract_objectt::union_abstract_objectt(const typet &type):`
`30`	`30`	`abstract_objectt(type)`
`31`	`31`	`{`
`32`		`- assert(type.id()==ID_union);`
	`32`	`+ PRECONDITION(type.id()==ID_union);`
`33`	`33`	`}`
`34`	`34`
`35`	`35`	`/*******************************************************************\`
`@@ -52,7 +52,7 @@ union_abstract_objectt::union_abstract_objectt(`
`52`	`52`	`const typet &type, bool top, bool bottom):`
`53`	`53`	`abstract_objectt(type, top, bottom)`
`54`	`54`	`{`
`55`		`- assert(type.id()==ID_union);`
	`55`	`+ PRECONDITION(type.id()==ID_union);`
`56`	`56`	`}`
`57`	`57`
`58`	`58`	`/*******************************************************************\`
`@@ -74,7 +74,7 @@ union_abstract_objectt::union_abstract_objectt(`
`74`	`74`	`const namespacet &ns):`
`75`	`75`	`abstract_objectt(expr, environment, ns)`
`76`	`76`	`{`
`77`		`- assert(ns.follow(expr.type()).id()==ID_union);`
	`77`	`+ PRECONDITION(ns.follow(expr.type()).id()==ID_union);`
`78`	`78`	`}`
`79`	`79`
`80`	`80`	`/**`