| Commit message (Collapse) | Author | Age | Files | Lines |
|
|
|
|
| |
Previous scripts were relying on the order in which apply's HO
unification performs reductions, for a goal that could be solved by
reflexivity.
|
| |
|
| |
|
| |
|
|
|
|
|
|
|
| |
32-bit executables cannot be built since XCode 10.0 (sep 2018).
32-bit executables cannot be executed since MacOS 10.15 (oct 2019).
Better remove x86-32 support and fail at configuration time instead of
at the end of the build.
|
|
|
|
|
|
| |
Not all pre-processors concatenate string literal lists, however they
are allowed in _Static_assert. This is similar to the rules for inline
assembly etc.
|
| |
|
|
|
|
| |
__builtin_sqrt (no "f") is the name used by GCC and Clang.
|
|
|
|
|
|
| |
Share the testing code for built-in functions that are available on
all target platforms.
Improve testing of __builtin_clz* and __builtin_ctz*
|
|
|
|
| |
These functions are now available on all targets.
|
|
|
|
| |
Using the "rbit" instruction (reverse bits).
|
|
|
|
| |
Using binary search loops expanded at point of use.
|
| |
|
|
|
|
| |
__builtin_fabs has already been expanded in backend/Selection.v .
|
|
|
|
| |
We check that this builtin function is only called from within a variadic
function and has the correct number of arguments.
|
| |
|
|
|
|
|
| |
Added error descriptions for the new syntax errors introduced by
'_Static_assert'.
|
| |
|
|
|
|
|
| |
Returns 1 if the argument is a constant expression, 0 otherwise.
Closes: #366
|
| |
|
|
|
|
|
|
| |
We check in the initial environment if a function is already defined to
avoid redefinition of functions that are part of the builtin
environment.
|
| |
|
|
|
|
|
|
|
| |
If ocamlopt is not available, use ocamlc instead of ocamlopt to build
auxiliary tools (tools/modorder, tools/ndfun).
This is a follow-up to commit 9af28924.
|
|
|
|
|
|
|
| |
This is a follow-up to commit 3b1f3dd5, which was wrong in that
errors in a shell pipeline were not correctly detected.
Fixes: #363
|
| |
|
| |
|
|
|
|
| |
This reverts commit 1a01ad629109cdb60fddae3787e3a589d20e9790.
|
|
|
|
|
|
| |
The version string dumped in the file should be the same as the version
string printed by `-version`. The option is also not printed by `-help`
since it is for internal use only.
|
| |
|
| |
|
| |
|
|
|
|
|
|
| |
If ocamlopt (the native-code OCaml compiler) is not available,
fall back to building with ocamlc (the bytecode OCaml compiler).
Fixes: #359
|
|
|
|
|
| |
Use `ocamlfind query menhirLib` in preference to `menhir --suggest-menhirLib`.
Fixes: #363
|
| |
|
| |
|
| |
|
|
|
|
|
| |
The name_of_register and register_of_name function are shared between
all architectures and can be moved in a common file.
|
|
|
|
|
| |
The function is in fact just a call to the
function`is_callee_save_register` from `Conventions1.v`.
|
|
|
|
|
|
|
| |
The function String.uppercase was deprecated and the replacement
function String.upercase_ascii was only available from OCaml 4.03.0.
Since the minimal OCaml version is now 4.05.0 we can use the function
String.upercase_ascii.
|
|
|
|
|
| |
Replace the pattern `try Some (Hashtbl.find ...) with Not_found -> None`
by a call to the function Hashtbl.find_opt.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
A typical example is `(void) __builtin_sel(a, b, c)`.
It is safe to generate zero code for these uses of builtins
because builtins whose semantics are known to the compiler
are pure. Other builtins with side effects (e.g. `__builtin_trap`)
are not known and will remain in the compiled code.
It is useful to generate zero code for these uses of builtins
because some of them (e.g. `__builtin_sel`) must be transformed
into proper CminorSel expressions during instruction selection.
Otherwise, they propagate all the way to ExpandAsm, causing
a "not implemented" error there.
|
|
|
|
| |
In particular __builtin_sel.
|
|
|
|
|
|
|
| |
Based on testing with beta-1 release.
The deprecation warning about the "omega" tactic is ignored while we
decide when to switch to "lia" instead.
|
|
|
|
|
|
|
| |
As detected by the new warning in Coq 8.12.
The use of Fixpoint here is not warranted and either an oversight or a
leftover from an earlier version.
|
|
|
|
| |
Follow-up to commit 070babef.
|
|
|
|
|
|
|
|
| |
This is useful for statements such as `(void) expr;` where we would
prefer not to explicitly compute intermediate values of type `void`
and store them in Clight temporary variables.
See issue #361 for a real-world occurrence of this phenomenon.
|
|
|
|
| |
Updated configure script to also allow coq version 8.11.2
|
|
|
|
| |
__builtin_ais_annot is not supported for macOS nor for Cygwin.
|
|
|
|
|
|
|
|
|
|
|
|
| |
The printing of EF_annot and EF_annot_val was missing the extra "kind"
parameter introduced in commit 6a010b4.
Also: the automatic translation of annotations into Coq assertions
was confusing and prevented other uses of __builtin_annot statements
in conjunction with clightgen. I believe it was never used.
This commit removes this translation.
Closes: #360
|
|
|
|
| |
Closes: #358
|