source: driver/extracted/policyFront.mli @ 3106

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

New extraction.

File size: 2.6 KB
Line 
1open Preamble
2
3open Div_and_mod
4
5open Jmeq
6
7open Russell
8
9open Util
10
11open Bool
12
13open Relations
14
15open Nat
16
17open List
18
19open Hints_declaration
20
21open Core_notation
22
23open Pts
24
25open Logic
26
27open Types
28
29open Extralib
30
31open Status
32
33open BitVectorTrie
34
35open String
36
37open Integers
38
39open AST
40
41open LabelledObjects
42
43open Proper
44
45open PositiveMap
46
47open Deqsets
48
49open ErrorMessages
50
51open PreIdentifiers
52
53open Errors
54
55open Lists
56
57open Positive
58
59open Identifiers
60
61open CostLabel
62
63open ASM
64
65open Exp
66
67open Setoids
68
69open Monad
70
71open Option
72
73open Extranat
74
75open Vector
76
77open FoldStuff
78
79open BitVector
80
81open Arithmetic
82
83open Fetch
84
85open Assembly
86
87type ppc_pc_map =
88  (Nat.nat, (Nat.nat, Assembly.jump_length) Types.prod
89  BitVectorTrie.bitVectorTrie) Types.prod
90
91val jmpeqb : Assembly.jump_length -> Assembly.jump_length -> Bool.bool
92
93val expand_relative_jump_internal_unsafe :
94  Assembly.jump_length -> (ASM.subaddressing_mode -> ASM.subaddressing_mode
95  ASM.preinstruction) -> ASM.instruction List.list
96
97val strip_target :
98  ASM.identifier ASM.preinstruction -> (ASM.subaddressing_mode ->
99  ASM.subaddressing_mode ASM.preinstruction, ASM.instruction) Types.sum
100
101val expand_relative_jump_unsafe :
102  Assembly.jump_length -> ASM.identifier ASM.preinstruction ->
103  ASM.instruction List.list
104
105val expand_pseudo_instruction_unsafe :
106  Assembly.jump_length -> ASM.pseudo_instruction -> ASM.instruction List.list
107
108val instruction_size_jmplen :
109  Assembly.jump_length -> ASM.pseudo_instruction -> Nat.nat
110
111val max_length :
112  Assembly.jump_length -> Assembly.jump_length -> Assembly.jump_length
113
114val dec_jmple :
115  Assembly.jump_length -> Assembly.jump_length -> (__, __) Types.sum
116
117val dec_eq_jump_length :
118  Assembly.jump_length -> Assembly.jump_length -> (__, __) Types.sum
119
120val create_label_map :
121  ASM.labelled_instruction List.list -> Fetch.label_map Types.sig0
122
123val select_reljump_length :
124  Fetch.label_map -> ppc_pc_map -> ppc_pc_map -> Nat.nat -> ASM.identifier ->
125  Nat.nat -> Assembly.jump_length
126
127val select_call_length :
128  Fetch.label_map -> ppc_pc_map -> ppc_pc_map -> Nat.nat -> ASM.identifier ->
129  Assembly.jump_length
130
131val select_jump_length :
132  Fetch.label_map -> ppc_pc_map -> ppc_pc_map -> Nat.nat -> ASM.identifier ->
133  Assembly.jump_length
134
135val destination_of :
136  ASM.identifier ASM.preinstruction -> ASM.identifier Types.option
137
138val length_of : ASM.identifier ASM.preinstruction -> Nat.nat
139
140val jump_expansion_step_instruction :
141  Fetch.label_map -> ppc_pc_map -> ppc_pc_map -> Nat.nat -> ASM.identifier
142  ASM.preinstruction -> Assembly.jump_length Types.option
143
144val jump_expansion_start :
145  ASM.labelled_instruction List.list Types.sig0 -> Fetch.label_map ->
146  ppc_pc_map Types.option Types.sig0
147
Note: See TracBrowser for help on using the repository browser.