diff --git a/convert.ml b/convert.ml
index 2e2e262525f62c023c894fe6cb9c79937dab29df..e1a6bf921d89c876684cbe3f45bf972175b6776f 100644
--- a/convert.ml
+++ b/convert.ml
@@ -2215,217 +2215,231 @@ and convert_incr_statement env incr does_remove_virtual =
let stmts = List.fold_left (add_temp env) [stmt] aux in
env, mk_expr_l loc (GNU_BODY { blabels=[]; battrs=[]; bstmts = stmts })
-and convert_statement env st does_remove_virtual =
+and convert_statement env st does_remove_virtual : statement list * Convert_env.env =
let open Current_loc.Operators in
- let rec add_temps tmps stmt =
+ let rec add_temps tmps (stmts : statement list) : statement list =
match tmps with
- | [] -> stmt
+ | [] -> stmts
| (def,init) :: tl ->
- let loc = Convert_env.get_loc env in
- let stmt =
+ let stmts =
match init with
- | None -> stmt
+ | None -> stmts
| Some s ->
- SEQUENCE(s, make_stmt env stmt,loc)
+ s :: stmts
in
- let stmt =
+ let stmts =
match def with
- | None -> stmt
+ | None -> stmts
| Some def ->
let def = make_stmt env (DEFINITION def) in
- let stmt = make_stmt env stmt in
- SEQUENCE(def,stmt,loc)
+ def :: stmts
in
- add_temps tl stmt
+ add_temps tl stmts
in
- let add_temps_update tmps stmt =
+ let add_temps_update tmps (stmts : statement list) : statement list =
match tmps with
- | [] -> stmt
+ | [] -> stmts
| _ ->
let block = List.fold_left (add_temp_update env) [] tmps in
- make_block_stmt env (stmt::block)
+ [ make_block_stmt env (stmts@block) ]
+ in
+ let mk_single env node = [ make_stmt env node ] in
+ let mk_stmt_from_list env stmts =
+ match stmts with
+ | [] -> assert false
+ | [ s ] -> s
+ | sl -> make_block_stmt env sl
in
let env = Convert_env.set_loc env (find_loc_stmt st) in
let cloc = Convert_env.get_loc env in
let<> UpdatedCurrentLoc = cloc in
- let raw, env =
- match st with
- | Nop _ -> NOP (None, cloc), env
- | Code_annot (_,annot) ->
- let env, c_annot = Convert_acsl.convert_code_annot env annot in
- CODE_ANNOT(c_annot,cloc), env
- | Return (_,Some e) ->
- let e = add_temporary (* env *) e in
+ match st with
+ | Nop _ -> mk_single env (NOP (None, cloc)), env
+ | Code_annot (_,annot) ->
+ let env, c_annot = Convert_acsl.convert_code_annot env annot in
+ mk_single env (CODE_ANNOT(c_annot,cloc)), env
+ | Return (_,Some e) ->
+ let e = add_temporary (* env *) e in
+ let env, aux, e = convert_full_expr env e does_remove_virtual in
+ let e = convert_ref env (Convert_env.get_current_return_type env) e in
+ let aux = preserved_returned_object aux e in
+ let stmts = mk_single env (RETURN(e, cloc)) in
+ let stmts = add_temps aux stmts in
+ stmts, env
+ | Return(_, None) ->
+ mk_single env (RETURN({expr_loc = cloc; expr_node = NOTHING},cloc)), env
+ | Expression (_,e) ->
+ let env, aux, e =
+ convert_full_expr ~drop_temp:true env e does_remove_virtual
+ in
+ let stmt = mk_single env (COMPUTATION(e,cloc)) in
+ add_temps aux stmt, env
+ | VirtualExpression (_,e) ->
+ if does_remove_virtual then mk_single env (NOP (None, cloc)), env
+ else
let env, aux, e = convert_full_expr env e does_remove_virtual in
- let e = convert_ref env (Convert_env.get_current_return_type env) e in
- let aux = preserved_returned_object aux e in
- let stmt = RETURN(e, cloc) in
- let stmts = add_temps aux stmt in
- stmts, env
- | Return(_, None) ->
- RETURN({expr_loc = cloc; expr_node = NOTHING},cloc), env
- | Expression (_,e) ->
- let env, aux, e =
- convert_full_expr ~drop_temp:true env e does_remove_virtual
- in
- add_temps aux (COMPUTATION(e,cloc)), env
- | VirtualExpression (_,e) ->
- if does_remove_virtual then NOP (None, cloc), env
+ let stmt = mk_single env (COMPUTATION(e,cloc)) in
+ add_temps aux stmt, env
+ | Ghost_block(_,stmts) ->
+ let old_ghost = Convert_env.is_ghost env in
+ let env = Convert_env.set_ghost env true in
+ let b, env = convert_block env stmts does_remove_virtual in
+ let env = Convert_env.set_ghost env old_ghost in
+ mk_single env (BLOCK(b,cloc,cloc)), env
+ | Block(_,stmts) ->
+ let b, env = convert_block env stmts does_remove_virtual in
+ mk_single env (BLOCK(b, cloc, cloc)), env
+ | Condition(_,cond,true_action,false_action) ->
+ let env, aux, cond = convert_condition env cond does_remove_virtual in
+ let true_action, env =
+ convert_statement env true_action does_remove_virtual
+ in
+ let false_action, env =
+ convert_statement env false_action does_remove_virtual
+ in
+ let true_stmt = mk_stmt_from_list env true_action in
+ let false_stmt = mk_stmt_from_list env false_action in
+ let if_stmt = mk_single env (IF(cond,true_stmt,false_stmt,cloc)) in
+ add_temps aux if_stmt, env
+ | Label(_,lab) ->
+ let stmt = make_stmt env (NOP (None, cloc)) in
+ mk_single env (LABEL(lab,stmt,cloc)), env
+ | Goto(_,lab) ->
+ mk_single env (GOTO(lab,cloc)), env
+ | Switch(_,cond,cases) ->
+ let env, aux, cond = convert_condition env cond does_remove_virtual in
+ let cases_loc = find_loc_case_stmt_list cases in
+ let cases_loc = Cil_datatype.Location.of_lexing_loc cases_loc in
+ let cases, env =
+ List.fold_left
+ (convert_case_statement does_remove_virtual) ([],env) cases
+ in
+ let cases = { blabels = []; battrs = []; bstmts = List.rev cases } in
+ let cases = make_stmt env (BLOCK(cases,cases_loc,cases_loc)) in
+ let switch = mk_single env (SWITCH(cond,cases,cloc)) in
+ add_temps aux switch, env
+ | VarDecl (_, name, typ, init) ->
+ let env, (base, decl) = convert_specifiers env typ does_remove_virtual in
+ let qual_name = { prequalification = []; decl_name = name } in
+ let attrs = add_fc_destructor_attr env typ [] in
+ let env =
+ if List.mem Static typ.qualifier then
+ let extern = Convert_env.is_extern_c env in
+ let env = Convert_env.set_extern_c env true in
+ let env = Convert_env.add_global_var env qual_name typ.plain_type in
+ Convert_env.set_extern_c env extern
else
- let env, aux, e = convert_full_expr env e does_remove_virtual in
- add_temps aux (COMPUTATION(e,cloc)), env
- | Ghost_block(_,stmts) ->
- let old_ghost = Convert_env.is_ghost env in
- let env = Convert_env.set_ghost env true in
- let b, env = convert_block env stmts does_remove_virtual in
- let env = Convert_env.set_ghost env old_ghost in
- BLOCK(b,cloc,cloc), env
- | Block(_,stmts) ->
- let b, env = convert_block env stmts does_remove_virtual in
- BLOCK(b, cloc, cloc), env
- | Condition(_,cond,true_action,false_action) ->
- let env, aux, cond = convert_condition env cond does_remove_virtual in
- let true_action, env =
- convert_statement env true_action does_remove_virtual
- in
- let false_action, env =
- convert_statement env false_action does_remove_virtual
- in
- add_temps aux (IF(cond,true_action,false_action,cloc)), env
- | Label(_,lab) ->
- let stmt = make_stmt env (NOP (None, cloc)) in
- LABEL(lab,stmt,cloc), env
- | Goto(_,lab) ->
- GOTO(lab,cloc), env
- | Switch(_,cond,cases) ->
- let env, aux, cond = convert_condition env cond does_remove_virtual in
- let cases_loc = find_loc_case_stmt_list cases in
- let cases_loc = Cil_datatype.Location.of_lexing_loc cases_loc in
- let cases, env =
- List.fold_left
- (convert_case_statement does_remove_virtual) ([],env) cases
- in
- let cases = { blabels = []; battrs = []; bstmts = List.rev cases } in
- let cases = make_stmt env (BLOCK(cases,cases_loc,cases_loc)) in
- add_temps aux (SWITCH(cond,cases,cloc)), env
- | VarDecl (_, name, typ, init) ->
- let env, (base, decl) = convert_specifiers env typ does_remove_virtual in
- let qual_name = { prequalification = []; decl_name = name } in
- let attrs = add_fc_destructor_attr env typ [] in
- let env =
- if List.mem Static typ.qualifier then
- let extern = Convert_env.is_extern_c env in
- let env = Convert_env.set_extern_c env true in
- let env = Convert_env.add_global_var env qual_name typ.plain_type in
- Convert_env.set_extern_c env extern
- else
- Convert_env.add_local_var env name typ.plain_type
- in
- let var = Local qual_name in
- let env, aux, init, e =
- match init with
- | None -> env, empty_aux, NO_INIT, None
- | Some e -> convert_initializer env typ var e does_remove_virtual
- in
- let decl init =
- DECDEF(None, (base,[(name, decl JUSTBASE,attrs,cloc),init]), cloc)
- in
- let stmt =
- match aux with
- | [] ->
- let def = DEFINITION (decl init) in
- (match e with
- | None -> def
- | Some stmt -> SEQUENCE (make_stmt env def, stmt, cloc))
- | _ ->
- (* We put all these declarations in a special block,
- but the initial declaration itself need to stay out of it.
- *)
- let def = DEFINITION (decl NO_INIT) in
- let block =
- match e with
- | None ->
- let var_expr = { expr_loc = cloc; expr_node = VARIABLE name } in
- mk_compound_init env var_expr typ init
- | Some s -> s.stmt_node
- in
- let block = add_temps aux block in
- SEQUENCE (make_stmt env def, make_stmt env block, cloc)
- in
- stmt, env
- | Break _ -> BREAK (cloc), env
- | Continue _ -> CONTINUE (cloc), env
- | While (_, cond, body, annot) ->
- let env, aux, cond = convert_full_expr env cond does_remove_virtual in
- let body,env = convert_statement env body does_remove_virtual in
- let body = add_temps_update aux body in
- let env, annot =
- Convert_env.env_map Convert_acsl.convert_code_annot env annot
- in
- add_temps aux (WHILE(annot,cond,body,cloc)), env
- | DoWhile (_, cond, body,annot) ->
- let env, aux, cond = convert_full_expr env cond does_remove_virtual in
- let body, env = convert_statement env body does_remove_virtual in
- let body = add_temps_update aux body in
- let env, annot =
- Convert_env.env_map Convert_acsl.convert_code_annot env annot
- in
- add_temps aux (DOWHILE(annot, cond, body, cloc)), env
- | For(_, init, cond, incr, body,annot) ->
- let init, stmts, ienv =
- convert_init_statement env init does_remove_virtual
- in
- let ienv, aux, cond = match cond with
- | None -> ienv, empty_aux, { expr_loc = cloc ; expr_node = NOTHING }
- | Some cond -> convert_full_expr ienv cond does_remove_virtual
- in
- let ienv, incr =
- convert_incr_statement ienv incr does_remove_virtual
- in
- let ienv, annot =
- Convert_env.env_map Convert_acsl.convert_code_annot ienv annot
- in
- let body, ienv = convert_statement ienv body does_remove_virtual in
- let body = add_temps_update aux body in
- let loop = FOR(annot,init,cond,incr,body,cloc) in
- let stmt =
- match stmts, aux with
- [], [] -> loop
- | [], l -> add_temps l loop
- | _,[] -> make_block ienv (stmts @ [make_stmt env loop])
- | _, l ->
- let block = List.fold_left (add_temp env) [make_stmt env loop] l in
- make_block ienv (stmts @ block)
- in
- stmt, Convert_env.unscope ienv env
- | TryCatch (_, t, c) ->
- let t, env = convert_stmt_list env t does_remove_virtual in
- let t = make_block_stmt env t in
- let c, env =
- List.fold_left
- (convert_catch_clause does_remove_virtual) ([], env) c
- in
- let c = List.rev c in
- TRY_CATCH(t,c,cloc), env
- | GccInlineAsm(_, qual, instr, details) ->
- let qual = List.map (fun x -> cv_to_attr (convert_cv x)) qual in
- let convert_asm_IO asm_io =
- List.map
- (fun {aIO_name=n;constraints=c;expr=e}->
- let (_,_,e)=convert_full_expr env e does_remove_virtual in (n,c,e))
- asm_io
- in
- let details = match details with
- | None -> None
- | Some {outputs=o; inputs=i; clobbers=c; ad_labels=l} ->
- Some
- { aoutputs=convert_asm_IO o;
- ainputs=convert_asm_IO i;
- aclobbers=c; alabels=l }
- in
- ASM(qual, instr, details, cloc), env
- in
- make_stmt env raw, env
+ Convert_env.add_local_var env name typ.plain_type
+ in
+ let var = Local qual_name in
+ let env, aux, init, e =
+ match init with
+ | None -> env, empty_aux, NO_INIT, None
+ | Some e -> convert_initializer env typ var e does_remove_virtual
+ in
+ let decl init =
+ DECDEF(None, (base,[(name, decl JUSTBASE,attrs,cloc),init]), cloc)
+ in
+ let stmts =
+ match aux with
+ | [] ->
+ let def = DEFINITION (decl init) in
+ (match e with
+ | None -> mk_single env def
+ | Some stmt -> make_stmt env def :: [ stmt ])
+ | _ ->
+ (* We put all these declarations in a special block,
+ but the initial declaration itself need to stay out of it.
+ *)
+ let def = DEFINITION (decl NO_INIT) in
+ let def_stmt = make_stmt env def in
+ let block =
+ match e with
+ | None ->
+ let var_expr = { expr_loc = cloc; expr_node = VARIABLE name } in
+ make_stmt env (mk_compound_init env var_expr typ init)
+ | Some s -> s
+ in
+ let block = add_temps aux [block] in
+ def_stmt :: block
+ in
+ stmts, env
+ | Break _ -> mk_single env (BREAK cloc), env
+ | Continue _ -> mk_single env (CONTINUE cloc), env
+ | While (_, cond, body, annot) ->
+ let env, aux, cond = convert_full_expr env cond does_remove_virtual in
+ let body,env = convert_statement env body does_remove_virtual in
+ let body = add_temps_update aux body in
+ let env, annot =
+ Convert_env.env_map Convert_acsl.convert_code_annot env annot
+ in
+ let block = mk_stmt_from_list env body in
+ let while_stmt = mk_single env (WHILE(annot,cond,block,cloc)) in
+ add_temps aux while_stmt, env
+ | DoWhile (_, cond, body,annot) ->
+ let env, aux, cond = convert_full_expr env cond does_remove_virtual in
+ let body, env = convert_statement env body does_remove_virtual in
+ let body = add_temps_update aux body in
+ let env, annot =
+ Convert_env.env_map Convert_acsl.convert_code_annot env annot
+ in
+ let block = mk_stmt_from_list env body in
+ let dowhile_stmt = mk_single env (DOWHILE(annot,cond,block,cloc)) in
+ add_temps aux dowhile_stmt, env
+ | For(_, init, cond, incr, body,annot) ->
+ let init, stmts, ienv =
+ convert_init_statement env init does_remove_virtual
+ in
+ let ienv, aux, cond = match cond with
+ | None -> ienv, empty_aux, { expr_loc = cloc ; expr_node = NOTHING }
+ | Some cond -> convert_full_expr ienv cond does_remove_virtual
+ in
+ let ienv, incr =
+ convert_incr_statement ienv incr does_remove_virtual
+ in
+ let ienv, annot =
+ Convert_env.env_map Convert_acsl.convert_code_annot ienv annot
+ in
+ let body, ienv = convert_statement ienv body does_remove_virtual in
+ let body = add_temps_update aux body in
+ let block = mk_stmt_from_list env body in
+ let loop = mk_single env (FOR(annot,init,cond,incr,block,cloc)) in
+ let stmts =
+ match stmts, aux with
+ [], [] -> loop
+ | [], l -> add_temps l loop
+ | _,[] -> [ make_block_stmt ienv (stmts @ loop) ]
+ | _, l ->
+ let block = List.fold_left (add_temp env) loop l in
+ [ make_block_stmt ienv (stmts @ block) ]
+ in
+ stmts, Convert_env.unscope ienv env
+ | TryCatch (_, t, c) ->
+ let t, env = convert_stmt_list env t does_remove_virtual in
+ let t = make_block_stmt env t in
+ let c, env =
+ List.fold_left
+ (convert_catch_clause does_remove_virtual) ([], env) c
+ in
+ let c = List.rev c in
+ mk_single env (TRY_CATCH(t,c,cloc)), env
+ | GccInlineAsm(_, qual, instr, details) ->
+ let qual = List.map (fun x -> cv_to_attr (convert_cv x)) qual in
+ let convert_asm_IO asm_io =
+ List.map
+ (fun {aIO_name=n;constraints=c;expr=e}->
+ let (_,_,e)=convert_full_expr env e does_remove_virtual in (n,c,e))
+ asm_io
+ in
+ let details = match details with
+ | None -> None
+ | Some {outputs=o; inputs=i; clobbers=c; ad_labels=l} ->
+ Some
+ { aoutputs=convert_asm_IO o;
+ ainputs=convert_asm_IO i;
+ aclobbers=c; alabels=l }
+ in
+ mk_single env (ASM(qual, instr, details, cloc)), env
and convert_catch_clause does_remove_virtual (acc,env) { typed_arg; cbody } =
let var, env =
@@ -2482,8 +2496,8 @@ and convert_stmt_list env l does_remove_virtual =
let (stmts, env) =
List.fold_left
(fun (acc, env) stmt ->
- let (s,env) = convert_statement env stmt does_remove_virtual in
- s::acc, env)
+ let (sl,env) = convert_statement env stmt does_remove_virtual in
+ List.rev sl @ acc, env)
([],env) l
in
List.rev stmts, env