| Commit message (Collapse) | Author | Age | Files | Lines |
|
|
|
|
|
| |
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/
|
|/ |
|
|
|
|
| |
compatibility, and not "unsigned int", as previously implemented.
|
|
|
|
| |
The original code produces wrong results if res and al are the same register.
|
| |
|
| |
|
| |
|
|\
| |
| | |
Add "-conf <filename>" command-line option. Support relative paths for stdlib and tools.
|
| | |
|
| |
| |
| |
| |
| |
| | |
This option allows it to specify a .ini file that is in the usual
search path.
Bug 17431
|
| |
| |
| |
| |
| |
| |
| |
| | |
The tools now can be specified by 3 ways:
-Relative to the compcert.ini file
-With absolute path to the location
-As a simple filename which lies on the PATH variable.
Bug 17431
|