aboutsummaryrefslogtreecommitdiffstats
Commit message (Collapse)AuthorAgeFilesLines
* Revised semantics of comparisons between a pointer and 0.Xavier Leroy2015-03-159-31/+44
| | | | | | | | | | | 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.
* Missing initialization of current_function_sig.Xavier Leroy2015-03-143-3/+6
|
* 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.
* Merge pull request #21 from AbsInt/backend_printerXavier Leroy2015-03-1011-3167/+3116
|\ | | | | Re-factoring of the asm printers.
| * Merge branch 'master' into backend_printerBernhard Schommer2015-03-102-11/+12
| |\ | |/ |/|
* | Merge branch 'master' of https://github.com/AbsInt/CompCertXavier Leroy2015-03-071-4/+0
|\ \
| * | Removed unused target cleansource.Bernhard Schommer2015-03-051-4/+0
| | |
* | | Issue #26: problems with big escape sequences in string/char literals.Xavier Leroy2015-03-071-7/+12
|/ / | | | | | | | | | | - Error instead of warning if escape sequence overflows one character. - Wrong normalization of L'x' to char instead of wchar_t. - More careful overflow tests.
| * Merge branch 'master' into backend_printerBernhard Schommer2015-03-033-216/+7
| |\ | |/ |/|
* | Removed leftover references to recdepend.Xavier Leroy2015-02-281-6/+5
| |
* | Removed the recdepend again and replaced it by a builtin Make function.Bernhard Schommer2015-02-272-214/+6
| |
* | Removed the glob files from doc/ instead of doc/glob/Bernhard Schommer2015-02-261-1/+1
| |
| * Merge branch 'master' into backend_printerBernhard Schommer2015-02-2611-339/+646
| |\ | |/ |/| | | | | Conflicts: ia32/PrintAsm.ml
* | Updated the recdepend tool to avoid printing of ./ at the begining and ↵Bernhard Schommer2015-02-252-52/+50
| | | | | | | | printing duplicated -I flags.
* | Added a small ocamlfile that calls ocamlfind recursivly over a given directory.Bernhard Schommer2015-02-243-5/+218
| |
* | Merge github.com:AbsInt/CompCertBernhard Schommer2015-02-239-334/+430
|\ \
| * | Update clightgen with respect to new representation of composites.Xavier Leroy2015-02-203-232/+151
| | |
| * | Merge pull request #23 from AbsInt/no-shellXavier Leroy2015-02-206-102/+279
| |\ \ | | | | | | | | No Shell
| | * | Removed the Unix from the libraries for cchecklink.Bernhard Schommer2015-02-201-2/+3
| | | |
| | * | Merge branch 'no-shell' of github.com:AbsInt/CompCert into compcert_windowsBernhard Schommer2015-02-195-96/+272
| | |\ \
| | | * \ Merge branch 'master' into no-shellBernhard Schommer2015-02-1981-2496/+6257
| | | |\ \ | | |_|/ / | |/| | |
| | | * | Use Unix.create_process instead of Sys.command (continued).Xavier Leroy2014-12-293-96/+122
| | | | |
| | | * | Use Unix.create_process instead of Sys.command to run external tools.Xavier Leroy2014-12-192-0/+150
| | | | | | | | | | | | | | | | | | | | | | | | | Revised parsing of compcert.ini file to split arguments into words like POSIX shell does (including quotes).
| | * | | Merge github.com:AbsInt/CompCert into compcert_windowsBernhard Schommer2015-02-1966-2277/+5719
| | |\ \ \ | | |/ / / | |/| | |
| * | | | The parameter should also have the old name.Bernhard Schommer2015-02-191-3/+3
| | | | |
| | * | | Removed the linker flag again.Bernhard Schommer2015-01-202-4/+4
| | | | |
* | | | | Removed the MinGW port.Bernhard Schommer2015-02-191-53/+3
| | | | |
* | | | | Merge github.com:AbsInt/CompCertBernhard Schommer2015-02-1919-15/+935
|\| | | |
* | | | | Use lcomm instead of .local for Mingw.Bernhard Schommer2015-02-101-2/+2
| | | | |
* | | | | Added new Mingw Printer. Currently the only difference to the Cygwin printer ↵Bernhard Schommer2015-02-101-13/+55
| | | | | | | | | | | | | | | | | | | | is that every symbol must start with an "_".
| | | | * Merge branch 'master' into backend_printerBernhard Schommer2015-02-1918-8/+928
| | | | |\ | | |_|_|/ | |/| | | | | | | | | | | | | Conflicts: ia32/PrintAsm.ml
| * | | | Added back symbol functions in the different printer, since they are still ↵Bernhard Schommer2015-02-191-3/+10
| | | | | | | | | | | | | | | | | | | | needed.
| * | | | Changed the symbol function back to its old definition.Bernhard Schommer2015-02-191-10/+3
| | | | |
| * | | | C reference implementation of the int64 helper functions.Xavier Leroy2015-02-1418-8/+928
|/ / / / | | | | | | | | | | | | In test_int64.c: don't test FP->int64 conversions when the FP argument is out of range.
| | | * Removed unused sel_target, changed cygwin symbol names and changed the ↵Bernhard Schommer2015-02-195-7/+11
| | | | | | | | | | | | | | | | default function aligment to be target dependent.
| | | * Added an elf prefix to all common elf functions in PrintAsmaux.Bernhard Schommer2015-02-185-36/+50
| | | |
| | | * Changed print_fun/var_info to be functions instead of booleans.Bernhard Schommer2015-02-185-18/+16
| | | |
| | | * Removed some style issues.Bernhard Schommer2015-02-183-76/+82
| | | |
| | | * Changed arm backend to the common backend printer.Bernhard Schommer2015-02-097-1194/+1145
| | | |
| | | * Merge remote-tracking branch 'origin/master' into backend_printerBernhard Schommer2015-02-093-231/+226
| | | |\ | |_|_|/ |/| | |
* | | | Interpreter produces more detailed trace, including name of semantic rules used.Xavier Leroy2015-02-083-231/+226
| | | | | | | | | | | | | | | | | | | | | | | | 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".
| | | * Changed the ia32 backend to the new Printer.Bernhard Schommer2015-02-065-1035/+983
| | | |
| | | * Changed the ASM printer of the powerpc to the generalized backend.Bernhard Schommer2015-02-055-792/+850
| | | |
| | | * Moved more common functions into a seperate file.Bernhard Schommer2015-02-044-137/+69
| | | |
| | | * Started moving common backend functions into one file.Bernhard Schommer2015-02-033-84/+114
| |_|/ |/| |
* | | Changed the print_globaldef function of the powerpc backend to look like the ↵Bernhard Schommer2015-01-281-10/+2
| | | | | | | | | | | | functions used in the arm and ia32 backend.
* | | Add weaker variants of theorems find_funct_ptr_exists and find_var_exists.Xavier Leroy2015-01-231-70/+122
| | | | | | | | | | | | | | | | | | | | | | | | Instead of assuming name uniqueness for all definitions in the program, these variants only assume uniqueness for a particular name. Use this approach to weaken the hypotheses for match_program and transf_program_partial_augment.
* | | Merge branch 'named-structs'Xavier Leroy2015-01-2336-1630/+4023
|\ \ \ | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | - 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-318-80/+2101
| | | | | | | | | | | | | | | | | | | | Use these constructor functions in C2C to rely less on the types produced by the unverified elaborator.
generated by cgit (git 2.34.1) at 2024-07-05 03:58:56 +0000