From c85e957812d4581f17a534f3754c555a6a2a2243 Mon Sep 17 00:00:00 2001 From: Michael Schmidt Date: Wed, 20 Mar 2019 20:16:21 +0100 Subject: Improve overflow check for integer literals (#157) The previous check was incomplete for integer literals in base 10. Bug 26119 --- cparser/Elab.ml | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) (limited to 'cparser') diff --git a/cparser/Elab.ml b/cparser/Elab.ml index 7a0b05de..a3915dc4 100644 --- a/cparser/Elab.ml +++ b/cparser/Elab.ml @@ -295,14 +295,16 @@ let parse_int base s = | _ -> assert false in let v = ref 0L in for i = 0 to String.length s - 1 do - if !v < 0L || !v > max_val then raise Overflow; - v := Int64.mul !v (Int64.of_int base); let c = s.[i] in let digit = if c >= '0' && c <= '9' then Char.code c - 48 else if c >= 'A' && c <= 'F' then Char.code c - 55 else raise Bad_digit in if digit >= base then raise Bad_digit; + if !v < 0L || !v > max_val then raise Overflow; + (* because (2^64 - 1) % 10 = 5, not 9 *) + if base = 10 && !v = max_val && digit > 5 then raise Overflow; + v := Int64.mul !v (Int64.of_int base); v := Int64.add !v (Int64.of_int digit) done; !v -- cgit From 5cee733c33bd53c0f58e9896f238ab862e224e46 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Mon, 8 Apr 2019 16:51:12 +0200 Subject: Reset scope ids later. In order to avoid adding ranges to the wrong scopes due to inlining they are numbered consecutively for the whole compilation unit. Bug 26234 --- cparser/Unblock.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'cparser') diff --git a/cparser/Unblock.ml b/cparser/Unblock.ml index da8049a5..66b497cc 100644 --- a/cparser/Unblock.ml +++ b/cparser/Unblock.ml @@ -340,7 +340,6 @@ and unblock_block env ctx ploc = function let unblock_fundef env f = local_variables := []; - next_scope_id := 0; curr_fun_id:= f.fd_name.stamp; (* TODO: register the parameters as being declared in function scope *) let body = unblock_stmt env [] no_loc f.fd_body in @@ -398,5 +397,6 @@ let rec unblock_glob env accu = function (* Entry point *) let program p = + next_scope_id := 0; {gloc = no_loc; gdesc = Gdecl(Storage_extern, debug_id, debug_ty, None)} :: unblock_glob (Builtins.environment()) [] p -- cgit From 39bca2093650f3dbe18e60ad19818b939a96b971 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Mon, 6 May 2019 17:00:10 +0200 Subject: Ensure flushing of the error formatter. Since the error formatter is not automatically flushed at program exit we need to ensure that it is flushed at exit. --- cparser/Diagnostics.ml | 4 ++++ 1 file changed, 4 insertions(+) (limited to 'cparser') diff --git a/cparser/Diagnostics.ml b/cparser/Diagnostics.ml index 172affab..2b8a3eb4 100644 --- a/cparser/Diagnostics.ml +++ b/cparser/Diagnostics.ml @@ -18,6 +18,10 @@ open Format open Commandline +(* Ensure that the error formatter is flushed at exit *) +let _ = + at_exit (pp_print_flush err_formatter) + (* Should errors be treated as fatal *) let error_fatal = ref false -- cgit From 02d8736514c3c9c1542f50b07524f4ffa0588cb8 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Fri, 10 May 2019 14:34:59 +0200 Subject: Fix various scoping issues (#163) Pass the environment to all expr eval functions since the functions themselve may be called recursively and modify the environment. The other change introduces new scopes that are strict subsets of their surrounding scopes for if, switch, while, do and for statement, as prescribed by ISO C standards. --- cparser/Elab.ml | 107 +++++++++++++++++++++++++++++--------------------------- 1 file changed, 56 insertions(+), 51 deletions(-) (limited to 'cparser') diff --git a/cparser/Elab.ml b/cparser/Elab.ml index a3915dc4..4b326f78 100644 --- a/cparser/Elab.ml +++ b/cparser/Elab.ml @@ -1708,7 +1708,7 @@ let elab_expr ctx loc env a = error "arithmetic on a pointer to an incomplete type %a in binary '%c'" (print_typ env) ty s in - let check_static_var id sto ty = + let check_static_var env id sto ty = if ctx.ctx_nonstatic_inline && sto = Storage_static && List.mem AConst (attributes_of_type env ty) @@ -1722,7 +1722,7 @@ let elab_expr ctx loc env a = | VARIABLE s -> begin match wrap Env.lookup_ident loc env s with | (id, Env.II_ident(sto, ty)) -> - check_static_var id sto ty; + check_static_var env id sto ty; { edesc = EVar id; etyp = ty },env | (id, Env.II_enum v) -> { edesc = EConst(CEnum(id, v)); etyp = TInt(enum_ikind, []) },env @@ -1859,9 +1859,9 @@ let elab_expr ctx loc env a = { edesc = ECall(b1, bl'); etyp = res },env | UNARY(POSINCR, a1) -> - elab_pre_post_incr_decr Opostincr "increment" a1 + elab_pre_post_incr_decr env Opostincr "increment" a1 | UNARY(POSDECR, a1) -> - elab_pre_post_incr_decr Opostdecr "decrement" a1 + elab_pre_post_incr_decr env Opostdecr "decrement" a1 (* 6.5.4 Cast operators *) @@ -2020,20 +2020,20 @@ let elab_expr ctx loc env a = end | UNARY(PREINCR, a1) -> - elab_pre_post_incr_decr Opreincr "increment" a1 + elab_pre_post_incr_decr env Opreincr "increment" a1 | UNARY(PREDECR, a1) -> - elab_pre_post_incr_decr Opredecr "decrement" a1 + elab_pre_post_incr_decr env Opredecr "decrement" a1 (* 6.5.5 to 6.5.12 Binary operator expressions *) | BINARY(MUL, a1, a2) -> - elab_binary_arithmetic "*" Omul a1 a2 + elab_binary_arithmetic env "*" Omul a1 a2 | BINARY(DIV, a1, a2) -> - elab_binary_arithmetic "/" Odiv a1 a2 + elab_binary_arithmetic env "/" Odiv a1 a2 | BINARY(MOD, a1, a2) -> - elab_binary_integer "%" Omod a1 a2 + elab_binary_integer env "%" Omod a1 a2 | BINARY(ADD, a1, a2) -> let b1,env = elab env a1 in @@ -2083,37 +2083,37 @@ let elab_expr ctx loc env a = { edesc = EBinop(Osub, b1, b2, tyop); etyp = tyres },env | BINARY(SHL, a1, a2) -> - elab_shift "<<" Oshl a1 a2 + elab_shift env "<<" Oshl a1 a2 | BINARY(SHR, a1, a2) -> - elab_shift ">>" Oshr a1 a2 + elab_shift env ">>" Oshr a1 a2 | BINARY(EQ, a1, a2) -> - elab_comparison Oeq a1 a2 + elab_comparison env Oeq a1 a2 | BINARY(NE, a1, a2) -> - elab_comparison One a1 a2 + elab_comparison env One a1 a2 | BINARY(LT, a1, a2) -> - elab_comparison Olt a1 a2 + elab_comparison env Olt a1 a2 | BINARY(GT, a1, a2) -> - elab_comparison Ogt a1 a2 + elab_comparison env Ogt a1 a2 | BINARY(LE, a1, a2) -> - elab_comparison Ole a1 a2 + elab_comparison env Ole a1 a2 | BINARY(GE, a1, a2) -> - elab_comparison Oge a1 a2 + elab_comparison env Oge a1 a2 | BINARY(BAND, a1, a2) -> - elab_binary_integer "&" Oand a1 a2 + elab_binary_integer env "&" Oand a1 a2 | BINARY(BOR, a1, a2) -> - elab_binary_integer "|" Oor a1 a2 + elab_binary_integer env "|" Oor a1 a2 | BINARY(XOR, a1, a2) -> - elab_binary_integer "^" Oxor a1 a2 + elab_binary_integer env "^" Oxor a1 a2 (* 6.5.13 and 6.5.14 Logical operator expressions *) | BINARY(AND, a1, a2) -> - elab_logical_operator "&&" Ologand a1 a2 + elab_logical_operator env "&&" Ologand a1 a2 | BINARY(OR, a1, a2) -> - elab_logical_operator "||" Ologor a1 a2 + elab_logical_operator env "||" Ologor a1 a2 (* 6.5.15 Conditional expressions *) | QUESTION(a1, a2, a3) -> @@ -2229,7 +2229,7 @@ let elab_expr ctx loc env a = { edesc = EBinop (Ocomma, b1, b2, ty2); etyp = ty2 },env (* Elaboration of pre- or post- increment/decrement *) - and elab_pre_post_incr_decr op msg a1 = + and elab_pre_post_incr_decr env op msg a1 = let b1,env = elab env a1 in if not (is_modifiable_lvalue env b1) then error "expression is not assignable"; @@ -2238,7 +2238,7 @@ let elab_expr ctx loc env a = { edesc = EUnop(op, b1); etyp = b1.etyp },env (* Elaboration of binary operators over integers *) - and elab_binary_integer msg op a1 a2 = + and elab_binary_integer env msg op a1 a2 = let b1,env = elab env a1 in let b2,env = elab env a2 in if not ((is_integer_type env b1.etyp) && (is_integer_type env b2.etyp)) then @@ -2248,7 +2248,7 @@ let elab_expr ctx loc env a = { edesc = EBinop(op, b1, b2, tyres); etyp = tyres },env (* Elaboration of binary operators over arithmetic types *) - and elab_binary_arithmetic msg op a1 a2 = + and elab_binary_arithmetic env msg op a1 a2 = let b1,env = elab env a1 in let b2,env = elab env a2 in if not ((is_arith_type env b1.etyp) && (is_arith_type env b2.etyp)) then @@ -2258,7 +2258,7 @@ let elab_expr ctx loc env a = { edesc = EBinop(op, b1, b2, tyres); etyp = tyres },env (* Elaboration of shift operators *) - and elab_shift msg op a1 a2 = + and elab_shift env msg op a1 a2 = let b1,env = elab env a1 in let b2,env = elab env a2 in if not ((is_integer_type env b1.etyp) && (is_integer_type env b2.etyp)) then @@ -2268,7 +2268,7 @@ let elab_expr ctx loc env a = { edesc = EBinop(op, b1, b2, tyres); etyp = tyres },env (* Elaboration of comparisons *) - and elab_comparison op a1 a2 = + and elab_comparison env op a1 a2 = let b1,env = elab env a1 in let b2,env = elab env a2 in let resdesc = @@ -2305,7 +2305,7 @@ let elab_expr ctx loc env a = { edesc = resdesc; etyp = TInt(IInt, []) },env (* Elaboration of && and || *) - and elab_logical_operator msg op a1 a2 = + and elab_logical_operator env msg op a1 a2 = let b1,env = elab env a1 in let b2,env = elab env a2 in if not ((is_scalar_type env b1.etyp) && (is_scalar_type env b2.etyp)) then @@ -2887,48 +2887,49 @@ let rec elab_stmt env ctx s = (* 6.8.4 Conditional statements *) | If(a, s1, s2, loc) -> - let a',env = elab_expr ctx loc env a in - if not (is_scalar_type env a'.etyp) then + let a',env' = elab_expr ctx loc (Env.new_scope env) a in + if not (is_scalar_type env' a'.etyp) then error loc "controlling expression of 'if' does not have scalar type (%a invalid)" - (print_typ env) a'.etyp; - let s1',env = elab_stmt env ctx s1 in - let s2',env = + (print_typ env') a'.etyp; + let s1' = elab_stmt_new_scope env' ctx s1 in + let s2' = match s2 with - | None -> sskip,env - | Some s2 -> elab_stmt env ctx s2 + | None -> sskip + | Some s2 -> elab_stmt_new_scope env' ctx s2 in { sdesc = Sif(a', s1', s2'); sloc = elab_loc loc },env (* 6.8.5 Iterative statements *) | WHILE(a, s1, loc) -> - let a',env = elab_expr ctx loc env a in - if not (is_scalar_type env a'.etyp) then + let a',env' = elab_expr ctx loc (Env.new_scope env) a in + if not (is_scalar_type env' a'.etyp) then error loc "controlling expression of 'while' does not have scalar type (%a invalid)" - (print_typ env) a'.etyp; - let s1',env = elab_stmt env (ctx_loop ctx) s1 in + (print_typ env') a'.etyp; + let s1' = elab_stmt_new_scope env' (ctx_loop ctx) s1 in { sdesc = Swhile(a', s1'); sloc = elab_loc loc },env | DOWHILE(a, s1, loc) -> - let s1',env = elab_stmt env (ctx_loop ctx) s1 in - let a',env = elab_expr ctx loc env a in - if not (is_scalar_type env a'.etyp) then + let s1' = elab_stmt_new_scope env (ctx_loop ctx) s1 in + let a',env' = elab_expr ctx loc (Env.new_scope env) a in + if not (is_scalar_type env' a'.etyp) then error loc "controlling expression of 'while' does not have scalar type (%a invalid)" - (print_typ env) a'.etyp; + (print_typ env') a'.etyp; { sdesc = Sdowhile(s1', a'); sloc = elab_loc loc },env | FOR(fc, a2, a3, s1, loc) -> + let env' = Env.new_scope env in let (a1', env_decls, decls') = match fc with | Some (FC_EXP a1) -> - let a1,env = elab_for_expr ctx loc env (Some a1) in + let a1,env = elab_for_expr ctx loc env' (Some a1) in (a1, env, None) | None -> - let a1,env = elab_for_expr ctx loc env None in + let a1,env = elab_for_expr ctx loc env' None in (a1, env, None) | Some (FC_DECL def) -> let (dcl, env') = elab_definition true true ctx.ctx_nonstatic_inline - (Env.new_scope env) def in + env' def in let loc = elab_loc (Cabshelper.get_definitionloc def) in (sskip, env', Some(List.map (fun d -> {sdesc = Sdecl d; sloc = loc}) dcl)) in @@ -2940,7 +2941,7 @@ let rec elab_stmt env ctx s = if not (is_scalar_type env_test a2'.etyp) then error loc "controlling expression of 'for' does not have scalar type (%a invalid)" (print_typ env) a2'.etyp; let a3',env_for = elab_for_expr ctx loc env_test a3 in - let s1',env_body = elab_stmt env_for (ctx_loop ctx) s1 in + let s1' = elab_stmt_new_scope env_for (ctx_loop ctx) s1 in let sfor = { sdesc = Sfor(a1', a2', a3', s1'); sloc = elab_loc loc } in begin match decls' with | None -> sfor,env @@ -2949,11 +2950,11 @@ let rec elab_stmt env ctx s = (* 6.8.4 Switch statement *) | SWITCH(a, s1, loc) -> - let a',env = elab_expr ctx loc env a in - if not (is_integer_type env a'.etyp) then + let a',env' = elab_expr ctx loc (Env.new_scope env) a in + if not (is_integer_type env' a'.etyp) then error loc "controlling expression of 'switch' does not have integer type (%a invalid)" - (print_typ env) a'.etyp; - let s1',env = elab_stmt env (ctx_switch ctx) s1 in + (print_typ env') a'.etyp; + let s1' = elab_stmt_new_scope env' (ctx_switch ctx) s1 in check_switch_cases s1'; { sdesc = Sswitch(a', s1'); sloc = elab_loc loc },env @@ -3027,6 +3028,10 @@ let rec elab_stmt env ctx s = | DEFINITION def -> error (Cabshelper.get_definitionloc def) "ill-placed definition"; sskip,env +(* Elaborate a statement as a block whose scope is a strict subset of the scope + of its enclosing block. *) +and elab_stmt_new_scope env ctx s = + fst (elab_stmt (Env.new_scope env) ctx s) and elab_block loc env ctx b = let b',_ = elab_block_body (Env.new_scope env) ctx b in -- cgit From df81fb38c941852919246371840c5fdb003ad0fb Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Mon, 6 May 2019 17:32:44 +0200 Subject: Check for reserved keywords. `_Complex` and `_Imaginary` are reserved keywords. Since CompCert does not support these types they could be used as identifiers. However the standard requires to reject this. --- cparser/Lexer.mll | 9 ++++++++- 1 file changed, 8 insertions(+), 1 deletion(-) (limited to 'cparser') diff --git a/cparser/Lexer.mll b/cparser/Lexer.mll index b2a668f0..7cf22eef 100644 --- a/cparser/Lexer.mll +++ b/cparser/Lexer.mll @@ -23,11 +23,18 @@ module SSet = Set.Make(String) let lexicon : (string, Cabs.cabsloc -> token) Hashtbl.t = Hashtbl.create 17 let ignored_keywords : SSet.t ref = ref SSet.empty +let reserved_keyword loc id = + Diagnostics.fatal_error (loc.Cabs.filename, loc.Cabs.lineno) + "illegal use of reserved keyword `%s'" id + let () = List.iter (fun (key, builder) -> Hashtbl.add lexicon key builder) - [ ("_Alignas", fun loc -> ALIGNAS loc); + [ + ("_Alignas", fun loc -> ALIGNAS loc); ("_Alignof", fun loc -> ALIGNOF loc); ("_Bool", fun loc -> UNDERSCORE_BOOL loc); + ("_Complex", fun loc -> reserved_keyword loc "_Complex"); + ("_Imaginary", fun loc -> reserved_keyword loc "_Imaginary"); ("__alignof", fun loc -> ALIGNOF loc); ("__alignof__", fun loc -> ALIGNOF loc); ("__asm", fun loc -> ASM loc); -- cgit From 1e821bc1f1fb7a6b73ff1468b8b34f61b78cf304 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Mon, 6 May 2019 18:54:31 +0200 Subject: Change to AbsInt version string. The AbsInt build number no longer contains "release", so it must be printed additionally. --- cparser/Diagnostics.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'cparser') diff --git a/cparser/Diagnostics.ml b/cparser/Diagnostics.ml index 2b8a3eb4..2eaf6436 100644 --- a/cparser/Diagnostics.ml +++ b/cparser/Diagnostics.ml @@ -473,7 +473,7 @@ let raise_on_errors () = let crash exn = if Version.buildnr <> "" && Version.tag <> "" then begin let backtrace = Printexc.get_backtrace () in - eprintf "%tThis is CompCert, %s, Build:%s, Tag:%s%t\n" + eprintf "%tThis is CompCert, Release %s, Build:%s, Tag:%s%t\n" bc Version.version Version.buildnr Version.tag rsc; eprintf "Backtrace (please include this in your support request):\n%s" backtrace; -- cgit From 99918e4118e0ea644b20e37a13ceb31d935fdda5 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Tue, 7 May 2019 16:36:41 +0200 Subject: Reworked elaboration of declarations/definitions. Since a definition/declaration is completed with after the separator to the next init group member it is also possible to use it for example in the next init group member: char s[]="miaou", buf[sizeof s]; In order to ensure that this works the declarations are added to the environment directly during the elaboration of the init member group instead of later. --- cparser/Elab.ml | 278 ++++++++++++++++++++++++++++---------------------------- 1 file changed, 138 insertions(+), 140 deletions(-) (limited to 'cparser') diff --git a/cparser/Elab.ml b/cparser/Elab.ml index 4b326f78..f79750c2 100644 --- a/cparser/Elab.ml +++ b/cparser/Elab.ml @@ -941,31 +941,7 @@ and elab_name_group loc env (spec, namelist) = ((id, add_attributes_type a ty), env1) in (mmap elab_one_name env' namelist, sto) -(* Elaboration of an init-name group *) -and elab_init_name_group loc env (spec, namelist) = - let (sto, inl, noret, tydef, bty, env') = - elab_specifier ~only:(namelist=[]) loc env spec in - if noret && tydef then - error loc "'_Noreturn' can only appear on functions"; - let elab_one_name env (Init_name (Name (id, decl, attr, loc), init)) = - let ((ty, _), env1) = - elab_type_declarator loc env bty decl in - let a = elab_attributes env attr in - let has_fun_typ = is_function_type env ty in - if inl && not has_fun_typ then - error loc "'inline' can only appear on functions"; - let a' = - if noret then begin - warning loc Celeven_extension "_Noreturn functions are a C11 extension"; - if not has_fun_typ then - error loc "'_Noreturn' can only appear on functions"; - add_attributes [Attr("noreturn",[])] a - end else a in - if has_std_alignas env ty && has_fun_typ then - error loc "alignment specified for function '%s'" id; - ((id, add_attributes_type a' ty, init), env1) in - (mmap elab_one_name env' namelist, sto, tydef) (* Elaboration of a field group *) @@ -2373,113 +2349,101 @@ let __func__type_and_init s = (* Elaboration of top-level and local definitions *) -let enter_typedefs loc env sto dl = - if sto <> Storage_default then - error loc "non-default storage class on 'typedef' definition"; - if dl = [] then - warning loc Missing_declarations "typedef requires a name"; - List.fold_left (fun env (s, ty, init) -> - if init <> NO_INIT then - error loc "initializer in typedef"; - if has_std_alignas env ty then - error loc "alignment specified for typedef '%s'" s; - List.iter - (fun a -> match class_of_attribute a with - | Attr_object | Attr_struct -> - error loc "attribute '%s' not allowed in 'typedef'" - (name_of_attribute a) - | _ -> ()) - (attributes_of_type_no_expand ty); - match previous_def Env.lookup_typedef env s with - | Some (s',ty') when Env.in_current_scope env s' -> - if equal_types env ty ty' then begin - warning loc Celeven_extension "redefinition of typedef '%s' is a C11 extension" s; - env - end else begin - error loc "typedef redefinition with different types (%a vs %a)" - (print_typ env) ty (print_typ env) ty'; - env - end - | _ -> - if redef Env.lookup_ident env s then - error loc "redefinition of '%s' as different kind of symbol" s; - let (id, env') = Env.enter_typedef env s ty in - check_reduced_alignment loc env' ty; - emit_elab env loc (Gtypedef(id, ty)); - env') env dl - -let enter_decdefs local nonstatic_inline loc env sto dl = - (* Sanity checks on storage class *) - if (sto = Storage_auto || sto = Storage_register) && not local then - fatal_error loc "illegal storage class %s on file-scoped variable" - (name_of_storage_class sto); - if sto <> Storage_default && dl = [] then - warning loc Missing_declarations "declaration does not declare anything"; - let enter_decdef (decls, env) (s, ty, init) = - let isfun = is_function_type env ty in - if sto = Storage_register && has_std_alignas env ty then - error loc "alignment specified for 'register' object '%s'" s; - if sto = Storage_extern && init <> NO_INIT then - error loc "'extern' declaration variable has an initializer"; - if local && isfun then begin - match sto with - | Storage_static -> - error loc "function declared in block scope cannot have 'static' storage class" - | Storage_auto | Storage_register -> - error loc "illegal storage class %s on function" - (name_of_storage_class sto) - | _ -> () - end; - if is_qualified_array ty then - error loc "type qualifier used in array declarator outside of function prototype"; - (* Local variable declarations with default storage are treated as 'auto'. - Local function declarations with default storage remain with - default storage. *) - let sto1 = - if local && sto = Storage_default && not isfun - then Storage_auto - else sto in - (* enter ident in environment with declared type, because - initializer can refer to the ident *) - let (id, sto', env1, ty, linkage) = - enter_or_refine_ident local loc env s sto1 ty in - if init <> NO_INIT && not local then - add_global_define loc s; - if not isfun && is_void_type env ty then - fatal_error loc "'%s' has incomplete type" s; - (* process the initializer *) - let (ty', init') = elab_initializer loc env1 s ty init in - (* update environment with refined type *) - let env2 = Env.add_ident env1 id sto' ty' in - (* check for incomplete type *) - if not isfun && wrap incomplete_type loc env ty' then - if not local && sto' = Storage_static then begin - warning loc Tentative_incomplete_static "tentative static definition with incomplete type"; - end else if local && sto' <> Storage_extern then - error loc "variable has incomplete type %a" (print_typ env) ty'; - (* check if alignment is reduced *) - check_reduced_alignment loc env ty'; - (* check for static variables in nonstatic inline functions *) - if local && nonstatic_inline - && sto' = Storage_static - && not (List.mem AConst (attributes_of_type env ty')) then - warning loc Static_in_inline "non-constant static local variable '%s' in inline function may be different in different files" s; - if local && not isfun && sto' <> Storage_extern && sto' <> Storage_static then - (* Local definition *) - ((sto', id, ty', init') :: decls, env2) +let enter_typedef loc env sto (s, ty, init) = + if init <> NO_INIT then + error loc "initializer in typedef"; + if has_std_alignas env ty then + error loc "alignment specified for typedef '%s'" s; + List.iter + (fun a -> match class_of_attribute a with + | Attr_object | Attr_struct -> + error loc "attribute '%s' not allowed in 'typedef'" + (name_of_attribute a) + | _ -> ()) + (attributes_of_type_no_expand ty); + match previous_def Env.lookup_typedef env s with + | Some (s',ty') when Env.in_current_scope env s' -> + if equal_types env ty ty' then begin + warning loc Celeven_extension "redefinition of typedef '%s' is a C11 extension" s; + env + end else begin - (* Global definition *) - emit_elab ~linkage env2 loc (Gdecl(sto', id, ty', init')); - (* Make sure the initializer is constant. *) - begin match init' with + error loc "typedef redefinition with different types (%a vs %a)" + (print_typ env) ty (print_typ env) ty'; + env + end + | _ -> + if redef Env.lookup_ident env s then + error loc "redefinition of '%s' as different kind of symbol" s; + let (id, env') = Env.enter_typedef env s ty in + check_reduced_alignment loc env' ty; + emit_elab env loc (Gtypedef(id, ty)); + env' + +let enter_decdef local nonstatic_inline loc sto (decls, env) (s, ty, init) = + let isfun = is_function_type env ty in + if sto = Storage_register && has_std_alignas env ty then + error loc "alignment specified for 'register' object '%s'" s; + if sto = Storage_extern && init <> NO_INIT then + error loc "'extern' declaration variable has an initializer"; + if local && isfun then begin + match sto with + | Storage_static -> + error loc "function declared in block scope cannot have 'static' storage class" + | Storage_auto | Storage_register -> + error loc "illegal storage class %s on function" + (name_of_storage_class sto) + | _ -> () + end; + if is_qualified_array ty then + error loc "type qualifier used in array declarator outside of function prototype"; + (* Local variable declarations with default storage are treated as 'auto'. + Local function declarations with default storage remain with + default storage. *) + let sto1 = + if local && sto = Storage_default && not isfun + then Storage_auto + else sto in + (* enter ident in environment with declared type, because + initializer can refer to the ident *) + let (id, sto', env1, ty, linkage) = + enter_or_refine_ident local loc env s sto1 ty in + if init <> NO_INIT && not local then + add_global_define loc s; + if not isfun && is_void_type env ty then + fatal_error loc "'%s' has incomplete type" s; + (* process the initializer *) + let (ty', init') = elab_initializer loc env1 s ty init in + (* update environment with refined type *) + let env2 = Env.add_ident env1 id sto' ty' in + (* check for incomplete type *) + if not isfun && wrap incomplete_type loc env ty' then + if not local && sto' = Storage_static then begin + warning loc Tentative_incomplete_static "tentative static definition with incomplete type"; + end + else if local && sto' <> Storage_extern then + error loc "variable has incomplete type %a" (print_typ env) ty'; + (* check if alignment is reduced *) + check_reduced_alignment loc env ty'; + (* check for static variables in nonstatic inline functions *) + if local && nonstatic_inline + && sto' = Storage_static + && not (List.mem AConst (attributes_of_type env ty')) then + warning loc Static_in_inline "non-constant static local variable '%s' in inline function may be different in different files" s; + if local && not isfun && sto' <> Storage_extern && sto' <> Storage_static then + (* Local definition *) + ((sto', id, ty', init') :: decls, env2) + else begin + (* Global definition *) + emit_elab ~linkage env2 loc (Gdecl(sto', id, ty', init')); + (* Make sure the initializer is constant. *) + begin match init' with | Some i when not (Ceval.is_constant_init env2 i) -> - error loc "initializer is not a compile-time constant" + error loc "initializer is not a compile-time constant" | _ -> () - end; - (decls, env2) - end in - let (decls, env') = List.fold_left enter_decdef ([], env) dl in - (List.rev decls, env') + end; + (decls, env2) + end (* Processing of K&R-style function definitions. Synopsis: T f(X1, ..., Xn) @@ -2735,6 +2699,51 @@ let elab_fundef genv spec name defs body loc = genv (* Definitions *) +let elab_decdef (for_loop: bool) (local: bool) (nonstatic_inline: bool) + (env: Env.t) ((spec, namelist): Cabs.init_name_group) + (loc: Cabs.cabsloc) : decl list * Env.t = + let (sto, inl, noret, tydef, bty, env') = + elab_specifier ~only:(namelist=[]) loc env spec in + (* Sanity checks on storage class *) + if tydef then begin + if sto <> Storage_default then + error loc "non-default storage class on 'typedef' definition"; + if namelist = [] then + warning loc Missing_declarations "typedef requires a name"; + end else begin + if (sto = Storage_auto || sto = Storage_register) && not local then + fatal_error loc "illegal storage class %s on file-scoped variable" + (name_of_storage_class sto); + if sto <> Storage_default && namelist = [] then + warning loc Missing_declarations "declaration does not declare anything"; + end; + let elab_one_name (decls, env) (Init_name (Name (id, decl, attr, loc), init)) = + let ((ty, _), env1) = + elab_type_declarator loc env bty decl in + let a = elab_attributes env attr in + let has_fun_typ = is_function_type env ty in + if for_loop && (has_fun_typ || sto = Storage_extern || sto = Storage_static || tydef) then + error loc "declaration of non-local variable in 'for' loop" ; + if has_fun_typ then begin + if noret then + warning loc Celeven_extension "_Noreturn functions are a C11 extension"; + end else begin + if inl then + error loc "'inline' can only appear on functions"; + if noret then + error loc "'_Noreturn' can only appear on functions"; + end; + let a' = if noret then add_attributes [Attr ("noreturn", [])] a else a in + if has_std_alignas env ty && has_fun_typ then + error loc "alignment specified for function '%s'" id; + let decl = (id, add_attributes_type a' ty, init) in + if tydef then + (decls, enter_typedef loc env1 sto decl) + else + enter_decdef local nonstatic_inline loc sto (decls, env1) decl + in + let (decls, env') = List.fold_left elab_one_name ([],env') namelist in + (List.rev decls, env') let elab_definition (for_loop: bool) (local: bool) (nonstatic_inline: bool) (env: Env.t) (def: Cabs.definition) @@ -2749,18 +2758,7 @@ let elab_definition (for_loop: bool) (local: bool) (nonstatic_inline: bool) (* "int x = 12, y[10], *z" *) | DECDEF(init_name_group, loc) -> - let ((dl, env1), sto, tydef) = - elab_init_name_group loc env init_name_group in - if for_loop then begin - let fun_declaration = List.exists (fun (_, ty, _) -> is_function_type env ty) dl in - if fun_declaration || sto = Storage_extern || sto = Storage_static || tydef then - error loc "declaration of non-local variable in 'for' loop" ; - end; - if tydef then - let env2 = enter_typedefs loc env1 sto dl - in ([], env2) - else - enter_decdefs local nonstatic_inline loc env1 sto dl + elab_decdef for_loop local nonstatic_inline env init_name_group loc (* pragma *) | PRAGMA(s, loc) -> -- cgit From 45f7c8be7179942d9667a5a26cb1bb6f6fcd2d04 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Mon, 20 May 2019 19:33:52 +0200 Subject: Add a check for the args of unprototyped calls. The arguments that are passed to an unprototyped function must also be checked to be valid types passed to a function, i.e. they must be complete types after argument conversion. --- cparser/Elab.ml | 11 ++++++++--- 1 file changed, 8 insertions(+), 3 deletions(-) (limited to 'cparser') diff --git a/cparser/Elab.ml b/cparser/Elab.ml index f79750c2..13aab900 100644 --- a/cparser/Elab.ml +++ b/cparser/Elab.ml @@ -1815,7 +1815,7 @@ let elab_expr ctx loc env a = emit_elab ~linkage env loc (Gdecl(sto, id, ty, None)); { edesc = EVar id; etyp = ty },env | _ -> elab env a1 in - let bl = mmap elab env al in + let (bl, env) = mmap elab env al in (* Extract type information *) let (res, args, vararg) = match unroll env b1.etyp with @@ -1830,8 +1830,13 @@ let elab_expr ctx loc env a = (* Type-check the arguments against the prototype *) let bl',env = match args with - | None -> bl - | Some proto -> elab_arguments 1 bl proto vararg in + | None -> + List.iter (fun arg -> + let arg_typ = argument_conversion env arg.etyp in + if incomplete_type env arg_typ then + error "argument type %a is incomplete" (print_typ env) arg.etyp; + ) bl; (bl,env) + | Some proto -> elab_arguments 1 (bl, env) proto vararg in { edesc = ECall(b1, bl'); etyp = res },env | UNARY(POSINCR, a1) -> -- cgit From 8b0724fdb1af4f89a603f7bde4b5b625c870e111 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Fri, 31 May 2019 11:55:57 +0200 Subject: Fix misspellings in messages, man pages, and comments This is a manual, partial merge of Github pull request #296 by @Fourchaux. flocq/, cparser/MenhirLib/ and parts of test/ have not been changed because these are local copies and the fixes should be performed upstream. --- cparser/Cutil.ml | 2 +- cparser/Diagnostics.ml | 2 +- cparser/Diagnostics.mli | 8 ++++---- cparser/Elab.ml | 2 +- cparser/handcrafted.messages | 4 ++-- 5 files changed, 9 insertions(+), 9 deletions(-) (limited to 'cparser') diff --git a/cparser/Cutil.ml b/cparser/Cutil.ml index cf67015a..7329767a 100644 --- a/cparser/Cutil.ml +++ b/cparser/Cutil.ml @@ -947,7 +947,7 @@ let binary_conversion env t1 t2 = end | _, _ -> assert false -(* Conversion on function arguments (with protoypes) *) +(* Conversion on function arguments (with prototypes) *) let argument_conversion env t = (* Arrays and functions degrade automatically to pointers *) diff --git a/cparser/Diagnostics.ml b/cparser/Diagnostics.ml index 2eaf6436..51dcab47 100644 --- a/cparser/Diagnostics.ml +++ b/cparser/Diagnostics.ml @@ -32,7 +32,7 @@ let max_error = ref 0 let diagnostics_show_option = ref true (* Test if color diagnostics are available by testing if stderr is a tty - and if the environment varibale TERM is set + and if the environment variable TERM is set *) let color_diagnostics = let term = try Sys.getenv "TERM" with Not_found -> "" in diff --git a/cparser/Diagnostics.mli b/cparser/Diagnostics.mli index ded8019f..6a3c11c8 100644 --- a/cparser/Diagnostics.mli +++ b/cparser/Diagnostics.mli @@ -22,22 +22,22 @@ exception Abort (** Exception raised upon fatal errors *) val check_errors : unit -> unit - (** Check whether errors occured and raise abort if an error occured *) + (** Check whether errors occurred and raise abort if an error occurred *) type warning_type = | Unnamed (** warnings which cannot be turned off *) | Unknown_attribute (** usage of unsupported/unknown attributes *) - | Zero_length_array (** gnu extension for zero lenght arrays *) + | Zero_length_array (** gnu extension for zero length arrays *) | Celeven_extension (** C11 features *) | Gnu_empty_struct (** gnu extension for empty struct *) - | Missing_declarations (** declation which do not declare anything *) + | Missing_declarations (** declaration which do not declare anything *) | Constant_conversion (** dangerous constant conversions *) | Int_conversion (** pointer <-> int conversions *) | Varargs (** promotable vararg argument *) | Implicit_function_declaration (** deprecated implicit function declaration *) | Pointer_type_mismatch (** pointer type mismatch in ?: operator *) | Compare_distinct_pointer_types (** comparison between different pointer types *) - | Implicit_int (** implict int parameter or return type *) + | Implicit_int (** implicit int parameter or return type *) | Main_return_type (** wrong return type for main *) | Invalid_noreturn (** noreturn function containing return *) | Return_type (** void return in non-void function *) diff --git a/cparser/Elab.ml b/cparser/Elab.ml index 13aab900..9cca930d 100644 --- a/cparser/Elab.ml +++ b/cparser/Elab.ml @@ -2632,7 +2632,7 @@ let elab_fundef genv spec name defs body loc = For prototyped functions this has been done by [elab_fundef_name] already, but some parameter may have been shadowed by the function name, while it should be the other way around, e.g. - [int f(int f) { return f+1; }], with [f] refering to the + [int f(int f) { return f+1; }], with [f] referring to the parameter [f] and not to the function [f] within the body of the function. *) let lenv = diff --git a/cparser/handcrafted.messages b/cparser/handcrafted.messages index 95077739..6d972439 100644 --- a/cparser/handcrafted.messages +++ b/cparser/handcrafted.messages @@ -4477,7 +4477,7 @@ translation_unit_file: VOID PRE_NAME TYPEDEF_NAME PACKED LPAREN CONSTANT RPAREN ## # We have just parsed a list of attribute specifiers, but we cannot -# print it because it is not available. We do not know wether it is +# print it because it is not available. We do not know whether it is # part of the declaration or whether it is part of the first K&R parameter # declaration. @@ -4599,7 +4599,7 @@ translation_unit_file: PACKED LPAREN BUILTIN_OFFSETOF XOR_ASSIGN ## Ill-formed __builtin_offsetof. -At this point, an opening paranthesis '(' is expected. +At this point, an opening parenthesis '(' is expected. #------------------------------------------------------------------------------ -- cgit