| Commit message (Collapse) | Author | Age | Files | Lines |
|---|
| |
|
|
|
|
| |
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
|
| | | |
|
| |/ |
|
| | |
|
| | |
|
| | |
|
| |
|
|
|
| |
The arm dwarf float registers constants are larger than 2 bytes.
Bug 20489
|
| | |
|
| |
|
|
|
| |
A non reseted Hashtbl caused problems with multiple input files.
Bug 20462
|
| |
|
|
|
|
| |
Since the dwarf register names for x86_32 and x86_64 differ it is
wrong to hardcode the dwarf register number for rsp to 4.
Bug 20461
|
| |
|
|
| |
The warning for C11 features is now also triggered for _Noreturn.
|
| |
|
|
|
|
| |
The warning missing declarations is now also triggered for
declarations without name in field lists of composite types if
the declaration is not an anonymous composite or a bitfield member.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
This fixes two issues:
1- The 'size' and 'alignment' arguments of __builtin_memcpy_aligned were declared with type 'unsigned int', which is not good for a 64-bit platform.
2- The corresponding arguments were not cast to type 'unsigned int', causing compilation errors if e.g. the size argument is a 64-bit integer.
(Reported by Michael Schmidt.)
The fix:
1- Evaluate the 3rd and 4th arguments at type size_t
2- Support both Vint and Vlong as results of this evaluation
3- Declare these arguments with type 'unsigned long'.
Supporting work: in lib/Camlcoq.ml, add Z.modulo and Z.is_power2 operations.
Concerning part 3 of the fix, type size_t would be better for future
platforms where size_t is bigger than unsigned long, but some more
work is needed to delay the evaluation of C2C.builtins_generic to
after Cutil.size_t_ikind() is stable, or, equivalently, to evaluate
the cparser/ machine configuration before C2C initializes.
|
| |
|
|
| |
This comes handy in the next commit where constval_cast is used from C2C.
|
| |
|
|
|
|
|
| |
is 64 bits
It was wrongly assumed that 'long' is 32 bits.
(Reported by Michael Schmidt.)
|
| |
|
|
|
| |
Address constants need to be 64bit also in the debug information.
Bug 20335
|
| | |
|
| | |
|
| |\ |
|
| | |
| |
| |
| |
| |
| | |
Calls to variadic or unprototyped functions set this register to reflect the number of arguments passed in XMM registers. Thus we must make sure that rax is not used to hold the pointer to the function being called.
(Report by Michael Schmidt.)
|
| | | |
|
| |/ |
|
| | |
|
| | |
|
| | |
|
| | |
|
| |\ |
|
| | | |
|
| | | |
|
