source: driver/extracted/frontEndMem.mli @ 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.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 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 FoldStuff
44
45open BitVector
46
47open Positive
48
49open Z
50
51open BitVectorZ
52
53open Pointers
54
55open Div_and_mod
56
57open Jmeq
58
59open Russell
60
61open Util
62
63open Bool
64
65open Relations
66
67open Nat
68
69open List
70
71open Hints_declaration
72
73open Core_notation
74
75open Pts
76
77open Logic
78
79open Types
80
81open Extralib
82
83open GenMem
84
85open Coqlib
86
87open Values
88
89open FrontEndVal
90
91val loadn :
92  GenMem.mem -> Pointers.pointer -> Nat.nat -> ByteValues.beval List.list
93  Types.option
94
95val load :
96  AST.typ -> GenMem.mem -> Pointers.pointer -> Values.val0 Types.option
97
98val loadv : AST.typ -> GenMem.mem -> Values.val0 -> Values.val0 Types.option
99
100val storen :
101  GenMem.mem -> Pointers.pointer -> ByteValues.beval List.list -> GenMem.mem
102  Types.option
103
104val store :
105  AST.typ -> GenMem.mem -> Pointers.pointer -> Values.val0 -> GenMem.mem
106  Types.option
107
108val storev :
109  AST.typ -> GenMem.mem -> Values.val0 -> Values.val0 -> GenMem.mem
110  Types.option
111
112val valid_pointer : GenMem.mem -> Pointers.pointer -> Bool.bool
113
Note: See TracBrowser for help on using the repository browser.