source: driver/extracted/joint_LTL_LIN_semantics.mli @ 3106

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

New extraction.

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