source: extracted/clight_classified_system.mli @ 2803

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

More code extracted, used to debug the compiler.

File size: 1.1 KB
Line 
1open Preamble
2
3open IOMonad
4
5open IO
6
7open Sets
8
9open Listb
10
11open StructuredTraces
12
13open TypeComparison
14
15open ClassifyOp
16
17open Events
18
19open Smallstep
20
21open CostLabel
22
23open Csyntax
24
25open Extra_bool
26
27open Coqlib
28
29open Values
30
31open FrontEndVal
32
33open Hide
34
35open ByteValues
36
37open Division
38
39open Z
40
41open BitVectorZ
42
43open Pointers
44
45open GenMem
46
47open FrontEndMem
48
49open Proper
50
51open PositiveMap
52
53open Deqsets
54
55open Extralib
56
57open Lists
58
59open Identifiers
60
61open Exp
62
63open Arithmetic
64
65open Vector
66
67open Div_and_mod
68
69open Util
70
71open FoldStuff
72
73open BitVector
74
75open Extranat
76
77open Integers
78
79open AST
80
81open ErrorMessages
82
83open Option
84
85open Setoids
86
87open Monad
88
89open Jmeq
90
91open Russell
92
93open Positive
94
95open PreIdentifiers
96
97open Bool
98
99open Relations
100
101open Nat
102
103open List
104
105open Hints_declaration
106
107open Core_notation
108
109open Pts
110
111open Logic
112
113open Types
114
115open Errors
116
117open Globalenvs
118
119open Csem
120
121open Clight_abstract
122
123open SmallstepExec
124
125open Cexec
126
127open Executions
128
129open Measurable
130
131val clight_stack_ident :
132  Clight_abstract.cl_genv -> Clight_abstract.clight_state -> AST.ident
133
134val clight_pcs : Measurable.preclassified_system
135
Note: See TracBrowser for help on using the repository browser.