95 open Hints_declaration
111 (** val clight_labelled : Csem.state -> Bool.bool **)
112 let clight_labelled = function
113 | Csem.State (f, s0, k, e, m) ->
115 | Csyntax.Sskip -> Bool.False
116 | Csyntax.Sassign (x, x0) -> Bool.False
117 | Csyntax.Scall (x, x0, x1) -> Bool.False
118 | Csyntax.Ssequence (x, x0) -> Bool.False
119 | Csyntax.Sifthenelse (x, x0, x1) -> Bool.False
120 | Csyntax.Swhile (x, x0) -> Bool.False
121 | Csyntax.Sdowhile (x, x0) -> Bool.False
122 | Csyntax.Sfor (x, x0, x1, x2) -> Bool.False
123 | Csyntax.Sbreak -> Bool.False
124 | Csyntax.Scontinue -> Bool.False
125 | Csyntax.Sreturn x -> Bool.False
126 | Csyntax.Sswitch (x, x0) -> Bool.False
127 | Csyntax.Slabel (x, x0) -> Bool.False
128 | Csyntax.Sgoto x -> Bool.False
129 | Csyntax.Scost (x, x0) -> Bool.True)
130 | Csem.Callstate (x, x0, x1, x2, x3) -> Bool.False
131 | Csem.Returnstate (x, x0, x1) -> Bool.False
132 | Csem.Finalstate x -> Bool.False
142 open StructuredTraces
144 (** val clight_classify : Csem.state -> StructuredTraces.status_class **)
145 let clight_classify = function
146 | Csem.State (x, x0, x1, x2, x3) -> StructuredTraces.Cl_other
147 | Csem.Callstate (x, x0, x1, x2, x3) -> StructuredTraces.Cl_call
148 | Csem.Returnstate (x, x0, x1) -> StructuredTraces.Cl_return
149 | Csem.Finalstate x -> StructuredTraces.Cl_other
151 type clight_state = Csem.state
153 type cl_genv = Csem.genv
155 type cl_env = Csem.env
157 type cl_cont = Csem.cont
160 Csyntax.function0 -> Csyntax.statement -> Csem.cont -> Csem.env ->
161 GenMem.mem -> Csem.state **)
162 let clState x x0 x1 x2 x3 =
163 Csem.State (x, x0, x1, x2, x3)
165 (** val clReturnstate :
166 Values.val0 -> Csem.cont -> GenMem.mem -> Csem.state **)
167 let clReturnstate x x0 x1 =
168 Csem.Returnstate (x, x0, x1)
170 (** val clCallstate :
171 AST.ident -> Csyntax.clight_fundef -> Values.val0 List.list -> Csem.cont
172 -> GenMem.mem -> Csem.state **)
173 let clCallstate x x0 x1 x2 x3 =
174 Csem.Callstate (x, x0, x1, x2, x3)
176 (** val clKseq : Csyntax.statement -> Csem.cont -> Csem.cont **)