I was using the BCT from the CodePlex site. As I said, I couldn't get it to work with a C# DLL with the only real line of code being:
Console.WriteLine("Done!"); Here's the top bit of the stack trace:
The byte-code translator failed with uncaught exception: Stack empty.
Stack trace: at System.ThrowHelper.ThrowInvalidOperationException(ExceptionResource resource)
at BytecodeTranslator.ExpressionTraverser.Visit(IMethodCall methodCall) in C:\CodePlex\Boogie\BCT\BytecodeTranslator\ExpressionTraverser.cs:line 336
at Microsoft.Cci.MutableCodeModel.MethodCall.Dispatch(ICodeVisitor visitor) in C:\CodePlex\CCICodePlex\Ast\Sources\MutableCodeModel\Expressions.cs:line 1892
at Microsoft.Cci.BaseCodeTraverser.Visit(IExpression expression) in C:\CodePlex\CCICodePlex\Ast\Sources\CodeModel\Visitors.cs:line 994
I tried this with both a debug and release build. Here's what happened when I tried it against the Spec# compiled AbsInt.dll:
Non-Class StructuralTypes.Function_optional(NonNullType) CallSite_optional(NonNullType) Element was found
The byte-code translator failed with uncaught exception: Non-Class Type StructuralTypes.Function_optional(NonNullType) CallSite_optional(NonNullType) Element is not yet supported.
Stack trace: at BytecodeTranslator.ToplevelTraverser.Visit(ITypeDefinition typeDefinition) in C:\CodePlex\Boogie\BCT\BytecodeTranslator\ToplevelTraverser.cs:line 67
at Microsoft.Cci.BaseMetadataTraverser.Visit(INamespaceMember namespaceMember) in C:\CodePlex\CCICodePlex\Ast\Metadata\Sources\MetadataHelper\Visitors.cs:line 877
As I said, I assume I've just compiled BCT incorrectly. As far as I can tell, I have all the latest code and it seems to compile fine.
From your respose, it sounds like Boogie, or at least what is on the CodePlex site, is not what is being used by Code Contracts in VS 2010/.Net 4.0. The reason I was considering Boogie was that it was solid enough for VS 2010/.Net 4.0. I'm still very interested
in using it, but more hesitant to put large amounts of my personal time into it.
I would love to see something like FxCop but with a very powerful static analysis language like Boogie. Since I hadn't seen anybody else talk about this, I was going to give it a try myself. I'm thinking something like the Code "SQL" in NDepend.
I want to get much deeper than NDepend does since it is very similar to what FxCop can do since they both work with IL pretty much directly.
What I'm thinking is that the BCT can translate my assembly into whatever *.bpl files. I can then add in a *.bpl for each "rule" I'm trying to check and execute it. Does that sound like something that is possible?