aboutsummaryrefslogtreecommitdiffstats
Commit message (Expand)AuthorAgeFilesLines
* Also check statement of label statement.Bernhard Schommer2018-04-271-1/+2
* Detect duplicate 'case' or 'default' statements within a 'switch'Xavier Leroy2018-04-271-0/+41
* Record value of constant expression in C.Scase constructorXavier Leroy2018-04-276-10/+10
* Detect 'case' and 'default' outside a 'switch' statementXavier Leroy2018-04-271-1/+7
* Additional checks on typedefs (#101)Bernhard Schommer2018-04-261-0/+4
* Earlier, more comprehensive check for constant initializers (#88)Xavier Leroy2018-04-263-4/+99
* Check for enums that have the same tag as composites (#100)Bernhard Schommer2018-04-251-1/+8
* Add diagnostic for illegal use of void (Bug 23342)Michael Schmidt2018-04-251-0/+2
* Initialization of anonymous bit-fields in structsXavier Leroy2018-04-252-1/+21
* Bitfields transformation: record the fields after transformationXavier Leroy2018-04-251-4/+20
* Initialization of union bit fieldsXavier Leroy2018-04-253-3/+45
* Bug 23346, Bug 23406Bernhard Schommer2018-04-250-0/+0
* Improved handling and diagnostics for the `auto` storage class (#99)Xavier Leroy2018-04-254-26/+52
* Use "fix <name> <number>" instead of "fix <number>"Xavier Leroy2018-04-251-8/+8
* Support Coq version 8.8.0Xavier Leroy2018-04-251-3/+3
* Upgrade Flocq to version 2.6.1 from upstream (#71)Xavier Leroy2018-04-258-171/+423
* Accept empty enum declaration after nonempty enum definition (#87)Bernhard Schommer2018-04-221-1/+1
* Better check for incomplete types in pointer subtraction (#92)Bernhard Schommer2018-04-201-0/+1
* Warn when volatile struct is assigned to a normal structBernhard Schommer2018-04-191-0/+3
* Function defintions: keep the attributes from previous declarations (#89)Bernhard Schommer2018-04-191-1/+3
* Bug 23410Bernhard Schommer2018-04-110-0/+0
* Revert "preserve static initialized variables (#81)"Xavier Leroy2018-04-101-9/+2
* Check for redefinition of globals and preserve static initialized variables (...Bernhard Schommer2018-04-092-6/+33
* Reject illegal initializations of aggregates at top-level (#79)Xavier Leroy2018-04-061-1/+10
* Define C11 conditional feature macros (#77)Bernhard Schommer2018-04-061-1/+10
* Allow declaration of composites in bitfield size.Bernhard Schommer2018-04-051-11/+20
* Error for subtraction arithmetic type - pointer type (#73)Bernhard Schommer2018-04-051-3/+0
* Bug 23327Bernhard Schommer2018-04-030-0/+0
* Turn delicate case of designated re-initialization into error (#70)Xavier Leroy2018-03-303-38/+62
* Reject casts to struct/union types (#68)Bernhard Schommer2018-03-291-3/+0
* Don't overwrite initializer of anonymous union member. (#69)Bernhard Schommer2018-03-291-1/+1
* Fix 23332Bernhard Schommer2018-03-280-0/+0
* Change Implicit Arguments to Arguments (#225)Jasper Hugunin2018-03-285-17/+14
* Sizeof and _Alignof are not allowed on bit-fields (#67)Bernhard Schommer2018-03-273-1/+17
* Bug 23320Bernhard Schommer2018-03-270-0/+0
* Fix mistake in Bitfield transformation (#66)Michael Schmidt2018-03-271-2/+2
* Arrays should decay to pointers (#65)Bernhard Schommer2018-03-271-2/+3
* Improve error messages for anonymous bit-fields (#64)Bernhard Schommer2018-03-231-7/+10
* Do not allow inline on main and warn for Noreturn (#63)Bernhard Schommer2018-03-231-0/+4
* Add newline directly on list in annot.Bernhard Schommer2018-03-132-4/+7
* Anchor patterns to the top-level directory when appropriateXavier Leroy2018-03-131-47/+47
* Print size argument of Init_space as Z not as int32Xavier Leroy2018-03-133-3/+3
* Introduce more brackets for register annotation.Bernhard Schommer2018-03-121-4/+5
* Removed deprecated lemma.Bernhard Schommer2018-03-121-1/+1
* Do not use "Require" inside sections (#224)Xavier Leroy2018-03-122-5/+2
* Added seperator in warning msg. Bug 23179Bernhard Schommer2018-03-091-1/+1
* StructPassing and annotations, continuedXavier Leroy2018-03-091-9/+7
* Do not transfer arguments for annotations.Bernhard Schommer2018-03-091-2/+5
* Add explicit interface to cparser/pre_parser_aux.mlXavier Leroy2018-03-092-5/+28
* StructPassing: do not transform arguments to annotation built-insXavier Leroy2018-03-091-2/+6