source: extracted/aSMCosts.mli @ 2601

Last change on this file since 2601 was 2601, checked in by sacerdot, 8 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: 2.0 KB
Line 
1open Preamble
2
3open LabelledObjects
4
5open Coqlib
6
7open Floats
8
9open Arithmetic
10
11open Integers
12
13open AST
14
15open CostLabel
16
17open Proper
18
19open PositiveMap
20
21open Deqsets
22
23open PreIdentifiers
24
25open Errors
26
27open Extralib
28
29open Setoids
30
31open Monad
32
33open Option
34
35open Lists
36
37open Positive
38
39open Identifiers
40
41open Char
42
43open String
44
45open Extranat
46
47open Vector
48
49open Div_and_mod
50
51open Jmeq
52
53open Russell
54
55open Types
56
57open List
58
59open Util
60
61open FoldStuff
62
63open Bool
64
65open Hints_declaration
66
67open Core_notation
68
69open Pts
70
71open Logic
72
73open Relations
74
75open Nat
76
77open BitVector
78
79open ASM
80
81open BitVectorTrie
82
83open Fetch
84
85open StructuredTraces
86
87open AbstractStatus
88
89open Status
90
91open StatusProofs
92
93open Sets
94
95open Listb
96
97open Interpret
98
99val aSM_abstract_status :
100  BitVector.byte BitVectorTrie.bitVectorTrie -> CostLabel.costlabel
101  BitVectorTrie.bitVectorTrie -> StructuredTraces.abstract_status
102
103val trace_any_label_length :
104  BitVector.byte BitVectorTrie.bitVectorTrie -> CostLabel.costlabel
105  BitVectorTrie.bitVectorTrie -> StructuredTraces.trace_ends_with_ret ->
106  Status.status -> Status.status -> StructuredTraces.trace_any_label ->
107  Nat.nat
108
109val all_program_counter_list : Nat.nat -> BitVector.bitVector List.list
110
111val compute_paid_trace_any_label :
112  BitVector.byte BitVectorTrie.bitVectorTrie -> CostLabel.costlabel
113  BitVectorTrie.bitVectorTrie -> StructuredTraces.trace_ends_with_ret ->
114  Status.status -> Status.status -> StructuredTraces.trace_any_label ->
115  Nat.nat
116
117val compute_paid_trace_label_label :
118  BitVector.byte BitVectorTrie.bitVectorTrie -> CostLabel.costlabel
119  BitVectorTrie.bitVectorTrie -> StructuredTraces.trace_ends_with_ret ->
120  Status.status -> Status.status -> StructuredTraces.trace_label_label ->
121  Nat.nat
122
123val block_cost' :
124  BitVector.byte BitVectorTrie.bitVectorTrie -> BitVector.word -> Nat.nat ->
125  CostLabel.costlabel BitVectorTrie.bitVectorTrie -> Bool.bool -> Nat.nat
126  Types.sig0
127
128val block_cost :
129  BitVector.byte BitVectorTrie.bitVectorTrie -> BitVector.word ->
130  CostLabel.costlabel BitVectorTrie.bitVectorTrie -> Nat.nat Types.sig0
131
Note: See TracBrowser for help on using the repository browser.