source: extracted/cexec.mli @ 2746

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

Extracted code for the whole compiler.
The space cost model is not there yet.

I have fixed by hand the few extraction problems
(i.e. composed coercions not extracted and type
definitions with wrong syntax).

I have also changed all axioms to be implemented
so that they do not fail at initialization time.

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