source: driver/extracted/cexec.mli @ 3106

Last change on this file since 3106 was 2773, checked in by sacerdot, 7 years ago
  1. everything extracted again after all bugs in Matita's extraction have been fixed. No more need for manual patching
  2. new extraction after file reorganization (by James)
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 Exp
48
49open Arithmetic
50
51open Extranat
52
53open Vector
54
55open FoldStuff
56
57open BitVector
58
59open Z
60
61open BitVectorZ
62
63open Pointers
64
65open Coqlib
66
67open Values
68
69open Events
70
71open Proper
72
73open ErrorMessages
74
75open Option
76
77open Setoids
78
79open Monad
80
81open Positive
82
83open PreIdentifiers
84
85open Errors
86
87open IOMonad
88
89open IO
90
91open SmallstepExec
92
93open TypeComparison
94
95open ClassifyOp
96
97open Smallstep
98
99open Csyntax
100
101open Extra_bool
102
103open FrontEndVal
104
105open Hide
106
107open ByteValues
108
109open GenMem
110
111open FrontEndMem
112
113open Globalenvs
114
115open Csem
116
117val exec_bool_of_val : Values.val0 -> Csyntax.type0 -> Bool.bool Errors.res
118
119val try_cast_null :
120  GenMem.mem -> AST.intsize -> BitVector.bitVector -> Csyntax.type0 ->
121  Csyntax.type0 -> Values.val0 Errors.res
122
123val ptr_like_type : Csyntax.type0 -> Bool.bool
124
125val exec_cast :
126  GenMem.mem -> Values.val0 -> Csyntax.type0 -> Csyntax.type0 -> Values.val0
127  Errors.res
128
129val load_value_of_type' :
130  Csyntax.type0 -> GenMem.mem -> (Pointers.block, Pointers.offset) Types.prod
131  -> Values.val0 Types.option
132
133val exec_lvalue :
134  Csem.genv -> Csem.env -> GenMem.mem -> Csyntax.expr -> ((Pointers.block,
135  Pointers.offset) Types.prod, Events.trace) Types.prod Errors.res
136
137val exec_lvalue' :
138  Csem.genv -> Csem.env -> GenMem.mem -> Csyntax.expr_descr -> Csyntax.type0
139  -> ((Pointers.block, Pointers.offset) Types.prod, Events.trace) Types.prod
140  Errors.res
141
142val exec_expr :
143  Csem.genv -> Csem.env -> GenMem.mem -> Csyntax.expr -> (Values.val0,
144  Events.trace) Types.prod Errors.res
145
146val exec_exprlist :
147  Csem.genv -> Csem.env -> GenMem.mem -> Csyntax.expr List.list ->
148  (Values.val0 List.list, Events.trace) Types.prod Errors.res
149
150val exec_alloc_variables :
151  Csem.env -> GenMem.mem -> (AST.ident, Csyntax.type0) Types.prod List.list
152  -> (Csem.env, GenMem.mem) Types.prod
153
154val 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
157
158val is_is_call_cont : Csem.cont -> (__, __) Types.sum
159
160val is_Sskip : Csyntax.statement -> (__, __) Types.sum
161
162val store_value_of_type' :
163  Csyntax.type0 -> GenMem.mem -> (Pointers.block, Pointers.offset) Types.prod
164  -> Values.val0 -> GenMem.mem Types.option
165
166val exec_step :
167  Csem.genv -> Csem.state -> (IO.io_out, IO.io_in, (Events.trace, Csem.state)
168  Types.prod) IOMonad.iO
169
170val make_global : Csyntax.clight_program -> Csem.genv
171
172val make_initial_state : Csyntax.clight_program -> Csem.state Errors.res
173
174val is_final : Csem.state -> Integers.int Types.option
175
176val is_final_state : Csem.state -> (Integers.int Types.sig0, __) Types.sum
177
178val exec_steps :
179  Nat.nat -> Csem.genv -> Csem.state -> (IO.io_out, IO.io_in, (Events.trace,
180  Csem.state) Types.prod) IOMonad.iO
181
182val clight_exec : (IO.io_out, IO.io_in) SmallstepExec.trans_system
183
184val clight_fullexec : (IO.io_out, IO.io_in) SmallstepExec.fullexec
185
Note: See TracBrowser for help on using the repository browser.