source: extracted/frontEndVal.mli @ 2716

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

...

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