63 open Hints_declaration
132 Nat.nat -> Nat.nat -> Bool.bool -> BitVector.bitVector ->
133 BitVector.bitVector Types.option
135 val pred_bitsize_of_intsize : AST.intsize -> Nat.nat
137 val signed : AST.signedness -> Bool.bool
140 AST.intsize -> AST.intsize -> AST.signedness -> AST.signedness -> AST.bvint
141 -> AST.bvint Types.option
143 val size_lt_dec : AST.intsize -> AST.intsize -> (__, __) Types.sum
145 val size_not_lt_to_ge : AST.intsize -> AST.intsize -> (__, __) Types.sum
147 val sign_eq_dect : AST.signedness -> AST.signedness -> (__, __) Types.sum
149 val necessary_conditions :
150 AST.intsize -> AST.signedness -> AST.intsize -> AST.signedness -> Bool.bool
152 val assert_int_value :
153 Values.val0 Types.option -> AST.intsize -> BitVector.bitVector Types.option
155 val binop_simplifiable : Csyntax.binary_operation -> Bool.bool
157 val simplify_inside : Csyntax.expr -> Csyntax.expr Types.sig0
160 Csyntax.expr -> AST.intsize -> AST.signedness -> (Bool.bool, Csyntax.expr)
161 Types.prod Types.sig0
163 val simplify_e : Csyntax.expr -> Csyntax.expr
165 val simplify_ls : Csyntax.labeled_statements -> Csyntax.labeled_statements
167 val simplify_statement : Csyntax.statement -> Csyntax.statement
169 val simplify_function : Csyntax.function0 -> Csyntax.function0
171 val simplify_fundef : Csyntax.clight_fundef -> Csyntax.clight_fundef
173 val simplify_program : Csyntax.clight_program -> Csyntax.clight_program