source: driver/extracted/abstractStatus.mli @ 3085

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

Semantics of ASM in place (up to return values and function call names).
The test example badly diverges in ASM after being ok in LIN.

File size: 1.5 KB
Line 
1open Preamble
2
3open Hide
4
5open Integers
6
7open AST
8
9open Division
10
11open Exp
12
13open Arithmetic
14
15open Extranat
16
17open Vector
18
19open FoldStuff
20
21open BitVector
22
23open Z
24
25open BitVectorZ
26
27open Pointers
28
29open Coqlib
30
31open Values
32
33open Events
34
35open IOMonad
36
37open IO
38
39open Sets
40
41open Listb
42
43open Proper
44
45open PositiveMap
46
47open Deqsets
48
49open ErrorMessages
50
51open PreIdentifiers
52
53open Errors
54
55open Extralib
56
57open Setoids
58
59open Monad
60
61open Option
62
63open Div_and_mod
64
65open Russell
66
67open Util
68
69open List
70
71open Lists
72
73open Nat
74
75open Positive
76
77open Types
78
79open Identifiers
80
81open CostLabel
82
83open Jmeq
84
85open Hints_declaration
86
87open Core_notation
88
89open Pts
90
91open Logic
92
93open Relations
94
95open Bool
96
97open StructuredTraces
98
99open BitVectorTrie
100
101open String
102
103open LabelledObjects
104
105open ASM
106
107open Status
108
109open Fetch
110
111val aSM_classify00 : 'a1 ASM.preinstruction -> StructuredTraces.status_class
112
113val aSM_classify0 : ASM.instruction -> StructuredTraces.status_class
114
115val current_instruction0 :
116  BitVector.byte BitVectorTrie.bitVectorTrie -> BitVector.word ->
117  ASM.instruction
118
119val current_instruction :
120  BitVector.byte BitVectorTrie.bitVectorTrie -> Status.status ->
121  ASM.instruction
122
123val current_instruction_label :
124  BitVector.byte BitVectorTrie.bitVectorTrie -> CostLabel.costlabel
125  BitVectorTrie.bitVectorTrie -> Status.status -> CostLabel.costlabel
126  Types.option
127
128val word_deqset : Deqsets.deqSet
129
130val oC_classify :
131  BitVector.byte BitVectorTrie.bitVectorTrie -> Status.status ->
132  StructuredTraces.status_class
133
Note: See TracBrowser for help on using the repository browser.