| Commit message (Collapse) | Author | Age | Files | Lines |
|\
| |
| | |
Implement offsetof via builtin
|
| |
| |
| |
| |
| |
| |
| | |
Instead of multiplying the array constant directly with the
size of the offset the cautious_mul function is used to detect
potential overflows.
Bug 20765
|
| | |
|
| |
| |
| |
| |
| |
| | |
Gcc and clang do not raise an error for this, also it should work
for the last array element which can be without size.
Bug 20765
|
| | |
|
| | |
|
| |
| |
| |
| |
| |
| |
| |
| |
| | |
The c standard allows member designators for offsetof. The current
implementation works by recursively combining the offset of each
of the member designators. For array access the size of the
subtypes is multiplied by the index and for members the offset of
the member is calculated.
Bug 20765
|
| |
| |
| |
| |
| |
| |
| |
| | |
The problem was that sub structs are were not correctly aligned.
The new version is much simpler and uses the sizeof_struct to
calculate the individual offsets and add them up to get correct
offest.
Bug 20765
|
| | |
|
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
The implementation of offsetof as macro in the form
((size_t) &((ty*) NULL)->member) has the problem that it cannot be
used everywhere were an integer constant expression is allowed,
for example in initiliazers of global variables and there is also
no check for the case that member is of bitifield type.
The new implementation adds a builtin function for this which is
replaced by an integer constant during elaboration.
Bug 20765
|
| |
| |
| |
| |
| |
| |
| | |
The new Makefile variable LINK_OPT can be used to specify
additional linker flags for different operating systems, like
linking with setargv.obj under windows.
Bug 20871
|
| |
| |
| |
| | |
Follow-up to commit 1df1830
|
| | |
|
| |
| |
| |
| | |
Those three functions can be useful to implement front-ends for languages other than C.
|
| |
| |
| |
| |
| |
| |
| |
| |
| | |
The new option -fdiagnostics-format allows it to switch between
the three different format version:
-ccomp (default) with file:line:
-vi with file+line:
-msvc with file(line):
Bug 19872
|
| | |
|
| | |
|
| |
| |
| |
| |
| |
| | |
Controls whether the [-Woption] is printed in the diagnostic
message for mappable warnings/errors.
Bug 19872
|
| |
| |
| |
| |
| |
| |
| | |
The option -fmax-errors limits the number of errors that are
reported before the compilation is aborted. The default 0 means no
limit.
Bug 19872
|
| | |
|
| | |
|
| | |
|
| | |
|
| |
| |
| |
| |
| | |
GCC treats files with .sx extension in the same way as it treats
files with .S suffix.
|
| |
| |
| |
| |
| | |
Anonymous members no longer are printed in the debug information.
Fix 20798
|
|/ |
|
| |
|
|
|
|
|
|
|
| |
Instead of just accepting a string the function is changed to
accept a format string. This removes a lot of artificial sprintfs
in calls to the functions.
Bug 19872
|
|
|
|
|
|
| |
Instead of escaping all newlines etc for the help options use
quoted strings.
Bug 19872
|
|
|
|
|
|
| |
More functions are now documented. Furthermore compcert now prints
"ccomp:" instead of nothing for unknown locations.
Bug 19872
|
| |
|
| |
|
| |
|
| |
|
|
|
|
|
|
|
|
| |
If CompCert crashes because of an uncaught exception the exception
is caught toplevel and the backtrace is printed plus an additional
message to include the backtrace in a support request, if buildnr
and tag are available.
Bug 20681.
|
| |
|
| |
|
| |
|
|\
| |
| | |
Next try for support of anonymous structs.
|
| |
| |
| |
| | |
"try ...; true with _ -> false" is dangerous if "..." raises unexpected exceptions such as Out_of_memory or Stack_overflow.
|
| | |
|
| | |
|
| |
| |
| |
| |
| |
| |
| |
| | |
The naming of anonymous structs is performed by an additional step
in elab_struct_or_union_info instead of in elab_field_group.
Also the aux functions are renamed to access.
Bug 20003
|
| |
| |
| |
| |
| |
| | |
Instead of using idents the anonymous fileds get names of the
for <anon>_c where c is a counter of all anonymous members.
Bug 20003
|
| |
| |
| |
| |
| |
| |
| |
| | |
Applied to the 92-constructor 'operation' type, 'decide equality' produces a huge transparent term that causes the VM compiler to generate huge code and exceeed a memory limit of Coq on 32-bit platforms. (The limit is OCaml's, really.)
The lib/BoolEqual.v file defines alternative tactics to build decidable equalities where the transparent part of the definition is smaller (O(N^2) instead of O(N^3)). The proof parts are still huge (O(N^3)) but they are opaque.
Fixes #151
|
| | |
|
| | |
|
| | |
|
| |
| |
| |
| |
| |
| | |
Since the test for emit constants has moved before the printing of
the instruction the no_fallthrough of the last test should be used.
Bug 20598
|
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
Switch tables were able to screw up the book keeping for emiting
constants in code. Now we estimate the size of an instruction
before printing it by the safe upper bound of 12 for normal
instructions, 1024 for inline assembler and
(2 or 3 + length switch tbl) * 4 for switch tables depending on
thumb etc.
Bug 20598
|