From ce4951549999f403446415c135ad1403a16a15c3 Mon Sep 17 00:00:00 2001 From: xleroy Date: Mon, 12 Nov 2012 13:42:22 +0000 Subject: Globalenvs: allocate one-byte block with permissions Nonempty for each function definition, so that comparisons between function pointers are correctly defined. AST, Globalenvs, and many other files: represent programs as a list of (function or variable) definitions instead of two lists, one for functions and the other for variables. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2067 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- Changelog | 6 ++++++ 1 file changed, 6 insertions(+) (limited to 'Changelog') diff --git a/Changelog b/Changelog index af9ce00..e5cee60 100644 --- a/Changelog +++ b/Changelog @@ -7,6 +7,9 @@ Improvements in confidence: top of the Flocq library. Language semantics: +- Comparison between function pointers is now correctly defined + in the semantics of CompCert C (it was previously undefined behavior, + by mistake). - The "&&" and "||" operators are now primitive in CompCert C and are given explicit semantic rules, instead of being expressed in terms of "_ ? _ : _" as in previous CompCert releases. @@ -28,6 +31,9 @@ Internal simplifications: - Clight: removed dependencies on CompCert C syntax and semantics. - Cminor: suppressed the "Oboolval" and "Onotbool" operators, which can be expressed in terms of "Ocmpu" at no performance costs. +- All languages: programs are now presented as a list of global definitions + (of functions or variables) instead of two lists, one for functions + and the other for variables. Other changes: - For compatibility with other C compilers, output files are now generated -- cgit v1.2.3