[Mono-dev] type 0x20 not handled in do_mono_metadata_parse_type

[Vladimir Klebanov]

Hello,

I'm trying to run Boogie (the Microsoft Research program verifier,
http://boogie.codeplex.com/releases/view/48961 ) on Mono on Linux, but
this is not working out well. I get:

Boogie program verifier version 2, Copyright (c) 2003-2010, Microsoft.
type 0x20 not handled in do_mono_metadata_parse_type on image
/home/vladimir/Downloads/Boogie/Core.dll

Unhandled Exception: System.TypeLoadException: Could not load type
'Typespec 0x1b000023'.
  at Microsoft.Boogie.Parser.ProcSignature (Boolean
allowWhereClausesOnFormals, IToken& name,
Microsoft.Boogie.TypeVariableSeq& typeParams,
Microsoft.Boogie.VariableSeq& ins, Microsoft.Boogie.VariableSeq& outs,
Microsoft.Boogie.QKeyValue& kv) [0x00000] in <filename unknown>:0
  at Microsoft.Boogie.Parser.Procedure (Microsoft.Boogie.Procedure&
proc, Microsoft.Boogie.Implementation& impl) [0x00000] in <filename
unknown>:0
  at Microsoft.Boogie.Parser.BoogiePL () [0x00000] in <filename unknown>:0
  at Microsoft.Boogie.Parser.Parse () [0x00000] in <filename unknown>:0
  at Microsoft.Boogie.Parser.Parse (System.String filename,
System.Collections.Generic.List`1 defines, Microsoft.Boogie.Program&
program) [0x00000] in <filename unknown>:0
  at Microsoft.Boogie.OnlyBoogie.ParseBoogieProgram
(System.Collections.Generic.List`1 fileNames, Boolean
suppressTraceOutput) [0x00000] in <filename unknown>:0
  at Microsoft.Boogie.OnlyBoogie.ProcessFiles
(System.Collections.Generic.List`1 fileNames) [0x00000] in <filename
unknown>:0
  at Microsoft.Boogie.OnlyBoogie.Main (System.String[] args) [0x00000]
in <filename unknown>:0

Does anyone have any ideas why this happens?


Mono JIT compiler version 2.8.1 (tarball Fri Nov 12 14:07:16 UTC 2010)
Copyright (C) 2002-2010 Novell, Inc and Contributors. www.mono-project.com
        TLS:           __thread
        SIGSEGV:       altstack
        Notifications: epoll
        Architecture:  x86
        Disabled:      none
        Misc:          debugger softdebug
        LLVM:          yes(2.8svn-mono)
        GC:            Included Boehm (with typed GC and Parallel Mark)


Thanks.

Vladimir

-- 
Vladimir Klebanov
Postdoctoral Researcher, Application-oriented Formal Verification
Karlsruhe Institute of Technology
http://formal.iti.kit.edu/~klebanov