source: extracted/memProperties.mli @ 2717

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

Extracted code for the whole compiler.
The space cost model is not there yet.

I have fixed by hand the few extraction problems
(i.e. composed coercions not extracted and type
definitions with wrong syntax).

I have also changed all axioms to be implemented
so that they do not fail at initialization time.

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