Project

General

Profile

Revision af5af1e8 src/horn_backend.ml

View differences:

src/horn_backend.ml
20 20
  | Types.Tarrow _
21 21
  | _                     -> Format.eprintf "internal error: pp_type %a@." 
22 22
                             Types.print_ty t; assert false
23
    
24 23

  
25 24
let pp_decl_var fmt id = 
26 25
  Format.fprintf fmt "(declare-var %s %a)"
......
30 29
let pp_var fmt id = Format.pp_print_string fmt id.var_id
31 30

  
32 31

  
32
let pp_conj pp fmt l = 
33
  match l with 
34
    [] -> assert false
35
  | [x] -> pp fmt x
36
  | _ -> fprintf fmt "(and @[<v 0>%a@]@ )" (Utils.fprintf_list ~sep:" " pp) l
37
    
38

  
39

  
33 40
let concat prefix x = if prefix = "" then x else prefix ^ "." ^ x 
34 41
let rename f = (fun v -> {v with var_id = f v.var_id } )
35 42
let rename_machine p = rename (fun n -> concat p n)
......
134 141
      let (n,_) = List.assoc i m.minstances in
135 142
      match node_name n, inputs, outputs with
136 143
      | "_arrow", [i1; i2], [o] -> begin
137
         if init then
138
           pp_assign
139
   	     m
140
   	     self
141
   	     (pp_horn_var m) 
142
	     (* (pp_horn_val self (pp_horn_var m) fmt o) *)
143
	     fmt
144
   	     o.var_type (LocalVar o) i1
145
         else
146
           pp_assign
147
   	     m self (pp_horn_var m) fmt
148
   	     o.var_type (LocalVar o) i2
149
	     
144
        if init then
145
          pp_assign
146
   	    m
147
   	    self
148
   	    (pp_horn_var m) 
149
	    fmt
150
   	    o.var_type (LocalVar o) i1
151
        else
152
          pp_assign
153
   	    m self (pp_horn_var m) fmt
154
   	    o.var_type (LocalVar o) i2
155
	    
150 156
      end
151 157
      | name, _, _ ->  
152 158
	begin
153 159
	  let target_machine = List.find (fun m  -> m.mname.node_id = name) machines in
154 160
	  if init then
155
	  Format.fprintf fmt "(%a %a%t%a%t%a)"
156
	    pp_machine_init_name (node_name n) 
157
	    (* inputs *)
158
	    (Utils.fprintf_list ~sep:" " (pp_horn_val self (pp_horn_var m))) inputs
159
	    (Utils.pp_final_char_if_non_empty " " inputs) 
160
	    (* outputs *)
161
	    (Utils.fprintf_list ~sep:" " (pp_horn_val self (pp_horn_var m))) (List.map (fun v -> LocalVar v) outputs)
162
	    (Utils.pp_final_char_if_non_empty " " outputs)
163
	    (* memories (next) *)
164
	    (Utils.fprintf_list ~sep:" " pp_var) (
165
  	      rename_machine_list 
166
		(concat m.mname.node_id i) 
167
		(rename_next_list (* concat m.mname.node_id i *) 
168
		   (full_memory_vars machines target_machine)
169
		) 
170
	     )
161
	    Format.fprintf fmt "(%a %a%t%a%t%a)"
162
	      pp_machine_init_name (node_name n) 
163
	      (* inputs *)
164
	      (Utils.fprintf_list ~sep:" " (pp_horn_val self (pp_horn_var m))) 
165
	      inputs
166
	      (Utils.pp_final_char_if_non_empty " " inputs) 
167
	      (* outputs *)
168
	      (Utils.fprintf_list ~sep:" " (pp_horn_val self (pp_horn_var m))) 
169
	      (List.map (fun v -> LocalVar v) outputs)
170
	      (Utils.pp_final_char_if_non_empty " " outputs)
171
	      (* memories (next) *)
172
	      (Utils.fprintf_list ~sep:" " pp_var) (
173
  		rename_machine_list 
174
		  (concat m.mname.node_id i) 
175
		  (rename_next_list (full_memory_vars machines target_machine)
176
		  ) 
177
	       )
171 178
	  else
172 179
	    Format.fprintf fmt "(%a %a%t%a%t%a)"
173 180
	      pp_machine_step_name (node_name n) 
174 181
	      (Utils.fprintf_list ~sep:" " (pp_horn_val self (pp_horn_var m))) inputs
175 182
	      (Utils.pp_final_char_if_non_empty " " inputs) 
176
	      (Utils.fprintf_list ~sep:" " (pp_horn_val self (pp_horn_var m))) (List.map (fun v -> LocalVar v) outputs)
183
	      (Utils.fprintf_list ~sep:" " (pp_horn_val self (pp_horn_var m))) 
184
	      (List.map (fun v -> LocalVar v) outputs)
177 185
	      (Utils.pp_final_char_if_non_empty " " outputs)
178 186
	      (Utils.fprintf_list ~sep:" " pp_var) (
179 187
		(rename_machine_list 
180 188
		   (concat m.mname.node_id i) 
181
		   (rename_current_list (* concat m.mname.node_id i *) 
182
		      (full_memory_vars machines target_machine))
189
		   (rename_current_list (full_memory_vars machines target_machine))
183 190
		) @ 
184 191
		  (rename_machine_list 
185 192
		     (concat m.mname.node_id i) 
186
		     (rename_next_list (* concat m.mname.node_id i *) 
187
			(full_memory_vars machines target_machine))
193
		     (rename_next_list (full_memory_vars machines target_machine))
188 194
		  ) 
189 195
	       )
190 196
	    
......
194 200
      let (n,_) = List.assoc i m.mcalls in
195 201
      Format.fprintf fmt "(%s %a%t%a)"
196 202
	(node_name n)
197
	(Utils.fprintf_list ~sep:" " (pp_horn_val self (pp_horn_var m))) inputs
203
	(Utils.fprintf_list ~sep:" " (pp_horn_val self (pp_horn_var m))) 
204
	inputs
198 205
	(Utils.pp_final_char_if_non_empty " " inputs) 
199
	(Utils.fprintf_list ~sep:" " (pp_horn_val self (pp_horn_var m))) (List.map (fun v -> LocalVar v) outputs)
200
	(* (Utils.fprintf_list ~sep:" " (pp_horn_var m)) outputs  *)
206
	(Utils.fprintf_list ~sep:" " (pp_horn_val self (pp_horn_var m))) 
207
	(List.map (fun v -> LocalVar v) outputs)
201 208
    )
202 209

  
203 210
let pp_machine_init (m: machine_t) self fmt inst =
......
229 236
    pp_assign
230 237
      m self (pp_horn_var m) fmt
231 238
      i.var_type (StateVar i) v
232
  | MStep ([i0], i, vl) when Basic_library.is_internal_fun i  -> assert false (* This should not happen anymore *)
233
(*    pp_machine_instr machines ~init:init m self fmt (MLocalAssign (i0, Fun (i, vl))) *)
239
  | MStep ([i0], i, vl) when Basic_library.is_internal_fun i  -> 
240
    assert false (* This should not happen anymore *)
234 241
  | MStep (il, i, vl) ->
235 242
    pp_instance_call machines ~init:init m self fmt i vl il
236 243
  | MBranch (g,hl) ->
237 244
    if hl <> [] && let t = fst (List.hd hl) in t = tag_true || t = tag_false
238 245
    then (* boolean case, needs special treatment in C because truth value is not unique *)
239
	 (* may disappear if we optimize code by replacing last branch test with default *)
246
      (* may disappear if we optimize code by replacing last branch test with default *)
240 247
      let tl = try List.assoc tag_true  hl with Not_found -> [] in
241 248
      let el = try List.assoc tag_false hl with Not_found -> [] in
242 249
      pp_conditional machines ~init:init m self fmt g tl el
......
279 286
	 (List.map (fun v -> v.var_type) (stateless_vars machines m));
280 287
       
281 288
       (* Rule for single predicate *)
282
       Format.fprintf fmt "@[<v 2>(rule (=> @ (and @[<v 0>%a@]@ )@ (%a %a)@]@.))@.@."
283
	 (Utils.fprintf_list ~sep:"@ " 
284
	    (pp_instr 
285
	       true (* In this case, the boolean init can be set to true or false. 
286
		       The node is stateless. *)
287
	       m.mname.node_id)
288
	 ) 
289
       Format.fprintf fmt "@[<v 2>(rule (=> @ %a@ (%a %a)@]@.))@.@."
290
	 (pp_conj (pp_instr 
291
		     true (* In this case, the boolean init can be set to true or false. 
292
			     The node is stateless. *)
293
		     m.mname.node_id)
294
	 )
289 295
	 m.mstep.step_instrs
290 296
	 pp_machine_stateless_name m.mname.node_id
291 297
	 (Utils.fprintf_list ~sep:" " pp_var) (stateless_vars machines m);
......
295 301
       (* Declaring predicate *)
296 302
       Format.fprintf fmt "(declare-rel %a (%a))@."
297 303
	 pp_machine_init_name m.mname.node_id
298
	 (Utils.fprintf_list ~sep:" " pp_type) (List.map (fun v -> v.var_type) (init_vars machines m));
304
	 (Utils.fprintf_list ~sep:" " pp_type) 
305
	 (List.map (fun v -> v.var_type) (init_vars machines m));
299 306
       
300 307
       Format.fprintf fmt "(declare-rel %a (%a))@."
301 308
	 pp_machine_step_name m.mname.node_id
302
	 (Utils.fprintf_list ~sep:" " pp_type) (List.map (fun v -> v.var_type) (step_vars machines m));
309
	 (Utils.fprintf_list ~sep:" " pp_type) 
310
	 (List.map (fun v -> v.var_type) (step_vars machines m));
311
       
303 312
       Format.pp_print_newline fmt ();
304 313

  
305
   (* Rule for init *)
306
       Format.fprintf fmt "@[<v 2>(rule (=> @ (and @[<v 0>%a@]@ )@ (%a %a)@]@.))@.@."
307
	 (Utils.fprintf_list ~sep:"@ " (pp_instr true m.mname.node_id)) m.mstep.step_instrs
314
       (* Rule for init *)
315
       Format.fprintf fmt "@[<v 2>(rule (=> @ %a@ (%a %a)@]@.))@.@."
316
	 (pp_conj (pp_instr true m.mname.node_id)) m.mstep.step_instrs
308 317
	 pp_machine_init_name m.mname.node_id
309 318
	 (Utils.fprintf_list ~sep:" " pp_var) (init_vars machines m);
310 319

  
311
   (* Rule for step *)
312
       Format.fprintf fmt "@[<v 2>(rule (=> @ (and @[<v 0>%a@]@ )@ (%a %a)@]@.))@.@."
313
	 (Utils.fprintf_list ~sep:"@ " (pp_instr false m.mname.node_id)) m.mstep.step_instrs
320
       (* Rule for step *)
321
       Format.fprintf fmt "@[<v 2>(rule (=> @ %a@ (%a %a)@]@.))@.@."
322
	 (pp_conj (pp_instr false m.mname.node_id)) m.mstep.step_instrs
314 323
	 pp_machine_step_name m.mname.node_id
315 324
	 (Utils.fprintf_list ~sep:" " pp_var) (step_vars machines m);
325

  
326
       (* Adding assertions *)
327
       (match m.mstep.step_asserts with
328
       | [] -> ()
329
       | assertsl -> begin
330
	 let pp_val = pp_horn_val ~is_lhs:true m.mname.node_id pp_var in
331
	 
332
	 Format.fprintf fmt "; Asserts@.";
333
	 Format.fprintf fmt "(assert @[<v 2>%a@]@ )@.@.@."
334
	   (pp_conj pp_val) assertsl;
335
	 
336
	 (** TEME: the following code is the one we described. But it generates a segfault in z3 
337
	 Format.fprintf fmt "; Asserts for init@.";
338
	 Format.fprintf fmt "@[<v 2>(assert (=> @ (and @[<v 0>%a@]@ (%a %a))@ %a@]@.))@.@.@."
339
	   (Utils.fprintf_list ~sep:"@ " (pp_instr true m.mname.node_id)) m.mstep.step_instrs
340
	   pp_machine_init_name m.mname.node_id
341
	   (Utils.fprintf_list ~sep:" " pp_var) (init_vars machines m)
342
	   (pp_conj pp_val) assertsl; 
343
	  
344
	 Format.fprintf fmt "; Asserts for step@.";
345
	 Format.fprintf fmt "@[<v 2>(assert (=> @ (and @[<v 0>%a@]@ (%a %a))@ %a@]@.))@.@."
346
	   (Utils.fprintf_list ~sep:"@ " (pp_instr false m.mname.node_id)) m.mstep.step_instrs
347

  
348
	   pp_machine_step_name m.mname.node_id
349
	   (Utils.fprintf_list ~sep:" " pp_var) (step_vars machines m)
350
	   (pp_conj pp_val) assertsl
351
      	 *)
352
       end
353
       );
354
       
316 355
(*
317 356
       match m.mspec with
318 357
	 None -> () (* No node spec; we do nothing *)
......
329 368

  
330 369

  
331 370

  
332
let main_print machines fmt = 
333
if !Options.main_node <> "" then 
334
  begin
335
    let node = !Options.main_node in
336
    let machine = get_machine machines node in
337

  
371
let collecting_semantics machines fmt node machine =
338 372
    Format.fprintf fmt "; Collecting semantics for node %s@.@." node;
339 373
    (* We print the types of the main node "memory tree" TODO: add the output *)
340 374
    let main_output =
......
359 393
      else
360 394
	pp_machine_init_name, pp_machine_step_name
361 395
    in
362
    
396

  
363 397
    Format.fprintf fmt "(declare-rel MAIN (%a))@."
364 398
      (Utils.fprintf_list ~sep:" " pp_type) 
365 399
      (List.map (fun v -> v.var_type) main_memory_next);
......
379 413
      (Utils.fprintf_list ~sep:" " pp_var) main_memory_current
380 414
      step_name node
381 415
      (Utils.fprintf_list ~sep:" " pp_var) (step_vars machines machine)
382
      (Utils.fprintf_list ~sep:" " pp_var) main_memory_next ;
416
      (Utils.fprintf_list ~sep:" " pp_var) main_memory_next 
383 417

  
384
    Format.fprintf fmt "; Property def@.";
385
    Format.fprintf fmt "(declare-rel ERR ())@.";
386
    Format.fprintf fmt "@[<v 2>(rule (=> @ (and @[<v 0>(not (and %a))@ (MAIN %a)@])@ ERR))@."
387
      (Utils.fprintf_list ~sep:" " pp_var) main_output
388
      (Utils.fprintf_list ~sep:" " pp_var) main_memory_next
418
let check_prop machines fmt node machine =
419
  let main_output =
420
    rename_machine_list machine.mname.node_id machine.mstep.step_outputs
421
  in
422
  let main_memory_next = 
423
    (rename_next_list (full_memory_vars machines machine)) @ main_output
424
  in
425
  Format.fprintf fmt "; Property def@.";
426
  Format.fprintf fmt "(declare-rel ERR ())@.";
427
  Format.fprintf fmt "@[<v 2>(rule (=> @ (and @[<v 0>(not %a)@ (MAIN %a)@])@ ERR))@."
428
    (pp_conj pp_var) main_output
429
    (Utils.fprintf_list ~sep:" " pp_var) main_memory_next
389 430
    ;
390
    Format.fprintf fmt "(query ERR)@.";
431
  if !Options.horn_queries then
432
    Format.fprintf fmt "(query ERR)@."
391 433

  
392
    ()
434

  
435
let cex_computation machines fmt node machine =
436
    Format.fprintf fmt "; CounterExample computation for node %s@.@." node;
437
    (* We print the types of the cex node "memory tree" TODO: add the output *)
438
    let cex_input =
439
     rename_machine_list machine.mname.node_id machine.mstep.step_inputs
440
    in
441
    let cex_input_dummy = 
442
     rename_machine_list ("dummy" ^ machine.mname.node_id) machine.mstep.step_inputs
443
    in
444
    let cex_output =
445
     rename_machine_list machine.mname.node_id machine.mstep.step_outputs
446
    in
447
    let cex_output_dummy = 
448
     rename_machine_list ("dummy" ^ machine.mname.node_id) machine.mstep.step_outputs
449
    in
450
    let cex_memory_next = 
451
      cex_input @ (rename_next_list (full_memory_vars machines machine)) @ cex_output
452
    in
453
    let cex_memory_current = 
454
      cex_input_dummy @ (rename_current_list (full_memory_vars machines machine)) @ cex_output_dummy
455
    in
456

  
457
    (* Special case when the cex node is stateless *)
458
    let init_name, step_name = 
459
      if is_stateless machine then
460
	pp_machine_stateless_name, pp_machine_stateless_name
461
      else
462
	pp_machine_init_name, pp_machine_step_name
463
    in
464

  
465
    Format.fprintf fmt "(declare-rel CEX (Int %a))@.@."
466
      (Utils.fprintf_list ~sep:" " pp_type) 
467
      (List.map (fun v -> v.var_type) cex_memory_next);
468
    
469
    Format.fprintf fmt "; Initial set@.";
470
    Format.fprintf fmt "@[<v 2>(rule (=> @ (and @[<v 0>INIT_STATE@ (@[<v 0>%a %a@])@]@ )@ (CEX 0 %a)@]@.))@.@."
471
      init_name node
472
      (Utils.fprintf_list ~sep:" " pp_var) (init_vars machines machine)
473
      (Utils.fprintf_list ~sep:" " pp_var) cex_memory_next ;
474

  
475
    Format.fprintf fmt "; Inductive def@.";
476
    (* Declare dummy inputs. Outputs should have been declared previously with collecting sem *)
477
    (Utils.fprintf_list ~sep:" " (fun fmt v -> Format.fprintf fmt "%a@." pp_decl_var v)) fmt cex_input_dummy;
478
    Format.fprintf fmt "(declare-var cexcpt Int)@.";
479
    Format.fprintf fmt 
480
      "@[<v 2>(rule (=> @ (and @[<v 0>(CEX cexcpt %a)@ (@[<v 0>%a %a@])@]@ )@ (CEX (+ 1 cexcpt) %a)@]@.))@.@."
481
      (Utils.fprintf_list ~sep:" " pp_var) cex_memory_current
482
      step_name node
483
      (Utils.fprintf_list ~sep:" " pp_var) (step_vars machines machine)
484
      (Utils.fprintf_list ~sep:" " pp_var) cex_memory_next 
485

  
486
let get_cex machines fmt node machine =
487
    let cex_input =
488
     rename_machine_list machine.mname.node_id machine.mstep.step_inputs
489
    in
490
    let cex_output =
491
     rename_machine_list machine.mname.node_id machine.mstep.step_outputs
492
    in
493
  let cex_memory_next = 
494
    cex_input @ (rename_next_list (full_memory_vars machines machine)) @ cex_output
495
  in
496
  Format.fprintf fmt "; Property def@.";
497
  Format.fprintf fmt "(declare-rel CEXTRACE ())@.";
498
  Format.fprintf fmt "@[<v 2>(rule (=> @ (and @[<v 0>(not %a)@ (CEX cexcpt %a)@])@ CEXTRACE))@."
499
    (pp_conj pp_var) cex_output
500
    (Utils.fprintf_list ~sep:" " pp_var) cex_memory_next
501
    ;
502
  if !Options.horn_queries then
503
    Format.fprintf fmt "(query CEXTRACE)@."
504

  
505

  
506
let main_print machines fmt = 
507
if !Options.main_node <> "" then 
508
  begin
509
    let node = !Options.main_node in
510
    let machine = get_machine machines node in
511

  
512

  
513
    collecting_semantics machines fmt node machine;
514
    check_prop machines fmt node machine;
515

  
516
    cex_computation machines fmt node machine;
517
    get_cex machines fmt node machine 
393 518
end
394 519

  
395 520

  
......
399 524
  main_print machines fmt 
400 525

  
401 526

  
527
let traces_file fmt basename prog machines =
528
  Format.fprintf fmt 
529
    "; Horn code traceability generated by %s@.; SVN version number %s@.@."
530
    (Filename.basename Sys.executable_name) 
531
    Version.number;
532

  
533
  (* We extract the annotation dealing with traceability *)
534
  let machines_traces = List.map (fun m -> 
535
    let traces : (ident * expr) list= 
536
      let all_annots = List.flatten (List.map (fun ann -> ann.annots) m.mannot) in
537
      let filtered = 
538
	List.filter (fun (kwds, _) -> kwds = ["horn_backend";"trace"]) all_annots 
539
      in
540
      let content = List.map snd filtered in
541
      (* Elements are supposed to be a pair (tuple): variable, expression *)
542
      List.map (fun ee -> 
543
	match ee.eexpr_quantifiers, ee.eexpr_qfexpr.expr_desc with 
544
	| [], Expr_tuple [v;e] -> (
545
	  match v.expr_desc with 
546
	  | Expr_ident vid -> vid, e 
547
	  | _ -> assert false )
548
	| _ -> assert false)
549
	content
550
    in
551
    
552
    m, traces
553

  
554
  ) machines
555
  in
556

  
557
  (* Compute memories associated to each machine *)
558
  let compute_mems m =
559
    let rec aux fst prefix m =
560
      (List.map (fun mem -> (prefix, mem)) m.mmemory) @
561
	List.fold_left (fun accu (id, (n, _)) -> 
562
	  let name = node_name n in 
563
	  if name = "_arrow" then accu else
564
	    let machine_n = get_machine machines name in
565
	    ( aux false ((id,machine_n)::prefix) machine_n ) 
566
	    @ accu
567
	) [] m.minstances 
568
    in
569
    aux true [] m
570
  in
571

  
572
  List.iter (fun m ->
573
    Format.fprintf fmt "; Node %s@." m.mname.node_id;
574
    
575
    let memories_old = 
576
      List.map (fun (p, v) -> 
577
	let machine = match p with | [] -> m | (_,m')::_ -> m' in
578
	let traces = List.assoc machine machines_traces in
579
	if List.mem_assoc v.var_id traces then
580
	  (* We take the expression associated to variable v in the trace info *)
581
	  p, List.assoc v.var_id traces
582
	else
583
	  (* We keep the variable as is: we create an expression v *)
584
	  p, mkexpr Location.dummy_loc (Expr_ident v.var_id)
585
	    
586
      ) (compute_mems m) 
587
    in
588
    let memories_next = (* We remove the topest pre in each expression *)
589
      List.map 
590
	(fun (prefix, ee) -> 
591
	  match ee.expr_desc with 
592
	  | Expr_pre e -> prefix, e 
593
	  | _ -> Format.eprintf 
594
	    "Mem Failure: (prefix: %a, eexpr: %a)@.@?" 
595
	    (Utils.fprintf_list ~sep:"," 
596
	       (fun fmt (id,n) -> fprintf fmt "(%s,%s)" id n.mname.node_id )) 
597
	    (List.rev prefix) 
598
	    Printers.pp_expr ee; 
599
	    assert false)
600
	memories_old
601
    in
602

  
603
    let pp_prefix_rev fmt prefix =
604
      Utils.fprintf_list ~sep:"." (fun fmt (id,n) -> fprintf fmt "(%s,%s)" id n.mname.node_id) fmt (List.rev prefix)
605
    in
606

  
607
    Format.fprintf fmt "; Init predicate@.";
608

  
609
    Format.fprintf fmt "; horn encoding@.";
610
    Format.fprintf fmt "(%a %a)@."
611
      pp_machine_init_name m.mname.node_id
612
      (Utils.fprintf_list ~sep:" " pp_var) (init_vars machines m);
613

  
614
    Format.fprintf fmt "; original expressions@.";
615
    Format.fprintf fmt "(%a %a%t%a)@."
616
      pp_machine_init_name m.mname.node_id
617
      (Utils.fprintf_list ~sep:" " pp_var) (m.mstep.step_inputs@m.mstep.step_outputs)
618
      (fun fmt -> match memories_next with [] -> () | _ -> fprintf fmt " ")
619
      (Utils.fprintf_list ~sep:" " (fun fmt (prefix, ee) -> fprintf fmt "%a(%a)" pp_prefix_rev prefix Printers.pp_expr ee)) memories_next;
620

  
621
    Format.pp_print_newline fmt ();
622
    Format.fprintf fmt "; Step predicate@.";
623

  
624
    Format.fprintf fmt "; horn encoding@.";
625
    Format.fprintf fmt "(%a %a)@."
626
      pp_machine_step_name m.mname.node_id
627
      (Utils.fprintf_list ~sep:" " pp_var) (step_vars machines m);
628
    Format.fprintf fmt "; original expressions@.";
629
    Format.fprintf fmt "(%a %a%t%a)@."
630
      pp_machine_step_name m.mname.node_id
631
      (Utils.fprintf_list ~sep:" " pp_var) (m.mstep.step_inputs@m.mstep.step_outputs)
632
      (fun fmt -> match memories_old with [] -> () | _ -> fprintf fmt " ")
633
      (Utils.fprintf_list ~sep:" " (fun fmt (prefix,ee) -> fprintf fmt "%a(%a)" pp_prefix_rev prefix Printers.pp_expr ee)) (memories_old@memories_next);
634
    Format.pp_print_newline fmt ();    
635
  ) (List.rev machines);
636
  
637

  
402 638
(* Local Variables: *)
403 639
(* compile-command:"make -C .." *)
404 640
(* End: *)

Also available in: Unified diff