Fixes for correct array literal C generation.
This commit is contained in:
parent
3a0b1f9e16
commit
9301ed0b09
3 changed files with 20 additions and 3 deletions
|
@ -188,6 +188,17 @@ let rec translate kind context e =
|
|||
let context, e_list = translate_app kind context app.a_op e_list in
|
||||
context, { e with e_desc = Eapp(app, e_list, r) }
|
||||
| Eiterator (it, app, n, e_list, reset) ->
|
||||
(* Add an intermediate equation for each array lit argument. *)
|
||||
let add_eq_for_array exp (context, e_list) = match exp.e_desc with
|
||||
| Econst { se_desc = Sarray _; } ->
|
||||
let id = Ident.fresh "arr" in
|
||||
let eq = mk_equation (Evarpat id) exp in
|
||||
let exp = { exp with e_desc = (Evar id); } in
|
||||
let var = mk_var_dec ~clock:exp.e_ck id exp.e_ty in
|
||||
((var :: fst context, eq :: snd context), exp :: e_list)
|
||||
| _ -> (context, exp :: e_list) in
|
||||
let context, e_list =
|
||||
List.fold_right add_eq_for_array e_list (context, []) in
|
||||
let context, e_list =
|
||||
translate_list function_args_kind context e_list in
|
||||
context, { e with e_desc = Eiterator(it, app, n, e_list, reset) }
|
||||
|
|
|
@ -240,7 +240,7 @@ and pp_cexpr fmt ce = match ce with
|
|||
| Cstructlit (s, el) ->
|
||||
fprintf fmt "(%a){@[%a@]}" pp_string s (pp_list1 pp_cexpr ",") el
|
||||
| Carraylit el ->
|
||||
fprintf fmt "((int *){@[%a@]})" (pp_list1 pp_cexpr ",") el (* WRONG *)
|
||||
fprintf fmt "((int []){@[%a@]})" (pp_list1 pp_cexpr ",") el (* WRONG *)
|
||||
and pp_clhs fmt lhs = match lhs with
|
||||
| Cvar s -> pp_string fmt s
|
||||
| Cderef lhs' -> fprintf fmt "*%a" pp_clhs lhs'
|
||||
|
|
|
@ -255,6 +255,7 @@ let rec cexpr_of_static_exp se =
|
|||
| Sfloat f -> Cconst (Ccfloat f)
|
||||
| Sbool b -> Cconst (Ctag (if b then "TRUE" else "FALSE"))
|
||||
| Sconstructor c -> Cconst (Ctag (shortname c))
|
||||
| Sarray sl -> Carraylit (List.map cexpr_of_static_exp sl)
|
||||
| Sarray_power(n,c) ->
|
||||
let cc = cexpr_of_static_exp c in
|
||||
Carraylit (repeat_list cc (int_of_static_exp n))
|
||||
|
@ -423,8 +424,13 @@ let rec create_affect_const var_env dest c =
|
|||
match c.se_desc with
|
||||
| Sarray_power(c, n) ->
|
||||
let x = gen_symbol () in
|
||||
[ Cfor(x, 0, int_of_static_exp n,
|
||||
create_affect_const var_env (Carray (dest, Clhs (Cvar x))) c) ]
|
||||
[Cfor(x, 0, int_of_static_exp n,
|
||||
create_affect_const var_env (Carray (dest, Clhs (Cvar x))) c)]
|
||||
| Sarray cl ->
|
||||
let create_affect_idx c (i, affl) =
|
||||
let dest = Carray (dest, Cconst (Ccint i)) in
|
||||
(i - 1, create_affect_const var_env dest c @ affl) in
|
||||
snd (List.fold_right create_affect_idx cl (List.length cl - 1, []))
|
||||
| _ -> [Caffect (dest, cexpr_of_exp var_env (mk_exp (Econst c)))]
|
||||
|
||||
(** [cstm_of_act obj_env mods act] translates the Obj action [act] to a list of
|
||||
|
|
Loading…
Reference in a new issue