source: extracted/memProperties.mli @ 2601

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

Extraction to ocaml is now working, with a couple of bugs left.
One limitation is that it is not possible to have two files with the
same name in different directories. Therefore this commit renames files
to avoid this situation.

The extracted directory contains:

  1. a snapshot of the .ml(i) files extracted from CerCo? by running ocamlc.opt -extract_ocaml compiler.ma The files have been patched by hand to implement all strings and fix the bugs.
  2. a file PROBLEMS that describes the remaining problems, i.e. bugs and axioms to be implemented

To obtain the compiler, run ocamlbuild compiler.byte.
At the moment it fails because of the three remaining axioms.

File size: 1023 bytes
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 CostLabel
46
47open Proper
48
49open PositiveMap
50
51open Deqsets
52
53open PreIdentifiers
54
55open Errors
56
57open Extralib
58
59open Setoids
60
61open Monad
62
63open Option
64
65open Lists
66
67open Positive
68
69open Identifiers
70
71open Coqlib
72
73open Floats
74
75open Arithmetic
76
77open Char
78
79open String
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.