summaryrefslogtreecommitdiff
path: root/BCT/BytecodeTranslator/CLRSemantics.cs
blob: 8b7cda22782b6122cc25b76333103e76b7bd12e7 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
//-----------------------------------------------------------------------------
//
// Copyright (C) Microsoft Corporation.  All Rights Reserved.
//
//-----------------------------------------------------------------------------
using System;
using System.Collections.Generic;
using System.Linq;
using System.Text;

using Microsoft.Cci;
using Microsoft.Cci.MetadataReader;
using Microsoft.Cci.MutableCodeModel;
using Microsoft.Cci.Contracts;
using Microsoft.Cci.ILToCodeModel;

using Bpl = Microsoft.Boogie;
using BytecodeTranslator.TranslationPlugins;

namespace BytecodeTranslator {

  public class CLRSemantics : TraverserFactory {

    public override Translator getTranslator(Sink sink, IDictionary<IUnit, IContractProvider> contractProviders, IDictionary<IUnit, PdbReader> pdbReaders) {
      Translator translator = new BaseTranslator(this, sink, contractProviders, pdbReaders);
      return translator;
    }

    public override ExpressionTraverser MakeExpressionTraverser(Sink sink, StatementTraverser/*?*/ statementTraverser, bool contractContext, bool expressionIsStatement) {
      return new CLRExpressionSemantics(sink, statementTraverser, contractContext, expressionIsStatement);
    }


    public class CLRExpressionSemantics : ExpressionTraverser {

      public CLRExpressionSemantics(Sink sink, StatementTraverser/*?*/ statementTraverser, bool contractContext, bool expressionIsStatement)
        : base(sink, statementTraverser, contractContext, expressionIsStatement) { }
      
    }
  }
}