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

src/backends/C/c_backend_spec.ml

@@ -202,6 +202,8 @@ let pp_exists pp_l pp_r fmt (l, r) =
 
 let pp_equal pp_l pp_r fmt (l, r) = fprintf fmt "%a == %a" pp_l l pp_r r
 
+let pp_gequal pp_l pp_r fmt (l, r) = fprintf fmt "%a >= %a" pp_l l pp_r r
+
 let pp_implies pp_l pp_r fmt (l, r) =
   fprintf fmt "@[<v>%a ==>@ %a@]" pp_l l pp_r r
 
@@ -252,12 +254,12 @@ let pp_locals m =
 
 let pp_ptr_decl fmt v = pp_ptr fmt v.var_id
 
-let pp_basic_assign_spec pp_l pp_r fmt typ var_name value =
+let pp_basic_assign_spec ?(pp_op=pp_equal) pp_l pp_r fmt typ var_name value =
   if Types.is_real_type typ && !Options.mpfr then assert false
     (* Mpfr.pp_inject_assign pp_var fmt (var_name, value) *)
-  else pp_equal pp_l pp_r fmt (var_name, value)
+  else pp_op pp_l pp_r fmt (var_name, value)
 
-let pp_assign_spec m self_l pp_var_l indirect_l self_r pp_var_r indirect_r fmt
+let pp_assign_spec ?pp_op m self_l pp_var_l indirect_l self_r pp_var_r indirect_r fmt
     (var_type, var_name, value) =
   let depth = expansion_depth value in
   let loop_vars = mk_loop_variables m var_type depth in
@@ -265,7 +267,7 @@ let pp_assign_spec m self_l pp_var_l indirect_l self_r pp_var_r indirect_r fmt
   let aux typ fmt vars =
     match vars with
     | [] ->
-      pp_basic_assign_spec
+      pp_basic_assign_spec ?pp_op
         (pp_value_suffix
            ~indirect:indirect_l
            m
@@ -564,6 +566,17 @@ module PrintSpec = struct
             fmt
             ((Arrow.arrow_id, (mem_in, inst)), ())
         else pp_eq fmt ()
+      | GEqual (a, b) ->
+        pp_assign_spec ~pp_op:pp_gequal
+          m
+          mem_out
+          (pp_c_var_read ~test_output:false m)
+          indirect_l
+          mem_in
+          (pp_c_var_read ~test_output:false m)
+          indirect_r
+          fmt
+          (type_of_l_value a, val_of_expr a, val_of_expr b)
       | And fs ->
         pp_and_l pp_spec' fmt fs
       | Or fs ->

src/backends/C/c_backend_src.ml

@@ -369,9 +369,9 @@ module Main (Mod : MODIFIERS_SRC) = struct
             "@[<v 2>switch(%a) {@,%a@,}@]"
             (pp_c_val m self (pp_c_var_read m))
             g
-            (pp_print_list
+            (pp_print_list_i
                ~pp_open_box:pp_open_vbox0
-               (pp_machine_branch dependencies m self mem))
+               (pp_machine_branch dependencies m self mem (List.length hl)))
             hl
       | MSpec s ->
         fprintf fmt "@[/*@@ %s */@]@ " s
@@ -380,10 +380,12 @@ module Main (Mod : MODIFIERS_SRC) = struct
     in
     fprintf fmt "%a%a" pp_instr instr (Mod.pp_step_instr_spec m self mem) instr
 
-  and pp_machine_branch dependencies m self mem fmt (t, h) =
+  and pp_machine_branch dependencies m self mem n fmt i (t, h) =
     fprintf
       fmt
-      "@[<v 2>case %a:@,%a@,break;@]"
+      (if i = n - 1
+       then "@[<v 2>default: // %a@,%a@]"
+       else "@[<v 2>case %a:@,%a@,break;@]")
       pp_c_tag
       t
       (pp_print_list

src/machine_code_common.ml

@@ -112,6 +112,8 @@ module PrintSpec = struct
         pp_print_string fmt "false"
       | Equal (a, b) ->
         fprintf fmt "%a == %a" pp_expr a pp_expr b
+      | GEqual (a, b) ->
+        fprintf fmt "%a >= %a" pp_expr a pp_expr b
       | And fs ->
         pp_print_list
           ~pp_sep:(fun fmt () -> fprintf fmt "@ ∧ ")

src/spec_common.ml

@@ -115,6 +115,9 @@ let mk_branch_tr x =
   | [ (h1, spec1); (h2, spec2) ] when h1 = tag_false && h2 = tag_true ->
     Ternary (Var x, spec2, spec1)
   | hl ->
-    And (List.map (fun (t, spec) -> Imply (Equal (Var x, Tag t), spec)) hl)
+    let n = List.length hl in
+    And (List.mapi (fun k (t, spec) ->
+        let c = if k = n - 1 then GEqual (Var x, Tag t) else Equal (Var x, Tag t) in
+        Imply (c, spec)) hl)
 
 let mk_assign_tr x v = Equal (Var x, Val v)

src/spec_types.ml

@@ -46,6 +46,7 @@ type 'a formula_t =
   | True
   | False
   | Equal : ('a, left_v) expression_t * ('a, 'b) expression_t -> 'a formula_t
+  | GEqual : ('a, left_v) expression_t * ('a, 'b) expression_t -> 'a formula_t
   | And of 'a formula_t list
   | Or of 'a formula_t list
   | Imply of 'a formula_t * 'a formula_t

src/spec_types.mli

@@ -39,6 +39,7 @@ type 'a formula_t =
   | True
   | False
   | Equal : ('a, left_v) expression_t * ('a, 'b) expression_t -> 'a formula_t
+  | GEqual : ('a, left_v) expression_t * ('a, 'b) expression_t -> 'a formula_t
   | And of 'a formula_t list
   | Or of 'a formula_t list
   | Imply of 'a formula_t * 'a formula_t