source: extracted/semantics_blocks.mli @ 2881

Last change on this file since 2881 was 2881, checked in by sacerdot, 8 years ago

...

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