Project

General

Profile

« Previous | Next » 

Revision 6d1693b9

Added by LĂ©lio Brun 7 months ago

work on spec generation almost done

View differences:

src/machine_code_types.ml
23 23
    instr_desc: instr_t_desc; (* main data: the content *)
24 24
    (* lustre_expr: expr option; (* possible representation as a lustre expression *) *)
25 25
    lustre_eq: eq option;     (* possible representation as a lustre flow equation *)
26
    instr_spec: mc_formula_t
26
    instr_spec: mc_formula_t list
27 27
  }
28 28
and instr_t_desc =
29 29
  | MLocalAssign of var_decl * value_t
30 30
  | MStateAssign of var_decl * value_t
31
  | MReset of ident
31
  | MClearReset
32
  | MSetReset of ident
32 33
  | MNoReset of ident
33 34
  | MStep of var_decl list * ident * value_t list
34 35
  | MBranch of value_t * (label * instr_t list) list
......
47 48
type static_call = top_decl * (Dimension.dim_expr list)
48 49

  
49 50
type mc_transition_t = value_t transition_t
51
type mc_memory_pack_t = value_t memory_pack_t
50 52

  
51 53
type machine_spec = {
52 54
  mnode_spec: node_spec_t option;
53
  mtransitions: mc_transition_t list
55
  mtransitions: mc_transition_t list;
56
  mmemory_packs: mc_memory_pack_t list
54 57
}
55 58
  
56 59
type machine_t = {

Also available in: Unified diff