source: extracted/aSMCostsSplit.mli @ 2649

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

...

File size: 1.4 KB
Line 
1open Preamble
2
3open StructuredTraces
4
5open AbstractStatus
6
7open Status
8
9open StatusProofs
10
11open Sets
12
13open Listb
14
15open Interpret
16
17open BitVectorTrie
18
19open Fetch
20
21open String
22
23open LabelledObjects
24
25open Arithmetic
26
27open Integers
28
29open AST
30
31open CostLabel
32
33open Proper
34
35open PositiveMap
36
37open Deqsets
38
39open ErrorMessages
40
41open PreIdentifiers
42
43open Errors
44
45open Extralib
46
47open Setoids
48
49open Monad
50
51open Option
52
53open Lists
54
55open Positive
56
57open Identifiers
58
59open Extranat
60
61open Vector
62
63open Div_and_mod
64
65open Jmeq
66
67open Russell
68
69open Types
70
71open List
72
73open Util
74
75open FoldStuff
76
77open Bool
78
79open Hints_declaration
80
81open Core_notation
82
83open Pts
84
85open Logic
86
87open Relations
88
89open Nat
90
91open BitVector
92
93open ASM
94
95open ASMCosts
96
97open UtilBranch
98
99val traverse_code_internal :
100  BitVector.byte BitVectorTrie.bitVectorTrie -> CostLabel.costlabel
101  BitVectorTrie.bitVectorTrie -> BitVector.word -> Nat.nat -> Nat.nat
102  Identifiers.identifier_map Types.sig0
103
104val traverse_code :
105  BitVector.byte BitVectorTrie.bitVectorTrie -> CostLabel.costlabel
106  BitVectorTrie.bitVectorTrie -> Nat.nat Identifiers.identifier_map
107  Types.sig0
108
109val compute_costs :
110  BitVector.byte List.list -> CostLabel.costlabel BitVectorTrie.bitVectorTrie
111  -> Nat.nat Identifiers.identifier_map Types.sig0
112
113val aSM_cost_map :
114  (BitVector.byte List.list, CostLabel.costlabel BitVectorTrie.bitVectorTrie)
115  Types.prod -> StructuredTraces.as_cost_map
116
Note: See TracBrowser for help on using the repository browser.