source: driver/extracted/bEMem.ml @ 3106

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

Semantics files committed.

File size: 1.0 KB
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
87(** val is_addressable : AST.region -> Bool.bool **)
88let is_addressable = function
89| AST.XData -> Bool.True
90| AST.Code -> Bool.True
91
92type address = (ByteValues.beval, ByteValues.beval) Types.prod
93
94(** val pointer_of_address : address -> Pointers.pointer Errors.res **)
95let pointer_of_address p =
96  let { Types.fst = v1; Types.snd = v2 } = p in
97  ByteValues.pointer_of_bevals (List.Cons (v1, (List.Cons (v2, List.Nil))))
98
Note: See TracBrowser for help on using the repository browser.