Please file a bug report On Tue, Nov 30, 2010 at 12:06 PM, Vladimir Klebanov <[email protected]>wrote:
> 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 > _______________________________________________ > Mono-devel-list mailing list > [email protected] > http://lists.ximian.com/mailman/listinfo/mono-devel-list >
_______________________________________________ Mono-devel-list mailing list [email protected] http://lists.ximian.com/mailman/listinfo/mono-devel-list
