Changeset 2797 for extracted/csyntax.ml


Ignore:
Timestamp:
Mar 7, 2013, 12:55:34 PM (7 years ago)
Author:
sacerdot
Message:

Extracted again after James's cleanup and the implementation of the
new testing function to be used in the untrusted code.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/csyntax.ml

    r2775 r2797  
    12031203    (type0 -> (AST.ident, type0) Types.prod List.list -> (AST.ident, type0)
    12041204    Types.prod List.list -> statement -> 'a1) -> function0 -> 'a1 **)
    1205 let rec function_rect_Type4 h_mk_function x_4352 =
     1205let rec function_rect_Type4 h_mk_function x_4365 =
    12061206  let { fn_return = fn_return0; fn_params = fn_params0; fn_vars = fn_vars0;
    1207     fn_body = fn_body0 } = x_4352
     1207    fn_body = fn_body0 } = x_4365
    12081208  in
    12091209  h_mk_function fn_return0 fn_params0 fn_vars0 fn_body0
     
    12121212    (type0 -> (AST.ident, type0) Types.prod List.list -> (AST.ident, type0)
    12131213    Types.prod List.list -> statement -> 'a1) -> function0 -> 'a1 **)
    1214 let rec function_rect_Type5 h_mk_function x_4354 =
     1214let rec function_rect_Type5 h_mk_function x_4367 =
    12151215  let { fn_return = fn_return0; fn_params = fn_params0; fn_vars = fn_vars0;
    1216     fn_body = fn_body0 } = x_4354
     1216    fn_body = fn_body0 } = x_4367
    12171217  in
    12181218  h_mk_function fn_return0 fn_params0 fn_vars0 fn_body0
     
    12211221    (type0 -> (AST.ident, type0) Types.prod List.list -> (AST.ident, type0)
    12221222    Types.prod List.list -> statement -> 'a1) -> function0 -> 'a1 **)
    1223 let rec function_rect_Type3 h_mk_function x_4356 =
     1223let rec function_rect_Type3 h_mk_function x_4369 =
    12241224  let { fn_return = fn_return0; fn_params = fn_params0; fn_vars = fn_vars0;
    1225     fn_body = fn_body0 } = x_4356
     1225    fn_body = fn_body0 } = x_4369
    12261226  in
    12271227  h_mk_function fn_return0 fn_params0 fn_vars0 fn_body0
     
    12301230    (type0 -> (AST.ident, type0) Types.prod List.list -> (AST.ident, type0)
    12311231    Types.prod List.list -> statement -> 'a1) -> function0 -> 'a1 **)
    1232 let rec function_rect_Type2 h_mk_function x_4358 =
     1232let rec function_rect_Type2 h_mk_function x_4371 =
    12331233  let { fn_return = fn_return0; fn_params = fn_params0; fn_vars = fn_vars0;
    1234     fn_body = fn_body0 } = x_4358
     1234    fn_body = fn_body0 } = x_4371
    12351235  in
    12361236  h_mk_function fn_return0 fn_params0 fn_vars0 fn_body0
     
    12391239    (type0 -> (AST.ident, type0) Types.prod List.list -> (AST.ident, type0)
    12401240    Types.prod List.list -> statement -> 'a1) -> function0 -> 'a1 **)
    1241 let rec function_rect_Type1 h_mk_function x_4360 =
     1241let rec function_rect_Type1 h_mk_function x_4373 =
    12421242  let { fn_return = fn_return0; fn_params = fn_params0; fn_vars = fn_vars0;
    1243     fn_body = fn_body0 } = x_4360
     1243    fn_body = fn_body0 } = x_4373
    12441244  in
    12451245  h_mk_function fn_return0 fn_params0 fn_vars0 fn_body0
     
    12481248    (type0 -> (AST.ident, type0) Types.prod List.list -> (AST.ident, type0)
    12491249    Types.prod List.list -> statement -> 'a1) -> function0 -> 'a1 **)
    1250 let rec function_rect_Type0 h_mk_function x_4362 =
     1250let rec function_rect_Type0 h_mk_function x_4375 =
    12511251  let { fn_return = fn_return0; fn_params = fn_params0; fn_vars = fn_vars0;
    1252     fn_body = fn_body0 } = x_4362
     1252    fn_body = fn_body0 } = x_4375
    12531253  in
    12541254  h_mk_function fn_return0 fn_params0 fn_vars0 fn_body0
     
    13221322    clight_fundef -> 'a1 **)
    13231323let rec clight_fundef_rect_Type4 h_CL_Internal h_CL_External = function
    1324 | CL_Internal x_4384 -> h_CL_Internal x_4384
    1325 | CL_External (x_4387, x_4386, x_4385) -> h_CL_External x_4387 x_4386 x_4385
     1324| CL_Internal x_4397 -> h_CL_Internal x_4397
     1325| CL_External (x_4400, x_4399, x_4398) -> h_CL_External x_4400 x_4399 x_4398
    13261326
    13271327(** val clight_fundef_rect_Type5 :
     
    13291329    clight_fundef -> 'a1 **)
    13301330let rec clight_fundef_rect_Type5 h_CL_Internal h_CL_External = function
    1331 | CL_Internal x_4391 -> h_CL_Internal x_4391
    1332 | CL_External (x_4394, x_4393, x_4392) -> h_CL_External x_4394 x_4393 x_4392
     1331| CL_Internal x_4404 -> h_CL_Internal x_4404
     1332| CL_External (x_4407, x_4406, x_4405) -> h_CL_External x_4407 x_4406 x_4405
    13331333
    13341334(** val clight_fundef_rect_Type3 :
     
    13361336    clight_fundef -> 'a1 **)
    13371337let rec clight_fundef_rect_Type3 h_CL_Internal h_CL_External = function
    1338 | CL_Internal x_4398 -> h_CL_Internal x_4398
    1339 | CL_External (x_4401, x_4400, x_4399) -> h_CL_External x_4401 x_4400 x_4399
     1338| CL_Internal x_4411 -> h_CL_Internal x_4411
     1339| CL_External (x_4414, x_4413, x_4412) -> h_CL_External x_4414 x_4413 x_4412
    13401340
    13411341(** val clight_fundef_rect_Type2 :
     
    13431343    clight_fundef -> 'a1 **)
    13441344let rec clight_fundef_rect_Type2 h_CL_Internal h_CL_External = function
    1345 | CL_Internal x_4405 -> h_CL_Internal x_4405
    1346 | CL_External (x_4408, x_4407, x_4406) -> h_CL_External x_4408 x_4407 x_4406
     1345| CL_Internal x_4418 -> h_CL_Internal x_4418
     1346| CL_External (x_4421, x_4420, x_4419) -> h_CL_External x_4421 x_4420 x_4419
    13471347
    13481348(** val clight_fundef_rect_Type1 :
     
    13501350    clight_fundef -> 'a1 **)
    13511351let rec clight_fundef_rect_Type1 h_CL_Internal h_CL_External = function
    1352 | CL_Internal x_4412 -> h_CL_Internal x_4412
    1353 | CL_External (x_4415, x_4414, x_4413) -> h_CL_External x_4415 x_4414 x_4413
     1352| CL_Internal x_4425 -> h_CL_Internal x_4425
     1353| CL_External (x_4428, x_4427, x_4426) -> h_CL_External x_4428 x_4427 x_4426
    13541354
    13551355(** val clight_fundef_rect_Type0 :
     
    13571357    clight_fundef -> 'a1 **)
    13581358let rec clight_fundef_rect_Type0 h_CL_Internal h_CL_External = function
    1359 | CL_Internal x_4419 -> h_CL_Internal x_4419
    1360 | CL_External (x_4422, x_4421, x_4420) -> h_CL_External x_4422 x_4421 x_4420
     1359| CL_Internal x_4432 -> h_CL_Internal x_4432
     1360| CL_External (x_4435, x_4434, x_4433) -> h_CL_External x_4435 x_4434 x_4433
    13611361
    13621362(** val clight_fundef_inv_rect_Type4 :
     
    15321532(** val mode_rect_Type4 :
    15331533    (AST.typ -> 'a1) -> 'a1 -> (AST.typ -> 'a1) -> AST.typ -> mode -> 'a1 **)
    1534 let rec mode_rect_Type4 h_By_value h_By_reference h_By_nothing x_4472 = function
     1534let rec mode_rect_Type4 h_By_value h_By_reference h_By_nothing x_4485 = function
    15351535| By_value t -> h_By_value t
    15361536| By_reference -> h_By_reference
     
    15391539(** val mode_rect_Type5 :
    15401540    (AST.typ -> 'a1) -> 'a1 -> (AST.typ -> 'a1) -> AST.typ -> mode -> 'a1 **)
    1541 let rec mode_rect_Type5 h_By_value h_By_reference h_By_nothing x_4477 = function
     1541let rec mode_rect_Type5 h_By_value h_By_reference h_By_nothing x_4490 = function
    15421542| By_value t -> h_By_value t
    15431543| By_reference -> h_By_reference
     
    15461546(** val mode_rect_Type3 :
    15471547    (AST.typ -> 'a1) -> 'a1 -> (AST.typ -> 'a1) -> AST.typ -> mode -> 'a1 **)
    1548 let rec mode_rect_Type3 h_By_value h_By_reference h_By_nothing x_4482 = function
     1548let rec mode_rect_Type3 h_By_value h_By_reference h_By_nothing x_4495 = function
    15491549| By_value t -> h_By_value t
    15501550| By_reference -> h_By_reference
     
    15531553(** val mode_rect_Type2 :
    15541554    (AST.typ -> 'a1) -> 'a1 -> (AST.typ -> 'a1) -> AST.typ -> mode -> 'a1 **)
    1555 let rec mode_rect_Type2 h_By_value h_By_reference h_By_nothing x_4487 = function
     1555let rec mode_rect_Type2 h_By_value h_By_reference h_By_nothing x_4500 = function
    15561556| By_value t -> h_By_value t
    15571557| By_reference -> h_By_reference
     
    15601560(** val mode_rect_Type1 :
    15611561    (AST.typ -> 'a1) -> 'a1 -> (AST.typ -> 'a1) -> AST.typ -> mode -> 'a1 **)
    1562 let rec mode_rect_Type1 h_By_value h_By_reference h_By_nothing x_4492 = function
     1562let rec mode_rect_Type1 h_By_value h_By_reference h_By_nothing x_4505 = function
    15631563| By_value t -> h_By_value t
    15641564| By_reference -> h_By_reference
     
    15671567(** val mode_rect_Type0 :
    15681568    (AST.typ -> 'a1) -> 'a1 -> (AST.typ -> 'a1) -> AST.typ -> mode -> 'a1 **)
    1569 let rec mode_rect_Type0 h_By_value h_By_reference h_By_nothing x_4497 = function
     1569let rec mode_rect_Type0 h_By_value h_By_reference h_By_nothing x_4510 = function
    15701570| By_value t -> h_By_value t
    15711571| By_reference -> h_By_reference
Note: See TracChangeset for help on using the changeset viewer.