| Commit message (Collapse) | Author | Age | Files | Lines |
... | |
|
|
|
|
|
|
|
|
| |
Previously, using an unknown builtin function was treated like any
other call to an undeclared function: a warning was emitted, and
an error occurred at link-time.
With this commit, using an unknown builtin function is an error,
like in Clang.
|
|
|
|
|
|
|
| |
The `__builtin_nop` function is documented only for PowerPC.
It was added to the other architectures by copy paste, but has no
known uses. So, remove `__builtin_nop` from all architectures
but PowerPC.
|
| |
|
| |
|
|
|
|
|
|
|
|
|
| |
In addressing modes for load and store instructions, the offset must be a multiple of the memory size being accessed. When accessing global variables, this may not be the case if the alignment of the variable is less than its size. Errors occur at link time.
This PR extends the check for a representable offset for the addressing of global
variables to also check whether the variable is correctly aligned. Only if both conditions are
met can we generate the short sequence Padrp / ADadr. Otherwise we go through the generic
loadsymbol sequence.
|
| |
|
| |
|
|
|
|
|
|
|
| |
Instead of constructing four different lists for maintaining the
state of the warnings only one list is now used. This list contains
the name of the warning and a boolean indicating whether this option
should be active by default. The rest is computed from this list.
|
| |
|
|
|
|
| |
A stronger `intuition` in the near future would break this use of `intuition`.
|
|
|
| |
At least OCaml 4.05 is now required as well as Coq 8.8.
|
|
|
|
| |
The proposed proof only uses `zify` for closing the goal. This is
needed for Coq PR #10982 which changes the inner working of `zify`.
|
| |
|
|
|
|
|
| |
A "dollar" sign in a function name or a global variable name was producing
incorrect Coq identifiers. (Issue #319.)
|
| |
|
|
|
|
|
|
|
| |
Some hints will move from the core database to the `ordered_type` database
(see https://github.com/coq/coq/pull/9772).
This commit prepares for this move by adding `with ordered_type` to the invocations
of `auto` and `eauto` that use the hints in question.
|
| |
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
* Extend check for incomplete type.
Extended the check to also include a check for variables with
incomplete object type that are not arrays, that have an
initializer. Furthermore the warning includes the type and variable
name.
* Warning for incomplete type in compound literals.
Incomplete types are not allowed for compound literals, except for
array types.
* Extend type printing function.
The type of a typedeof of an anonymous type should not be printed.
Furthermore added '<anonymous>' to the printing of anonymous types.
* Unify incomplete type errors message.
The incomplete type error messages should all look the same including
name of the variable, parameter, etc. and then the incomplete type.
|
|
|
|
| |
Treat doc as documentation and tests as vendored for github linguist
|
|
|
|
|
|
| |
In ISO C, inline functions behaves differently whether they have been declared `extern` at least once or not (i.e. all the declarations have no `extern` and no `static` modifier).
Hence, functions that have been declared / defined `extern` once should remain `extern` when redeclared without `extern`. This gives the ISO C behavior for inline functions and has no impact for non-inline functions.
|
|
|
|
|
|
|
|
| |
If the first argument to `isel` is GPR0, it reads as the constant 0.
This cannot occur in code generated by CompCert, due to the fact that
GPR0 is not available as register for register allocation. However the
assembler semantics should be as close as possible to the actual
hardware.
|
| |
|
|
|
|
|
|
|
|
| |
Initially, the "bench" entries of the test suite used a "xtime" utility
developed in-house and not publically available.
This commit adds a version of "xtime" written in OCaml (tools/xtime.ml)
and updates the "bench" entries of the test/*/Makefile to use it.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
The temporary variables introduced by SimplLocals reuse the same
integer identifiers as the local variables they come from. This commit
ensures that these variables are printed as "$var", where "var"
is the original variable name, instead of "$NNN" as before.
The "$NNN" form is retained for temporary variables that do not
correspond to a source-level local variable, such as the temporary
variables introduced by SimplExpr.
This commit should make no difference for "ccomp -dclight", because
the Clight that is printed is the Clight version 1 produced by
SimplExpr, where every temporary is fresh and does not correspond
to a source-level local variable.
This commit does change the output of "clightgen -dclight", because
the Clight that is printed is the Clight version 2 produced by
SimplLocals. The printed Clight is much more legible thanks to
the more meaningful temporary variable names.
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
The Clight output of clightgen is Clight version 2, after SimplLocals
conversion, where function parameters are temporary variables, not
variables.
This commit makes sure the function parameters are printed as
temporary variables and not as variables. In passing, it
generalizes the Clight pretty-printer so that it can print
both Clight version 1 and Clight version 2.
Closes: #314
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
The json export prints formatted json, which takes a lot of
additional time, however the result is only consumed by other tools
and not meant for human reading.
This commit implements several small changes in order to speedup
the json export:
* Removal of usage of the Format Module
* Replacing `fprintf` calls by calls to function that print
directly, such as `output_string`, etc.
* Replacing list of all instruction names by a set of all
instructions
|
|
|
|
| |
"omega" fails in Coq 8.7, but not in 8.8 and later.
|
|\
| |
| |
| | |
Support target architecture AArch64 (ARMv8 in 64-bit mode)
|
| |
| |
| |
| |
| |
| |
| |
| | |
The argument is of type Tlong, not Tint.
This caused spurious errors in RTLtyping.
Also: in AArch64/PrintOp.ml, print Cmaskl{zero,notzero} with "&l"
to distinguish them from Cmask{zero,notzero}.
|
| |
| |
| |
| | |
These instructions are generated by __builtin_memcpy.
|
| |
| |
| | |
Some changes were not correctly propagated to all architectures.
|
| |
| |
| |
| | |
With special emphasis on the use of the AArch64 fmov #imm instruction.
|
| |
| |
| |
| |
| | |
This commit adds a back-end for the AArch64 architecture, namely ARMv8
in 64-bit mode.
|
| | |
|
| | |
|
| |
| |
| |
| |
| |
| | |
Syntax is "pat ?? bexpr => action".
The whole case is selected only when "pat" matches and then "bexpr"
evaluates to "true".
|
| | |
|
| | |
|
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
This is a variant of exec_straight where it is allowed to take zero steps.
In other words, exec_straight0 is the "star" relation, while exec_straight
is the "plus" relation.
In the end we need "plus" relations in simulation diagrams, to show
the absence of stuttering. But the "star" relation exec_straight0 is
useful to reason about code fragments that are always preceded or
followed by at least one instruction.
|
| | |
|
| |
| |
| |
| | |
Should simplify reasoning over Boolean equalities.
|
| | |
|
| |
| |
| |
| | |
Just ensure sign_ext 0 x = zero. This simplifies some statements and proofs.
|
| | |
|
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
There was a misunderstanding on the asm syntax for 3-operand instructions
such as vfmadd132: when the Intel manual reads
vfmadd132 res, arg2, arg3
the corresponding GNU asm syntax is
vfmadd132 arg3, arg2, res
but not
vfmadd132 arg2, arg3, res
Closes: #188
|
| | |
|
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
The "undeclared-scope" warning fires when we use a "notation" scope
before having declared it. This is a good thing, except that
the "Declare Scope" vernacular that declares a scope was introduced
in Coq 8.10 and is not available in earlier versions.
Hence there is no way to avoid triggering the warning yet remain
compatible with pre-8.10 Coq versions.
This commit silences the warning. It will have to revisited when
Coq 8.10 is the oldest version of Coq we support in CompCert.
|
| | |
|