Fixing new incompleteness, no object's runtime type is a union type

src/nagini_translation/translators/type_domain_factory.py

@@ -49,6 +49,7 @@ def get_default_axioms(self,
             self.create_reflexivity_axiom(ctx),
             self.create_extends_implies_subtype_axiom(ctx),
             self.create_null_type_axiom(ctx),
+            self.create_union_basic_axiom(ctx),
             self.create_object_subtype_axiom(ctx),
             self.create_subtype_exclusion_axiom(ctx),
             self.create_subtype_exclusion_axiom_2(ctx),
@@ -622,6 +623,28 @@ def create_null_type_axiom(self, ctx: Context) -> 'silver.ast.DomainAxiom':
         return self.viper.DomainAxiom('null_nonetype', body, position, info,
                                       self.type_domain)
 
+    def create_union_basic_axiom(self, ctx: Context) -> 'silver.ast.DomainAxiom':
+        """
+        Creates an axiom that states that the type of null is None:
+
+        forall r: Ref :: { typeof(r) }
+          get_basic(typeof(r)) != union_basic()
+        """
+        position, info = self.no_position(ctx), self.no_info(ctx)
+        arg_r = self.viper.LocalVarDecl('r', self.viper.Ref, position, info)
+        var_r = self.viper.LocalVar('r', self.viper.Ref, position, info)
+        typeof = self.typeof(var_r, ctx)
+        basic = self.viper.DomainFuncApp('get_basic', [typeof], self.type_type(),
+                                         position, info, self.type_domain)
+        union_basic = self.viper.DomainFuncApp('union_basic', [], self.type_type(),
+                                               position, info, self.type_domain)
+        inequality = self.viper.NeCmp(basic, union_basic, position, info)
+        trigger = self.viper.Trigger([typeof], position, info)
+        body = self.viper.Forall([arg_r], [trigger],
+                                 inequality, position, info)
+        return self.viper.DomainAxiom('nothing_has_union_type', body, position, info,
+                                      self.type_domain)
+
     def create_object_type(self, ctx: Context) -> 'silver.ast.DomainFunc':
         return self.create_type_function(OBJECT_TYPE, 0, self.no_position(ctx),
                                          self.no_info(ctx))[0]