Ignore:
Timestamp:
Mar 25, 2013, 11:30:01 PM (8 years ago)
Author:
sacerdot
Message:

New extraction. Novely: a pre-main is used in the back-end. Initialization
of global data is performed in LINToASM.

Note: the cost-emission of the initialization costlabel in the front-end is
virtual, but not performed in the traces I generate and print. To be fixed
(how?)

File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/semantics.mli

    r2875 r2951  
    55open ASMCostsSplit
    66
     7open StructuredTraces
     8
    79open AbstractStatus
    810
     
    8991open RTLabsToRTL
    9092
     93open CostInj
     94
     95open Deqsets_extra
     96
     97open CostMisc
     98
     99open Listb_extra
     100
     101open CostSpec
     102
     103open CostCheck
     104
     105open BitVectorTrie
     106
     107open Graphs
     108
     109open Order
     110
     111open Registers
     112
     113open RTLabs_syntax
     114
     115open ToRTLabs
     116
     117open FrontEndOps
     118
     119open Cminor_syntax
     120
     121open ToCminor
     122
     123open MemProperties
     124
     125open MemoryInjections
     126
     127open Fresh
     128
     129open SwitchRemoval
     130
     131open Sets
     132
     133open Listb
     134
     135open Star
     136
     137open Frontend_misc
     138
     139open CexecInd
     140
     141open CexecSound
     142
     143open Casts
     144
     145open ClassifyOp
     146
     147open Smallstep
     148
     149open Extra_bool
     150
     151open FrontEndVal
     152
     153open Hide
     154
     155open ByteValues
     156
     157open GenMem
     158
     159open FrontEndMem
     160
     161open Globalenvs
     162
     163open Csem
     164
     165open SmallstepExec
     166
     167open Division
     168
     169open Z
     170
     171open BitVectorZ
     172
     173open Pointers
     174
     175open Values
     176
     177open Events
     178
     179open IOMonad
     180
     181open IO
     182
     183open Cexec
     184
     185open TypeComparison
     186
     187open SimplifyCasts
     188
     189open CostLabel
     190
     191open Coqlib
     192
     193open Proper
     194
     195open PositiveMap
     196
     197open Deqsets
     198
     199open ErrorMessages
     200
     201open PreIdentifiers
     202
     203open Errors
     204
     205open Extralib
     206
     207open Lists
     208
     209open Positive
     210
     211open Identifiers
     212
     213open Exp
     214
     215open Arithmetic
     216
     217open Vector
     218
     219open Div_and_mod
     220
     221open Util
     222
     223open FoldStuff
     224
     225open BitVector
     226
     227open Jmeq
     228
     229open Russell
     230
     231open List
     232
     233open Setoids
     234
     235open Monad
     236
     237open Option
     238
     239open Extranat
     240
     241open Bool
     242
     243open Relations
     244
     245open Nat
     246
     247open Integers
     248
     249open Hints_declaration
     250
     251open Core_notation
     252
     253open Pts
     254
     255open Logic
     256
     257open Types
     258
     259open AST
     260
     261open Csyntax
     262
     263open Label
     264
     265open Compiler
     266
     267open Stacksize
     268
    91269open Executions
    92270
    93 open StructuredTraces
     271open Measurable
     272
     273open Clight_abstract
     274
     275open Clight_classified_system
     276
     277open Cminor_semantics
     278
     279open Cminor_abstract
     280
     281open Cminor_classified_system
    94282
    95283open RTLabs_semantics
     
    97285open RTLabs_abstract
    98286
    99 open RTLabs_traces
    100 
    101 open CostInj
    102 
    103 open Deqsets_extra
    104 
    105 open CostMisc
    106 
    107 open Listb_extra
    108 
    109 open CostSpec
    110 
    111 open CostCheck
    112 
    113 open Initialisation
    114 
    115 open BitVectorTrie
    116 
    117 open Graphs
    118 
    119 open Order
    120 
    121 open Registers
    122 
    123 open RTLabs_syntax
    124 
    125 open ToRTLabs
    126 
    127 open FrontEndOps
    128 
    129 open Cminor_syntax
    130 
    131 open ToCminor
    132 
    133 open MemProperties
    134 
    135 open MemoryInjections
    136 
    137 open Fresh
    138 
    139 open SwitchRemoval
    140 
    141 open Sets
    142 
    143 open Listb
    144 
    145 open Star
    146 
    147 open Frontend_misc
    148 
    149 open CexecInd
    150 
    151 open CexecSound
    152 
    153 open Casts
    154 
    155 open ClassifyOp
    156 
    157 open Smallstep
    158 
    159 open Extra_bool
    160 
    161 open FrontEndVal
    162 
    163 open Hide
    164 
    165 open ByteValues
    166 
    167 open GenMem
    168 
    169 open FrontEndMem
    170 
    171 open Globalenvs
    172 
    173 open Csem
    174 
    175 open SmallstepExec
    176 
    177 open Division
    178 
    179 open Z
    180 
    181 open BitVectorZ
    182 
    183 open Pointers
    184 
    185 open Values
    186 
    187 open Events
    188 
    189 open IOMonad
    190 
    191 open IO
    192 
    193 open Cexec
    194 
    195 open TypeComparison
    196 
    197 open SimplifyCasts
    198 
    199 open CostLabel
    200 
    201 open Coqlib
    202 
    203 open Proper
    204 
    205 open PositiveMap
    206 
    207 open Deqsets
    208 
    209 open ErrorMessages
    210 
    211 open PreIdentifiers
    212 
    213 open Errors
    214 
    215 open Extralib
    216 
    217 open Lists
    218 
    219 open Positive
    220 
    221 open Identifiers
    222 
    223 open Exp
    224 
    225 open Arithmetic
    226 
    227 open Vector
    228 
    229 open Div_and_mod
    230 
    231 open Util
    232 
    233 open FoldStuff
    234 
    235 open BitVector
    236 
    237 open Jmeq
    238 
    239 open Russell
    240 
    241 open List
    242 
    243 open Setoids
    244 
    245 open Monad
    246 
    247 open Option
    248 
    249 open Extranat
    250 
    251 open Bool
    252 
    253 open Relations
    254 
    255 open Nat
    256 
    257 open Integers
    258 
    259 open Hints_declaration
    260 
    261 open Core_notation
    262 
    263 open Pts
    264 
    265 open Logic
    266 
    267 open Types
    268 
    269 open AST
    270 
    271 open Csyntax
    272 
    273 open Label
    274 
    275 open Compiler
    276 
    277 open Measurable
    278 
    279 open Clight_abstract
    280 
    281 open Clight_classified_system
    282 
    283 open Cminor_semantics
    284 
    285 open Cminor_abstract
    286 
    287 open Cminor_classified_system
    288 
    289287open RTLabs_classified_system
    290288
     289open ExtraMonads
     290
    291291open ExtraGlobalenvs
    292292
     
    297297open Joint_semantics
    298298
     299open SemanticsUtils
     300
    299301open Traces
    300302
    301303open Joint_fullexec
    302 
    303 open ExtraMonads
    304 
    305 open SemanticsUtils
    306304
    307305open RTL_semantics
Note: See TracChangeset for help on using the changeset viewer.