source: driver/extracted/cminor_abstract.ml @ 3106

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

Cminor semantics exported.

File size: 3.3 KB
Line 
1open Preamble
2
3open FrontEndOps
4
5open Cminor_syntax
6
7open SmallstepExec
8
9open Extra_bool
10
11open Globalenvs
12
13open IOMonad
14
15open IO
16
17open FrontEndVal
18
19open Hide
20
21open ByteValues
22
23open GenMem
24
25open FrontEndMem
26
27open CostLabel
28
29open Proper
30
31open PositiveMap
32
33open Deqsets
34
35open Extralib
36
37open Lists
38
39open Identifiers
40
41open Integers
42
43open AST
44
45open Division
46
47open Exp
48
49open Arithmetic
50
51open Extranat
52
53open Vector
54
55open FoldStuff
56
57open BitVector
58
59open Z
60
61open BitVectorZ
62
63open Pointers
64
65open ErrorMessages
66
67open Option
68
69open Setoids
70
71open Monad
72
73open Positive
74
75open PreIdentifiers
76
77open Errors
78
79open Div_and_mod
80
81open Jmeq
82
83open Russell
84
85open Util
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 Coqlib
106
107open Values
108
109open Events
110
111open Cminor_semantics
112
113type cminor_state = Cminor_semantics.state
114
115(** val cminor_labelled : Cminor_semantics.state -> Bool.bool **)
116let cminor_labelled = function
117| Cminor_semantics.State (x, st, x0, x3, x4, x5, x7) ->
118  (match st with
119   | Cminor_syntax.St_skip -> Bool.False
120   | Cminor_syntax.St_assign (x8, x9, x10) -> Bool.False
121   | Cminor_syntax.St_store (x8, x9, x10) -> Bool.False
122   | Cminor_syntax.St_call (x8, x9, x10) -> Bool.False
123   | Cminor_syntax.St_seq (x8, x9) -> Bool.False
124   | Cminor_syntax.St_ifthenelse (x8, x9, x10, x11, x12) -> Bool.False
125   | Cminor_syntax.St_return x8 -> Bool.False
126   | Cminor_syntax.St_label (x8, x9) -> Bool.False
127   | Cminor_syntax.St_goto x8 -> Bool.False
128   | Cminor_syntax.St_cost (x8, x9) -> Bool.True)
129| Cminor_semantics.Callstate (x, x0, x1, x2, x3) -> Bool.False
130| Cminor_semantics.Returnstate (x, x0, x1) -> Bool.False
131| Cminor_semantics.Finalstate x -> Bool.False
132
133open Sets
134
135open Listb
136
137open StructuredTraces
138
139(** val cminor_classify :
140    Cminor_semantics.state -> StructuredTraces.status_class **)
141let cminor_classify = function
142| Cminor_semantics.State (x, x0, x1, x4, x5, x6, x8) ->
143  StructuredTraces.Cl_other
144| Cminor_semantics.Callstate (x, x0, x1, x2, x3) -> StructuredTraces.Cl_call
145| Cminor_semantics.Returnstate (x, x0, x1) -> StructuredTraces.Cl_return
146| Cminor_semantics.Finalstate x -> StructuredTraces.Cl_other
147
148type cm_genv = Cminor_semantics.genv
149
150type cm_env = Cminor_semantics.env
151
152type cm_cont = Cminor_semantics.cont
153
154(** val cm_eval_expr :
155    Cminor_semantics.genv -> AST.typ -> Cminor_syntax.expr ->
156    Cminor_semantics.env -> Pointers.block -> GenMem.mem -> (Events.trace,
157    Values.val0) Types.prod Errors.res **)
158let cm_eval_expr ge ty0 e en sp m =
159  Cminor_semantics.eval_expr ge ty0 e en sp m
160
161(** val cmState :
162    Cminor_syntax.internal_function -> Cminor_syntax.stmt ->
163    Cminor_semantics.env -> GenMem.mem -> Pointers.block ->
164    Cminor_semantics.cont -> Cminor_semantics.stack -> Cminor_semantics.state **)
165let cmState f s en m sp k st =
166  Cminor_semantics.State (f, s, en, m, sp, k, st)
167
168(** val cmReturnstate :
169    Values.val0 Types.option -> GenMem.mem -> Cminor_semantics.stack ->
170    Cminor_semantics.state **)
171let cmReturnstate x x0 x1 =
172  Cminor_semantics.Returnstate (x, x0, x1)
173
174(** val cmCallstate :
175    AST.ident -> Cminor_syntax.internal_function AST.fundef -> Values.val0
176    List.list -> GenMem.mem -> Cminor_semantics.stack ->
177    Cminor_semantics.state **)
178let cmCallstate x x0 x1 x2 x3 =
179  Cminor_semantics.Callstate (x, x0, x1, x2, x3)
180
Note: See TracBrowser for help on using the repository browser.