95 open Hints_declaration
111 open Cminor_semantics
113 type cminor_state = Cminor_semantics.state
115 (** val cminor_labelled : Cminor_semantics.state -> Bool.bool **)
116 let cminor_labelled = function
117 | Cminor_semantics.State (x, st, x0, x3, x4, x5, x7) ->
119 | Cminor_syntax.St_skip -> Bool.False
120 | Cminor_syntax.St_assign (x8, x9, x10) -> Bool.False
121 | Cminor_syntax.St_store (x8, x9, x10) -> Bool.False
122 | Cminor_syntax.St_call (x8, x9, x10) -> Bool.False
123 | Cminor_syntax.St_seq (x8, x9) -> Bool.False
124 | Cminor_syntax.St_ifthenelse (x8, x9, x10, x11, x12) -> Bool.False
125 | Cminor_syntax.St_return x8 -> Bool.False
126 | Cminor_syntax.St_label (x8, x9) -> Bool.False
127 | Cminor_syntax.St_goto x8 -> Bool.False
128 | Cminor_syntax.St_cost (x8, x9) -> Bool.True)
129 | Cminor_semantics.Callstate (x, x0, x1, x2, x3) -> Bool.False
130 | Cminor_semantics.Returnstate (x, x0, x1) -> Bool.False
131 | Cminor_semantics.Finalstate x -> Bool.False
137 open StructuredTraces
139 (** val cminor_classify :
140 Cminor_semantics.state -> StructuredTraces.status_class **)
141 let cminor_classify = function
142 | Cminor_semantics.State (x, x0, x1, x4, x5, x6, x8) ->
143 StructuredTraces.Cl_other
144 | Cminor_semantics.Callstate (x, x0, x1, x2, x3) -> StructuredTraces.Cl_call
145 | Cminor_semantics.Returnstate (x, x0, x1) -> StructuredTraces.Cl_return
146 | Cminor_semantics.Finalstate x -> StructuredTraces.Cl_other
148 type cm_genv = Cminor_semantics.genv
150 type cm_env = Cminor_semantics.env
152 type cm_cont = Cminor_semantics.cont
154 (** val cm_eval_expr :
155 Cminor_semantics.genv -> AST.typ -> Cminor_syntax.expr ->
156 Cminor_semantics.env -> Pointers.block -> GenMem.mem -> (Events.trace,
157 Values.val0) Types.prod Errors.res **)
158 let cm_eval_expr ge ty0 e en sp m =
159 Cminor_semantics.eval_expr ge ty0 e en sp m
162 Cminor_syntax.internal_function -> Cminor_syntax.stmt ->
163 Cminor_semantics.env -> GenMem.mem -> Pointers.block ->
164 Cminor_semantics.cont -> Cminor_semantics.stack -> Cminor_semantics.state **)
165 let cmState f s en m sp k st =
166 Cminor_semantics.State (f, s, en, m, sp, k, st)
168 (** val cmReturnstate :
169 Values.val0 Types.option -> GenMem.mem -> Cminor_semantics.stack ->
170 Cminor_semantics.state **)
171 let cmReturnstate x x0 x1 =
172 Cminor_semantics.Returnstate (x, x0, x1)
174 (** val cmCallstate :
175 AST.ident -> Cminor_syntax.internal_function AST.fundef -> Values.val0
176 List.list -> GenMem.mem -> Cminor_semantics.stack ->
177 Cminor_semantics.state **)
178 let cmCallstate x x0 x1 x2 x3 =
179 Cminor_semantics.Callstate (x, x0, x1, x2, x3)