Project

General

Profile

« Previous | Next » 

Revision 36454535

Added by Pierre-Loïc Garoche over 10 years ago

Merged horn_traces branch

View differences:

src/machine_code.ml
86 86
  step_outputs: var_decl list;
87 87
  step_locals: var_decl list;
88 88
  step_instrs: instr_t list;
89
  step_asserts: value_t list;
89 90
}
90 91

  
91 92
type static_call = top_decl * (Dimension.dim_expr list)
......
103 104
}
104 105

  
105 106
let pp_step fmt s =
106
  Format.fprintf fmt "@[<v>inputs : %a@ outputs: %a@ locals : %a@ checks : %a@ instrs : @[%a@]@]@ "
107
  Format.fprintf fmt "@[<v>inputs : %a@ outputs: %a@ locals : %a@ checks : %a@ instrs : @[%a@]@ asserts : @[%a@]@]@ "
107 108
    (Utils.fprintf_list ~sep:", " Printers.pp_var) s.step_inputs
108 109
    (Utils.fprintf_list ~sep:", " Printers.pp_var) s.step_outputs
109 110
    (Utils.fprintf_list ~sep:", " Printers.pp_var) s.step_locals
110 111
    (Utils.fprintf_list ~sep:", " (fun fmt (_, c) -> pp_val fmt c)) s.step_checks
111 112
    (Utils.fprintf_list ~sep:"@ " pp_instr) s.step_instrs
113
    (Utils.fprintf_list ~sep:", " pp_val) s.step_asserts
114

  
112 115

  
113 116
let pp_static_call fmt (node, args) =
114 117
 Format.fprintf fmt "%s<%a>"
......
117 120

  
118 121
let pp_machine fmt m =
119 122
  Format.fprintf fmt 
120
    "@[<v 2>machine %s@ mem      : %a@ instances: %a@ init     : %a@ step     :@   @[<v 2>%a@]@ @]@ "
123
    "@[<v 2>machine %s@ mem      : %a@ instances: %a@ init     : %a@ step     :@   @[<v 2>%a@]@ @  spec : @[%t@]@  annot : @[%a@]@]@ "
121 124
    m.mname.node_id
122 125
    (Utils.fprintf_list ~sep:", " Printers.pp_var) m.mmemory
123 126
    (Utils.fprintf_list ~sep:", " (fun fmt (o1, o2) -> Format.fprintf fmt "(%s, %a)" o1 pp_static_call o2)) m.minstances
124 127
    (Utils.fprintf_list ~sep:"@ " pp_instr) m.minit
125 128
    pp_step m.mstep
129
    (fun fmt -> match m.mspec with | None -> () | Some spec -> Printers.pp_spec fmt spec)
130
    (Utils.fprintf_list ~sep:"@ " Printers.pp_expr_annot) m.mannot
126 131

  
127 132
(* Returns the declared stateless status and the computed one. *)
128 133
let get_stateless_status m =
......
199 204
      step_instrs = [conditional (StateVar var_state)
200 205
			         [MStateAssign(var_state, Cst (const_of_bool false));
201 206
                                  MLocalAssign(var_output, LocalVar var_input1)]
202
                                 [MLocalAssign(var_output, LocalVar var_input2)] ]
207
                                 [MLocalAssign(var_output, LocalVar var_input2)] ];
208
      step_asserts = [];
203 209
    };
204 210
    mspec = None;
205 211
    mannot = [];
......
457 463
  ;
458 464

  
459 465
  let init_args = ISet.empty, [], Utils.IMap.empty, List.fold_right (fun l -> ISet.add l) nd.node_locals ISet.empty, [] in
466
  (* memories, init instructions, node calls, local variables (including memories), step instrs *)
460 467
  let m, init, j, locals, s = translate_eqs nd init_args (List.rev eqs_rev) in
461 468
  let mmap = Utils.IMap.fold (fun i n res -> (i, n)::res) j [] in
462 469
  {
......
479 486
	| "horn" -> s
480 487
	| "C" | "java" | _ -> join_guards_list s
481 488
      );
489
      step_asserts = 
490
	let exprl = List.map (fun assert_ -> assert_.assert_expr ) nd.node_asserts in
491
	List.map (translate_expr nd init_args) exprl
492
	;
482 493
    };
483 494
    mspec = nd.node_spec;
484 495
    mannot = nd.node_annot;

Also available in: Unified diff