Changeset 2773 for extracted/csem.mli
 Timestamp:
 Mar 4, 2013, 10:03:33 AM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

extracted/csem.mli
r2730 r2773 94 94 95 95 open Globalenvs 96 97 open BitVectorTrie98 96 99 97 open CostLabel … … 153 151 val sem_cmp : 154 152 Integers.comparison > Values.val0 > Csyntax.type0 > Values.val0 > 155 Csyntax.type0 > GenMem.mem 1> Values.val0 Types.option153 Csyntax.type0 > GenMem.mem > Values.val0 Types.option 156 154 157 155 val cast_bool_to_target : … … 164 162 val sem_binary_operation : 165 163 Csyntax.binary_operation > Values.val0 > Csyntax.type0 > Values.val0 > 166 Csyntax.type0 > GenMem.mem 1> Csyntax.type0 > Values.val0 Types.option164 Csyntax.type0 > GenMem.mem > Csyntax.type0 > Values.val0 Types.option 167 165 168 166 val cast_int_int : … … 170 168 BitVector.bitVector 171 169 172 type genv 0= Csyntax.clight_fundef Globalenvs.genv_t170 type genv = Csyntax.clight_fundef Globalenvs.genv_t 173 171 174 172 type env = Pointers.block Identifiers.identifier_map … … 177 175 178 176 val load_value_of_type : 179 Csyntax.type0 > GenMem.mem 1> Pointers.block > Pointers.offset >177 Csyntax.type0 > GenMem.mem > Pointers.block > Pointers.offset > 180 178 Values.val0 Types.option 181 179 182 180 val store_value_of_type : 183 Csyntax.type0 > GenMem.mem 1> Pointers.block > Pointers.offset >184 Values.val0 > GenMem.mem 1Types.option181 Csyntax.type0 > GenMem.mem > Pointers.block > Pointers.offset > 182 Values.val0 > GenMem.mem Types.option 185 183 186 184 val blocks_of_env : env > Pointers.block List.list … … 315 313 val call_cont : cont > cont 316 314 317 type state 0=318  State of Csyntax.function0 * Csyntax.statement * cont * env * GenMem.mem 1315 type state = 316  State of Csyntax.function0 * Csyntax.statement * cont * env * GenMem.mem 319 317  Callstate of AST.ident * Csyntax.clight_fundef * Values.val0 List.list 320 * cont * GenMem.mem 1321  Returnstate of Values.val0 * cont * GenMem.mem 1318 * cont * GenMem.mem 319  Returnstate of Values.val0 * cont * GenMem.mem 322 320  Finalstate of Integers.int 323 321 324 322 val state_rect_Type4 : 325 (Csyntax.function0 > Csyntax.statement > cont > env > GenMem.mem 1>326 'a1) > (AST.ident > Csyntax.clight_fundef > Values.val0 List.list > 327 cont > GenMem.mem 1 > 'a1) > (Values.val0 > cont > GenMem.mem1 > 'a1)328 > (Integers.int > 'a1) > state0> 'a1323 (Csyntax.function0 > Csyntax.statement > cont > env > GenMem.mem > 324 'a1) > (AST.ident > Csyntax.clight_fundef > Values.val0 List.list > 325 cont > GenMem.mem > 'a1) > (Values.val0 > cont > GenMem.mem > 'a1) > 326 (Integers.int > 'a1) > state > 'a1 329 327 330 328 val state_rect_Type5 : 331 (Csyntax.function0 > Csyntax.statement > cont > env > GenMem.mem 1>332 'a1) > (AST.ident > Csyntax.clight_fundef > Values.val0 List.list > 333 cont > GenMem.mem 1 > 'a1) > (Values.val0 > cont > GenMem.mem1 > 'a1)334 > (Integers.int > 'a1) > state0> 'a1329 (Csyntax.function0 > Csyntax.statement > cont > env > GenMem.mem > 330 'a1) > (AST.ident > Csyntax.clight_fundef > Values.val0 List.list > 331 cont > GenMem.mem > 'a1) > (Values.val0 > cont > GenMem.mem > 'a1) > 332 (Integers.int > 'a1) > state > 'a1 335 333 336 334 val state_rect_Type3 : 337 (Csyntax.function0 > Csyntax.statement > cont > env > GenMem.mem 1>338 'a1) > (AST.ident > Csyntax.clight_fundef > Values.val0 List.list > 339 cont > GenMem.mem 1 > 'a1) > (Values.val0 > cont > GenMem.mem1 > 'a1)340 > (Integers.int > 'a1) > state0> 'a1335 (Csyntax.function0 > Csyntax.statement > cont > env > GenMem.mem > 336 'a1) > (AST.ident > Csyntax.clight_fundef > Values.val0 List.list > 337 cont > GenMem.mem > 'a1) > (Values.val0 > cont > GenMem.mem > 'a1) > 338 (Integers.int > 'a1) > state > 'a1 341 339 342 340 val state_rect_Type2 : 343 (Csyntax.function0 > Csyntax.statement > cont > env > GenMem.mem 1>344 'a1) > (AST.ident > Csyntax.clight_fundef > Values.val0 List.list > 345 cont > GenMem.mem 1 > 'a1) > (Values.val0 > cont > GenMem.mem1 > 'a1)346 > (Integers.int > 'a1) > state0> 'a1341 (Csyntax.function0 > Csyntax.statement > cont > env > GenMem.mem > 342 'a1) > (AST.ident > Csyntax.clight_fundef > Values.val0 List.list > 343 cont > GenMem.mem > 'a1) > (Values.val0 > cont > GenMem.mem > 'a1) > 344 (Integers.int > 'a1) > state > 'a1 347 345 348 346 val state_rect_Type1 : 349 (Csyntax.function0 > Csyntax.statement > cont > env > GenMem.mem 1>350 'a1) > (AST.ident > Csyntax.clight_fundef > Values.val0 List.list > 351 cont > GenMem.mem 1 > 'a1) > (Values.val0 > cont > GenMem.mem1 > 'a1)352 > (Integers.int > 'a1) > state0> 'a1347 (Csyntax.function0 > Csyntax.statement > cont > env > GenMem.mem > 348 'a1) > (AST.ident > Csyntax.clight_fundef > Values.val0 List.list > 349 cont > GenMem.mem > 'a1) > (Values.val0 > cont > GenMem.mem > 'a1) > 350 (Integers.int > 'a1) > state > 'a1 353 351 354 352 val state_rect_Type0 : 355 (Csyntax.function0 > Csyntax.statement > cont > env > GenMem.mem 1>356 'a1) > (AST.ident > Csyntax.clight_fundef > Values.val0 List.list > 357 cont > GenMem.mem 1 > 'a1) > (Values.val0 > cont > GenMem.mem1 > 'a1)358 > (Integers.int > 'a1) > state0> 'a1353 (Csyntax.function0 > Csyntax.statement > cont > env > GenMem.mem > 354 'a1) > (AST.ident > Csyntax.clight_fundef > Values.val0 List.list > 355 cont > GenMem.mem > 'a1) > (Values.val0 > cont > GenMem.mem > 'a1) > 356 (Integers.int > 'a1) > state > 'a1 359 357 360 358 val state_inv_rect_Type4 : 361 state 0> (Csyntax.function0 > Csyntax.statement > cont > env >362 GenMem.mem 1> __ > 'a1) > (AST.ident > Csyntax.clight_fundef >363 Values.val0 List.list > cont > GenMem.mem 1> __ > 'a1) > (Values.val0364 > cont > GenMem.mem 1> __ > 'a1) > (Integers.int > __ > 'a1) > 'a1359 state > (Csyntax.function0 > Csyntax.statement > cont > env > 360 GenMem.mem > __ > 'a1) > (AST.ident > Csyntax.clight_fundef > 361 Values.val0 List.list > cont > GenMem.mem > __ > 'a1) > (Values.val0 362 > cont > GenMem.mem > __ > 'a1) > (Integers.int > __ > 'a1) > 'a1 365 363 366 364 val state_inv_rect_Type3 : 367 state 0> (Csyntax.function0 > Csyntax.statement > cont > env >368 GenMem.mem 1> __ > 'a1) > (AST.ident > Csyntax.clight_fundef >369 Values.val0 List.list > cont > GenMem.mem 1> __ > 'a1) > (Values.val0370 > cont > GenMem.mem 1> __ > 'a1) > (Integers.int > __ > 'a1) > 'a1365 state > (Csyntax.function0 > Csyntax.statement > cont > env > 366 GenMem.mem > __ > 'a1) > (AST.ident > Csyntax.clight_fundef > 367 Values.val0 List.list > cont > GenMem.mem > __ > 'a1) > (Values.val0 368 > cont > GenMem.mem > __ > 'a1) > (Integers.int > __ > 'a1) > 'a1 371 369 372 370 val state_inv_rect_Type2 : 373 state 0> (Csyntax.function0 > Csyntax.statement > cont > env >374 GenMem.mem 1> __ > 'a1) > (AST.ident > Csyntax.clight_fundef >375 Values.val0 List.list > cont > GenMem.mem 1> __ > 'a1) > (Values.val0376 > cont > GenMem.mem 1> __ > 'a1) > (Integers.int > __ > 'a1) > 'a1371 state > (Csyntax.function0 > Csyntax.statement > cont > env > 372 GenMem.mem > __ > 'a1) > (AST.ident > Csyntax.clight_fundef > 373 Values.val0 List.list > cont > GenMem.mem > __ > 'a1) > (Values.val0 374 > cont > GenMem.mem > __ > 'a1) > (Integers.int > __ > 'a1) > 'a1 377 375 378 376 val state_inv_rect_Type1 : 379 state 0> (Csyntax.function0 > Csyntax.statement > cont > env >380 GenMem.mem 1> __ > 'a1) > (AST.ident > Csyntax.clight_fundef >381 Values.val0 List.list > cont > GenMem.mem 1> __ > 'a1) > (Values.val0382 > cont > GenMem.mem 1> __ > 'a1) > (Integers.int > __ > 'a1) > 'a1377 state > (Csyntax.function0 > Csyntax.statement > cont > env > 378 GenMem.mem > __ > 'a1) > (AST.ident > Csyntax.clight_fundef > 379 Values.val0 List.list > cont > GenMem.mem > __ > 'a1) > (Values.val0 380 > cont > GenMem.mem > __ > 'a1) > (Integers.int > __ > 'a1) > 'a1 383 381 384 382 val state_inv_rect_Type0 : 385 state 0> (Csyntax.function0 > Csyntax.statement > cont > env >386 GenMem.mem 1> __ > 'a1) > (AST.ident > Csyntax.clight_fundef >387 Values.val0 List.list > cont > GenMem.mem 1> __ > 'a1) > (Values.val0388 > cont > GenMem.mem 1> __ > 'a1) > (Integers.int > __ > 'a1) > 'a1389 390 val state_discr : state 0 > state0> __391 392 val state_jmdiscr : state 0 > state0> __383 state > (Csyntax.function0 > Csyntax.statement > cont > env > 384 GenMem.mem > __ > 'a1) > (AST.ident > Csyntax.clight_fundef > 385 Values.val0 List.list > cont > GenMem.mem > __ > 'a1) > (Values.val0 386 > cont > GenMem.mem > __ > 'a1) > (Integers.int > __ > 'a1) > 'a1 387 388 val state_discr : state > state > __ 389 390 val state_jmdiscr : state > state > __ 393 391 394 392 val find_label_ls :
Note: See TracChangeset
for help on using the changeset viewer.