GetType (in boogie) should not return an abstract type about tinybct HOT 4 OPEN

Currently we only support test from a C# code. I could not find a way to generate this boogie code. However the issue still exists.

You should append this boogie procedure to the translation of DynamicDispatch.cs

procedure  DynamicDispatch.DynamicDispatch.test8$System.Object(a : Ref) 
{
	assert $DynamicType(a) != T$DynamicDispatch.Animal();	
}

Corral reports that the assert can fail.

I guess that the original C# would be something like this (not supported yet).

        static void test8(Animal a)
        {
            Contract.Assert(a.GetType().Equals(typeof(Animal)));
        }

from tinybct.

I think this is a duplicate of issue #6. Please update (and remove duplicate label) if I'm wrong.

from tinybct.

What I tried to show is that $DynamicType can never (the intended behaviour) be an abstract type even if the reference is subtype of an abstract class (ie: in the hierarchy )

#6 as far as I know is that it could return a type that is not even in the hierarchy.

I think both issues are not solved yet.

from tinybct.

from tinybct.