aboutsummaryrefslogtreecommitdiffstats
Commit message (Collapse)AuthorAgeFilesLines
...
| * | Fixed typos.Bernhard Schommer2016-08-311-8/+8
| | | | | | | | | | | | | | | | | | Removed duplicated of, changed string to string literal for wording than the C standard. Bug 18004
| * | bug 18004, fix some typos/grammarMichael Schmidt2016-08-301-1/+1
| | |
| * | bug 18004, fix some typos/grammarMichael Schmidt2016-08-301-4/+4
| | |
| * | Fixed types in Elab.ml. Bug 18004Bernhard Schommer2016-08-291-5/+5
| | |
| * | Merge branch 'master' into advanced-diagnosticsBernhard Schommer2016-08-291-8/+18
| |\ \
| * \ \ Merge branch 'master' into advanced-diagnosticsBernhard Schommer2016-08-2956-577/+1051
| |\ \ \
| * | | | Added raw printing of types without formatting.Bernhard Schommer2016-08-163-5/+11
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This avoids introducing line breaks during printing of function types. Bug 18004
| * | | | Additional test for color output.Bernhard Schommer2016-08-056-75/+102
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Color output is only enabled if stderr is a tty, and the environment variable TERM is not empty or dumb. Bug 18004
| * | | | Classified all warnings and added various options.Bernhard Schommer2016-07-2916-358/+690
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Now each warning either has a name and can be turned on/off, made into an error,etc. or is a warning that always will be triggered. The message of the warnings are similar to the ones emited by gcc/clang and all fit into one line. Furthermore the diagnostics are now colored if colored output is available. Bug 18004
* | | | | IA32: model integer division and modulus closer to the machineXavier Leroy2016-09-185-50/+187
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | lib/Integers.v: define division-remainder of a double word by a word ia32/Asm.v: use it to give Pdiv and Pidiv their "true" semantics like in the processor; add Pcltd as an instruction ia32/*: adapt accordingly Additional benefit: Pcltd could be used for an alternate implementation of shrximm.
* | | | | Enrich Decidableplus and use it to simplify Cexec.do_ef_memcpyXavier Leroy2016-09-173-31/+39
| | | | | | | | | | | | | | | | | | | | Inline directives in extraction.v make the Caml output efficient and almost nice.
* | | | | Decidableplus: remove stuff that was cut-and-paste from Coq 8.5 libraryXavier Leroy2016-09-171-48/+1
| | | | | | | | | | | | | | | | | | | | The cut-and-paste was for compatibility with Coq 8.4
* | | | | Added option to specify sdump folder. Fix 19816.Bernhard Schommer2016-09-161-2/+7
| | | | |
* | | | | improve fixup code (bug 19792)Michael Schmidt2016-09-151-0/+2
| | | | |
* | | | | Add interference for indirect calls.Bernhard Schommer2016-09-155-6/+22
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Avoids problems with overwritting the registe containing the function address. Bug 19779
* | | | | Add missing fixup-code for ARM EABI (bug 19792)Michael Schmidt2016-09-141-2/+0
| | | | |
* | | | | add missing print operatorMichael Schmidt2016-09-141-0/+1
| | | | |
* | | | | Removed some implict arguments.Bernhard Schommer2016-09-053-33/+14
| |_|/ / |/| | | | | | | | | | | Also changed Local Open to Open Local.
* | | | Pass the environment of k&r param elaboration.Bernhard Schommer2016-08-291-8/+10
| | | | | | | | | | | | | | | | | | | | | | | | The environment where the types are inserted is passed back to allow introducing structs in k&r parameters. Bug 19668
* | | | Fixed spelling mistake and unnamed fields.Bernhard Schommer2016-08-291-3/+6
| | | | | | | | | | | | | | | | | | | | | | | | The previous fix for duplicated members was also triggered for unnamed members. Bug 19665
* | | | Added check for duplicated members. Bug 19665Bernhard Schommer2016-08-291-0/+5
| |/ / |/| |
* | | Use old scope in after parameter parsing.Bernhard Schommer2016-08-261-1/+1
| | | | | | | | | | | | | | | | | | Not decrementing the scopes again after a parameter parsing lead to other scoping problems. Bug 19656.
* | | Reuse types from parameters in function definitonsBernhard Schommer2016-08-253-41/+47
| | | | | | | | | | | | | | | | | | In order to allow introducing structs in parameter definitions the environment must keep the type information. Bug 19602
* | | Test if struct is redefined as union or otherwise.Bernhard Schommer2016-08-251-0/+2
| | | | | | | | | | | | | | | | | | If a declaration of a composite is encountered it is also tested if the kind is equal. Bug 19630.
* | | Simplify test. Bug 19629Bernhard Schommer2016-08-251-4/+1
| | |
* | | Test for illegal first argument in __builtin_debug.Bernhard Schommer2016-08-251-2/+6
| | | | | | | | | | | | | | | | | | | | | The test is extended for integer constants smaller than 0. Also the default constant used for the error is no longer 0 since this is not a positive number. Bug 19629
* | | Merge pull request #118 from AbsInt/armebXavier Leroy2016-08-2437-471/+657
|\ \ \ | | | | | | | | Support for ARM Big Endian
| * \ \ fix merge conflictsMichael Schmidt2016-08-1717-15/+235
| |\ \ \
| * | | | update help text in configure scriptMichael Schmidt2016-08-081-13/+14
| | | | |
| * | | | port fix for configure from m-schmidt/EndiannessPlaygroundMichael Schmidt2016-08-071-0/+5
| | | | |
| * | | | Changed configure target for arm big endian.Bernhard Schommer2016-08-051-27/+12
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Instead of an addition -little or -big at the end the configure script now accepts armeb* for the big endian arm targets. Bug 19418
| * | | | Implement support for big endian arm targets.Bernhard Schommer2016-08-0537-472/+667
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Adds support for the big endian arm targets by making the target endianess flag configurable, adding support for the big endian calling conventions, rewriting memory access patterns and adding big endian versions of the runtime functions. Bug 19418
* | | | | PR#113, PR#122: Unspillable temporaries causing register allocation to failXavier Leroy2016-08-241-1/+6
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The spilling strategy for 2-address operations was strange in the case where the first argument needs spilling but not (yet) the result: a Xreload instruction was generated which prevented future spilling of the result. Fixed by generating Xmove instead of Xreload in this case.
* | | | | Print prototypes for malloc and free.Bernhard Schommer2016-08-231-1/+1
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The declarations of malloc and free should also be printed for CompCert C. Bug 19616.
* | | | | Fix for initialization of incomplete typesBernhard Schommer2016-08-233-5/+8
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Since some incomplete types are allowed in initialization just test whether the default initilization exists. Bug 19601
* | | | | Added types found in cast to Environment.Bernhard Schommer2016-08-231-2/+2
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | New types introduced in casts are now inserted into the right Environment and carried along. Bug 19614.
* | | | | Revert "Reuse env from during parameter elaboration."Bernhard Schommer2016-08-231-4/+4
| | | | | | | | | | | | | | | | | | | | This reverts commit c64c4ab2526ad87a3506c9e1fdf31fa1446c16eb.
* | | | | Reuse env from during parameter elaboration.Bernhard Schommer2016-08-221-4/+4
| | | | | | | | | | | | | | | | | | | | | | | | | Allows adding struct definitions in function parameters. Bug 19602.
* | | | | Better error message for function initializerBernhard Schommer2016-08-221-0/+4
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Initializers for function variables are not allowed. CompCert now reports an error and exits. Bug 19606
* | | | | Also print declarations in CompCert C.Bernhard Schommer2016-08-221-0/+20
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The PrintCsyntax now first emits declarations for all functions and variables in order to allow foward declarations. Bug 19598.
* | | | | Print whole command line.Bernhard Schommer2016-08-221-8/+8
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | When response files are used CompCert should still print all command line arguments since the response file is deleted after usage. Bug 19297.
* | | | | Test for incomplete type during initialization.Bernhard Schommer2016-08-221-1/+6
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Before the initializazion is computed we check wether the type is incomplete. Bug 19601
* | | | | Error for va_start in non-vararg function.Bernhard Schommer2016-08-221-27/+31
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | CompCert now reports an error for usage of the va_start macro in non variadic functions. Bug 19600.
* | | | | Added missing , in PrintCsyntax. Bug 19599Bernhard Schommer2016-08-221-1/+1
| | | | |
* | | | | Added check for incomplete parameter types.Bernhard Schommer2016-08-201-1/+5
| | | | | | | | | | | | | | | | | | | | | | | | | Parameters also need to be checked for incomplete types. Bug 19596
* | | | | Exit earlier on invalid alignof and sizeof.Bernhard Schommer2016-08-191-4/+4
| |_|_|/ |/| | | | | | | | | | | | | | | | | | | Alginof and sizeof applied to incomplete types now exit earlier with a fatal error. Bug 19594.
* | | | Disallow void as type for variables.Bernhard Schommer2016-08-181-0/+2
| |/ / |/| | | | | | | | | | | | | | This allows problems in elaboration of the initializers for variables of void type. Bug 19577.
* | | Exit earlier on empty union.Bernhard Schommer2016-08-171-1/+5
| | | | | | | | | | | | | | | | | | | | | Instead of a warning for an empty union CompCert reports an error and exits. This avoids problems during the generation of initializers for these. Bug 19565.
* | | Merge pull request #107 from AbsInt/add-fileXavier Leroy2016-08-1712-10/+219
|\ \ \ | | | | | | | | Add support for response files
| * | | Moved quoting functions in ResponsefileBernhard Schommer2016-08-165-36/+44
| | | | | | | | | | | | | | | | | | | | | | | | Also corrected some typos and corrected exception handling for expandargv. Bug 18308