Add two invariants

Owen Jones · Owen Jones · commit b4ceea17af50 · 2017-11-20T13:37:36.000Z
diff --git a/src/pointer-analysis/external_value_set_expr.h b/src/pointer-analysis/external_value_set_expr.h
@@ -187,6 +187,9 @@ class external_value_set_exprt:public exprt
       return "external_objects"+type_to_basename(declared_on_type);
     case external_value_set_typet::PRECISE:
     {
+      DATA_INVARIANT(
+        !access_path_entries().empty(),
+        "Only root object EVSs can have an empty access path");
       std::ostringstream ret;
       ret << id2string(label().get_value());
       for(
@@ -216,6 +219,7 @@ class external_value_set_exprt:public exprt
   void extend_access_path(
     const access_path_entry_exprt &newentry, external_value_set_typet evs_type)
   {
+    PRECONDITION(evs_type!=external_value_set_typet::ROOT_OBJECT);
     set_external_value_set_type(evs_type);
     switch(evs_type)
     {

Original file line number	Diff line number	Diff line change
`@@ -187,6 +187,9 @@ class external_value_set_exprt:public exprt`
`187`	`187`	`return "external_objects"+type_to_basename(declared_on_type);`
`188`	`188`	`case external_value_set_typet::PRECISE:`
`189`	`189`	`{`
	`190`	`+ DATA_INVARIANT(`
	`191`	`+ !access_path_entries().empty(),`
	`192`	`+ "Only root object EVSs can have an empty access path");`
`190`	`193`	`std::ostringstream ret;`
`191`	`194`	`ret << id2string(label().get_value());`
`192`	`195`	`for(`
`@@ -216,6 +219,7 @@ class external_value_set_exprt:public exprt`
`216`	`219`	`void extend_access_path(`
`217`	`220`	`const access_path_entry_exprt &newentry, external_value_set_typet evs_type)`
`218`	`221`	`{`
	`222`	`+ PRECONDITION(evs_type!=external_value_set_typet::ROOT_OBJECT);`
`219`	`223`	`set_external_value_set_type(evs_type);`
`220`	`224`	`switch(evs_type)`
`221`	`225`	`{`