source: driver/extracted/memProperties.ml @ 3106

Last change on this file since 3106 was 2773, checked in by sacerdot, 7 years ago
  1. everything extracted again after all bugs in Matita's extraction have been fixed. No more need for manual patching
  2. new extraction after file reorganization (by James)
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 Lists
64
65open Positive
66
67open Identifiers
68
69open Exp
70
71open Arithmetic
72
73open Vector
74
75open Div_and_mod
76
77open Util
78
79open FoldStuff
80
81open BitVector
82
83open Jmeq
84
85open Russell
86
87open List
88
89open Setoids
90
91open Monad
92
93open Option
94
95open Extranat
96
97open Bool
98
99open Relations
100
101open Nat
102
103open Integers
104
105open Hints_declaration
106
107open Core_notation
108
109open Pts
110
111open Logic
112
113open Types
114
115open AST
116
117open Csyntax
118
119open TypeComparison
120
121open Frontend_misc
122
123open SmallstepExec
124
125open Cexec
126
127(** val z_of_offset : Pointers.offset -> Z.z **)
128let z_of_offset ofs =
129  BitVectorZ.z_of_unsigned_bitvector Pointers.offset_size (Pointers.offv ofs)
130
131(** val shiftn : Pointers.offset -> Nat.nat -> Pointers.offset **)
132let rec shiftn off = function
133| Nat.O -> off
134| Nat.S n ->
135  shiftn
136    (Pointers.shift_offset (Nat.S (Nat.S Nat.O)) off
137      (Arithmetic.bitvector_of_nat (Nat.S (Nat.S Nat.O)) (Nat.S Nat.O))) n
138
Note: See TracBrowser for help on using the repository browser.