Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / backends / C / c_backend_spec.ml @ cd670fe1

History | View | Annotate | Download (4.75 KB)

1
(**************************************************************************)
2
(*     Printing spec for c *)
3

    
4
(**************************************************************************)
5

    
6

    
7
let pp_econst fmt c = 
8
  match c with
9
    | EConst_int i -> pp_print_int fmt i
10
    | EConst_real r -> pp_print_string fmt r
11
    | EConst_float r -> pp_print_float fmt r
12
    | EConst_bool b -> pp_print_bool fmt b
13
    | EConst_string s -> pp_print_string fmt ("\"" ^ s ^ "\"")
14

    
15
let rec pp_eexpr is_output fmt eexpr = 
16
  let pp_eexpr = pp_eexpr is_output in
17
  match eexpr.eexpr_desc with
18
    | EExpr_const c -> pp_econst fmt c
19
    | EExpr_ident id -> 
20
      if is_output id then pp_print_string fmt ("*" ^ id) else pp_print_string fmt id
21
    | EExpr_tuple el -> Utils.fprintf_list ~sep:"," pp_eexpr fmt el
22
    | EExpr_arrow (e1, e2) -> fprintf fmt "%a -> %a" pp_eexpr e1 pp_eexpr e2
23
    | EExpr_fby (e1, e2) -> fprintf fmt "%a fby %a" pp_eexpr e1 pp_eexpr e2
24
    (* | EExpr_concat (e1, e2) -> fprintf fmt "%a::%a" pp_eexpr e1 pp_eexpr e2 *)
25
    (* | EExpr_tail e -> fprintf fmt "tail %a" pp_eexpr e *)
26
    | EExpr_pre e -> fprintf fmt "pre %a" pp_eexpr e
27
    | EExpr_when (e, id) -> fprintf fmt "%a when %s" pp_eexpr e id
28
    | EExpr_merge (id, e1, e2) -> 
29
      fprintf fmt "merge (%s, %a, %a)" id pp_eexpr e1 pp_eexpr e2
30
    | EExpr_appl (id, e, r) -> pp_eapp is_output fmt id e r
31
    | EExpr_forall (vars, e) -> fprintf fmt "forall %a; %a" Printers.pp_node_args vars pp_eexpr e 
32
    | EExpr_exists (vars, e) -> fprintf fmt "exists %a; %a" Printers.pp_node_args vars pp_eexpr e 
33

    
34

    
35
    (* | EExpr_whennot _ *)
36
    (* | EExpr_uclock _ *)
37
    (* | EExpr_dclock _ *)
38
    (* | EExpr_phclock _ -> assert false *)
39
and pp_eapp is_output fmt id e r =
40
  let pp_eexpr = pp_eexpr is_output in
41
  match r with
42
  | None ->
43
    (match id, e.eexpr_desc with
44
    | "+", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a + %a)" pp_eexpr e1 pp_eexpr e2
45
    | "uminus", _ -> fprintf fmt "(- %a)" pp_eexpr e
46
    | "-", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a - %a)" pp_eexpr e1 pp_eexpr e2
47
    | "*", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a * %a)" pp_eexpr e1 pp_eexpr e2
48
    | "/", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a / %a)" pp_eexpr e1 pp_eexpr e2
49
    | "mod", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a mod %a)" pp_eexpr e1 pp_eexpr e2
50
    | "&&", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a && %a)" pp_eexpr e1 pp_eexpr e2
51
    | "||", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a || %a)" pp_eexpr e1 pp_eexpr e2
52
    | "xor", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a ^^ %a)" pp_eexpr e1 pp_eexpr e2
53
    | "impl", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a ==> %a)" pp_eexpr e1 pp_eexpr e2
54
    | "<", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a < %a)" pp_eexpr e1 pp_eexpr e2
55
    | "<=", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a <= %a)" pp_eexpr e1 pp_eexpr e2
56
    | ">", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a > %a)" pp_eexpr e1 pp_eexpr e2
57
    | ">=", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a >= %a)" pp_eexpr e1 pp_eexpr e2
58
    | "!=", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a != %a)" pp_eexpr e1 pp_eexpr e2
59
    | "=", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a == %a)" pp_eexpr e1 pp_eexpr e2
60
    | "not", _ -> fprintf fmt "(! %a)" pp_eexpr e
61
    | "ite", EExpr_tuple([e1;e2;e3]) -> fprintf fmt "(if %a then %a else %a)" pp_eexpr e1 pp_eexpr e2 pp_eexpr e3
62
    | _ -> fprintf fmt "%s (%a)" id pp_eexpr e)
63
  | Some x -> fprintf fmt "%s (%a) every %s" id pp_eexpr e x 
64

    
65
let pp_ensures is_output fmt e =
66
  match e with
67
    | EnsuresExpr e -> fprintf fmt "ensures %a;@ " (pp_eexpr is_output) e
68
    | SpecObserverNode (name, args) -> fprintf fmt "observer %s (%a);@ " name (Utils.fprintf_list ~sep:", " (pp_eexpr is_output)) args
69

    
70
let pp_acsl_spec outputs fmt spec =
71
  let is_output = fun oid -> List.exists (fun v -> v.var_id = oid) outputs in
72
  let pp_eexpr = pp_eexpr is_output in
73
  fprintf fmt "@[<v 2>/*@@ ";
74
  Utils.fprintf_list ~sep:"" (fun fmt r -> fprintf fmt "requires %a;@ " pp_eexpr r) fmt spec.requires;
75
  Utils.fprintf_list ~sep:"" (pp_ensures is_output) fmt spec.ensures;
76
  fprintf fmt "@ ";
77
  (* fprintf fmt "assigns *self%t%a;@ "  *)
78
  (*   (fun fmt -> if List.length outputs > 0 then fprintf fmt ", ") *)
79
  (*   (fprintf_list ~sep:"," (fun fmt v -> fprintf fmt "*%s" v.var_id)) outputs; *)
80
  Utils.fprintf_list ~sep:"@ " (fun fmt (name, assumes, requires) -> 
81
    fprintf fmt "behavior %s:@[@ %a@ %a@]" 
82
      name
83
      (Utils.fprintf_list ~sep:"@ " (fun fmt r -> fprintf fmt "assumes %a;" pp_eexpr r)) assumes
84
      (Utils.fprintf_list ~sep:"@ " (pp_ensures is_output)) requires
85
  ) fmt spec.behaviors;
86
  fprintf fmt "@]@ */@.";
87
  ()
88

    
89

    
90

    
91

    
92
let print_machine_decl_prefix fmt m =
93
   (* Print specification if any *)
94
   (match m.mspec with
95
  | None -> ()
96
  | Some spec -> 
97
    pp_acsl_spec m.mstep.step_outputs fmt spec
98
  )
99

    
100
(* Local Variables: *)
101
(* compile-command:"make -C ../../.." *)
102
(* End: *)