19 open Hints_declaration
117 val exec_bool_of_val : Values.val0 -> Csyntax.type0 -> Bool.bool Errors.res
120 GenMem.mem -> AST.intsize -> BitVector.bitVector -> Csyntax.type0 ->
121 Csyntax.type0 -> Values.val0 Errors.res
123 val ptr_like_type : Csyntax.type0 -> Bool.bool
126 GenMem.mem -> Values.val0 -> Csyntax.type0 -> Csyntax.type0 -> Values.val0
129 val load_value_of_type' :
130 Csyntax.type0 -> GenMem.mem -> (Pointers.block, Pointers.offset) Types.prod
131 -> Values.val0 Types.option
134 Csem.genv -> Csem.env -> GenMem.mem -> Csyntax.expr -> ((Pointers.block,
135 Pointers.offset) Types.prod, Events.trace) Types.prod Errors.res
138 Csem.genv -> Csem.env -> GenMem.mem -> Csyntax.expr_descr -> Csyntax.type0
139 -> ((Pointers.block, Pointers.offset) Types.prod, Events.trace) Types.prod
143 Csem.genv -> Csem.env -> GenMem.mem -> Csyntax.expr -> (Values.val0,
144 Events.trace) Types.prod Errors.res
147 Csem.genv -> Csem.env -> GenMem.mem -> Csyntax.expr List.list ->
148 (Values.val0 List.list, Events.trace) Types.prod Errors.res
150 val exec_alloc_variables :
151 Csem.env -> GenMem.mem -> (AST.ident, Csyntax.type0) Types.prod List.list
152 -> (Csem.env, GenMem.mem) Types.prod
154 val exec_bind_parameters :
155 Csem.env -> GenMem.mem -> (AST.ident, Csyntax.type0) Types.prod List.list
156 -> Values.val0 List.list -> GenMem.mem Errors.res
158 val is_is_call_cont : Csem.cont -> (__, __) Types.sum
160 val is_Sskip : Csyntax.statement -> (__, __) Types.sum
162 val store_value_of_type' :
163 Csyntax.type0 -> GenMem.mem -> (Pointers.block, Pointers.offset) Types.prod
164 -> Values.val0 -> GenMem.mem Types.option
167 Csem.genv -> Csem.state -> (IO.io_out, IO.io_in, (Events.trace, Csem.state)
168 Types.prod) IOMonad.iO
170 val make_global : Csyntax.clight_program -> Csem.genv
172 val make_initial_state : Csyntax.clight_program -> Csem.state Errors.res
174 val is_final : Csem.state -> Integers.int Types.option
176 val is_final_state : Csem.state -> (Integers.int Types.sig0, __) Types.sum
179 Nat.nat -> Csem.genv -> Csem.state -> (IO.io_out, IO.io_in, (Events.trace,
180 Csem.state) Types.prod) IOMonad.iO
182 val clight_exec : (IO.io_out, IO.io_in) SmallstepExec.trans_system
184 val clight_fullexec : (IO.io_out, IO.io_in) SmallstepExec.fullexec