source: extracted/interpret.mli @ 2716

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

...

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