source: driver/extracted/simplifyCasts.mli @ 3106

Last change on this file since 3106 was 3059, checked in by sacerdot, 7 years ago

New extraction

File size: 2.3 KB
Line 
1open Preamble
2
3open CostLabel
4
5open Coqlib
6
7open Proper
8
9open PositiveMap
10
11open Deqsets
12
13open ErrorMessages
14
15open PreIdentifiers
16
17open Errors
18
19open Extralib
20
21open Lists
22
23open Positive
24
25open Identifiers
26
27open Exp
28
29open Arithmetic
30
31open Vector
32
33open Div_and_mod
34
35open Util
36
37open FoldStuff
38
39open BitVector
40
41open Jmeq
42
43open Russell
44
45open List
46
47open Setoids
48
49open Monad
50
51open Option
52
53open Extranat
54
55open Bool
56
57open Relations
58
59open Nat
60
61open Integers
62
63open Hints_declaration
64
65open Core_notation
66
67open Pts
68
69open Logic
70
71open Types
72
73open AST
74
75open Csyntax
76
77open TypeComparison
78
79open ClassifyOp
80
81open Smallstep
82
83open Extra_bool
84
85open FrontEndVal
86
87open Hide
88
89open ByteValues
90
91open GenMem
92
93open FrontEndMem
94
95open Globalenvs
96
97open Csem
98
99open SmallstepExec
100
101open Division
102
103open Z
104
105open BitVectorZ
106
107open Pointers
108
109open Values
110
111open Events
112
113open IOMonad
114
115open IO
116
117open Cexec
118
119open Casts
120
121open CexecInd
122
123open Sets
124
125open Listb
126
127open Star
128
129open Frontend_misc
130
131val reduce_bits :
132  Nat.nat -> Nat.nat -> Bool.bool -> BitVector.bitVector ->
133  BitVector.bitVector Types.option
134
135val pred_bitsize_of_intsize : AST.intsize -> Nat.nat
136
137val signed : AST.signedness -> Bool.bool
138
139val simplify_int :
140  AST.intsize -> AST.intsize -> AST.signedness -> AST.signedness -> AST.bvint
141  -> AST.bvint Types.option
142
143val size_lt_dec : AST.intsize -> AST.intsize -> (__, __) Types.sum
144
145val size_not_lt_to_ge : AST.intsize -> AST.intsize -> (__, __) Types.sum
146
147val sign_eq_dect : AST.signedness -> AST.signedness -> (__, __) Types.sum
148
149val necessary_conditions :
150  AST.intsize -> AST.signedness -> AST.intsize -> AST.signedness -> Bool.bool
151
152val assert_int_value :
153  Values.val0 Types.option -> AST.intsize -> BitVector.bitVector Types.option
154
155val binop_simplifiable : Csyntax.binary_operation -> Bool.bool
156
157val simplify_inside : Csyntax.expr -> Csyntax.expr Types.sig0
158
159val simplify_expr :
160  Csyntax.expr -> AST.intsize -> AST.signedness -> (Bool.bool, Csyntax.expr)
161  Types.prod Types.sig0
162
163val simplify_e : Csyntax.expr -> Csyntax.expr
164
165val simplify_ls : Csyntax.labeled_statements -> Csyntax.labeled_statements
166
167val simplify_statement : Csyntax.statement -> Csyntax.statement
168
169val simplify_function : Csyntax.function0 -> Csyntax.function0
170
171val simplify_fundef : Csyntax.clight_fundef -> Csyntax.clight_fundef
172
173val simplify_program : Csyntax.clight_program -> Csyntax.clight_program
174
Note: See TracBrowser for help on using the repository browser.