Project

General

Profile

« Previous | Next » 

Revision e164af45

Added by LĂ©lio Brun over 2 years ago

working version with additional asserts to make the axiom work

View differences:

src/backends/C/c_backend_spec.ml
107 107

  
108 108
let pp_at pp_v fmt (v, l) = fprintf fmt "\\at(%a, %s)" pp_v v l
109 109

  
110
let pp_at_pre pp_v fmt v = pp_at pp_v fmt (v, "Pre")
111

  
110 112
let find_machine f =
111 113
  List.find (fun m -> m.mname.node_id = f)
112 114

  
......
1460 1462
      | None ->
1461 1463
        [ mem, pp_print_string ])
1462 1464

  
1463
  let pp_contract fmt machines _self m =
1464
    match m.mspec.mnode_spec with
1465
    | Some (NodeSpec f) ->
1466
      let m_f = find_machine f machines in
1467
      pp_acsl_line'_cut
1468
        (pp_ghost
1469
           (fun fmt () ->
1470
              fprintf
1471
                fmt
1472
                "%a(%a%a);"
1473
                pp_machine_step_name
1474
                m_f.mname.node_id
1475
                (pp_comma_list ~pp_eol:pp_print_comma (pp_c_var_read m))
1476
                m_f.mstep.step_inputs
1477
                (pp_comma_list (pp_c_var_write m))
1478
                m_f.mstep.step_outputs))
1479
        fmt ()
1480
    | _ -> ()
1465
  let pp_contract fmt machines _self mem m =
1466
    let pp_vars ?pp_eol = pp_comma_list ?pp_eol (pp_c_var_read m) in
1467
    match contract_of machines m with
1468
    | Some c, Some m_c ->
1469
      fprintf fmt "%a%a"
1470
        (pp_acsl_line'_cut
1471
           (pp_ghost
1472
              (fun fmt () ->
1473
                 fprintf
1474
                   fmt
1475
                   "%a(%a%a);"
1476
                   pp_machine_step_name
1477
                   m_c.mname.node_id
1478
                   (pp_vars ~pp_eol:pp_print_comma)
1479
                   m_c.mstep.step_inputs
1480
                   (pp_comma_list (pp_c_var_write m))
1481
                   m_c.mstep.step_outputs)))
1482
        ()
1483
        (pp_acsl_cut
1484
           (pp_print_option
1485
              (fun fmt -> function
1486
                 | Kinduction k ->
1487
                   let l = List.init k (fun n -> n + 1) in
1488
                   let pp_mem_in = pp_at_pre pp_ptr in
1489
                   let pp_mem_out = pp_ptr in
1490
                   pp_assert
1491
                     (pp_and
1492
                        (pp_and_l
1493
                           (fun fmt n ->
1494
                              (if n = k then
1495
                                 pp_k_induction_inductive_case
1496
                               else
1497
                                 pp_k_induction_base_case)
1498
                                m
1499
                                pp_mem_in
1500
                                pp_mem_out
1501
                                pp_vars
1502
                                fmt
1503
                                (n, mem, mem)))
1504
                        (pp_transition_aux m_c pp_print_string pp_print_string (pp_c_var_read m)))
1505
                     fmt
1506
                     (l, (m_c.mname.node_id,
1507
                          m_c.mstep.step_inputs @ m_c.mstep.step_outputs,
1508
                          "", ""))))) c.mc_proof
1509
        | _, _ -> ()
1481 1510

  
1482 1511
end
1483 1512

  

Also available in: Unified diff