| Commit message (Collapse) | Author | Age | Files | Lines |
|
|
|
|
|
| |
The code was mostly there for documentation effort. So warning
27 is deactivated again.
Bug 18349
|
|
|
|
|
|
| |
Since the invariant checks are not currently used and they are not
exported they are renamed to include a _ to avoid warning.
Bug 18394
|
|
|
|
| |
This reverts commit bac2a0854ea51217690bc6f225da62053ed7ac06.
|
|
|
|
|
|
| |
The ofs parameter is no longer used. Adopted the proofs and ml
code using it.
Bug 18394
|
|
|
|
|
| |
Removed unused code and code generating warnings.
Bug 18394
|
|
|
|
|
| |
Removed some unused functions and opens.
Bug 18394
|
|
|
|
|
| |
Removed unused functions and avoid warnings.
Bug 18394.
|
|
|
|
|
|
|
|
|
|
|
| |
Since the menhir version we use requires ocaml>4.02 we can also
upgrade the required ocaml version to >4.02 and remove the
deprecate String functions.
Also we now activate all warnings except for 4,9 und 27 for regular
code plus a bunch of warnings for the generated code. 4 and 9 are
not really usefull and 27 is deactivated since until the usage
string is printed in a way that requires no newline.
Bug 18394.
|
|
|
|
|
|
| |
Removed some unused variables, functions etc. and resolved some
problems which occur if all warnings except 3,4,9 and 29 are active.
Bug 18394.
|
|
|
|
|
|
| |
Compare the underlying array types, otherwise we end up in a
endless recursion.
Bug 18374
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
Added the gcc options for the preprocessor:
-Xpreprocessor
-M
-MM
-MF
-MG
-MP
-MT
-MQ
-nostdinc
-imacros
-idirafter
-isystem
-iquote
-P
-C
-CC
Also warn for not supported GCC options in the diab case.
Bug 18066
|
|\ |
|
| |
| |
| |
| |
| |
| | |
Added additional configuration entries to seperate tools from options in the
.ini files. Internally they are just concatenated in Configuration.ml which
allows it to still use old .ini files.
|
| |
| |
| |
| |
| |
| |
| | |
The Xassembler option passes one option to the assembler and can
be used to pass options to the underlying assembler that the gcc
driver does not recognize.
Bug 18066
|
| | |
|
|/
|
|
|
|
|
|
|
|
|
| |
CompCert now recognizes the gcc linker options:
-nostartfiles
-nodefaultlibs
-nostdlib
-s
-Xlinker <opt>
-u <symb>
Bug 18066.
|
| |
|
| |
|
| |
|
| |
|
| |
|
|
|
|
|
|
|
|
|
|
|
| |
Two reasons:
- The movs is not supported if rd or rs is r13 (the stack ptr register).
Newer versions of GNU as reject it, older versions were probably
emulating it.
- The purpose of setting the "s" flag on some operations is to
enable 16-bit encoding in Thumb2 mode. However, for "mov"
it is the non-s form that has a 16-bit encoding; the s form
is never more compact.
|
|
|
|
|
| |
The new option -static passes the -static flag to the linker.
Bug 18066.
|
| |
|
|\
| |
| | |
Better treatment of names in the clightgen tool
|
| |
| |
| |
| | |
clightgen now gives semi-readable and relatively stable names of the form _t'1, _t'2, _t'3, etc, to compiler-generated temporaries, instead of the unreadable and unstable NNN%positive notation generated previously.
|
|/
|
|
| |
This makes it easier to generate semi-meaningful names for compiler-generated temporaries in the clightgen tool.
|
| |
|
| |
|
|
|
|
|
|
|
| |
The -include option is passed to the preprocessor and -include <file>
is equivalent to writting #include "<file>" as first line in the
primary source file.
Bug 18066.
|
|\
| |
| |
| | |
Flag -doptions to save machine configuration and command-line flags to a JSON file.
|
| | |
|
| |
| |
| |
| |
| |
| | |
The new options dumps the compiler options in a json file per.
This includes the clflags, compcert.ini and machine settings.
Bug 17988.
|
| | |
|
| | |
|
| |
| |
| |
| |
| |
| | |
Since we cannot construct a default initializer for void types
we need to exit earlier.
Bug 18004.
|
| |
| |
| |
| |
| |
| | |
In parse_int it was not tested if the value of v is smaller than
zero. This allowed it that certain large integers were accepted
due to wrap around.
|
|/
|
|
|
| |
Implementing the same behavior as gcc anc clang.
Bug 18004
|
|
|
|
| |
The new option -dprepro allows it to keep the preprocessed source code files.
|
| |
|
|
|
|
|
|
| |
Gcc defines wint_t in the stddef header (even if it is not stanadard) and
additionally defines it if stddef is reincluded. The fix now defines it
before stddef is checked for reinclusion.
|
| |
|
|
|
|
|
|
| |
The typdef, enumerator and function_type types form the DebugTypes and
DwarfTypes shared a some fields. This commits renames them in order to
make them more unique and avoid potential name clashes.
|
|
|
|
|
|
|
| |
CompCert now prints if the assembler, linker or preprocessor
command failed and a hint for the user to get the full command
line.
Bug 17894
|
|
|
|
| |
The new configuration option -clightgen activates the build of clightgen.
|
|\
| |
| |
| | |
ssh://ssh.absint.com/common/repositories/git/tools/compcert
|
| |
| |
| |
| | |
17838
|
| |
| |
| |
| | |
Follow-up to commit f531d38
|
| |
| |
| |
| |
| |
| |
| | |
ARM: add __builtin_clzl, __builtin_clzll
IA32: add __builtin_clzl, __builtin_clzll,
__builtin_ctzl, __builtin_ctzll
Add corresponding tests in tests/regression/
|
|/ |
|