source: extracted/costInj.mli @ 3043

Last change on this file since 3043 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: 1.1 KB
RevLine 
[2730]1open Preamble
2
[2773]3open BitVectorTrie
4
[2730]5open Graphs
6
7open Order
8
9open Registers
10
11open FrontEndVal
12
13open Hide
14
15open ByteValues
16
[2951]17open GenMem
18
19open FrontEndMem
20
[2730]21open Division
22
23open Z
24
25open BitVectorZ
26
27open Pointers
28
[2951]29open Coqlib
[2730]30
[2951]31open Values
[2730]32
[2951]33open FrontEndOps
34
35open CostLabel
36
[2730]37open Proper
38
39open PositiveMap
40
41open Deqsets
42
[2951]43open ErrorMessages
44
45open PreIdentifiers
46
47open Errors
48
[2730]49open Extralib
50
51open Lists
52
[2951]53open Positive
54
[2730]55open Identifiers
56
57open Exp
58
59open Arithmetic
60
61open Vector
62
63open Div_and_mod
64
65open Util
66
67open FoldStuff
68
69open BitVector
70
[2951]71open Jmeq
[2730]72
[2951]73open Russell
[2730]74
[2951]75open List
[2730]76
77open Setoids
78
79open Monad
80
[2951]81open Option
[2730]82
[2951]83open Extranat
[2730]84
85open Bool
86
87open Relations
88
89open Nat
90
[2951]91open Integers
92
93open Types
94
95open AST
96
[2730]97open Hints_declaration
98
99open Core_notation
100
101open Pts
102
103open Logic
104
[2951]105open RTLabs_syntax
[2730]106
[2951]107open CostSpec
[2730]108
109val reverse_label_map :
110  RTLabs_syntax.statement Graphs.graph -> PreIdentifiers.identifier
111  Identifiers.identifier_map Types.option
112
113val check_fun_inj : RTLabs_syntax.internal_function -> Bool.bool
114
115val check_program_cost_injectivity :
116  RTLabs_syntax.rTLabs_program -> Bool.bool
117
[3043]118val check_program_cost_injectivity_prf :
119  RTLabs_syntax.rTLabs_program -> __ Errors.res
120
Note: See TracBrowser for help on using the repository browser.