95 open Hints_declaration
111 val clight_labelled : Csem.state -> Bool.bool
121 open StructuredTraces
123 val clight_classify : Csem.state -> StructuredTraces.status_class
125 type clight_state = Csem.state
127 type cl_genv = Csem.genv
129 type cl_env = Csem.env
131 type cl_cont = Csem.cont
134 Csyntax.function0 -> Csyntax.statement -> Csem.cont -> Csem.env ->
135 GenMem.mem -> Csem.state
137 val clReturnstate : Values.val0 -> Csem.cont -> GenMem.mem -> Csem.state
140 AST.ident -> Csyntax.clight_fundef -> Values.val0 List.list -> Csem.cont ->
141 GenMem.mem -> Csem.state
143 val clKseq : Csyntax.statement -> Csem.cont -> Csem.cont