]> matita.cs.unibo.it Git - pkg-cerco/acc-trusted.git/blob - extracted/policyStep.mli
Merge tag 'upstream/0.2'
[pkg-cerco/acc-trusted.git] / extracted / policyStep.mli
1 open Preamble
2
3 open Status
4
5 open BitVectorTrie
6
7 open String
8
9 open Integers
10
11 open AST
12
13 open LabelledObjects
14
15 open Proper
16
17 open PositiveMap
18
19 open Deqsets
20
21 open ErrorMessages
22
23 open PreIdentifiers
24
25 open Errors
26
27 open Lists
28
29 open Positive
30
31 open Identifiers
32
33 open CostLabel
34
35 open ASM
36
37 open Exp
38
39 open Setoids
40
41 open Monad
42
43 open Option
44
45 open Extranat
46
47 open Vector
48
49 open FoldStuff
50
51 open BitVector
52
53 open Arithmetic
54
55 open Fetch
56
57 open Assembly
58
59 open Div_and_mod
60
61 open Jmeq
62
63 open Russell
64
65 open Util
66
67 open Bool
68
69 open Relations
70
71 open Nat
72
73 open List
74
75 open Hints_declaration
76
77 open Core_notation
78
79 open Pts
80
81 open Logic
82
83 open Types
84
85 open Extralib
86
87 open PolicyFront
88
89 val jump_expansion_step :
90   ASM.labelled_instruction List.list Types.sig0 -> Fetch.label_map Types.sig0
91   -> PolicyFront.ppc_pc_map Types.sig0 -> (Bool.bool, PolicyFront.ppc_pc_map
92   Types.option) Types.prod Types.sig0
93