source: extracted/eRTLptr_semantics.mli @ 2890

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

Semantics files committed.

File size: 1.6 KB
Line 
1open Preamble
2
3open ExtraMonads
4
5open Deqsets_extra
6
7open State
8
9open Bind_new
10
11open BindLists
12
13open Blocks
14
15open TranslateUtils
16
17open ExtraGlobalenvs
18
19open I8051bis
20
21open String
22
23open Sets
24
25open Listb
26
27open LabelledObjects
28
29open BitVectorTrie
30
31open Graphs
32
33open I8051
34
35open Order
36
37open Registers
38
39open BackEndOps
40
41open Joint
42
43open BEMem
44
45open CostLabel
46
47open Events
48
49open IOMonad
50
51open IO
52
53open Extra_bool
54
55open Coqlib
56
57open Values
58
59open FrontEndVal
60
61open Hide
62
63open ByteValues
64
65open Division
66
67open Z
68
69open BitVectorZ
70
71open Pointers
72
73open GenMem
74
75open FrontEndMem
76
77open Proper
78
79open PositiveMap
80
81open Deqsets
82
83open Extralib
84
85open Lists
86
87open Identifiers
88
89open Exp
90
91open Arithmetic
92
93open Vector
94
95open Div_and_mod
96
97open Util
98
99open FoldStuff
100
101open BitVector
102
103open Extranat
104
105open Integers
106
107open AST
108
109open ErrorMessages
110
111open Option
112
113open Setoids
114
115open Monad
116
117open Jmeq
118
119open Russell
120
121open Positive
122
123open PreIdentifiers
124
125open Bool
126
127open Relations
128
129open Nat
130
131open List
132
133open Hints_declaration
134
135open Core_notation
136
137open Pts
138
139open Logic
140
141open Types
142
143open Errors
144
145open Globalenvs
146
147open Joint_semantics
148
149open SemanticsUtils
150
151open ERTL
152
153open ERTLptr
154
155open ERTL_semantics
156
157val ertlptr_save_frame :
158  Joint_semantics.call_kind -> Types.unit0 -> Joint_semantics.state_pc ->
159  Joint_semantics.state Errors.res
160
161val eval_ertlptr_seq :
162  AST.ident List.list -> 'a1 Joint_semantics.genv_gen -> ERTLptr.ertlptr_seq
163  -> AST.ident -> Joint_semantics.state -> Joint_semantics.state Errors.res
164
165val eRTLptr_sem_uns : __ Joint_semantics.sem_unserialized_params
166
167val eRTLptr_semantics : SemanticsUtils.sem_graph_params
168
Note: See TracBrowser for help on using the repository browser.