source: extracted/frontEndMem.mli @ 2649

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

...

File size: 1.2 KB
Line 
1open Preamble
2
3open Hide
4
5open ByteValues
6
7open Proper
8
9open PositiveMap
10
11open Deqsets
12
13open ErrorMessages
14
15open PreIdentifiers
16
17open Errors
18
19open Setoids
20
21open Monad
22
23open Option
24
25open Lists
26
27open Identifiers
28
29open Integers
30
31open AST
32
33open Division
34
35open Arithmetic
36
37open Extranat
38
39open Vector
40
41open FoldStuff
42
43open BitVector
44
45open Positive
46
47open Z
48
49open BitVectorZ
50
51open Pointers
52
53open Div_and_mod
54
55open Jmeq
56
57open Russell
58
59open Util
60
61open Bool
62
63open Relations
64
65open Nat
66
67open List
68
69open Hints_declaration
70
71open Core_notation
72
73open Pts
74
75open Logic
76
77open Types
78
79open Extralib
80
81open GenMem
82
83open Coqlib
84
85open Values
86
87open FrontEndVal
88
89val loadn :
90  GenMem.mem1 -> Pointers.pointer -> Nat.nat -> ByteValues.beval List.list
91  Types.option
92
93val load :
94  AST.typ -> GenMem.mem1 -> Pointers.pointer -> Values.val0 Types.option
95
96val loadv : AST.typ -> GenMem.mem1 -> Values.val0 -> Values.val0 Types.option
97
98val storen :
99  GenMem.mem1 -> Pointers.pointer -> ByteValues.beval List.list ->
100  GenMem.mem1 Types.option
101
102val store :
103  AST.typ -> GenMem.mem1 -> Pointers.pointer -> Values.val0 -> GenMem.mem1
104  Types.option
105
106val storev :
107  AST.typ -> GenMem.mem1 -> Values.val0 -> Values.val0 -> GenMem.mem1
108  Types.option
109
110val valid_pointer : GenMem.mem1 -> Pointers.pointer -> Bool.bool
111
Note: See TracBrowser for help on using the repository browser.