| Commit message (Collapse) | Author | Age | Files | Lines |
|
|
|
|
|
| |
Support <pointer> +/- <integer> where the pointer value is actually an integer (Vint) that has been converted to pointer type.
Such arithmetic, while not defined in ISO C, appears in the wild. If present in static initializers, it used to cause a compile-time failure ("not a compile-time constant"). Hence this relaxation.
|
| |
|
|
|
|
|
|
|
|
|
|
|
| |
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
|
| |
| |
| |
| |
| |
| | |
The path to the libcompert folder can be specified relative to the
location of the compcert.ini file.
Bug 17431
|
| |
| |
| |
| |
| |
| | |
Libcompcert was defined in thumb mode for armv7r but it should be
compild in thumb mode for armv7m.
Bug 17808.
|
| |
| |
| |
| |
| |
| | |
The C standard specifies that an enum type should be compatible
to some integer type (ISO/IEC 9899:TC3 §6.7.2.2p4).
Fix 16692
|
|\ \ |
|
| | | |
|
| | | |
|
| | | |
|
|/ /
| |
| |
| |
| | |
The binutils in bsd seem to support cfi directives but not the
cfi_sections directive.
|
| |
| |
| |
| |
| |
| | |
On older version of the binutils the cfi directives are not always
supported so we only print cfi_sections if the corresponding .ini
setting is set to true.
|
| | |
|