source: extracted/memProperties.ml @ 2649

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

...

File size: 1.3 KB
Line 
1open Preamble
2
3open Sets
4
5open Listb
6
7open IO
8
9open IOMonad
10
11open Star
12
13open ClassifyOp
14
15open Events
16
17open Smallstep
18
19open Extra_bool
20
21open Values
22
23open FrontEndVal
24
25open Hide
26
27open ByteValues
28
29open Division
30
31open Z
32
33open BitVectorZ
34
35open Pointers
36
37open GenMem
38
39open FrontEndMem
40
41open Globalenvs
42
43open Csem
44
45open CostLabel
46
47open Coqlib
48
49open Proper
50
51open PositiveMap
52
53open Deqsets
54
55open ErrorMessages
56
57open PreIdentifiers
58
59open Errors
60
61open Extralib
62
63open Setoids
64
65open Monad
66
67open Option
68
69open Lists
70
71open Positive
72
73open Identifiers
74
75open Arithmetic
76
77open Vector
78
79open Div_and_mod
80
81open Jmeq
82
83open Russell
84
85open List
86
87open Util
88
89open FoldStuff
90
91open BitVector
92
93open Extranat
94
95open Bool
96
97open Relations
98
99open Nat
100
101open Integers
102
103open Hints_declaration
104
105open Core_notation
106
107open Pts
108
109open Logic
110
111open Types
112
113open AST
114
115open Csyntax
116
117open TypeComparison
118
119open Frontend_misc
120
121open SmallstepExec
122
123open Cexec
124
125(** val z_of_offset : Pointers.offset -> Z.z **)
126let z_of_offset ofs =
127  BitVectorZ.z_of_unsigned_bitvector Pointers.offset_size (Pointers.offv ofs)
128
129(** val shiftn : Pointers.offset -> Nat.nat -> Pointers.offset **)
130let rec shiftn off = function
131| Nat.O -> off
132| Nat.S n ->
133  shiftn
134    (Pointers.shift_offset (Nat.S (Nat.S Nat.O)) off
135      (Arithmetic.bitvector_of_nat (Nat.S (Nat.S Nat.O)) (Nat.S Nat.O))) n
136
Note: See TracBrowser for help on using the repository browser.