source: driver/extracted/lIN_semantics.ml @ 3106

Last change on this file since 3106 was 2951, checked in by sacerdot, 7 years ago

New extraction. Novely: a pre-main is used in the back-end. Initialization
of global data is performed in LINToASM.

Note: the cost-emission of the initialization costlabel in the front-end is
virtual, but not performed in the traces I generate and print. To be fixed
(how?)

File size: 1.5 KB
Line 
1open Preamble
2
3open ExtraMonads
4
5open Deqsets_extra
6
7open State
8
9open Bind_new
10
11open BindLists
12
13open Blocks
14
15open TranslateUtils
16
17open ExtraGlobalenvs
18
19open I8051bis
20
21open BEMem
22
23open Events
24
25open IOMonad
26
27open IO
28
29open Joint_semantics
30
31open SemanticsUtils
32
33open Extra_bool
34
35open Coqlib
36
37open Values
38
39open FrontEndVal
40
41open GenMem
42
43open FrontEndMem
44
45open Globalenvs
46
47open String
48
49open Sets
50
51open Listb
52
53open LabelledObjects
54
55open BitVectorTrie
56
57open Graphs
58
59open I8051
60
61open Order
62
63open Registers
64
65open CostLabel
66
67open Hide
68
69open Proper
70
71open PositiveMap
72
73open Deqsets
74
75open ErrorMessages
76
77open PreIdentifiers
78
79open Errors
80
81open Extralib
82
83open Lists
84
85open Identifiers
86
87open Integers
88
89open AST
90
91open Division
92
93open Exp
94
95open Arithmetic
96
97open Setoids
98
99open Monad
100
101open Option
102
103open Extranat
104
105open Vector
106
107open Div_and_mod
108
109open Jmeq
110
111open Russell
112
113open List
114
115open Util
116
117open FoldStuff
118
119open BitVector
120
121open Types
122
123open Bool
124
125open Relations
126
127open Nat
128
129open Hints_declaration
130
131open Core_notation
132
133open Pts
134
135open Logic
136
137open Positive
138
139open Z
140
141open BitVectorZ
142
143open Pointers
144
145open ByteValues
146
147open BackEndOps
148
149open Joint
150
151open Joint_LTL_LIN
152
153open Joint_LTL_LIN_semantics
154
155open LIN
156
157(** val lIN_semantics : Joint_semantics.sem_params **)
158let lIN_semantics =
159  SemanticsUtils.sem_lin_params_to_sem_params { SemanticsUtils.slp_pars =
160    (Joint.lp_to_p__o__stmt_pars__o__uns_pars LIN.lIN);
161    SemanticsUtils.slp_sup = (fun _ ->
162    Joint_LTL_LIN_semantics.lTL_LIN_semantics);
163    SemanticsUtils.lin_pre_main_generator = LIN.lIN_premain }
164
Note: See TracBrowser for help on using the repository browser.