Permalink
Browse files

The base architecture for code-contracts analysis

  • Loading branch information...
1 parent 33d931c commit e8352f0bd13a2999064eece8af4214c540fbc156 @alexsatch alexsatch committed with marek-safar Jul 13, 2011
Showing with 37,226 additions and 69 deletions.
  1. +67 −0 man/cccheck.1
  2. +347 −68 mcs/class/Mono.CodeContracts/Mono.CodeContracts-net_4_0.csproj
  3. +81 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.AST.Visitors/CodeVisitor.cs
  4. +467 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.AST.Visitors/DefaultNodeVisitor.cs
  5. +35 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.AST.Visitors/IAggregateVisitor.cs
  6. +35 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.AST.Visitors/ICodeConsumer.cs
  7. +38 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.AST.Visitors/IExpressionILVisitor.cs
  8. +102 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.AST.Visitors/IILVisitor.cs
  9. +371 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.AST.Visitors/ILVisitorBase.cs
  10. +35 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.AST.Visitors/IMethodCodeConsumer.cs
  11. +34 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.AST.Visitors/ISymbolicExpressionVisitor.cs
  12. +42 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.AST.Visitors/ISyntheticILVisitor.cs
  13. +436 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.AST.Visitors/NodeInspector.cs
  14. +46 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.AST.Visitors/NodeVisitor.cs
  15. +36 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.AST.Visitors/ValueCodeVisitor.cs
  16. +38 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.AST/ArrayTypeNode.cs
  17. +86 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.AST/AssemblyNode.cs
  18. +46 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.AST/AssignmentStatement.cs
  19. +56 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.AST/BinaryExpression.cs
  20. +64 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.AST/BinaryOperator.cs
  21. +50 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.AST/Block.cs
  22. +50 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.AST/BlockExpression.cs
  23. +856 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.AST/BodyParser.cs
  24. +64 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.AST/Branch.cs
  25. +45 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.AST/CatchFilter.cs
  26. +66 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.AST/Class.cs
  27. +46 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.AST/Construct.cs
  28. +206 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.AST/CoreSystemTypes.cs
  29. +35 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.AST/EndFinally.cs
  30. +47 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.AST/Ensures.cs
  31. +43 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.AST/ExceptionHandler.cs
  32. +48 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.AST/Expression.cs
  33. +48 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.AST/ExpressionStatement.cs
  34. +42 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.AST/FaultHandler.cs
  35. +107 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.AST/Field.cs
  36. +55 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.AST/Literal.cs
  37. +65 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.AST/Local.cs
  38. +46 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.AST/Member.cs
  39. +58 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.AST/MemberBinding.cs
  40. +345 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.AST/Method.cs
  41. +57 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.AST/MethodCall.cs
  42. +66 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.AST/MethodContract.cs
  43. +39 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.AST/MethodContractElement.cs
  44. +69 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.AST/Module.cs
  45. +45 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.AST/NaryExpression.cs
  46. +38 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.AST/Node.cs
  47. +105 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.AST/NodeType.cs
  48. +58 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.AST/OperatorExtensions.cs
  49. +85 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.AST/Parameter.cs
  50. +143 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.AST/Property.cs
  51. +56 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.AST/Reference.cs
  52. +47 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.AST/Requires.cs
  53. +47 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.AST/Return.cs
  54. +40 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.AST/Statement.cs
  55. +58 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.AST/This.cs
  56. +335 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.AST/TypeNode.cs
  57. +55 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.AST/UnaryExpression.cs
  58. +47 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.AST/UnaryOperator.cs
  59. +36 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.AST/Variable.cs
  60. +62 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Analysis.Drivers/AnalysisDriver.cs
  61. +66 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Analysis.Drivers/BasicAnalysisDriver.cs
  62. +137 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Analysis.Drivers/BasicMethodDriver.cs
  63. +146 −0 ...lass/Mono.CodeContracts/Mono.CodeContracts.Static.Analysis.Drivers/CodeContractsAnalysisDriver.cs
  64. +38 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Analysis.Drivers/IBasicAnalysisDriver.cs
  65. +42 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Analysis.Drivers/IBasicMethodDriver.cs
  66. +40 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Analysis.Drivers/IMethodAnalysis.cs
  67. +37 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Analysis.Drivers/IMethodAnalysisFixPoint.cs
  68. +53 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Analysis.Drivers/IMethodDriver.cs
  69. +37 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Analysis.Drivers/IMethodResult.cs
  70. +157 −0 ...Contracts/Mono.CodeContracts.Static.Analysis.ExpressionAnalysis.Decoding/FullExpressionDecoder.cs
  71. +49 −0 ...ontracts/Mono.CodeContracts.Static.Analysis.ExpressionAnalysis.Decoding/IFullExpressionDecoder.cs
  72. +79 −0 ...Mono.CodeContracts/Mono.CodeContracts.Static.Analysis.ExpressionAnalysis.Decoding/QueryVisitor.cs
  73. +61 −0 ...ts/Mono.CodeContracts.Static.Analysis.ExpressionAnalysis.Decoding/VisitorForIsBinaryExpression.cs
  74. +58 −0 ....CodeContracts/Mono.CodeContracts.Static.Analysis.ExpressionAnalysis.Decoding/VisitorForIsInst.cs
  75. +49 −0 ....CodeContracts/Mono.CodeContracts.Static.Analysis.ExpressionAnalysis.Decoding/VisitorForIsNull.cs
  76. +56 −0 ...cts/Mono.CodeContracts.Static.Analysis.ExpressionAnalysis.Decoding/VisitorForIsUnaryExpression.cs
  77. +54 −0 ....CodeContracts/Mono.CodeContracts.Static.Analysis.ExpressionAnalysis.Decoding/VisitorForSizeOf.cs
  78. +88 −0 ...ts/Mono.CodeContracts.Static.Analysis.ExpressionAnalysis.Decoding/VisitorForUnderlyingVariable.cs
  79. +64 −0 ...CodeContracts/Mono.CodeContracts.Static.Analysis.ExpressionAnalysis.Decoding/VisitorForValueOf.cs
  80. +52 −0 ...odeContracts/Mono.CodeContracts.Static.Analysis.ExpressionAnalysis.Decoding/VisitorForVariable.cs
  81. +100 −0 ...Contracts/Mono.CodeContracts.Static.Analysis.ExpressionAnalysis.Decoding/VisitorForVariablesIn.cs
  82. +98 −0 ...ono.CodeContracts/Mono.CodeContracts.Static.Analysis.ExpressionAnalysis.Expressions/BinaryExpr.cs
  83. +85 −0 ...Mono.CodeContracts/Mono.CodeContracts.Static.Analysis.ExpressionAnalysis.Expressions/ConstExpr.cs
  84. +57 −0 ...lass/Mono.CodeContracts/Mono.CodeContracts.Static.Analysis.ExpressionAnalysis.Expressions/Expr.cs
  85. +87 −0 ...ono.CodeContracts/Mono.CodeContracts.Static.Analysis.ExpressionAnalysis.Expressions/IsInstExpr.cs
  86. +79 −0 .../Mono.CodeContracts/Mono.CodeContracts.Static.Analysis.ExpressionAnalysis.Expressions/NullExpr.cs
  87. +85 −0 ...ono.CodeContracts/Mono.CodeContracts.Static.Analysis.ExpressionAnalysis.Expressions/SizeOfExpr.cs
  88. +92 −0 ...Mono.CodeContracts/Mono.CodeContracts.Static.Analysis.ExpressionAnalysis.Expressions/UnaryExpr.cs
  89. +98 −0 ...class/Mono.CodeContracts/Mono.CodeContracts.Static.Analysis.ExpressionAnalysis/AnalysisDecoder.cs
  90. +100 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Analysis.ExpressionAnalysis/AssumeDecoder.cs
  91. +121 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Analysis.ExpressionAnalysis/ExprDomain.cs
  92. +88 −0 ...o.CodeContracts/Mono.CodeContracts.Static.Analysis.ExpressionAnalysis/ExpressionAnalysisFacade.cs
  93. +165 −0 ...ass/Mono.CodeContracts/Mono.CodeContracts.Static.Analysis.ExpressionAnalysis/ExpressionDecoder.cs
  94. +57 −0 ...o.CodeContracts/Mono.CodeContracts.Static.Analysis.ExpressionAnalysis/ExpressionDecoderAdapter.cs
  95. +132 −0 ...o.CodeContracts/Mono.CodeContracts.Static.Analysis.ExpressionAnalysis/ExpressionPrinterFactory.cs
  96. +411 −0 ...lass/Mono.CodeContracts/Mono.CodeContracts.Static.Analysis.ExpressionAnalysis/ILDecoderAdapter.cs
  97. +122 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Analysis.ExpressionAnalysis/ValueAnalysis.cs
  98. +112 −0 ...lass/Mono.CodeContracts/Mono.CodeContracts.Static.Analysis.HeapAnalysis.Paths/AccessPathFilter.cs
  99. +35 −0 ...lass/Mono.CodeContracts/Mono.CodeContracts.Static.Analysis.HeapAnalysis.Paths/IVisibilityCheck.cs
  100. +69 −0 ...Mono.CodeContracts/Mono.CodeContracts.Static.Analysis.HeapAnalysis.Paths/MethodCallPathElement.cs
  101. +67 −0 .../Mono.CodeContracts/Mono.CodeContracts.Static.Analysis.HeapAnalysis.Paths/ParameterPathElement.cs
  102. +63 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Analysis.HeapAnalysis.Paths/PathElement.cs
  103. +43 −0 ...class/Mono.CodeContracts/Mono.CodeContracts.Static.Analysis.HeapAnalysis.Paths/PathElementBase.cs
  104. +205 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Analysis.HeapAnalysis.Paths/PathElement`1.cs
  105. +110 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Analysis.HeapAnalysis.Paths/PathExtensions.cs
  106. +103 −0 ...ss/Mono.CodeContracts/Mono.CodeContracts.Static.Analysis.HeapAnalysis.Paths/SpecialPathElement.cs
  107. +34 −0 ...ono.CodeContracts/Mono.CodeContracts.Static.Analysis.HeapAnalysis.Paths/SpecialPathElementKind.cs
  108. +87 −0 ...deContracts/Mono.CodeContracts.Static.Analysis.HeapAnalysis.SymbolicGraph/AbstractDomainUpdate.cs
  109. +97 −0 ...ss/Mono.CodeContracts/Mono.CodeContracts.Static.Analysis.HeapAnalysis.SymbolicGraph/EdgeUpdate.cs
  110. +79 −0 ...odeContracts/Mono.CodeContracts.Static.Analysis.HeapAnalysis.SymbolicGraph/EliminateEdgeUpdate.cs
  111. +64 −0 .../Mono.CodeContracts/Mono.CodeContracts.Static.Analysis.HeapAnalysis.SymbolicGraph/EqualityPair.cs
  112. +60 −0 ...ono.CodeContracts/Mono.CodeContracts.Static.Analysis.HeapAnalysis.SymbolicGraph/EqualityUpdate.cs
  113. +53 −0 ...ss/Mono.CodeContracts/Mono.CodeContracts.Static.Analysis.HeapAnalysis.SymbolicGraph/IMergeInfo.cs
  114. +516 −0 ...ass/Mono.CodeContracts/Mono.CodeContracts.Static.Analysis.HeapAnalysis.SymbolicGraph/MergeInfo.cs
  115. +71 −0 ...ass/Mono.CodeContracts/Mono.CodeContracts.Static.Analysis.HeapAnalysis.SymbolicGraph/MultiEdge.cs
  116. +60 −0 ...no.CodeContracts/Mono.CodeContracts.Static.Analysis.HeapAnalysis.SymbolicGraph/MultiEdgeUpdate.cs
  117. +908 −0 ...lass/Mono.CodeContracts/Mono.CodeContracts.Static.Analysis.HeapAnalysis.SymbolicGraph/SymGraph.cs
  118. +62 −0 .../Mono.CodeContracts/Mono.CodeContracts.Static.Analysis.HeapAnalysis.SymbolicGraph/SymGraphTerm.cs
  119. +53 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Analysis.HeapAnalysis.SymbolicGraph/Update.cs
  120. +174 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Analysis.HeapAnalysis/AbstractType.cs
  121. +1,262 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Analysis.HeapAnalysis/AnalysisDecoder.cs
  122. +1,635 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Analysis.HeapAnalysis/Domain.cs
  123. +185 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Analysis.HeapAnalysis/FunctionsTable.cs
  124. +254 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Analysis.HeapAnalysis/HeapAnalysis.cs
  125. +35 −0 ...ss/Mono.CodeContracts/Mono.CodeContracts.Static.Analysis.HeapAnalysis/IAbstractDomainForEGraph.cs
  126. +33 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Analysis.HeapAnalysis/IConstantInfo.cs
  127. +63 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Analysis.HeapAnalysis/ISymGraph.cs
  128. +64 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Analysis.HeapAnalysis/LabeledSymbol.cs
  129. +48 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Analysis.HeapAnalysis/MethodWrapper.cs
  130. +72 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Analysis.HeapAnalysis/ParameterWrapper.cs
  131. +572 −0 ...lass/Mono.CodeContracts/Mono.CodeContracts.Static.Analysis.HeapAnalysis/StackToSymbolicAdapter.cs
  132. +78 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Analysis.HeapAnalysis/SymFunction.cs
  133. +79 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Analysis.HeapAnalysis/SymValue.cs
  134. +99 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Analysis.HeapAnalysis/SymbolicValue.cs
  135. +57 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Analysis.HeapAnalysis/TypeCache.cs
  136. +184 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Analysis.HeapAnalysis/ValueContextProvider.cs
  137. +91 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Analysis.HeapAnalysis/ValueDecoder.cs
  138. +191 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Analysis.HeapAnalysis/Wrapper.cs
  139. +418 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Analysis.NonNull/Analysis.cs
  140. +58 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Analysis.NonNull/Domain.cs
  141. +133 −0 ...class/Mono.CodeContracts/Mono.CodeContracts.Static.Analysis.NonNull/ExpressionAssertDischarger.cs
  142. +153 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Analysis.NonNull/ExpressionAssumeDecoder.cs
  143. +53 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Analysis.NonNull/NonNullAnalysisFacade.cs
  144. +92 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Analysis.StackAnalysis/APCMap.cs
  145. +67 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Analysis.StackAnalysis/SequenceGenerator.cs
  146. +606 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Analysis.StackAnalysis/StackDecoder.cs
  147. +41 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Analysis.StackAnalysis/StackDepthFactory.cs
  148. +707 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Analysis.StackAnalysis/StackDepthProvider.cs
  149. +127 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Analysis.StackAnalysis/StackInfo.cs
  150. +82 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Analysis.StackAnalysis/StackInfo`1.cs
  151. +90 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Analysis/CodeLayer.cs
  152. +57 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Analysis/CodeLayerFactory.cs
  153. +49 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Analysis/ICodeLayer.cs
  154. +50 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Analysis/IExpressionContext.cs
  155. +34 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Analysis/IExpressionContextProvider.cs
  156. +33 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Analysis/ILPrinter.cs
  157. +41 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Analysis/IMethodContext.cs
  158. +33 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Analysis/IMethodContextProvider.cs
  159. +35 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Analysis/IStackContext.cs
  160. +33 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Analysis/IStackContextProvider.cs
  161. +44 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Analysis/IValueContext.cs
  162. +33 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Analysis/IValueContextProvider.cs
  163. +469 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Analysis/PrinterFactory.cs
  164. +234 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.ContractExtraction/ContractExtractor.cs
  165. +221 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.ContractExtraction/ContractNodes.cs
  166. +91 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.ContractExtraction/GatherLocals.cs
  167. +332 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.ContractExtraction/HelperMethods.cs
  168. +48 −0 ...ass/Mono.CodeContracts/Mono.CodeContracts.Static.ContractExtraction/RepresentationForAttribute.cs
  169. +57 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.ControlFlow.Blocks/AssumeBlock.cs
  170. +42 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.ControlFlow.Blocks/BlockBase.cs
  171. +110 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.ControlFlow.Blocks/BlockWithLabels.cs
  172. +38 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.ControlFlow.Blocks/CatchFilterEntryBlock.cs
  173. +215 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.ControlFlow.Blocks/EnsuresBlock.cs
  174. +47 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.ControlFlow.Blocks/EntryBlock.cs
  175. +43 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.ControlFlow.Blocks/EntryExitBlock.cs
  176. +394 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.ControlFlow.Blocks/LabelAdapter.cs
  177. +67 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.ControlFlow.Blocks/MethodCallBlock.cs
  178. +44 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.ControlFlow.Blocks/NewObjCallBlock.cs
  179. +195 −0 ...ass/Mono.CodeContracts/Mono.CodeContracts.Static.ControlFlow.Subroutines.Builders/BlockBuilder.cs
  180. +164 −0 ...no.CodeContracts/Mono.CodeContracts.Static.ControlFlow.Subroutines.Builders/BlockStartGatherer.cs
  181. +73 −0 ...s/Mono.CodeContracts/Mono.CodeContracts.Static.ControlFlow.Subroutines.Builders/EnsuresFactory.cs
  182. +83 −0 .../Mono.CodeContracts/Mono.CodeContracts.Static.ControlFlow.Subroutines.Builders/RequiresFactory.cs
  183. +100 −0 ...deContracts/Mono.CodeContracts.Static.ControlFlow.Subroutines.Builders/SimpleSubroutineBuilder.cs
  184. +193 −0 ...ono.CodeContracts/Mono.CodeContracts.Static.ControlFlow.Subroutines.Builders/SubroutineBuilder.cs
  185. +75 −0 ...ono.CodeContracts/Mono.CodeContracts.Static.ControlFlow.Subroutines.Builders/SubroutineFactory.cs
  186. +221 −0 ...racts/Mono.CodeContracts.Static.ControlFlow.Subroutines.Builders/SubroutineWithHandlersBuilder.cs
  187. +152 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.ControlFlow.Subroutines/EnsuresSubroutine.cs
  188. +52 −0 ...ono.CodeContracts/Mono.CodeContracts.Static.ControlFlow.Subroutines/FaultFinallySubroutineBase.cs
  189. +43 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.ControlFlow.Subroutines/FaultSubroutine.cs
  190. +43 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.ControlFlow.Subroutines/FinallySubroutine.cs
  191. +63 −0 .../Mono.CodeContracts/Mono.CodeContracts.Static.ControlFlow.Subroutines/MethodContractSubroutine.cs
  192. +136 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.ControlFlow.Subroutines/MethodSubroutine.cs
  193. +160 −0 ...class/Mono.CodeContracts/Mono.CodeContracts.Static.ControlFlow.Subroutines/OldScanStateMachine.cs
  194. +85 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.ControlFlow.Subroutines/OldValueSubroutine.cs
  195. +85 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.ControlFlow.Subroutines/RequiresSubroutine.cs
  196. +58 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.ControlFlow.Subroutines/SimpleSubroutine.cs
  197. +782 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.ControlFlow.Subroutines/SubroutineBase.cs
  198. +130 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.ControlFlow.Subroutines/SubroutineFacade.cs
  199. +208 −0 ...ss/Mono.CodeContracts/Mono.CodeContracts.Static.ControlFlow.Subroutines/SubroutineWithHandlers.cs
  200. +289 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.ControlFlow/APC.cs
  201. +105 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.ControlFlow/APCDecoder.cs
  202. +83 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.ControlFlow/CFGBlock.cs
  203. +163 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.ControlFlow/ContractFilteredCFG.cs
  204. +194 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.ControlFlow/ControlFlowGraph.cs
  205. +52 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.ControlFlow/Edge.cs
  206. +222 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.ControlFlow/EdgeMap.cs
  207. +64 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.ControlFlow/EdgeTag.cs
  208. +36 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.ControlFlow/EdgeTagExtensions.cs
  209. +32 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.ControlFlow/EdgeVisitor.cs
  210. +64 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.ControlFlow/ICFG.cs
  211. +35 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.ControlFlow/IConstantInfo.cs
  212. +36 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.ControlFlow/IHandlerFilter.cs
  213. +35 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.ControlFlow/IMethodInfo.cs
  214. +33 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.ControlFlow/IStackInfo.cs
  215. +420 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.ControlFlow/RemoveBranchDelegator.cs
  216. +186 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.ControlFlow/Subroutine.cs
  217. +41 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.ControlFlow/SubroutineKind.cs
  218. +164 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.DataFlowAnalysis/DataFlowAnalysisBase.cs
  219. +46 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.DataFlowAnalysis/EdgeBasedWidening.cs
  220. +31 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.DataFlowAnalysis/EdgeConverter.cs
  221. +151 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.DataFlowAnalysis/ForwardAnalysis.cs
  222. +155 −0 ...lass/Mono.CodeContracts/Mono.CodeContracts.Static.DataFlowAnalysis/ForwardDataFlowAnalysisBase.cs
  223. +45 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.DataFlowAnalysis/IAnalysis.cs
  224. +34 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.DataFlowAnalysis/IFixPointInfo.cs
  225. +35 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.DataFlowAnalysis/IWidenStrategy.cs
  226. +33 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.DataFlowAnalysis/Joiner.cs
  227. +60 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.DataFlowAnalysis/StepWidening.cs
  228. +75 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.DataStructures/AbstractWorkList.cs
  229. +67 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.DataStructures/DecoratorHelper.cs
  230. +229 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.DataStructures/DepthFirst.cs
  231. +90 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.DataStructures/DoubleDictionary.cs
  232. +126 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.DataStructures/DoubleImmutableMap.cs
  233. +42 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.DataStructures/Dummy.cs
  234. +31 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.DataStructures/EdgeVisitor.cs
  235. +55 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.DataStructures/GraphWrapper.cs
  236. +36 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.DataStructures/IGraph.cs
  237. +46 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.DataStructures/IImmutableIntMap.cs
  238. +48 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.DataStructures/IImmutableMap.cs
  239. +48 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.DataStructures/IImmutableSet.cs
  240. +34 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.DataStructures/IIndexable.cs
  241. +35 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.DataStructures/ITypedProperties.cs
  242. +35 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.DataStructures/IWorkList.cs
  243. +114 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.DataStructures/ImmutableIntKeyMap.cs
  244. +146 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.DataStructures/ImmutableIntMap.cs
  245. +143 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.DataStructures/ImmutableMap.cs
  246. +169 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.DataStructures/ImmutableSet.cs
  247. +51 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.DataStructures/ImmutableSetExtensions.cs
  248. +54 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.DataStructures/Indexable.cs
  249. +131 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.DataStructures/LispList.cs
  250. +116 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.DataStructures/LispListExtensions.cs
  251. +46 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.DataStructures/Optional.cs
  252. +71 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.DataStructures/Pair.cs
  253. +110 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.DataStructures/PriorityQueue.cs
  254. +57 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.DataStructures/TypedKey.cs
  255. +60 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.DataStructures/TypedProperties.cs
  256. +34 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.DataStructures/VisitStatus.cs
  257. +61 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.DataStructures/WorkList.cs
  258. +11 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Extensions/Extensions.cs
  259. +221 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Lattices/EnvironmentDomain.cs
  260. +196 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Lattices/FlatDomain.cs
  261. +80 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Lattices/IAbstractDomain.cs
  262. +157 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Lattices/SetDomain.cs
  263. +86 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Providers/CodeContractDecoder.cs
  264. +543 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Providers/CodeProviderImpl.cs
  265. +11 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Providers/ICodeProvider.cs
  266. +44 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Providers/IContractProvider.cs
  267. +41 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Providers/IILDecoder.cs
  268. +169 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Providers/IMetaDataProvider.cs
  269. +49 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Providers/IMethodCodeProvider.cs
  270. +692 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Providers/MetaDataProvider.cs
  271. +140 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Proving/AssertionFinder.cs
  272. +135 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Proving/BasicFacts.cs
  273. +1,688 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Proving/BoxedExpression.cs
  274. +56 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Proving/BoxedExpressionExtensions.cs
  275. +184 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Proving/ComposedFactQuery.cs
  276. +212 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Proving/ConstantPropagationFactQuery.cs
  277. +37 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Proving/IFactBase.cs
  278. +42 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Proving/IFactQuery.cs
  279. +115 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Proving/SimpleLogicInference.cs
  280. +44 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static/CheckOptions.cs
  281. +68 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static/CheckResults.cs
  282. +136 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static/Checker.cs
  283. +33 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static/DebugOptions.cs
  284. +36 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static/ProofOutcome.cs
  285. +73 −0 mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static/ProofOutcomeExtensions.cs
  286. +283 −1 mcs/class/Mono.CodeContracts/Mono.CodeContracts.dll.sources
  287. +1 −0 mcs/tools/Makefile
  288. +9 −0 mcs/tools/cccheck/Makefile
  289. +66 −0 mcs/tools/cccheck/Program.cs
  290. +3 −0 mcs/tools/cccheck/cccheck.exe.sources
View
@@ -0,0 +1,67 @@
+.\"
+.\" cccheck manual page.
+.\" Copyright (C) 2011 Alexander Chebaturkin
+.\" Author:
+.\" Alexander Chebaturkin (chebaturkin@gmail.com)
+.\"
+.TH Mono "cccheck"
+.SH NAME
+cccheck \- Perform static code contracts verification for CLR assemblies.
+.SH SYNOPSIS
+.PP
+.B cccheck --assembly=<assembly> [options]
+.SH DESCRIPTION
+Perform static code contracts verification to find bugs and inconsistences
+between code and specification. This includes non-null, integer analyses.
+.PP
+The assembly must have been built with the symbol CONTRACTS_FULL defined,
+otherwise the calls to the contract methods will have been removed
+by the compiler.
+.PP
+Currently only Contract.Assume() and Contract.Assert() methods are
+supported. Only non-null analysis is supported, the consecutive analyses are
+in development. An error message will be shown if cccheck is unable to process
+all or some of the methods of specified assembly.
+.SH CONFIGURATION OPTIONS
+.TP
+.I "--assembly <assembly-name>"
+The assembly to perform static verification.
+.TP
+.I "--debug"
+Shows debug information about process of proving the assertions. It shows
+four layers of abstraction, raw layer, stack layer, heap layer,
+and substituted expression level.
+.TP
+.I "--method=<method-name-substring>"
+String for finding method. It filters all methods in assembly where method
+name has this parameter as a substring.
+.TP
+.I "--help"
+Show help for cccheck, listing configuration options.
+
+.SH EXAMPLES
+.TP
+Suppose you have a method:
+ void Method() {
+ object x = null;
+ int y = 1;
+ if (y % 2 == 1)
+ x = new object();
+ else
+ x = new string();
+
+ Contract.Assert(x != null);
+}
+
+After the verification the tool will have results in following format:
+"Assertion at : [Subroutine: <id> Block <blockId> PC <id>] :
+ is (true|false|unproven|unreachable)".
+(PC is a program counter)
+
+.SH AUTHOR
+Written by Alexander Chebaturkin
+.SH COPYRIGHT
+Copyright 2011 Alexander Chebaturkin.
+Released under MIT license.
+.SH WEB SITE
+Visit http://www.mono-project.com for details

Large diffs are not rendered by default.

Oops, something went wrong.
@@ -0,0 +1,81 @@
+using System;
+using System.IO;
+using Mono.CodeContracts.Static.Analysis;
+using Mono.CodeContracts.Static.ControlFlow;
+using Mono.CodeContracts.Static.DataFlowAnalysis;
+using Mono.CodeContracts.Static.DataStructures;
+using Mono.CodeContracts.Static.Providers;
+
+namespace Mono.CodeContracts.Static.AST.Visitors {
+ class CodeVisitor<Variable, Expression, ContextData, EdgeData>
+ : ILVisitorBase<APC, Expression, Variable, bool, bool>,
+ IAnalysis<APC, bool, IILVisitor<APC, Expression, Variable, bool, bool>, EdgeData>
+ where ContextData : IMethodContextProvider {
+ private ICodeLayer<Expression, Variable, ContextData, EdgeData> codeLayer;
+
+ public ContextData Context
+ {
+ get { return this.codeLayer.ILDecoder.ContextProvider; }
+ }
+
+ protected IMetaDataProvider MetaDataProvider
+ {
+ get { return this.codeLayer.MetaDataProvider; }
+ }
+
+ public void Run (ICodeLayer<Expression, Variable, ContextData, EdgeData> codeLayer)
+ {
+ this.codeLayer = codeLayer;
+ codeLayer.CreateForward (this) (true);
+ }
+
+ #region Overrides of ILVisitorBase<APC,Expression,Variable,bool,bool>
+ public override bool DefaultVisit (APC pc, bool data)
+ {
+ return data;
+ }
+ #endregion
+
+ #region Implementation of IAnalysis<APC,bool,IILVisitor<APC,Expression,Variable,bool,bool>,EdgeData>
+ public IILVisitor<APC, Expression, Variable, bool, bool> GetVisitor ()
+ {
+ return this;
+ }
+
+ public virtual bool Join (Pair<APC, APC> edge, bool newstate, bool prevstate, out bool weaker, bool widen)
+ {
+ weaker = false;
+ return true;
+ }
+
+ public bool ImmutableVersion (bool arg)
+ {
+ return arg;
+ }
+
+ public bool MutableVersion (bool arg)
+ {
+ return arg;
+ }
+
+ public bool EdgeConversion (APC @from, APC to, bool isJoinPoint, EdgeData data, bool state)
+ {
+ return state;
+ }
+
+ public bool IsBottom (APC pc, bool state)
+ {
+ return !state;
+ }
+
+ public Predicate<APC> SaveFixPointInfo (IFixPointInfo<APC, bool> fixPointInfo)
+ {
+ return null;
+ }
+
+ public void Dump (Pair<bool, TextWriter> pair)
+ {
+ }
+ #endregion
+ }
+}
Oops, something went wrong.

0 comments on commit e8352f0

Please sign in to comment.