source: driver/extracted/cminor_abstract.mli @ 3085

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

Cminor semantics exported.

File size: 1.8 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
115val cminor_labelled : Cminor_semantics.state -> Bool.bool
116
117open Sets
118
119open Listb
120
121open StructuredTraces
122
123val cminor_classify : Cminor_semantics.state -> StructuredTraces.status_class
124
125type cm_genv = Cminor_semantics.genv
126
127type cm_env = Cminor_semantics.env
128
129type cm_cont = Cminor_semantics.cont
130
131val cm_eval_expr :
132  Cminor_semantics.genv -> AST.typ -> Cminor_syntax.expr ->
133  Cminor_semantics.env -> Pointers.block -> GenMem.mem -> (Events.trace,
134  Values.val0) Types.prod Errors.res
135
136val cmState :
137  Cminor_syntax.internal_function -> Cminor_syntax.stmt ->
138  Cminor_semantics.env -> GenMem.mem -> Pointers.block ->
139  Cminor_semantics.cont -> Cminor_semantics.stack -> Cminor_semantics.state
140
141val cmReturnstate :
142  Values.val0 Types.option -> GenMem.mem -> Cminor_semantics.stack ->
143  Cminor_semantics.state
144
145val cmCallstate :
146  AST.ident -> Cminor_syntax.internal_function AST.fundef -> Values.val0
147  List.list -> GenMem.mem -> Cminor_semantics.stack -> Cminor_semantics.state
148
Note: See TracBrowser for help on using the repository browser.