diff options
Diffstat (limited to 'Changelog')
| -rw-r--r-- | Changelog | 137 |
1 files changed, 137 insertions, 0 deletions
@@ -1,3 +1,140 @@ +Release 3.4, 2018-09-17 +======================= + +Bug fixing: +- Redefinition of a typedef in a different scope was wrongly rejected. +- Attach `_Alignas(N)` and `__attribute((aligned(N)))` to names + instead of types, so that `_Alignas(16) int * p` means + "16-aligned pointer to int", not "pointer to 16-aligned int". +- For packed structs, fix a discrepancy between the size and alignment + computed during elaboration and those computed by the verified front-end + after expansion. +- Honor qualified array types in function parameters: if a parameter is + declared as e.g. `int t[const 4]`, it is now treated as `int * const t` + in the function body, not `int * t` like before. +- Reject `__builtin_offsetof(struct s, f)` if `f` is a bit-field. +- Wrong parsing of attributes having multiple arguments such as + `__attribute((packed(A,B,C)))`. +- If `__builtin_ais_annot` is followed immediately by a label (e.g. a + loop head), add a nop instruction to separate the annotation from + the label. +- Wrong parsing of the command-line options `-u <symbol>` and `-iquote`. +- PowerPC in hybrid 32/64 bit mode: reject %Q and %R register specifications + in inline assembly code, since 64-bit integer arguments are not split + in two registers. +- x86 64-bit mode: wrong expansion of __builtin_clzl and builtin_ctzl + (issue #127). + +New checks for ISO C conformance: +- Removed support for `_Alignof(expr)`, which is not C11; + only `_Alignof(ty)` is part of C11. +- Reject occurrences of `_Alignas` in places that are not allowed by C11, + e.g. in `typedef`. `__attribute((aligned(N)))` can be used instead. +- Reject occurrences of `restrict` in places that are not allowed by + C99 and C11. +- Reject structs composed of a single flexible array `struct { ty []; }`. +- Check that qualified array types such as `int t[const 4]` occur only + as function parameters, but nowhere else. +- In function definitions, reject function parameters that have no names. + +New warnings: +- Warn for flexible array types `ty[]` in places where they do not make sense. +- Warn for inline (not static inline) functions that declare + non-constant static variables. +- Optionally warn if the alignment of an object is reduced below its + natural alignment because of a _Alignas qualifier or an aligned attribute, + or a packed attribute. +- Warn for tentative static definitions with an incomplete type, e.g. + `static int x[];`. +- The warning about uses of C11 features is now off by default. + +Semantic preservation proof: +- Model the fact that external functions can destroy caller-save registers + and Outgoing stack slots; adapt the proofs accordingly. + +Coq and OCaml development: +- Support Coq versions 8.8.1 and 8.8.2. +- Support OCaml versions 4.7.0 and up. +- Support Menhir versions 20180530 and up. + +Others: +- Improved error handling in "configure" script (issue #244) +- clightgen adds configuration information to the generated .v file (issue #226) + + + +Release 3.3, 2018-05-30 +======================= + +New features: +- Introduced the __builtin_ais_annot built-in function to communicate + source-level annotations to AbsInt's a3 tool suite via a special + section in object and executable files. +- Improved C11 support: define the C11 conditional feature macros; + define the max_align_t type in stddef.h. +- PowerPC 64-bit port: new built-in functions for 64-bit load-store with + byte reversal and for 64-bit integer multiply high. +- x86 64 bits: add support for BSD. + +Bug fixing: +- Wrong code generated for unions containing several bit fields. +- Internal compiler errors for some initializers for structs and + unions containing bit-fields, and for anonymous members of unions. +- Missing error reporting for <integer> - <ptr> subtraction, + causing an internal retyping error later during compilation. +- String literals are l-values. +- String literals have array types, not pointer types. +- Array sizes >= 2^32 were handled incorrectly on 64-bit platforms. +- Wrong code generated for global variables of size 2^31 bytes or more. +- struct and union arguments to annotation builtins must be passed by + reference, regardless of the ABI calling conventions. +- "e1, e2" has pointer type if "e2" has array type. +- x86 64 bits: in "symbol + ofs" addressing modes, the offset "ofs" + must be limited to [-2^24, 2^24) otherwise linking can fail. + +New or improved diagnostics (errors and warnings): +- Warn for comparison of a pointer to a complete type and a pointer to + an incomplete type. +- More checks on variables declared in "for" loops: not static, not + extern, not function types. +- Reject empty declarations in K&R functions. +- Reject arrays of incomplete types. +- Reject duplicate 'case' or 'default' statements within a 'switch'. +- Reject 'case' and 'default' statements outside a 'switch'. +- Check that 'typedef' declares a name and doesn't contain '_Noreturn'. +- Function parameters are in the same scope as function local variables. +- More comprehensive constant-ness checks for initializers of global + or static local variables. +- Make sure an enum cannot have the same tag as a struct or an union. +- More checks on where the 'auto' storage class can be used. +- Accept empty enum declaration after nonempty enum definition. +- Reject pointers to incomplete types in ptr - ptr subtraction. +- When defining a function, take attributes (_Noreturn, etc) from + earlier declarations of the function into account. +- Better check for multiple definitions of functions or global variables. +- Reject illegal initializations of aggregates such as "char c[4] = 42;". +- Reject designated initializers where a member of a composite type is + re-initialized after the composite has been initialized as a whole. +- Reject casts to struct/union types. +- Reject sizeof(e) where e designates a bit-field member of a struct or union. +- "e1, e2" is not a compile-time constant expression even if e1 and e2 are. +- "main" function must not be "inline" +- Warn for functions declared extern after having been defined. +- Warn for function declarations after function definitions when the + declaration has more attributes than the definition. +- Warn for assignment of a volatile struct to a non-volatile struct. +- Warn for "main" function if declared _Noreturn. + +Coq development: +- Added support for Coq versions 8.7.2 and 8.8.0. +- Rewrote "Implicit Arguments" and "Require" inside sections, + these are obsolete in 8.8.0. +- Upgraded Flocq to version 2.6.1. +- Optionally install the .vo files for reuse by other projects + (options -install-coqdev and -coqdevdir to configure script; + automatically selected if option -clightgen is given). + + Release 3.2, 2018-01-15 ======================= |