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