source: driver/extracted/policyStep.mli @ 3106

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

New extraction.

File size: 864 bytes
Line 
1open Preamble
2
3open Status
4
5open BitVectorTrie
6
7open String
8
9open Integers
10
11open AST
12
13open LabelledObjects
14
15open Proper
16
17open PositiveMap
18
19open Deqsets
20
21open ErrorMessages
22
23open PreIdentifiers
24
25open Errors
26
27open Lists
28
29open Positive
30
31open Identifiers
32
33open CostLabel
34
35open ASM
36
37open Exp
38
39open Setoids
40
41open Monad
42
43open Option
44
45open Extranat
46
47open Vector
48
49open FoldStuff
50
51open BitVector
52
53open Arithmetic
54
55open Fetch
56
57open Assembly
58
59open Div_and_mod
60
61open Jmeq
62
63open Russell
64
65open Util
66
67open Bool
68
69open Relations
70
71open Nat
72
73open List
74
75open Hints_declaration
76
77open Core_notation
78
79open Pts
80
81open Logic
82
83open Types
84
85open Extralib
86
87open PolicyFront
88
89val 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
Note: See TracBrowser for help on using the repository browser.