source: driver/extracted/label.mli @ 3106

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

New major extraction that should have solved all remaining issues.
As tests/PROBLEMI shows, we still have some bugs with:

a) initialization of global data (regression)
b) function pointers call

File size: 2.7 KB
Line 
1open Preamble
2
3open CostLabel
4
5open Coqlib
6
7open Proper
8
9open PositiveMap
10
11open Deqsets
12
13open ErrorMessages
14
15open PreIdentifiers
16
17open Errors
18
19open Extralib
20
21open Lists
22
23open Positive
24
25open Identifiers
26
27open Exp
28
29open Arithmetic
30
31open Vector
32
33open Div_and_mod
34
35open Util
36
37open FoldStuff
38
39open BitVector
40
41open Jmeq
42
43open Russell
44
45open List
46
47open Setoids
48
49open Monad
50
51open Option
52
53open Extranat
54
55open Bool
56
57open Relations
58
59open Nat
60
61open Integers
62
63open Hints_declaration
64
65open Core_notation
66
67open Pts
68
69open Logic
70
71open Types
72
73open AST
74
75open Csyntax
76
77val labels_of_expr : Csyntax.expr -> CostLabel.costlabel List.list
78
79val labels_of_labeled_statements :
80  Csyntax.labeled_statements -> CostLabel.costlabel List.list
81
82val labels_of_statement : Csyntax.statement -> CostLabel.costlabel List.list
83
84val labels_of_clight_fundef :
85  (AST.ident, Csyntax.clight_fundef) Types.prod -> CostLabel.costlabel
86  List.list
87
88val labels_of_clight :
89  Csyntax.clight_program -> CostLabel.costlabel List.list
90
91type in_clight_label = CostLabel.costlabel Types.sig0
92
93type clight_cost_map = CostLabel.costlabel -> Nat.nat
94
95val clight_label_free : Csyntax.clight_program -> Bool.bool
96
97val add_cost_before :
98  Csyntax.statement -> Identifiers.universe -> (Csyntax.statement,
99  Identifiers.universe) Types.prod
100
101val add_cost_after :
102  Csyntax.statement -> Identifiers.universe -> (Csyntax.statement,
103  Identifiers.universe) Types.prod
104
105val add_cost_expr :
106  Csyntax.expr -> Identifiers.universe -> (Csyntax.expr,
107  Identifiers.universe) Types.prod
108
109val const_int : AST.intsize -> Nat.nat -> Csyntax.expr
110
111val label_expr_descr :
112  Csyntax.expr_descr -> Identifiers.universe -> Csyntax.type0 ->
113  (Csyntax.expr_descr, Identifiers.universe) Types.prod
114
115val label_expr :
116  Csyntax.expr -> Identifiers.universe -> (Csyntax.expr,
117  Identifiers.universe) Types.prod
118
119val label_exprs :
120  Csyntax.expr List.list -> Identifiers.universe -> (Csyntax.expr List.list,
121  Identifiers.universe) Types.prod
122
123val label_opt_expr :
124  Csyntax.expr Types.option -> Identifiers.universe -> (Csyntax.expr
125  Types.option, Identifiers.universe) Types.prod
126
127val label_lstatements :
128  Csyntax.labeled_statements -> Identifiers.universe ->
129  (Csyntax.labeled_statements, Identifiers.universe) Types.prod
130
131val label_statement :
132  Csyntax.statement -> Identifiers.universe -> (Csyntax.statement,
133  Identifiers.universe) Types.prod
134
135val label_function :
136  Identifiers.universe -> Csyntax.function0 -> (Csyntax.function0,
137  Identifiers.universe) Types.prod
138
139val label_fundef :
140  Identifiers.universe -> Csyntax.clight_fundef -> (Csyntax.clight_fundef,
141  Identifiers.universe) Types.prod
142
143val clight_label :
144  Csyntax.clight_program -> (Csyntax.clight_program, CostLabel.costlabel)
145  Types.prod
146
Note: See TracBrowser for help on using the repository browser.