| Commit message (Collapse) | Author | Age | Files | Lines |
|
|
|
|
|
|
|
|
|
|
|
| |
The Elab pass checks that the argument of 'case' is a compile-time constant
expression. This commit records the value of this expression in the
C.Scase AST generated by Elab, so that it can be used for further
diagnostics, i.e. checking (in Elab) for duplicate cases.
Note that C2C ignores the recorded value and recomputes the value of
the expression using Ceval.integer_expr. This is intentional:
Ceval.integer_expr is more trustworthy, as it is formally verified
against the CompCert C semantics.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
Adds a warning when a volatile struct is assigned to another
struct, that the volatile qualifier is ignored in this context.
Example:
```
volatile struct S s;
struct S t;
t = s; // did not warn before; now it warns
s = t; // did warn already
```
Bug 23489
|
|
|
|
|
| |
Init_space has an argument of type Z and it can exceed the range of a 32-bit integer.
Reported by Frédéric Besson.
|
|
|
|
|
|
| |
This will soon be deprecated by Coq.
Manual merge of pull request #224 by vbgl. Closes: #224
|
|
|
|
|
|
|
|
| |
The checks on the argument and format arguments are now performed
during C2C translation by calling the validate_ais_annotations
function and result in an error instead of a warning in the
backend to be more consistent with the rest of the builtin
functions.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
The ais annotations are now handled in a separate file shared
between all architectures. Also two different variants of
replacements are supported, %e which expands to ais expressions
and %l which also expands to an ais expression but is guaranted to
be usable as l-value in the ais annotation. Otherwise the new
warning is Wrong_is_parameter is generated.
Also an error message is generated if floating point variables are
used in ais annotations since a3 does not support them at the
moment.
Additionally an error message is generated for plain volatile
variables used, since they will enforce a volatile load and result
in the value being passed to the annotation instead of the address
as other global variables.
|
|
|
|
|
|
|
|
|
|
| |
The size (number of elements) of an array type is represented as an OCaml int64 in the parse tree, and as a Coq Z in the CompCert C AST. However, the C2C.convertInt function used to do this conversion produces a Coq int (32 bits) type, taking the array size modulo 2^32. This is not correct, esp. on a 64-bit target.
This commit refactors C2C around three integer conversion functions:
convertInt32 producing a Coq "int" (32 bit)
convertInt64 producing a Coq "int64" (64 bit)
convertIntZ producing a Coq "Z" (arbitrary precision)
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
* Module Cerrors is now called Diagnostic and can be used in parts of CompCert other than cparser/
* Replaced eprintf error. Instead of having eprintf msg; exit 2 use the functions from the
Diagnostics module.
* Raise on error before calling external tools.
* Added diagnostics to clightgen.
* Fix error handling of AsmToJson.
* Cleanup error handling of Elab and C2C.
*The implementation of location printing (file & line) is simplified and correctly prints valid filenames with invalid lines.
|
| |
|
| |
|
|
|
|
|
|
| |
Instead of two Boolean tests C2C.atom_is_{no,}inline, have a single
C2C.atom_inline function that returns one of the three possible values
stored in the the a_inline field.
|
|
|
|
|
|
|
| |
In order to correctly support the noinline attribute we must store
whether the function was specified with an inline specifer, had
a noinline attribute or nothing.
Bug 22642
|
|
|
|
| |
So that it looks more like valid C source.
|
| |
|
|
|
|
|
|
| |
The file and line information are now stored as comment string at
the start of each annotation.
Bug 22462
|
|\
| |
| |
| | |
Ensure FunInd or Recdef is imported if functional induction is used.
This is necessary for Coq 8.7.0.
|
| |
| |
| |
| |
| |
| | |
Coq 8.7 does not load FunInd in prelude anymore, so this is necessary.
Recdef exports FunInd, so if Recdef is imported, importing FunInd
is not required.
|
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
The ais annotations can be inserted via the new ais variants of
the builtin annotation. They mainly differe in that they have an
address format specifier '%addr' which will be replaced by the
adress in the binary.
The implementation simply prints a label for the builtin call
alongside a the text of the annotation as comment and inserts the
annotation together as acii string in a separate section
'ais_annotations' and replaces the usages of the address format
specifiers by the address of the label of the builtin call.
|
| | |
|
| |
| |
| |
| | |
Replace deprecated functions and theorems from the Coq standard library (version 8.6) by their non-deprecated counterparts.
|
|/
|
|
|
|
|
| |
The runtime functions are prefixed with compcert in order to
avoid potential clashes with runtime/builtin functions of other
compilers.
Bug 22062
|
|
|
|
|
|
| |
Fixes: Github issue #190.
Tint was used instead of the correct Tptr.
|
|
|
|
|
|
| |
Particularly annoying was the `*&x` sequence where `x` is a local variable, which would force stack-allocation of `x` early, generating extra loads and stores that could not always be optimized later (in CSE and Deadcode).
The `*&` sequences and, by symmetry, the `&*` sequences are now eliminated early during Clight generation, via smart constructors.
|
|
|
|
|
|
|
|
|
| |
ISO C99 states that "inline defintions", functions with inline
specifier that are not extern, does not provide an external
definition and another compilation unit can contain an external
definition. Thus in the case of non-static inline functions no
code should be generated.
Bug 21343
|
| |
|
|
|
|
| |
The noinline attribute prevents functions from inlining.
|
|
|
|
|
|
|
|
|
| |
The attribute unused can be used to indicate if a variable or
parameter is unused and no warning should be emitted for it.
Furthermore this commit simplifies the check by adding a generic
function to traverse the program.
Bug 19872
|
|
|
|
|
| |
This silences a warning of Coq 8.6.
Some "Implicit Arguments" remain in flocq/ but I'd rather not diverge from the released version of flocq if at all possible.
|
|
|
|
|
| |
Open Local becomes Local Open. This silences Coq 8.6's warning.
Also: remove one useless Require-inside-a-module that caused another warning.
|
|\
| |
| |
| | |
maximedenes-coq-8.6
|
| | |
|
| |
| |
| |
| | |
Not sure why, but it would be safer not to rely on automatic naming.
|
| | |
|
| |
| |
| |
| | |
I really like to have Floats and Values opened. The other opens I can live without, but Floats.Float.zero is just wrong.
|
|\ \ |
|
| | |
| | |
| | |
| | |
| | | |
- Mark the "noreturn" attribute as related to function types, so that it is correctly attached to the nearest enclosing function type.
- Add this attribute on functions declared / defined _Noreturn (with the C2011 keyword). The information is not used presently but could be useful later.
|
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
Introduce Cutil.class_of_attribute to return the class of the given attribute: one among
Attr_type attribute related to types (e.g. "aligned")
Attr_struct attribute related to struct/union/enum types (e.g. "packed")
Attr_function attribute related to function types (e.g. "noreturn")
Attr_name attribute related to variable and function declarations (e.g. "section")
Attr_unknown attribute was not declared
Cutil.declare_attribute is used to associate a class to a custom attribute.
Standard attributes (const, volatile, _Alignas, etc) are Attr_type.
cfronted/C2C.ml: declare the few attributes that CompCert honors currently.
cparser/GCC.ml: a bigger list of attributes taken from GCC, for reference only.
|
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
The treatment of attributes in the current CompCert is often surprising. For example,
attribute(xxx) char * x;
is parsed as "x is a pointer to a (char modified by attribute "xxx")", while for most attributes (e.g. section attributes) the expected meaning is "x, modified by attribute "xxx", has type pointer to char".
CompCert's current treatment comes from the fact that attributes are processed very much like the standard type modifiers `const` and `volatile`, i.e.
const char * x;
is really "x is a pointer to a const char", not "x is a const pointer to char".
This experiment introduces a distinction between type-related attributes (which include the standard modifiers `const` and `volatile`) and other attributes. The other, non-type-related attributes are "floated up" during elaboration so that they apply to the variable or function being declared or defined. In the examples above,
attribute(xxx) char * x; // "attribute(xxx)" applies to "x"
const char * x; // "const" applies to "char"
This may be a step in the right direction but is not the final story. In particular, the `packed` attribute is special-cased when applied to `struct`, like it was before, and future attributes concerning calling conventions would need to be floated up to function types but not higher than that.
|
| | | |
|
| | |
| | |
| | |
| | | |
The clashing identifiers are now referenced explicitly.
|
|/ / |
|
|/
|
|
|
|
|
| |
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
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
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.)
|
| |
|
| |
|
| |
|
|\
| |
| |
| | |
Support for 64-bit target processors + support for x86 in 64-bit mode
|
| |
| |
| |
| |
| |
| | |
During the experiments, the integer + pointer cases was removed from the semantics of the C addition operator. The idea was to turn integer + pointer into pointer + integer during elaboration, but it was not implemented.
On second thoughts, we can restore the integer + pointer cases in the formal semantics of CompCert C at low cost. This is what this commit does.
|