From cc2d157be19d52bbe666e6d5a7ee9879cff7bfc8 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Mon, 22 Aug 2016 12:29:10 +0200 Subject: Error for va_start in non-vararg function. CompCert now reports an error for usage of the va_start macro in non variadic functions. Bug 19600. --- cparser/Elab.ml | 58 ++++++++++++++++++++++++++++++--------------------------- 1 file changed, 31 insertions(+), 27 deletions(-) (limited to 'cparser/Elab.ml') diff --git a/cparser/Elab.ml b/cparser/Elab.ml index eeff41e1..b2426738 100644 --- a/cparser/Elab.ml +++ b/cparser/Elab.ml @@ -184,8 +184,8 @@ let enter_or_refine_ident local loc env s sto ty = let elab_expr_f : (cabsloc -> Env.t -> Cabs.expression -> C.exp * Env.t) ref = ref (fun _ _ _ -> assert false) -let elab_funbody_f : (C.typ -> Env.t -> statement -> C.stmt) ref - = ref (fun _ _ _ -> assert false) +let elab_funbody_f : (C.typ -> bool -> Env.t -> statement -> C.stmt) ref + = ref (fun _ _ _ _ -> assert false) (** * Elaboration of constants - C99 section 6.4.4 *) @@ -1323,7 +1323,7 @@ let elab_initializer loc env root ty ie = (* Elaboration of expressions *) -let elab_expr loc env a = +let elab_expr vararg loc env a = let err fmt = error loc fmt in (* non-fatal error *) let error fmt = fatal_error loc fmt in @@ -1400,6 +1400,8 @@ let elab_expr loc env a = (elaboration) --> __builtin_va_arg(ap, sizeof(ty)) *) | CALL((VARIABLE "__builtin_va_start" as a1), [a2; a3]) -> + if not vararg then + err "'va_start' used in function with fixed args"; let b1,env = elab env a1 in let b2,env = elab env a2 in let _b3,env = elab env a3 in @@ -1881,16 +1883,16 @@ let elab_expr loc env a = in elab env a (* Filling in forward declaration *) -let _ = elab_expr_f := elab_expr +let _ = elab_expr_f := (elab_expr false) -let elab_opt_expr loc env = function +let elab_opt_expr vararg loc env = function | None -> None,env - | Some a -> let a,env = (elab_expr loc env a) in + | Some a -> let a,env = (elab_expr vararg loc env a) in Some a,env -let elab_for_expr loc env = function +let elab_for_expr vararg loc env = function | None -> { sdesc = Sskip; sloc = elab_loc loc },env - | Some a -> let a,env = elab_expr loc env a in + | Some a -> let a,env = elab_expr vararg loc env a in { sdesc = Sdo a; sloc = elab_loc loc },env (* Handling of __func__ (section 6.4.2.2) *) @@ -2123,7 +2125,7 @@ let elab_fundef env spec name defs body loc = emit_elab ~debuginfo:false env3 loc (Gdecl(Storage_static, func_id, func_ty, Some func_init)); (* Elaborate function body *) - let body1 = !elab_funbody_f ty_ret env3 body in + let body1 = !elab_funbody_f ty_ret vararg env3 body in (* Special treatment of the "main" function *) let body2 = if s = "main" then begin @@ -2195,9 +2197,9 @@ and elab_definitions local env = function (* Extended asm *) -let elab_asm_operand loc env (ASMOPERAND(label, wide, chars, e)) = +let elab_asm_operand vararg loc env (ASMOPERAND(label, wide, chars, e)) = let s = elab_simple_string loc wide chars in - let e',env = elab_expr loc env e in + let e',env = elab_expr vararg loc env e in (label, s, e'),env @@ -2209,7 +2211,8 @@ type stmt_context = { ctx_return_typ: typ; (**r return type for the function *) ctx_labels: StringSet.t; (**r all labels defined in the function *) ctx_break: bool; (**r is 'break' allowed? *) - ctx_continue: bool (**r is 'continue' allowed? *) + ctx_continue: bool; (**r is 'continue' allowed? *) + ctx_vararg: bool; (**r is this a vararg function? *) } let stmt_labels stmt = @@ -2246,7 +2249,7 @@ let rec elab_stmt env ctx s = (* 6.8.3 Expression statements *) | COMPUTATION(a, loc) -> - let a,env = (elab_expr loc env a) in + let a,env = (elab_expr ctx.ctx_vararg loc env a) in { sdesc = Sdo a; sloc = elab_loc loc },env (* 6.8.1 Labeled statements *) @@ -2256,7 +2259,7 @@ let rec elab_stmt env ctx s = { sdesc = Slabeled(Slabel lbl, s1); sloc = elab_loc loc },env | CASE(a, s1, loc) -> - let a',env = elab_expr loc env a in + let a',env = elab_expr ctx.ctx_vararg loc env a in begin match Ceval.integer_expr env a' with | None -> error loc "argument of 'case' must be an integer compile-time constant" @@ -2277,7 +2280,7 @@ let rec elab_stmt env ctx s = (* 6.8.4 Conditional statements *) | If(a, s1, s2, loc) -> - let a',env = elab_expr loc env a in + let a',env = elab_expr ctx.ctx_vararg loc env a in if not (is_scalar_type env a'.etyp) then error loc "the condition of 'if' does not have scalar type"; let s1',env = elab_stmt env ctx s1 in @@ -2291,7 +2294,7 @@ let rec elab_stmt env ctx s = (* 6.8.5 Iterative statements *) | WHILE(a, s1, loc) -> - let a',env = elab_expr loc env a in + let a',env = elab_expr ctx.ctx_vararg loc env a in if not (is_scalar_type env a'.etyp) then error loc "the condition of 'while' does not have scalar type"; let s1',env = elab_stmt env (ctx_loop ctx) s1 in @@ -2299,7 +2302,7 @@ let rec elab_stmt env ctx s = | DOWHILE(a, s1, loc) -> let s1',env = elab_stmt env (ctx_loop ctx) s1 in - let a',env = elab_expr loc env a in + let a',env = elab_expr ctx.ctx_vararg loc env a in if not (is_scalar_type env a'.etyp) then error loc "the condition of 'while' does not have scalar type"; { sdesc = Sdowhile(s1', a'); sloc = elab_loc loc },env @@ -2308,10 +2311,10 @@ let rec elab_stmt env ctx s = let (a1', env', decls') = match fc with | Some (FC_EXP a1) -> - let a1,env = elab_for_expr loc env (Some a1) in + let a1,env = elab_for_expr ctx.ctx_vararg loc env (Some a1) in (a1, env, None) | None -> - let a1,env = elab_for_expr loc env None in + let a1,env = elab_for_expr ctx.ctx_vararg loc env None in (a1, env, None) | Some (FC_DECL def) -> let (dcl, env') = elab_definition true (Env.new_scope env) def in @@ -2321,11 +2324,11 @@ let rec elab_stmt env ctx s = let a2',env = match a2 with | None -> intconst 1L IInt,env - | Some a2 -> elab_expr loc env' a2 + | Some a2 -> elab_expr ctx.ctx_vararg loc env' a2 in if not (is_scalar_type env' a2'.etyp) then error loc "the condition of 'for' does not have scalar type"; - let a3',env' = elab_for_expr loc env' a3 in + let a3',env' = elab_for_expr ctx.ctx_vararg loc env' a3 in let s1',env' = elab_stmt env' (ctx_loop ctx) s1 in let sfor = { sdesc = Sfor(a1', a2', a3', s1'); sloc = elab_loc loc } in begin match decls' with @@ -2335,7 +2338,7 @@ let rec elab_stmt env ctx s = (* 6.8.4 Switch statement *) | SWITCH(a, s1, loc) -> - let a',env = elab_expr loc env a in + let a',env = elab_expr ctx.ctx_vararg loc env a in if not (is_integer_type env a'.etyp) then error loc "the argument of 'switch' is not an integer"; let s1',env = elab_stmt env (ctx_switch ctx) s1 in @@ -2353,7 +2356,7 @@ let rec elab_stmt env ctx s = (* 6.8.6 Return statements *) | RETURN(a, loc) -> - let a',env = elab_opt_expr loc env a in + let a',env = elab_opt_expr ctx.ctx_vararg loc env a in begin match (unroll env ctx.ctx_return_typ, a') with | TVoid _, None -> () | TVoid _, Some _ -> @@ -2394,8 +2397,8 @@ let rec elab_stmt env ctx s = | ASM(cv_specs, wide, chars, outputs, inputs, flags, loc) -> let a = elab_cvspecs env cv_specs in let s = elab_simple_string loc wide chars in - let outputs,env = mmap (elab_asm_operand loc) env outputs in - let inputs ,env= mmap (elab_asm_operand loc) env inputs in + let outputs,env = mmap (elab_asm_operand ctx.ctx_vararg loc) env outputs in + let inputs ,env= mmap (elab_asm_operand ctx.ctx_vararg loc) env inputs in let flags = List.map (fun (w,c) -> elab_simple_string loc w c) flags in { sdesc = Sasm(a, s, outputs, inputs, flags); sloc = elab_loc loc },env @@ -2428,12 +2431,13 @@ and elab_block_body env ctx sl = (* Elaboration of a function body. Return the corresponding C statement. *) -let elab_funbody return_typ env b = +let elab_funbody return_typ vararg env b = let ctx = { ctx_return_typ = return_typ; ctx_labels = stmt_labels b; ctx_break = false; - ctx_continue = false } in + ctx_continue = false; + ctx_vararg = vararg;} in fst(elab_stmt env ctx b) (* Filling in forward declaration *) -- cgit