aboutsummaryrefslogtreecommitdiffstats
Commit message (Collapse)AuthorAgeFilesLines
* Minor bug fixes in configure and Makefile.extrXavier Leroy2014-12-172-5/+6
|
* Merge branch 'master' into pure-makefilesXavier Leroy2014-12-1759-763/+2379
|\
| * Clean up support for common symbols. Uninitialized "const" symbols can be ↵Xavier Leroy2014-12-176-39/+71
| | | | | | | | common.
| * Use cp instead of symbolic links for executables.Xavier Leroy2014-12-171-15/+8
| | | | | | | | Now that we search for compcert.ini from Sys.executable, symbolic links cause compcert.ini not to be found.
| * Merge branch 'master' of https://github.com/AbsInt/CompCertXavier Leroy2014-12-175-19/+35
| |\
| | * Stdlib path is ignored when the configuration has_runtime_lib is set to false.Bernhard Schommer2014-12-151-2/+7
| | |
| | * Update the IA32/MacOS X port.Xavier Leroy2014-12-112-5/+7
| | | | | | | | | | | | | | | | | | - Prefix symbols with _ - Print indirect symbol definitions - Suppress __asm() macros in system header files
| | * Prevent constant propagation on Oindirectsymbol addresses.Xavier Leroy2014-12-111-2/+11
| | | | | | | | | | | | | | | (Otherwise they are turned into Oaddrsymbol or global addressing modes, causing linking issues on MacOS X.)
| | * Preserve single quotes (e.g. in CPREPRO) when generating compcert.iniXavier Leroy2014-12-111-10/+10
| | |
| * | Prototype the pointer so that the program has well defined semantics and ↵Xavier Leroy2014-12-171-1/+1
| |/ | | | | | | passes the reference interpreter.
| * Removed more unused variables.Bernhard Schommer2014-12-041-1/+0
| |
| * Removed unused variable and changed the search for the installation ↵Bernhard Schommer2014-12-042-6/+1
| | | | | | | | directory. Use Sys.executable_name instead of Sys.argv.(0).
| * Changed the comparison of jumptables.Bernhard Schommer2014-12-011-14/+7
| |
| * Wrong handling of block-local function declarations (in Elab.ml).Xavier Leroy2014-11-264-13/+31
| |
| * Use Bitstring.is_zeroes_bitstring from bitstring 2.0.4.Xavier Leroy GALLIUM2014-11-251-0/+8
| | | | | | | | The original code is less efficient and not tail recursive.
| * Merge pull request #2 from AbsInt/public-globalsXavier Leroy2014-11-2543-660/+2206
| |\ | | | | | | Public globals
| | * Update the ARM port.Xavier Leroy2014-11-242-50/+38
| | |
| | * Update PowerPC port.Xavier Leroy2014-11-242-21/+51
| | |
| | * Verification of the Unusedglob pass (removal of unreferenced static global ↵Xavier Leroy2014-11-2412-264/+1458
| | | | | | | | | | | | definitions). Assorted changes to ia32/Op.v. PowerPC and ARM need updating.
| | * Add Genv.public_symbol operation.Xavier Leroy2014-11-2424-263/+562
| | | | | | | | | | | | | | | 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-247-63/+98
| |/ | | | | | | For the moment, this field is ignored.
| * Use gettimeofday() instead of obsolete ftime().Xavier Leroy2014-11-242-11/+19
| | | | | | | | (Patch by Daniel Dickman.)
* | Use OCaml's .opt compilers when available.Xavier Leroy2014-12-173-32/+82
| | | | | | | | Cleanups in configure.
* | Remove ocamlbuild configuration files, no longer used.Xavier Leroy2014-11-222-23/+0
| |
* | Use String.map instead of reimplementing it ourselves.Xavier Leroy2014-11-221-5/+18
| | | | | | | | Avoids warnings with 4.02.
* | Replace ocamlbuild by a second-stage makefile to compile the OCaml code and ↵Xavier Leroy2014-11-225-59/+296
|/ | | | | | produce the executables. configure: add check for GNU make.
* Analysis of jump tables was using the wrong size.Xavier Leroy2014-11-171-1/+1
|
* Add flags to control individual optimization passes + flag -O0 for turning ↵Xavier Leroy2014-11-167-46/+128
| | | | them off.
* Revised parsing of command-line arguments (in preparation for adding more).Xavier Leroy2014-11-163-118/+250
| | | | | | Honor "ccomp -E foo.h" for GCC compatibility. Accept .o.ext files as object files for GCC compatibility. Fixed and improved handling of Cminor source files.
* build_from_parsed: simplified code + correctness proof.Xavier Leroy2014-11-151-15/+86
|
* cchecklink: added option "-files-from" to read .sdump file namesXavier Leroy2014-11-152-4/+29
| | | | from a file or from standard input.
* Tune behavior wrt warnings:Xavier Leroy2014-10-242-2/+3
| | | | | | - cchecklink was compiled with -warn-error, which is bad for production code - silence warning 3 (deprecated functions) - silence warning 20 (unused function argument) for Coq-extracted files.
* Deactivated the warning for deprecated features for compilation of ↵Bernhard Schommer2014-10-201-0/+1
| | | | cchecklink since it breaks the build with newer ocaml versions.
* Removed duplicated open.Bernhard Schommer2014-10-171-1/+0
|
* Revised translation of '&&' and '||' to Clight.Xavier Leroy2014-10-1311-124/+109
| | | | | | | | | | | 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.
* Update Makefile, dependencies, and Changelog after upgrade to Flocq 2.4.0.Xavier Leroy2014-10-093-1/+3
|
* Merge pull request #1 from jhjourdan/masterXavier Leroy2014-10-0921-942/+6030
|\ | | | | Upgrade to flocq 2.4.0
| * Upgrade to flocq 2.4.0Jacques-Henri Jourdan2014-10-0721-942/+6030
| |
* | Refactored the code of ia32/PrintAsm.ml by moving the functions depending on ↵Bernhard Schommer2014-10-081-138/+220
| | | | | | | | the target system in a seperate module.
* | Refactored the code of powerpc/PrintAsm.ml by moving the function depending ↵Bernhard Schommer2014-10-081-200/+236
|/ | | | on the target system in a seperate module.
* Refactored the code of arm/PrintAsm.ml in order to allow the parametrization ↵Bernhard Schommer2014-10-061-44/+86
| | | | of the printing code over the configuration-dependent bits.
* Removed environment variable for the stdlib_path and added a new variable ↵Bernhard Schommer2014-10-063-20/+20
| | | | for the configuration file.
* Change the way the tools like the linker, assembler, etc. are specified by ↵Bernhard Schommer2014-09-304-22/+113
| | | | including an .ini file parser. The .ini file is generated in the Makefile instead of the Configuration.ml file and parsed on start.
* Moved the timing facility to a seperate file.Bernhard Schommer2014-09-295-54/+68
|
* Refactoring in the printing of FP numbers.Xavier Leroy2014-09-241-8/+2
|
* Add theorem "elements_remove".Xavier Leroy2014-09-241-167/+178
| | | | | Use "elements_remove" to simplify the proof of "cardinal_remove". Simplify some of the proofs over function "xelements".
* Upgrade clightgen with the new features of CompCert 2.4 (single floats, etc).Xavier Leroy2014-09-241-7/+20
|
* GCCism: accept __volatile and __volatile__Xavier Leroy2014-09-211-0/+2
| | | | | These alternate keywords for "volatile" are used in some header files in the wild.
* Add .gitignore files.Xavier Leroy2014-09-216-0/+63
|
* Error instead of warning on illegal escape sequences.Xavier Leroy2014-09-212-1/+5
| | | | | | | | The previous behavior for illegal escape sequences (e.g. '\%') in character and string literals was to emit an error, then treat "\x" as "x". As reported by a user, this is dangerous, because the warning can go unnoticed, and other compilers can treat "\x" as "\\x" (backslash followed by 'x'). Better to error out.
generated by cgit (git 2.34.1) at 2024-07-02 23:06:47 +0000