Project

General

Profile

« Previous | Next » 

Revision 89fd79f0

Added by Lélio Brun over 2 years ago

a working version for automata with 'last' case of enums as default case

View differences:

src/backends/C/c_backend_spec.ml
202 202

  
203 203
let pp_equal pp_l pp_r fmt (l, r) = fprintf fmt "%a == %a" pp_l l pp_r r
204 204

  
205
let pp_gequal pp_l pp_r fmt (l, r) = fprintf fmt "%a >= %a" pp_l l pp_r r
206

  
205 207
let pp_implies pp_l pp_r fmt (l, r) =
206 208
  fprintf fmt "@[<v>%a ==>@ %a@]" pp_l l pp_r r
207 209

  
......
252 254

  
253 255
let pp_ptr_decl fmt v = pp_ptr fmt v.var_id
254 256

  
255
let pp_basic_assign_spec pp_l pp_r fmt typ var_name value =
257
let pp_basic_assign_spec ?(pp_op=pp_equal) pp_l pp_r fmt typ var_name value =
256 258
  if Types.is_real_type typ && !Options.mpfr then assert false
257 259
    (* Mpfr.pp_inject_assign pp_var fmt (var_name, value) *)
258
  else pp_equal pp_l pp_r fmt (var_name, value)
260
  else pp_op pp_l pp_r fmt (var_name, value)
259 261

  
260
let pp_assign_spec m self_l pp_var_l indirect_l self_r pp_var_r indirect_r fmt
262
let pp_assign_spec ?pp_op m self_l pp_var_l indirect_l self_r pp_var_r indirect_r fmt
261 263
    (var_type, var_name, value) =
262 264
  let depth = expansion_depth value in
263 265
  let loop_vars = mk_loop_variables m var_type depth in
......
265 267
  let aux typ fmt vars =
266 268
    match vars with
267 269
    | [] ->
268
      pp_basic_assign_spec
270
      pp_basic_assign_spec ?pp_op
269 271
        (pp_value_suffix
270 272
           ~indirect:indirect_l
271 273
           m
......
564 566
            fmt
565 567
            ((Arrow.arrow_id, (mem_in, inst)), ())
566 568
        else pp_eq fmt ()
569
      | GEqual (a, b) ->
570
        pp_assign_spec ~pp_op:pp_gequal
571
          m
572
          mem_out
573
          (pp_c_var_read ~test_output:false m)
574
          indirect_l
575
          mem_in
576
          (pp_c_var_read ~test_output:false m)
577
          indirect_r
578
          fmt
579
          (type_of_l_value a, val_of_expr a, val_of_expr b)
567 580
      | And fs ->
568 581
        pp_and_l pp_spec' fmt fs
569 582
      | Or fs ->
src/backends/C/c_backend_src.ml
369 369
            "@[<v 2>switch(%a) {@,%a@,}@]"
370 370
            (pp_c_val m self (pp_c_var_read m))
371 371
            g
372
            (pp_print_list
372
            (pp_print_list_i
373 373
               ~pp_open_box:pp_open_vbox0
374
               (pp_machine_branch dependencies m self mem))
374
               (pp_machine_branch dependencies m self mem (List.length hl)))
375 375
            hl
376 376
      | MSpec s ->
377 377
        fprintf fmt "@[/*@@ %s */@]@ " s
......
380 380
    in
381 381
    fprintf fmt "%a%a" pp_instr instr (Mod.pp_step_instr_spec m self mem) instr
382 382

  
383
  and pp_machine_branch dependencies m self mem fmt (t, h) =
383
  and pp_machine_branch dependencies m self mem n fmt i (t, h) =
384 384
    fprintf
385 385
      fmt
386
      "@[<v 2>case %a:@,%a@,break;@]"
386
      (if i = n - 1
387
       then "@[<v 2>default: // %a@,%a@]"
388
       else "@[<v 2>case %a:@,%a@,break;@]")
387 389
      pp_c_tag
388 390
      t
389 391
      (pp_print_list
src/machine_code_common.ml
112 112
        pp_print_string fmt "false"
113 113
      | Equal (a, b) ->
114 114
        fprintf fmt "%a == %a" pp_expr a pp_expr b
115
      | GEqual (a, b) ->
116
        fprintf fmt "%a >= %a" pp_expr a pp_expr b
115 117
      | And fs ->
116 118
        pp_print_list
117 119
          ~pp_sep:(fun fmt () -> fprintf fmt "@ ∧ ")
src/spec_common.ml
115 115
  | [ (h1, spec1); (h2, spec2) ] when h1 = tag_false && h2 = tag_true ->
116 116
    Ternary (Var x, spec2, spec1)
117 117
  | hl ->
118
    And (List.map (fun (t, spec) -> Imply (Equal (Var x, Tag t), spec)) hl)
118
    let n = List.length hl in
119
    And (List.mapi (fun k (t, spec) ->
120
        let c = if k = n - 1 then GEqual (Var x, Tag t) else Equal (Var x, Tag t) in
121
        Imply (c, spec)) hl)
119 122

  
120 123
let mk_assign_tr x v = Equal (Var x, Val v)
src/spec_types.ml
46 46
  | True
47 47
  | False
48 48
  | Equal : ('a, left_v) expression_t * ('a, 'b) expression_t -> 'a formula_t
49
  | GEqual : ('a, left_v) expression_t * ('a, 'b) expression_t -> 'a formula_t
49 50
  | And of 'a formula_t list
50 51
  | Or of 'a formula_t list
51 52
  | Imply of 'a formula_t * 'a formula_t
src/spec_types.mli
39 39
  | True
40 40
  | False
41 41
  | Equal : ('a, left_v) expression_t * ('a, 'b) expression_t -> 'a formula_t
42
  | GEqual : ('a, left_v) expression_t * ('a, 'b) expression_t -> 'a formula_t
42 43
  | And of 'a formula_t list
43 44
  | Or of 'a formula_t list
44 45
  | Imply of 'a formula_t * 'a formula_t

Also available in: Unified diff