blob: 0bbad693714546463d64521d44d6ce430584ae30 (
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
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
|
//-----------------------------------------------------------------------------
//
// 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;
namespace BytecodeTranslator {
/// <summary>
/// Class containing several static helper functions to convert
/// from Cci to Boogie Methodology
/// </summary>
class TranslationHelper {
public static Bpl.IToken CciLocationToBoogieToken(IEnumerable<ILocation> locations) {
Bpl.IToken tok = Bpl.Token.NoToken;
return tok;
}
public static Bpl.IToken CciLocationToBoogieToken(ILocation location) {
Bpl.IToken tok = Bpl.Token.NoToken;
return tok;
}
private static int tmpVarCounter = 0;
public static string GenerateTempVarName() {
return "$tmp" + (tmpVarCounter++).ToString();
}
public static string CreateUniqueMethodName(IMethodDefinition method) {
return method.ContainingType.ToString() + "." + method.Name.Value + "$" + method.Type.ResolvedType.ToString();
}
#region Temp Stuff that must be replaced as soon as there is real code to deal with this
public static Bpl.Type CciTypeToBoogie(ITypeDefinition type) {
return Bpl.Type.Int;
}
public static Bpl.Variable TempHeapVar() {
return new Bpl.GlobalVariable(Bpl.Token.NoToken, new Bpl.TypedIdent(Bpl.Token.NoToken, "$Heap", Bpl.Type.Int));
}
public static Bpl.Variable TempThisVar() {
return new Bpl.GlobalVariable(Bpl.Token.NoToken, new Bpl.TypedIdent(Bpl.Token.NoToken, "this", Bpl.Type.Int));
}
#endregion
}
}
|
