source: driver/extracted/clight_abstract.mli @ 3106

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

More code extracted, used to debug the compiler.

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