source: extracted/abstractStatus.mli @ 2960

Last change on this file since 2960 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
RevLine 
[2601]1open Preamble
2
[2773]3open Hide
[2649]4
[2773]5open Integers
[2601]6
[2773]7open AST
[2717]8
[2773]9open Division
10
[2717]11open Exp
12
[2601]13open Arithmetic
14
[2773]15open Extranat
[2601]16
[2773]17open Vector
[2601]18
[2773]19open FoldStuff
[2601]20
[2773]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
[2601]43open Proper
44
45open PositiveMap
46
47open Deqsets
48
[2649]49open ErrorMessages
50
[2601]51open PreIdentifiers
52
53open Errors
54
55open Extralib
56
57open Setoids
58
59open Monad
60
61open Option
62
[2773]63open Div_and_mod
[2601]64
[2773]65open Russell
[2601]66
[2773]67open Util
[2601]68
[2773]69open List
[2601]70
[2773]71open Lists
[2601]72
[2773]73open Nat
[2601]74
[2773]75open Positive
[2601]76
77open Types
78
[2773]79open Identifiers
[2601]80
[2773]81open CostLabel
[2601]82
[2773]83open Jmeq
[2601]84
85open Hints_declaration
86
87open Core_notation
88
89open Pts
90
91open Logic
92
93open Relations
94
[2773]95open Bool
[2601]96
[2773]97open StructuredTraces
[2601]98
[2773]99open BitVectorTrie
100
101open String
102
103open LabelledObjects
104
[2601]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
[2905]130val oC_classify :
[2601]131  BitVector.byte BitVectorTrie.bitVectorTrie -> Status.status ->
132  StructuredTraces.status_class
133
Note: See TracBrowser for help on using the repository browser.