source: extracted/bEMem.mli @ 2829

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

Semantics files committed.

File size: 801 bytes
Line 
1open Preamble
2
3open Hide
4
5open Proper
6
7open PositiveMap
8
9open Deqsets
10
11open ErrorMessages
12
13open PreIdentifiers
14
15open Errors
16
17open Extralib
18
19open Lists
20
21open Identifiers
22
23open Integers
24
25open AST
26
27open Division
28
29open Exp
30
31open Arithmetic
32
33open Setoids
34
35open Monad
36
37open Option
38
39open Extranat
40
41open Vector
42
43open Div_and_mod
44
45open Jmeq
46
47open Russell
48
49open List
50
51open Util
52
53open FoldStuff
54
55open BitVector
56
57open Types
58
59open Bool
60
61open Relations
62
63open Nat
64
65open Hints_declaration
66
67open Core_notation
68
69open Pts
70
71open Logic
72
73open Positive
74
75open Z
76
77open BitVectorZ
78
79open Pointers
80
81open ByteValues
82
83open GenMem
84
85type bemem = GenMem.mem
86
87val is_addressable : AST.region -> Bool.bool
88
89type address = (ByteValues.beval, ByteValues.beval) Types.prod
90
91val pointer_of_address : address -> Pointers.pointer Errors.res
92
Note: See TracBrowser for help on using the repository browser.