aboutsummaryrefslogtreecommitdiffstats
Commit message (Collapse)AuthorAgeFilesLines
* Make unnamed default + correct empty struct warning. Bug 18004Bernhard Schommer2016-09-212-2/+3
|
* Allow empty alignment attribute. Bug 18004Bernhard Schommer2016-09-211-0/+1
|
* Remove the duplicated :. Bug 18004Bernhard Schommer2016-09-211-3/+3
|
* Ignore also ignores the argunment. Bug 18004Bernhard Schommer2016-09-202-2/+7
|
* Merge pull request #139 from AbsInt/advanced-diagnosticsBernhard Schommer2016-09-2021-395/+781
|\ | | | | Advanced diagnostics
| * Fixed typos and reverted error message. Bug 18004Bernhard Schommer2016-09-051-9/+9
| |
| * Readded parameter number. Bug 18004Bernhard Schommer2016-09-011-6/+6
| |
| * Reworded warning. Bug 18004Bernhard Schommer2016-09-011-6/+6
| |
| * Simplified int to pointer tests.Bernhard Schommer2016-09-012-16/+17
| | | | | | | | | | | | Now the same warning is triggered for both cases, int to ptr and ptr to int. Bug 18004
| * Fixed error message for & operator. Bug 18004Bernhard Schommer2016-08-311-1/+1
| |
| * Added conformance warning.Bernhard Schommer2016-08-313-0/+4
| | | | | | | | | | | | This warning should be triggered if a feature is used that is not part of the code CompCert C language. Bug 18004
| * Added back logical operator in error. Bug 18004Bernhard Schommer2016-08-311-1/+1
| |
| * Reworded errors/warnings in Elab.Bernhard Schommer2016-08-311-60/+76
| | | | | | | | | | | | | | | | Some old errors/warnings messages were better before and are now rephrased. Furthermore some formulations are rephrased to match the used formulations of the ISO C stanard, e.g. storage class is replaced with storage-class. Bug 18004
| * Restored original bit-field warning. Bug 18004Bernhard Schommer2016-08-311-1/+1
| |
| * Updated comment string. Bug 18004.Bernhard Schommer2016-08-312-3/+3
| |
| * Readded warning about ignored volatile. Bug 18004Bernhard Schommer2016-08-311-1/+1
| |
| * Added missing literal. Bug 18004Bernhard Schommer2016-08-311-1/+1
| |
| * 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.
generated by cgit (git 2.34.1) at 2024-07-08 03:08:21 +0000