Project

General

Profile

« Previous | Next » 

Revision 0292f958

Added by Pierre-Loïc Garoche about 5 years ago

Export cocospec contract

View differences:

src/tools/seal/seal_export.ml
65 65 
  let e_step = process_sw (Corelang.add_pre_expr vl) sw_step in
66 66 
  let e_init_out = process_sw (fun x -> x) init_out in
67 67 
  let e_update_out = process_sw (Corelang.add_pre_expr vl) update_out in
68 
  let loc = Location.dummy_loc in
68 
  let loc = Location.dummy_loc in
69 
  (* Build the contract: guarentee output = orig_node(input) *)
70 
  let expr_of_vars vl =
71 
    Corelang.expr_of_expr_list loc
72 
      (List.map Corelang.expr_of_vdecl vl)
73 
  in
74 
  let input_e = expr_of_vars  copy_nd.node_inputs in
75 
  let output_e = expr_of_vars  copy_nd.node_outputs in
76 
  let call_orig_e =
77 
    Corelang.mkexpr loc (Expr_appl (orig_nd.node_id, input_e , None)) in
78 
  let args = Corelang.mkexpr loc (Expr_tuple([output_e; call_orig_e])) in
79 
  let eq_expr = (Corelang.mkexpr loc (Expr_appl ("=", args, None))) in
80 
  let contract = {
81 
      consts = [];
82 
      locals = [];
83 
      stmts = [];
84 
      assume = [];
85 
      guarantees = [Corelang.mkeexpr loc eq_expr];
86 
      modes = [];
87 
      imports = [];
88 
      spec_loc = loc;
89
90 
    }
91 
  in
69 92 
  { copy_nd with
70 93 
    node_id = copy_nd.node_id ^ "_seal";
71 94 
    node_locals = m.mmemory;
......
79 102 
                      eq_lhs = List.map (fun v -> v.var_id) copy_nd.node_outputs;
80 103 
                      eq_rhs = Corelang.mkexpr loc (Expr_arrow(e_init_out, e_update_out))
81 104 
                    };
82 
                 ]
105 
                 ];
106 
    node_spec = Some (Contract contract);
107
83 108 
(*
84 109 
                   il faut mettre un pre devant chaque memoire dans les updates comme dans les gardes par contre pas besoin de mettre de pre devant les entrees, ni dans les updates, ni dans les gardes
85 110 

  		












Also available in:  Unified diff