aboutsummaryrefslogtreecommitdiffstats
Commit message (Collapse)AuthorAgeFilesLines
* Changed cc_varargs to an option typeBernhard Schommer2020-12-2512-27/+36
| | | | | | Instead of being a simple boolean we now use an option type to record the number of fixed (non-vararg) arguments. Hence, `None` means not vararg, and `Some n` means `n` fixed arguments followed with varargs.
* configure: use `$make` instead of `make`Xavier Leroy2020-12-251-1/+1
| | | | | | To make sure it works if `gmake` is required. Fixes: #381
* configure script revised and simplifiedXavier Leroy2020-12-241-83/+43
| | | | | | | | Start from reasonable defaults before updating them per-target. Print more details in the final configuration summary. Update the "manual" mode.
* configure: support Coq 8.12.2Xavier Leroy2020-12-241-2/+2
|
* Configure the correct archiver to build runtime/libcompcert.aXavier Leroy2020-12-242-2/+8
| | | | | | | | | - Use `${toolprefix}ar` instead of `ar` so as to match the choice of C compiler (as proposed by Michael Soegtrop in PR #380) - Use the Diab archiver `dar` if configured for powerpc-eabi-diab Closes: #380
* x86 32 bits: ABI non-conformance for functions returning structs/unionsXavier Leroy2020-12-111-1/+1
| | | | | | | | The wrong value was returned in EAX, instead of the address of the struct/union. Report and fix by Zhenguo Yin. Fixes: #377
* Error when using -main without -interpXavier Leroy2020-12-061-0/+2
| | | | | | Outside of -interp mode, -main has no (known) effect but could be confused for a linker option that sets the program's entrypoint, say. It's safer to reject the option.
* PowerPC modeling of registers destroyed by pseudo-instructionsXavier Leroy2020-12-062-4/+6
| | | | Inlined built-in functions destroy GPR0
* ARM modeling of registers destroyed by pseudo-instructionsXavier Leroy2020-12-062-4/+6
| | | | | Pflid destroys IR14 Inlined built-in functions destroy IR14
* AArch64 modeling of registers destroyed by pseudo-instructionsXavier Leroy2020-12-062-8/+11
| | | | | | Pfmovimms, Pfmovimmd destroy X16 Pbtbl preserves X17 Inlined built-in functions destroy X16 and X30
* Remove Pfcfi, Pfcfiu, Pfctiu pseudoinstructionsXavier Leroy2020-12-0612-99/+23
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Also remove the Ofloatofint, Ofloatofintu, and Ointuoffloat PowerPC operations. The pseudoinstructions were used to implement these operations, as follows: Pfcfi : Ofloatofint i.e. the conversion signed int32 -> float64 Pfcfiu : Ofloatofintu i.e. the conversion unsigned int32 -> float64 Pfctiu : Ointuoffloat i.e. the conversion float64 -> unsigned int32 These pseudoinstructions were expanded (in Asmexpand.ml) in terms of Pfcfid : signed int64 -> float64 Pfctidz : float64 -> signed int64 and int32/int64 conversions. This commit performs this expansion during instruction selection (SelectOp.vp): floatofint(n) becomes floatoflong(longofint(n)) floatofintu(n) becomes floatoflong(longuofint(n)) intuoffloat(n) becomes cast32unsigned(longoffloat(n)) Then there is no need for the 3 removed operations and the 3 removed pseudoinstructions. More importantly, the correctness of these expansions is now proved as part of instruction selection, using the corresponding results from Floats.v.
* Updates for release 3.8v3.8Xavier Leroy2020-11-163-5/+10
|
* Do not use -warn-error when building from a release tarballXavier Leroy2020-11-141-2/+9
| | | | | Stopping on warnings is useful for development builds, but unhelpful for released software.
* Support Coq 8.12.1Xavier Leroy2020-11-142-3/+3
|
* Update READMEXavier Leroy2020-11-091-4/+4
|
* Update ChangesXavier Leroy2020-11-081-0/+48
|
* Added semantics for the PowerPC sel and mulh built-insBernhard Schommer2020-11-071-4/+44
| | | | | | | | The semantics of the various selection functions are defined analogously to the ones from the type generic sel function. The semantics for the various high word multiplication functions is defined using the Integer functions. Bug 30035
* Added missing printer for PowerPC 64 bit comparison.Bernhard Schommer2020-11-061-0/+8
| | | | | These comparisons are supported in the hybrid 64 bit mode. Bug 30035
* Added implementation for fmin/fmax for aarch64.Bernhard Schommer2020-11-063-0/+12
| | | | | The two built-in function map to the fmax and fmin instruction. Bug 30035
* Better "make clean"Xavier Leroy2020-11-011-1/+1
|
* Add -main option to specify entrypoint function in interpreter mode (#374)Xavier Leroy2020-10-304-20/+42
| | | | | | | When running unit tests with the CompCert reference interpreter, it's nice to be able to start execution at a given test function instead of having to write a main function. This PR adds a -main command-line option to give the name of the entry point function. The default is still main. Frama-C has a similar option. The function specified with -main is called with no arguments. If its return type is int, its return value is the exit status of the program. Otherwise, its return value is ignored and the program exits with status 0.
* Add `string_of_ident` conversionXavier Leroy2020-10-121-0/+110
| | | | | | This is the left inverse of `ident_to_string`. Closes: #372
* Remove -version-file optionXavier Leroy2020-10-121-19/+2
| | | | It is specific to AbsInt's commercial version of CompCert.
* Support Cygwin 64 bitsXavier Leroy2020-10-0517-118/+415
| | | | | | - Add support for the Win64 ABI to the x86_64 port - Update vararg support to handle Win64 conventions - Configure support for x86_64-cygwin64
* Test clightgen with -short-idents and -normalize optionsXavier Leroy2020-09-221-0/+6
| | | | Use different combination of options for different test files.
* Use exact arithmetic for printing positive numbersXavier Leroy2020-09-221-52/+56
| | | | | | And also for the computations in name_temporary. Overflowing OCaml's integer types is unlikely in actual use but happened in the past owing to another mistake (see issue #370).
* Fix computation of next temporary in -canonical-idents modeXavier Leroy2020-09-221-1/+12
| | | | | | | Variables were confused for temporaries, causing the temporaries introduced by this pass to be very big integers. Fixes: #370
* Support the use of already-installed MenhirLib and Flocq librariesXavier Leroy2020-09-2111-67/+82
| | | | configure flags -use-external-Flocq and -use external-MenhirLib.
* No need for -R options, _CoqProject contains them alreadyXavier Leroy2020-09-211-4/+2
|
* Check ptr arithmetic for ++ and --Bernhard Schommer2020-09-201-10/+16
| | | | | Also: improve check for ptr - integer. (Added by Xavier Leroy <xavier.leroy@college-de-france.fr>)
* Simplify two scripts in Zbits (#369)Maxime Dénès2020-09-181-2/+2
| | | | | Previous scripts were relying on the order in which apply's HO unification performs reductions, for a goal that could be solved by reflexivity.
* Add new static-assert token for deLexer utility; bug 29273Michael Schmidt2020-08-041-0/+1
|
* Add comments we missed to sync to GitHubChristoph Cullmann2020-07-301-0/+2
|
* Add missing comment for print_version_file_and_exitChristoph Cullmann2020-07-301-0/+1
|
* Remove support for x86-32 under macOSXavier Leroy2020-07-292-45/+3
| | | | | | | 32-bit executables cannot be built since XCode 10.0 (sep 2018). 32-bit executables cannot be executed since MacOS 10.15 (oct 2019). Better remove x86-32 support and fail at configuration time instead of at the end of the build.
* Allow string_literals_list in _Static_assert.Bernhard Schommer2020-07-272-24/+25
| | | | | | Not all pre-processors concatenate string literal lists, however they are allowed in _Static_assert. This is similar to the rules for inline assembly etc.
* Add test for __builtin_sqrt and __builtin_fabsfXavier Leroy2020-07-272-0/+7
|
* Add __builtin_sqrt as synonymous for __builtin_fsqrtXavier Leroy2020-07-277-5/+8
| | | | __builtin_sqrt (no "f") is the name used by GCC and Clang.
* Refactor regression testing of built-in functionsXavier Leroy2020-07-2713-110/+447
| | | | | | Share the testing code for built-in functions that are available on all target platforms. Improve testing of __builtin_clz* and __builtin_ctz*
* Move declarations of __builtin_clz* and __builtin_ctz* to C2C.mlXavier Leroy2020-07-275-46/+12
| | | | These functions are now available on all targets.
* AArch64 implementation of __builtin_ctz*Xavier Leroy2020-07-273-1/+11
| | | | Using the "rbit" instruction (reverse bits).
* RISC-V implementation of __builtin_clz* and __builtin_ctz*Xavier Leroy2020-07-272-0/+134
| | | | Using binary search loops expanded at point of use.
* Add support for __builtin_fabsfXavier Leroy2020-07-274-0/+13
|
* No need to process __builtin_fabs in $ARCH/Asmexpand.mlXavier Leroy2020-07-275-12/+0
| | | | __builtin_fabs has already been expanded in backend/Selection.v .
* More checks for __builtin_va_start (#250)Bernhard Schommer2020-07-211-6/+10
| | | | We check that this builtin function is only called from within a variadic function and has the correct number of arguments.
* cparser/handcrafted.messages: missing blank lineXavier Leroy2020-07-211-0/+1
|
* Updated handcrafted.messages.Bernhard Schommer2020-07-211-0/+108
| | | | | Added error descriptions for the new syntax errors introduced by '_Static_assert'.
* Support _Static_assert from C11Xavier Leroy2020-07-217-1060/+1116
|
* Support __builtin_constant_p as in GCC and Clang (#367)Xavier Leroy2020-07-211-0/+10
| | | | | Returns 1 if the argument is a constant expression, 0 otherwise. Closes: #366
* Use the correct location for Slabaled in transform.Bernhard Schommer2020-07-211-2/+2
|
generated by cgit (git 2.34.1) at 2024-06-30 23:14:41 +0000