source: driver/extracted/interpret.mli @ 3106

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

New extraction.

File size: 2.6 KB
Line 
1open Preamble
2
3open BitVectorTrie
4
5open String
6
7open Exp
8
9open Arithmetic
10
11open Vector
12
13open FoldStuff
14
15open BitVector
16
17open Extranat
18
19open Integers
20
21open AST
22
23open LabelledObjects
24
25open Proper
26
27open PositiveMap
28
29open Deqsets
30
31open ErrorMessages
32
33open PreIdentifiers
34
35open Errors
36
37open Extralib
38
39open Setoids
40
41open Monad
42
43open Option
44
45open Div_and_mod
46
47open Util
48
49open List
50
51open Lists
52
53open Bool
54
55open Relations
56
57open Nat
58
59open Positive
60
61open Identifiers
62
63open CostLabel
64
65open ASM
66
67open Types
68
69open Hints_declaration
70
71open Core_notation
72
73open Pts
74
75open Logic
76
77open Jmeq
78
79open Russell
80
81open Status
82
83open StatusProofs
84
85open Fetch
86
87open Hide
88
89open Division
90
91open Z
92
93open BitVectorZ
94
95open Pointers
96
97open Coqlib
98
99open Values
100
101open Events
102
103open IOMonad
104
105open IO
106
107open Sets
108
109open Listb
110
111open StructuredTraces
112
113open AbstractStatus
114
115val execute_1_preinstruction :
116  (Nat.nat, Nat.nat) Types.prod -> 'a2 -> ('a1 -> 'a2 Status.preStatus ->
117  BitVector.word) -> 'a1 ASM.preinstruction -> 'a2 Status.preStatus -> 'a2
118  Status.preStatus
119
120val execute_1_preinstruction_ok' :
121  (Nat.nat, Nat.nat) Types.prod -> 'a2 -> ('a1 -> 'a2 Status.preStatus ->
122  BitVector.word) -> 'a1 ASM.preinstruction -> 'a2 Status.preStatus -> 'a2
123  Status.preStatus Types.sig0
124
125val compute_target_of_unconditional_jump :
126  BitVector.word -> ASM.instruction -> BitVector.word
127
128val is_unconditional_jump : ASM.instruction -> Bool.bool
129
130val program_counter_after_other :
131  BitVector.word -> ASM.instruction -> BitVector.word
132
133val addr_of_relative :
134  'a1 -> ASM.subaddressing_mode -> 'a1 Status.preStatus -> BitVector.word
135
136val execute_1_0 :
137  BitVector.byte BitVectorTrie.bitVectorTrie -> Status.status ->
138  ((ASM.instruction, BitVector.word) Types.prod, Nat.nat) Types.prod ->
139  Status.status Types.sig0
140
141val current_instruction_cost :
142  BitVector.byte BitVectorTrie.bitVectorTrie -> Status.status -> Nat.nat
143
144val execute_1' :
145  BitVector.byte BitVectorTrie.bitVectorTrie -> Status.status ->
146  Status.status Types.sig0
147
148val execute_1 :
149  BitVector.byte BitVectorTrie.bitVectorTrie -> Status.status ->
150  Status.status
151
152val execute_1_pseudo_instruction0 :
153  (Nat.nat, Nat.nat) Types.prod -> ASM.pseudo_assembly_program ->
154  (ASM.identifier -> BitVector.word) -> (ASM.identifier -> BitVector.word) ->
155  Status.pseudoStatus -> ASM.pseudo_instruction -> BitVector.word ->
156  Status.pseudoStatus
157
158val execute_1_pseudo_instruction :
159  ASM.pseudo_assembly_program -> (BitVector.word -> __ -> (Nat.nat, Nat.nat)
160  Types.prod) -> (ASM.identifier -> BitVector.word) -> (ASM.identifier ->
161  BitVector.word) -> Status.pseudoStatus -> Status.pseudoStatus
162
163val execute :
164  Nat.nat -> BitVector.byte BitVectorTrie.bitVectorTrie -> Status.status ->
165  Status.status
166
Note: See TracBrowser for help on using the repository browser.