source: extracted/cexec.mli @ 2649

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

...

File size: 3.1 KB
Line 
1open Preamble
2
3open Div_and_mod
4
5open Jmeq
6
7open Russell
8
9open Util
10
11open Bool
12
13open Relations
14
15open Nat
16
17open List
18
19open Hints_declaration
20
21open Core_notation
22
23open Pts
24
25open Logic
26
27open Types
28
29open Extralib
30
31open CostLabel
32
33open PositiveMap
34
35open Deqsets
36
37open Lists
38
39open Identifiers
40
41open Integers
42
43open AST
44
45open Division
46
47open Arithmetic
48
49open Extranat
50
51open Vector
52
53open FoldStuff
54
55open BitVector
56
57open Z
58
59open BitVectorZ
60
61open Pointers
62
63open Coqlib
64
65open Values
66
67open Events
68
69open Proper
70
71open ErrorMessages
72
73open Option
74
75open Setoids
76
77open Monad
78
79open Positive
80
81open PreIdentifiers
82
83open Errors
84
85open IOMonad
86
87open IO
88
89open SmallstepExec
90
91open TypeComparison
92
93open ClassifyOp
94
95open Smallstep
96
97open Csyntax
98
99open Extra_bool
100
101open FrontEndVal
102
103open Hide
104
105open ByteValues
106
107open GenMem
108
109open FrontEndMem
110
111open Globalenvs
112
113open Csem
114
115val exec_bool_of_val : Values.val0 -> Csyntax.type0 -> Bool.bool Errors.res
116
117val try_cast_null :
118  GenMem.mem1 -> AST.intsize -> BitVector.bitVector -> Csyntax.type0 ->
119  Csyntax.type0 -> Values.val0 Errors.res
120
121val ptr_like_type : Csyntax.type0 -> Bool.bool
122
123val exec_cast :
124  GenMem.mem1 -> Values.val0 -> Csyntax.type0 -> Csyntax.type0 -> Values.val0
125  Errors.res
126
127val load_value_of_type' :
128  Csyntax.type0 -> GenMem.mem1 -> (Pointers.block, Pointers.offset)
129  Types.prod -> Values.val0 Types.option
130
131val exec_lvalue :
132  Csem.genv0 -> Csem.env -> GenMem.mem1 -> Csyntax.expr -> ((Pointers.block,
133  Pointers.offset) Types.prod, Events.trace) Types.prod Errors.res
134
135val exec_lvalue' :
136  Csem.genv0 -> Csem.env -> GenMem.mem1 -> Csyntax.expr_descr ->
137  Csyntax.type0 -> ((Pointers.block, Pointers.offset) Types.prod,
138  Events.trace) Types.prod Errors.res
139
140val exec_expr :
141  Csem.genv0 -> Csem.env -> GenMem.mem1 -> Csyntax.expr -> (Values.val0,
142  Events.trace) Types.prod Errors.res
143
144val exec_exprlist :
145  Csem.genv0 -> Csem.env -> GenMem.mem1 -> Csyntax.expr List.list ->
146  (Values.val0 List.list, Events.trace) Types.prod Errors.res
147
148val exec_alloc_variables :
149  Csem.env -> GenMem.mem1 -> (AST.ident, Csyntax.type0) Types.prod List.list
150  -> (Csem.env, GenMem.mem1) Types.prod
151
152val exec_bind_parameters :
153  Csem.env -> GenMem.mem1 -> (AST.ident, Csyntax.type0) Types.prod List.list
154  -> Values.val0 List.list -> GenMem.mem1 Errors.res
155
156val is_is_call_cont : Csem.cont -> (__, __) Types.sum
157
158val is_Sskip : Csyntax.statement -> (__, __) Types.sum
159
160val store_value_of_type' :
161  Csyntax.type0 -> GenMem.mem1 -> (Pointers.block, Pointers.offset)
162  Types.prod -> Values.val0 -> GenMem.mem1 Types.option
163
164val exec_step :
165  Csem.genv0 -> Csem.state0 -> (IO.io_out, IO.io_in, (Events.trace,
166  Csem.state0) Types.prod) IOMonad.iO
167
168val make_global0 : Csyntax.clight_program -> Csem.genv0
169
170val make_initial_state0 : Csyntax.clight_program -> Csem.state0 Errors.res
171
172val is_final0 : Csem.state0 -> Integers.int Types.option
173
174val is_final_state : Csem.state0 -> (Integers.int Types.sig0, __) Types.sum
175
176val exec_steps :
177  Nat.nat -> Csem.genv0 -> Csem.state0 -> (IO.io_out, IO.io_in,
178  (Events.trace, Csem.state0) Types.prod) IOMonad.iO
179
180val clight_exec : (IO.io_out, IO.io_in) SmallstepExec.trans_system
181
182val clight_fullexec : (IO.io_out, IO.io_in) SmallstepExec.fullexec
183
Note: See TracBrowser for help on using the repository browser.