Project

General

Profile

« Previous | Next » 

Revision 3d1f9d9f

Added by LĂ©lio Brun over 2 years ago

more agressive optim propagation in spec in order to remove unecessarry existential variables that were eliminated (helps the solvers)

View differences:

src/backends/C/c_backend_spec.ml
421 421
         then pp_double_cast pp
422 422
         else pp
423 423
       else pp) fmt v
424
    | Tag t ->
424
    | Tag (t, _) ->
425 425
      pp_print_string fmt t
426 426
    | Var v ->
427 427
      pp_var_decl fmt v
......
489 489
  let val_of_expr = function
490 490
    | Val v ->
491 491
      v
492
    | Tag t ->
492
    | Tag (t, _) ->
493 493
      id_to_tag t
494 494
    | Var v ->
495 495
      vdecl_to_val v
......
520 520

  
521 521
  let has_memory m = function Val v -> has_memory_val m v | _ -> false
522 522

  
523
  let pp_spec mode m =
523
  let pp_spec mode m fmt f =
524 524
    let rec pp_spec mode fmt f =
525 525
      let mem_in, mem_in', indirect_r, mem_out, mem_out', indirect_l =
526 526
        let self = mk_self m in
......
562 562
            (pp_c_var_read ~test_output:false m)
563 563
            indirect_r
564 564
            fmt
565
            (Spec_common.type_of_l_value a, val_of_expr a, val_of_expr b)
565
            (Spec_common.type_of_value a, val_of_expr a, val_of_expr b)
566 566
        in
567 567
        if has_memory m b then
568 568
          let inst = find_arrow Location.dummy m in
......
585 585
          (pp_c_var_read ~test_output:false m)
586 586
          indirect_r
587 587
          fmt
588
          (Spec_common.type_of_l_value a, val_of_expr a, val_of_expr b)
588
          (Spec_common.type_of_value a, val_of_expr a, val_of_expr b)
589 589
      | And fs ->
590 590
        pp_and_l pp_spec' fmt fs
591 591
      | Or fs ->
......
647 647
        pp_c_val m mem_in (pp_c_var_read ~test_output:true m) fmt v
648 648
    in
649 649

  
650
    pp_spec mode
650
    pp_spec mode fmt (Spec_common.red f)
651 651
end
652 652

  
653 653
let pp_predicate pp_l pp_r fmt (l, r) =

Also available in: Unified diff