Project

General

Profile

« Previous | Next » 

Revision d0f26f04

Added by LĂ©lio Brun 7 months ago

corrections for stateless nodes

View differences:

src/backends/Horn/horn_backend_traces.ml
27 27

  
28 28
(* Compute memories associated to each machine *)
29 29
let compute_mems machines m =
30
  let rec aux fst prefix m =
30
  let rec aux prefix m =
31 31
    List.map (fun mem -> prefix, mem) m.mmemory
32 32
    @ List.fold_left
33 33
        (fun accu (id, (n, _)) ->
......
35 35
          if name = "_arrow" then accu
36 36
          else
37 37
            let machine_n = get_machine machines name in
38
            aux false ((id, machine_n) :: prefix) machine_n @ accu)
38
            aux ((id, machine_n) :: prefix) machine_n @ accu)
39 39
        [] m.minstances
40 40
  in
41
  aux true [] m
41
  aux [] m
42 42

  
43 43
(* We extract the annotation dealing with traceability *)
44 44
let machines_traces machines =

Also available in: Unified diff