source: driver/extracted/clight_abstract.ml @ 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: 2.8 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
111(** val clight_labelled : Csem.state -> Bool.bool **)
112let clight_labelled = function
113| Csem.State (f, s0, k, e, m) ->
114  (match s0 with
115   | Csyntax.Sskip -> Bool.False
116   | Csyntax.Sassign (x, x0) -> Bool.False
117   | Csyntax.Scall (x, x0, x1) -> Bool.False
118   | Csyntax.Ssequence (x, x0) -> Bool.False
119   | Csyntax.Sifthenelse (x, x0, x1) -> Bool.False
120   | Csyntax.Swhile (x, x0) -> Bool.False
121   | Csyntax.Sdowhile (x, x0) -> Bool.False
122   | Csyntax.Sfor (x, x0, x1, x2) -> Bool.False
123   | Csyntax.Sbreak -> Bool.False
124   | Csyntax.Scontinue -> Bool.False
125   | Csyntax.Sreturn x -> Bool.False
126   | Csyntax.Sswitch (x, x0) -> Bool.False
127   | Csyntax.Slabel (x, x0) -> Bool.False
128   | Csyntax.Sgoto x -> Bool.False
129   | Csyntax.Scost (x, x0) -> Bool.True)
130| Csem.Callstate (x, x0, x1, x2, x3) -> Bool.False
131| Csem.Returnstate (x, x0, x1) -> Bool.False
132| Csem.Finalstate x -> Bool.False
133
134open IOMonad
135
136open IO
137
138open Sets
139
140open Listb
141
142open StructuredTraces
143
144(** val clight_classify : Csem.state -> StructuredTraces.status_class **)
145let clight_classify = function
146| Csem.State (x, x0, x1, x2, x3) -> StructuredTraces.Cl_other
147| Csem.Callstate (x, x0, x1, x2, x3) -> StructuredTraces.Cl_call
148| Csem.Returnstate (x, x0, x1) -> StructuredTraces.Cl_return
149| Csem.Finalstate x -> StructuredTraces.Cl_other
150
151type clight_state = Csem.state
152
153type cl_genv = Csem.genv
154
155type cl_env = Csem.env
156
157type cl_cont = Csem.cont
158
159(** val clState :
160    Csyntax.function0 -> Csyntax.statement -> Csem.cont -> Csem.env ->
161    GenMem.mem -> Csem.state **)
162let clState x x0 x1 x2 x3 =
163  Csem.State (x, x0, x1, x2, x3)
164
165(** val clReturnstate :
166    Values.val0 -> Csem.cont -> GenMem.mem -> Csem.state **)
167let clReturnstate x x0 x1 =
168  Csem.Returnstate (x, x0, x1)
169
170(** val clCallstate :
171    AST.ident -> Csyntax.clight_fundef -> Values.val0 List.list -> Csem.cont
172    -> GenMem.mem -> Csem.state **)
173let clCallstate x x0 x1 x2 x3 =
174  Csem.Callstate (x, x0, x1, x2, x3)
175
176(** val clKseq : Csyntax.statement -> Csem.cont -> Csem.cont **)
177let clKseq x x0 =
178  Csem.Kseq (x, x0)
179
Note: See TracBrowser for help on using the repository browser.