aboutsummaryrefslogtreecommitdiffstats
path: root/cfrontend
Commit message (Collapse)AuthorAgeFilesLines
* In AST.calling_conventions, record whether the original C function was ↵Xavier Leroy2015-05-223-20/+24
| | | | | | "old-style" unprototyped. Use this info in printing function types for Csyntax and Clight.
* Missing case in type_conditional (long long vs. int or float).Xavier Leroy2015-05-221-6/+3
|
* Ctyping: better typing of conditional expressions.Xavier Leroy2015-05-213-50/+200
| | | | | | | | | | | | Ctyping: define a typechecker for whole programs. Csyntax: introduce the type "pre-program" (non-dependent). C2C: use Ctyping.econdition instead of Ctyping.econdition'. Note: Ctyping.typecheck_program could be used as the first step in the verified compilation pipeline. Then, retyping would no longer be performed in C2C. We keep it this way (for the time being) because retyping errors are reported more precisely in C2C than in Ctyping.
* Extended inline asm: revised treatment of clobbered registers.Xavier Leroy2015-05-092-3/+3
| | | | | | | | | | - Treat clobbered registers as being destroyed by EF_inline_asm builtins (which is the truth, semantically). - To enable the above, represent clobbers as Coq strings rather than idents and move register_by_name from Machregsaux.ml to Machregs.v. - Side benefit: more efficient implementation of Machregsaux.name_of_register. -# Please enter the commit message for your changes. Lines starting
* Long-overdue renaming: val_inject -> Val.inject, etc, for consistency with ↵Xavier Leroy2015-04-304-80/+80
| | | | Val.lessdef, etc.
* Warn if a nonzero FP literal converts to infinity (overflow) or to 0 ↵Xavier Leroy2015-04-251-3/+17
| | | | | | (underflow). Also: spurious '\n' in C2C.warning.
* Use Cerrors for error reporting instead of rolling our own reporting in C2C.Xavier Leroy2015-04-211-11/+5
|
* Printing of EF_inline_asm builtins in GCC extended asm syntax.Xavier Leroy2015-04-211-0/+30
|
* Support for GCC-style extended asm, continued:Xavier Leroy2015-04-212-81/+16
| | | | | | | | - support "r", "m" and "i" constraints - support "%Q" and "%R" modifiers for register pairs - support register clobbers - split off analysis and transformation of asm statements in cparser/ExtendedAsm.ml
* Experiment: support a subset of GCC's extended asm statements.Xavier Leroy2015-04-172-10/+101
|
* Merge pull request #34 from AbsInt/extended-annotationsXavier Leroy2015-04-012-5/+4
|\ | | | | Extended annotations
| * Updated the Caml part. Added some more tests in annot1.c.Xavier Leroy2015-03-271-2/+1
| |
| * Extended arguments to annotations, continued:Xavier Leroy2015-03-271-3/+3
| | | | | | | | | | - Simplifications in RTLgen. - Updated Cexec.
* | Merge pull request #31 from AbsInt/null-ptr-cmpXavier Leroy2015-04-0113-128/+182
|\ \ | | | | | | Revised semantics of comparisons between a pointer and 0.
| * | Omission: forgot to treat pointer values in bool_of_val and sem_notbool.Xavier Leroy2015-03-2912-120/+182
| | |
| * | Revised semantics of comparisons between a pointer and 0.Xavier Leroy2015-03-154-8/+0
| |/ | | | | | | | | | | | | | | | | | | | | It used to be that a pointer value (Vptr) always compare unequal to the null pointer (Vint Int.zero). However, this may not be true in the final machine code when pointer addition overflows and wraps around to the bit pattern 0. This patch checks the validity of the pointer being compared with 0, and makes the comparison undefined if the pointer is out of bounds. Note: only the IA32 back-end was updated, ARM and PowerPC need updating.
* | Fix overflows in printers for clight and csyntax.Jacques-Henri Jourdan2015-04-012-2/+2
| |
* | Support va_arg for vararg arguments of composite (struct/union) types.Xavier Leroy2015-03-201-13/+37
|/ | | | ARM is done, IA32 and PowerPC remain to be updated.
* Issue #28: if the arguments of __builtin_memcpy_aligned are arrays, their ↵Xavier Leroy2015-03-101-1/+3
| | | | types must decay to pointer types in the "types" part of Ebuiltin.
* Interpreter produces more detailed trace, including name of semantic rules used.Xavier Leroy2015-02-082-136/+165
| | | | | | Cexec: record names of rules used in every reduction. Interp: print these rule names in -trace mode. Also: simplified the exploration in "-all" mode; give unique names to states. Csem: fix name of reduction rule "red_call".
* Merge branch 'named-structs'Xavier Leroy2015-01-2321-1418/+3717
|\ | | | | | | | | | | | | | | | | | | | | | | | | - Switch CompCert C / Clight AST of composite types (structs and unions) from a structural representation to a nominal representation, closer to concrete syntax. - This avoids algorithmic inefficiencies due to the structural representation. - Closes PR#4. - Smallstep: make small-step semantics more polymorphic in the type of the global environment. - Globalenvs: introduce Senv.t (symbol environments) as a restricted view on Genv.t (full global environments). - Events, Smallstep: use Senv instead of Genv to talk about global names.
| * Define a nonnegative integer "rank" for types to support structural ↵Xavier Leroy2015-01-102-22/+120
| | | | | | | | induction over composite types.
| * Add a type system for CompCert C and type-checking constructor functions.Xavier Leroy2014-12-312-64/+2079
| | | | | | | | | | Use these constructor functions in C2C to rely less on the types produced by the unverified elaborator.
| * Represent struct and union types by name instead of by structure.Xavier Leroy2014-12-2220-1308/+1518
| |
| * Introduce symbol environments (type Senv.t) as a restricted view on global ↵Xavier Leroy2014-11-263-44/+20
| | | | | | | | environments (type Genv.t). Use symbol environments instead of global environments for external functions (module Events).
* | Delay reads from !Machine.config before it is properly initialized.Xavier Leroy2015-01-221-2/+2
| | | | | | | | | | | | | | | | | | | | | | | | | | Several definitions in Cutil and elsewhere were accessing the default value of !Machine.config, before it is properly initialized in Driver. Delay evaluation of these definitions, and initialize Machine.config to nonsensical values so that lack of initialization is caught early (e.g. in Cutil.find_matching_*_kind). Also, following up on commit [3b8a094], don't use "wchar_t" typedef to type wide string literals, even if this typedef is in scope. The risk here is to hide an inconsistency between "wchar_t"'s definition in standard headers and CompCert's built-in definition.
* | Protect against redefinition of the __i64_xxx helper library functions.Xavier Leroy2015-01-201-1/+54
| | | | | | | | | | | | | | | | | | | | This is achieved by declaring these functions in C2C.ml, then re-checking their declarations in the global environment during the Selection pass. In passing, the "hf" parameter for SelectLong functions was removed and replaced by fixed identifiers corresponding to the actual names of the helper functions.
* | PR#19: there is no reason to reject an empty "switch" statement.Xavier Leroy2015-01-061-2/+0
| |
* | PR#15: vararg functions are not eligible for inlining.Xavier Leroy2015-01-021-1/+1
| |
* | Translation of wide string literals.Xavier Leroy2015-01-011-6/+57
|/ | | | | | | Closes PR#13. Also: give string literals type unsigned char [] or signed char [] depending on the machine configuration. (Instead of unsigned char [] before.)
* Add Genv.public_symbol operation.Xavier Leroy2014-11-245-22/+51
| | | | | Restrict pointer event values to public global names. Update proofs accordingly. PowerPC and ARM need updating.
* Record public global definitions via field "prog_public" in AST.program.Xavier Leroy2014-11-243-59/+68
| | | | For the moment, this field is ignored.
* Revised translation of '&&' and '||' to Clight.Xavier Leroy2014-10-1310-123/+108
| | | | | | | | | | | The previous translation (in SimplExpr) produced references to the same temporary variable with two different types (bool and int), which is not nice if we want to typecheck the generated Clight. The new translation avoids this and also gets rid of the double cast to bool then to int. The trick is to change Eparen (in CompCert C expressions) to take two types: the type to which the argument must be converted, and the type with which the resulting expression is seen.
* Tolerance in parsing of 'section' pragmaxleroy2014-09-171-0/+3
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2623 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* More careful detection of inlined builtins. Produces better error messages ↵xleroy2014-08-251-0/+1
| | | | | | if an unsupported __builtin_xxx function is used by mistake. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2617 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Support C99 compound literals (by expansion in Unblock pass).xleroy2014-08-211-0/+2
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2615 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Issue with switch labels that are negative 32-bit integers.xleroy2014-08-171-4/+7
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2567 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* - Support "switch" statements over 64-bit integersxleroy2014-08-1715-57/+102
| | | | | | | | | | | | | (in CompCert C to Cminor, included) - Translation of "switch" to decision trees or jumptables made generic over the sizes of integers and moved to the Cminor->CminorSel pass instead of CminorSel->RTL as before. - CminorSel: add "exitexpr" to support the above. - ValueDomain: more precise analysis of comparisons against an integer literal. E.g. "x >=u 0" is always true. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2565 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* All targets: add __builtin_membarxleroy2014-07-281-0/+5
| | | | | | | ARM: add __builtin_dsb __builtin_isb git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2554 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Merge of "newspilling" branch:xleroy2014-07-2318-249/+460
| | | | | | | | | | | | | | | - Support single-precision floats as first-class values - Introduce chunks Many32, Many64 and types Tany32, Tany64 to support saving and restoring registers without knowing the exact types (int/single/float) of their contents, just their sizes. - Memory model: generalize the opaque encoding of pointers to apply to any value, not just pointers, if chunks Many32/Many64 are selected. - More properties of FP arithmetic proved. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2537 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Cleaner, more resilient parsing of pragmas.xleroy2014-06-051-55/+25
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2507 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* - Re-added support for "__func__" identifier as per ISO C99.xleroy2014-05-151-3/+7
| | | | | | | | - Support for empty structs and unions - Better handling of "extern" and "extern inline" function definitions. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2493 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Clean-up pass on C types:xleroy2014-04-234-91/+324
| | | | | | | | | | | | | - Ctypes: add useful functions on attributes; remove attrs in typeconv (because attributes are meaningless on r-values) - C2C: fixed missing or redundant Evalof - Cop: ignore attributes in ptr + int and ptr - int (meaningless on r-values); add sanity check between typeconv/classify_binarith and the C99 standard. - cparser: fixed several cases where incorrect type annotations were put on expressions. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2457 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Continued: change typeconv t into incrdecr_type t for Epostincr.xleroy2014-04-162-3/+3
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2456 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Use "incrdecr_type ty" instead of "typeconv ty" as the intermediate typexleroy2014-04-153-7/+18
| | | | | | | for Epostincr operations. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2455 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Constprop: use "not" for "xorimm(-1)"; optimize == 1 and != 0 comparisons ↵xleroy2014-04-091-7/+3
| | | | | | | | | | over booleans. Select*: more systematic constant propagation; don't CP shifts by amounts outside of [0..31]. Driver: timer for whole compilation. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2452 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* __builtin_absfloat can be applied to integers too.xleroy2014-03-293-22/+60
| | | | | | | | More precise classification of float results of arithmetic operations, in preparation for future work on the C/Clight static type system. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2441 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* C: Support array initializers that are too short + default init for remainder.xleroy2014-03-283-54/+47
| | | | | | | | Elab: Handle C99 designated initializers. C2C, Initializers: more precise intermediate AST for initializers. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2439 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Support array initialization lists that are too shortxleroy2014-03-182-6/+14
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2432 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Beautify the output.xleroy2014-02-211-3/+7
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2414 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
generated by cgit (git 2.34.1) at 2024-06-30 23:30:42 +0000