/[eiffelstudio]/branches/eth/eve/Src/framework/eiffel2boogie/translation/e2b_shared_context.e
ViewVC logotype

Contents of /branches/eth/eve/Src/framework/eiffel2boogie/translation/e2b_shared_context.e

Parent Directory Parent Directory | Revision Log Revision Log


Revision 93597 - (show annotations)
Tue Dec 3 00:48:44 2013 UTC (5 years, 10 months ago) by julian
File size: 1253 byte(s)
AutoProof: special translation for lemma and functional
1 note
2 description: "Summary description for {E2B_SHARED_TRANSLATOR}."
3 author: ""
4 date: "$Date$"
5 revision: "$Revision$"
6
7 class
8 E2B_SHARED_CONTEXT
9
10 feature {NONE} -- Access: stateful
11
12 translation_pool: E2B_TRANSLATION_POOL
13 -- Shared translation pool.
14 once
15 create Result.make
16 end
17
18 boogie_universe: IV_UNIVERSE
19 -- Shared boogie universe.
20 do
21 Result := boogie_universe_cell.item
22 end
23
24 autoproof_errors: LINKED_LIST [E2B_AUTOPROOF_ERROR]
25 -- List of autoproof errors.
26 once
27 create Result.make
28 end
29
30 feature {NONE} -- Access: stateless
31
32 name_translator: E2B_NAME_TRANSLATOR
33 -- Shared global name translator.
34 once
35 create Result
36 end
37
38 translation_mapping: E2B_SPECIAL_MAPPING
39 -- Shared mapping for special translations.
40 once
41 create Result.make
42 end
43
44 messages: E2B_MESSAGES
45 -- Messages used in AutoProof.
46 once
47 create Result
48 end
49
50 feature -- Access (public)
51
52 options: E2B_OPTIONS
53 -- Shared translation options.
54 once
55 create Result.make
56 end
57
58 helper: E2B_HELPER
59 -- Shared helper.
60 once
61 create Result
62 end
63
64 feature {NONE} -- Implementation
65
66 boogie_universe_cell: CELL [IV_UNIVERSE]
67 -- Once cell holding shared boogie universe instance.
68 once
69 create Result.put (Void)
70 end
71
72 end

Properties

Name Value
svn:eol-style native
svn:keywords Author Date ID Revision

  ViewVC Help
Powered by ViewVC 1.1.23