aboutsummaryrefslogtreecommitdiffstats
Commit message (Collapse)AuthorAgeFilesLines
...
* | | GPR#84: add missing IA32 operators to PrintOpXavier Leroy2016-03-151-0/+3
| | |
* | | Merge pull request #90 from AbsInt/sem-castsXavier Leroy2016-03-1114-323/+368
|\ \ \ | | | | | | | | Make casts of pointers to _Bool semantically well defined
| * | | Make casts of pointers to _Bool semantically well defined (again).Xavier Leroy2016-03-0214-323/+368
| | | | | | | | | | | | | | | | | | | | | | | | In compCert 2.5 the semantics of pointer comparisons against the NULL pointer was made more accurate by making it undefined if the pointer is invalid (outside bounds). Technical difficulties prevented this change from being propagated to the semantics of casts from pointer types to the _Bool type, which involves an implicit pointer comparison against NULL. Hence, this kind of casts was temporarily given undefined semantics. This commit makes pointer-to-_Bool casts semantically defined (again), provided the pointer is valid. This reinstates the equivalence between casts to _Bool and comparisons != 0. The technical difficulties mentioned above came from the translation of assignments in a value context in the SimplExpr pass. The pass was lightly modified to work around the issue.
* | | | Merge branch 'relaxed-pointer-arithmetic'Bernhard Schommer2016-03-111-6/+21
|\ \ \ \ | |_|_|/ |/| | |
| * | | Relaxing the semantics of pointer arithmetic.Xavier Leroy2016-02-291-6/+21
| | | | | | | | | | | | | | | | | | | | | | | | 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.
* | | | Fixed typo in equal types.Bernhard Schommer2016-03-101-1/+1
| |_|/ |/| | | | | | | | | | | | | | Compare the underlying array types, otherwise we end up in a endless recursion. Bug 18374
* | | Added more support for gcc options.Bernhard Schommer2016-03-021-4/+75
| |/ |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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
* | Merge remote-tracking branch 'origin/configuration-split'Bernhard Schommer2016-02-293-23/+58
|\ \
| * | Split up tools and options.Bernhard Schommer2016-02-253-23/+58
| | | | | | | | | | | | | | | | | | 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.
* | | Added gcc's Xassembler option.Bernhard Schommer2016-02-291-3/+8
| | | | | | | | | | | | | | | | | | | | | 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
* | | Fixed typo. Bug 18066Bernhard Schommer2016-02-291-3/+4
| | |
* | | Added some gcc linker options.Bernhard Schommer2016-02-261-0/+22
|/ / | | | | | | | | | | | | | | | | | | | | CompCert now recognizes the gcc linker options: -nostartfiles -nodefaultlibs -nostdlib -s -Xlinker <opt> -u <symb> Bug 18066.
* | bug 18168, catch cases where variadic arguments are transfered via registersMichael Schmidt2016-02-241-2/+2
| |
* | bug 18168, fix offset computation for var-args in ARM stacklayoutMichael Schmidt2016-02-241-1/+1
| |
* | bug 18209, make message compatible to clangMichael Schmidt2016-02-231-1/+1
| |
* | bug 18209, check that input files existMichael Schmidt2016-02-231-0/+14
|/
* PR#87: include the BSD license in the LICENSE file.Xavier Leroy2016-02-191-1/+28
|
* Do not use "movs rd, rs" nor "movs rd, #imm" in Thumb2 mode.Xavier Leroy2016-02-181-2/+8
| | | | | | | | | | | 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.
* Added new option for static linking.Bernhard Schommer2016-02-161-0/+2
| | | | | The new option -static passes the -static flag to the linker. Bug 18066.
* Fixed regression introduced by refactoring of Driver.ml.Bernhard Schommer2016-02-151-3/+7
|
* Merge pull request #86 from AbsInt/clightgen-improvedBernhard Schommer2016-02-054-90/+114
|\ | | | | Better treatment of names in the clightgen tool
| * Naming of compiler-generated temporariesXavier Leroy2016-02-051-32/+76
| | | | | | | | 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.
| * Restart the name generator at first_unused_ident for every function.Xavier Leroy2016-02-053-58/+38
|/ | | | This makes it easier to generate semi-meaningful names for compiler-generated temporaries in the clightgen tool.
* Also print braces around the registers.Bernhard Schommer2016-02-041-2/+7
|
* Fixed missing \" in json printing for registers.Bernhard Schommer2016-02-041-2/+2
|
* Added gcc cmd-line option -include.Bernhard Schommer2016-02-031-0/+3
| | | | | | | 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.
* Merge pull request #85 from AbsInt/option_jsonXavier Leroy2016-02-024-107/+299
|\ | | | | | | Flag -doptions to save machine configuration and command-line flags to a JSON file.
| * Added version and compiler working directory to options dump.Bernhard Schommer2016-01-271-0/+4
| |
| * Added new option -doptions.Bernhard Schommer2016-01-272-4/+58
| | | | | | | | | | | | The new options dumps the compiler options in a json file per. This includes the clflags, compcert.ini and machine settings. Bug 17988.
| * Added printer for Configuration and finished Clflags.Bernhard Schommer2016-01-255-135/+201
| |
| * Started implementing a printer for Clflags.Bernhard Schommer2016-01-254-12/+80
| |
* | Make void always incomplete and exit on void members.Bernhard Schommer2016-02-022-2/+8
| | | | | | | | | | | | Since we cannot construct a default initializer for void types we need to exit earlier. Bug 18004.
* | Do test for wrap around on singed ocaml integers.Bernhard Schommer2016-01-281-1/+1
| | | | | | | | | | | | 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.
* | Allow adding of attributes in valid_assignment_attr.Bernhard Schommer2016-01-281-2/+2
|/ | | | | Implementing the same behavior as gcc anc clang. Bug 18004
* Added option to dump preprocessed source code.Bernhard Schommer2016-01-222-4/+13
| | | | The new option -dprepro allows it to keep the preprocessed source code files.
* Added warning for strict-sequences.Bernhard Schommer2016-01-211-1/+1
|
* Include fix for wint_t gcc problem.Bernhard Schommer2016-01-211-12/+16
| | | | | | 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.
* Removed the last remains of cchecklink.Bernhard Schommer2016-01-211-2/+0
|
* More unique debug types.Bernhard Schommer2016-01-143-26/+26
| | | | | | 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.
* More descriptive error message for failed command.Bernhard Schommer2016-01-111-4/+14
| | | | | | | 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
* Added configuration to enable clightgen build.Bernhard Schommer2015-12-282-10/+14
| | | | The new configuration option -clightgen activates the build of clightgen.
* Merge branch 'master' of ↵Bernhard Schommer2015-12-281-2/+4
|\ | | | | | | ssh://ssh.absint.com/common/repositories/git/tools/compcert
| * add options for include paths also to the command line of the assembler, bug ↵Michael Schmidt2015-12-231-2/+4
| | | | | | | | 17838
* | ARM: bug in expansion of __builtin_clzllXavier Leroy2015-12-221-1/+1
| | | | | | | | Follow-up to commit f531d38
* | Add CLZ builtins for ARM and IA32Xavier Leroy2015-12-2210-7/+68
| | | | | | | | | | | | | | ARM: add __builtin_clzl, __builtin_clzll IA32: add __builtin_clzl, __builtin_clzll, __builtin_ctzl, __builtin_ctzll Add corresponding tests in tests/regression/
* | Upgrade for release 2.6.Xavier Leroy2015-12-211-1/+8
|/
* The return type of __builtin_clz() et al is "int", as documented and for GCC ↵v2.6Xavier Leroy2015-12-214-6/+8
| | | | compatibility, and not "unsigned int", as previously implemented.
* powerpc/Asmexpand: fix expansion of __builtin_clzllXavier Leroy2015-12-201-2/+2
| | | | The original code produces wrong results if res and al are the same register.
* clightgen: update to recent change -fstruct-return/-fstruct-passingXavier Leroy2015-12-191-4/+7
|
* Update VERSION for release 2.6Xavier Leroy2015-12-191-2/+2
|
generated by cgit (git 2.34.1) at 2024-07-04 23:37:28 +0000