source: extracted/joint_LTL_LIN_semantics.mli @ 2829

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

Semantics files committed.

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