Commits · v2.7 · CertiCompil / Chamois-Arsene · GitLab

Snippets Groups Projects

Jun 30, 2016
- For the release, turn off -warn-error · 79abf4d9
  Xavier Leroy authored 8 years ago
  View commits for tag v2.7 v2.7
  
  79abf4d9
- common/Determinism.v: dual-license with GPL · db2445b3
  Xavier Leroy authored 8 years ago
  db2445b3
- Changelog update: mention -g for ARM and IA32 · e2e04450
  Xavier Leroy authored 8 years ago
  
  e2e04450
- Merge branch 'master' of ssh://github.com/AbsInt/CompCert · 599da987
  Xavier Leroy authored 8 years ago
  
  599da987
Jun 28, 2016
- Added back ;; · 0543cb79
  Bernhard Schommer authored 8 years ago
  
  0543cb79
- LICENSE: update the list of files that are dual-licensed under the GPL · 282f8a07
  Xavier Leroy authored 8 years ago
  
  282f8a07
- Activate advanced debug information for arm, ia32. · 711cea9f
  Bernhard Schommer authored 8 years ago
  711cea9f
- bug 19234, inherit varargs flag from previous function definitions for KR conversion · 56a6795d
  Michael Schmidt authored 8 years ago
  
  56a6795d
Jun 27, 2016
- Merge pull request #103 from AbsInt/KR_fundefs · 5ceb5de6
  Bernhard Schommer authored 8 years ago
  5ceb5de6
- Merge pull request #102 from AbsInt/memory_permissions · e005f76f
  Xavier Leroy authored 8 years ago
  e005f76f
Jun 24, 2016
- Also add braces for arm. Bug 19197 · c52ce2f8
  Bernhard Schommer authored 8 years ago
  
  c52ce2f8
- Revised handling of old-style, K&R function definitions · 096a6e38
  Xavier Leroy authored 8 years ago
  096a6e38
- Added braces back. Bug 19197 · fa4dc466
  Bernhard Schommer authored 8 years ago
  
  fa4dc466
- Moved assembler and linker into own files. · 410a5db3
  Bernhard Schommer authored 8 years ago
  410a5db3
- Deactivate options target dependend. · 01354123
  Bernhard Schommer authored 8 years ago
  01354123
Jun 22, 2016
- Stricter control of permissions in memory injections and extensions · fb44646e
  Xavier Leroy authored 8 years ago
  fb44646e
- Update in preparation for release 2.7 · 9b31f673
  Xavier Leroy authored 8 years ago
  
  9b31f673
- Improved handling of "rotate left" and "rotate right" operators · f849a03b
  Xavier Leroy authored 8 years ago
  f849a03b
- Driveraux.mli: fix documentation comment · 076e8fb1
  Xavier Leroy authored 8 years ago
  
  076e8fb1
Jun 21, 2016
- Remove code that will is deprecated in ocaml 4.03 · 7237ccb6
  Bernhard Schommer authored 8 years ago
  7237ccb6
- Pass the updated env through elab_expr. · 8f444dec
  Bernhard Schommer authored 8 years ago
  8f444dec
Jun 07, 2016
- fix '__builtin_annot_val' to '__builtin_annot_intval', such that CompCert can... · 3c4f1377
  Michael Schmidt authored 8 years ago
  3c4f1377
May 28, 2016
- Fixed warning 45 for ExportClight.ml. · 35041fb0
  Bernhard Schommer authored 8 years ago
  
  35041fb0
May 27, 2016
- Merge pull request #101 from fpottier/comment · bd5bcadf
  Bernhard Schommer authored 8 years ago
  bd5bcadf
- Fixed a comment. · acaf3211
  François Pottier authored 8 years ago
  
  acaf3211
- Merge pull request #99 from AbsInt/register-pairs · 5087ec78
  Xavier Leroy authored 8 years ago
  5087ec78
- Merge pull request #100 from AbsInt/driver-split · b45cdb9d
  Xavier Leroy authored 8 years ago
  b45cdb9d
May 24, 2016
- Added version string to Clightgen. · 8c28d063
  Bernhard Schommer authored 9 years ago
  8c28d063
- Escape all newlines. · daf677cd
  Bernhard Schommer authored 9 years ago
  daf677cd
- Moved shared frontend code in own file. · 0a450d3e
  Bernhard Schommer authored 9 years ago
  0a450d3e
- Moved some system functions into own module. · fbaeaaec
  Bernhard Schommer authored 9 years ago
  fbaeaaec
- ia32/Conventions1: remove commented-out proof attempt · 8d3dbd36
  Xavier Leroy authored 8 years ago
  
  8d3dbd36
- configure: regression on Menhir's minimal version · 4e2fb826
  Xavier Leroy authored 8 years ago
  
  4e2fb826
May 17, 2016
- Introduce register pairs to describe calling conventions more precisely · 82f9d1f9
  Xavier Leroy authored 9 years ago
  82f9d1f9
May 13, 2016
- bug 18925, fix loading of symbols for thumb: :lower16: and :upper16: are... · 672393ef
  Michael Schmidt authored 9 years ago
  672393ef
- Split dependency generation. · 9864e348
  Bernhard Schommer authored 9 years ago
  9864e348
- Respect COQBIN in configure script. · a91123a5
  Bernhard Schommer authored 9 years ago
  
  a91123a5
- Added option to pass linker options to gcc. · 19f2a76f
  Bernhard Schommer authored 9 years ago
  19f2a76f
May 11, 2016
- configure: bump Menhir required version to 20160303 · 0d48fd07
  Xavier Leroy authored 9 years ago
  0d48fd07
May 10, 2016
- fix typo 'clinker_option' in configure for OSX · 812ae094
  Michael Schmidt authored 9 years ago
  
  812ae094