Commits · 0132b8aa669adc10e6ca953d10d5c0b861f304b1 · CertiCompil / CompCert-IntrinSec · GitLab

Snippets Groups Projects

Due to inactivity, this project is scheduled to be deleted on 2037-01-22. Why is this scheduled?

Jul 27, 2020
- Allow string_literals_list in _Static_assert. · 0132b8aa
  Bernhard Schommer authored 4 years ago
  0132b8aa
- Add test for __builtin_sqrt and __builtin_fabsf · 896310e8
  Xavier Leroy authored 4 years ago
  
  896310e8
- Add __builtin_sqrt as synonymous for __builtin_fsqrt · 77ce8ba2
  Xavier Leroy authored 4 years ago
  77ce8ba2
- Refactor regression testing of built-in functions · 70f105e6
  Xavier Leroy authored 4 years ago
  70f105e6
- Move declarations of __builtin_clz* and __builtin_ctz* to C2C.ml · bc20d7c0
  Xavier Leroy authored 4 years ago
  bc20d7c0
- AArch64 implementation of __builtin_ctz* · a56e0c65
  Xavier Leroy authored 4 years ago
  a56e0c65
- RISC-V implementation of __builtin_clz* and __builtin_ctz* · 094ac30c
  Xavier Leroy authored 4 years ago
  094ac30c
- Add support for __builtin_fabsf · 4cf2fc41
  Xavier Leroy authored 4 years ago
  
  4cf2fc41
- No need to process __builtin_fabs in $ARCH/Asmexpand.ml · 465f6b41
  Xavier Leroy authored 4 years ago
  465f6b41
Jul 21, 2020
- More checks for __builtin_va_start (#250) · 907a9042
  Bernhard Schommer authored 4 years ago
  907a9042
- cparser/handcrafted.messages: missing blank line · b23f94bd
  Xavier Leroy authored 4 years ago
  
  b23f94bd
- Updated handcrafted.messages. · 2af7c98c
  Bernhard Schommer authored 4 years ago
  2af7c98c
- Support _Static_assert from C11 · a8ce85ad
  Xavier Leroy authored 4 years ago
  
  a8ce85ad
- Support __builtin_constant_p as in GCC and Clang (#367) · 3a1b0e98
  Xavier Leroy authored 4 years ago
  3a1b0e98
- Use the correct location for Slabaled in transform. · 4adf6e3a
  Bernhard Schommer authored 4 years ago
  
  4adf6e3a
Jul 20, 2020
- Added error for redefined builtin. · b4c6087c
  Bernhard Schommer authored 4 years ago
  b4c6087c
Jul 15, 2020
- Added missing semicolon. · 72f78307
  Bernhard Schommer authored 4 years ago
  
  72f78307
- Bytecode-only build, continued · 6b854265
  Xavier Leroy authored 4 years ago
  6b854265
- Revised detection of menhirLib directory, continued (#365) · 13e0566d
  Xavier Leroy authored 4 years ago
  13e0566d
Jul 09, 2020
- No trailing commas for --version-file option. · 72be849e
  Bernhard Schommer authored 4 years ago
  
  72be849e
Jul 08, 2020
- Fix typo. · a00de29b
  Bernhard Schommer authored 4 years ago
  
  a00de29b
- Revert "Use the same version string." · 43026322
  Bernhard Schommer authored 4 years ago
  43026322
- Use the same version string. · 1a01ad62
  Bernhard Schommer authored 4 years ago
  1a01ad62
- Remove no longer needed option enforce-buildnr · ae7eeb88
  Bernhard Schommer authored 4 years ago
  
  ae7eeb88
- Introduce additional "branch" build information. · f8cfbc1b
  Bernhard Schommer authored 4 years ago
  
  f8cfbc1b
- Add option to print version information in file · fdaa2a3e
  Bernhard Schommer authored 4 years ago
  
  fdaa2a3e
Jul 07, 2020
- Bytecode-only build (#243) · 9af28924
  Xavier Leroy authored 4 years ago
  9af28924
- Revised detection of menhirLib directory (#248) · 3b1f3dd5
  Xavier Leroy authored 4 years ago
  3b1f3dd5
Jul 01, 2020
- Added asserts for constraints of PowerPC builtins · bb9fa555
  Bernhard Schommer authored 4 years ago
  
  bb9fa555
- Fix typo in name of builtin function. · c94405f6
  Bernhard Schommer authored 4 years ago
  
  c94405f6
Jun 30, 2020
- Added missing hint database name. · fde84754
  Bernhard Schommer authored 4 years ago
  
  fde84754
Jun 28, 2020
- Move shared code in new file. · ad2ea9c2
  Bernhard Schommer authored 5 years ago
  ad2ea9c2
- Remove the `can_reserve_register` function. · faa1d7fb
  Bernhard Schommer authored 5 years ago
  faa1d7fb
- Use library function. · 127b00c5
  Bernhard Schommer authored 5 years ago
  127b00c5
- Use Hashtbl.find_opt. · 19aed83c
  Bernhard Schommer authored 5 years ago
  19aed83c
Jun 25, 2020
- Eliminate known builtins whose result is ignored · 7fe7aabe
  Xavier Leroy authored 4 years ago
  7fe7aabe
- Improve printing of builtin function invocations · c6b86fd5
  Xavier Leroy authored 4 years ago
  c6b86fd5
Jun 21, 2020
- Preliminary support for Coq 8.12 · 5b8578da
  Xavier Leroy authored 5 years ago
  5b8578da
- Transform non-recursive Fixpoint into Definition · 70609c93
  Xavier Leroy authored 5 years ago
  70609c93
Jun 15, 2020
- SimplExpr: remove unused definition "sd_cast_set" · 375c844e
  Xavier Leroy authored 5 years ago
  375c844e