Commits · 73c4de2d46fff171883965aafdac1ab5b2bb330e · CertiCompil / CompCert-KVX · GitLab

Snippets Groups Projects

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

Jul 18, 2016
- Update Changelog for release 2.7.1 · 73c4de2d
  Xavier Leroy authored 8 years ago
  
  View commits for tag v2.7.1 v2.7.1
  
  73c4de2d
Jul 11, 2016
- Merge pull request #105 from m-schmidt/master · c9cbfda0
  Xavier Leroy authored 9 years ago
  c9cbfda0
Jul 08, 2016
- Unwanted partial constant propagation in 64-bit integer arguments to builtins · 4c7650c3
  Xavier Leroy authored 9 years ago
  4c7650c3
- Port to Coq 8.5pl2 · e73d5db9
  Xavier Leroy authored 9 years ago
  e73d5db9
Jul 01, 2016
- add 'runtime' token to lexer · 2ef43e76
  Michael Schmidt authored 9 years ago
  
  2ef43e76
- extend cminor parser to accept "extern runtime" declarations · 948f5c78
  Michael Schmidt authored 9 years ago
  
  948f5c78
- add missing asmexpand step to cminor handler in driver · a90b94b4
  Michael Schmidt authored 9 years ago
  
  a90b94b4
Jun 30, 2016
- common/Determinism.v: dual-license with GPL · db2445b3
  Xavier Leroy authored 9 years ago
  db2445b3
- Changelog update: mention -g for ARM and IA32 · e2e04450
  Xavier Leroy authored 9 years ago
  
  e2e04450
- Merge branch 'master' of ssh://github.com/AbsInt/CompCert · 599da987
  Xavier Leroy authored 9 years ago
  
  599da987
Jun 28, 2016
- Added back ;; · 0543cb79
  Bernhard Schommer authored 9 years ago
  
  0543cb79
- LICENSE: update the list of files that are dual-licensed under the GPL · 282f8a07
  Xavier Leroy authored 9 years ago
  
  282f8a07
- Activate advanced debug information for arm, ia32. · 711cea9f
  Bernhard Schommer authored 9 years ago
  711cea9f
- bug 19234, inherit varargs flag from previous function definitions for KR conversion · 56a6795d
  Michael Schmidt authored 9 years ago
  
  56a6795d
Jun 27, 2016
- Merge pull request #103 from AbsInt/KR_fundefs · 5ceb5de6
  Bernhard Schommer authored 9 years ago
  5ceb5de6
- Merge pull request #102 from AbsInt/memory_permissions · e005f76f
  Xavier Leroy authored 9 years ago
  e005f76f
Jun 24, 2016
- Also add braces for arm. Bug 19197 · c52ce2f8
  Bernhard Schommer authored 9 years ago
  
  c52ce2f8
- Revised handling of old-style, K&R function definitions · 096a6e38
  Xavier Leroy authored 9 years ago
  096a6e38
- Added braces back. Bug 19197 · fa4dc466
  Bernhard Schommer authored 9 years ago
  
  fa4dc466
- Moved assembler and linker into own files. · 410a5db3
  Bernhard Schommer authored 9 years ago
  410a5db3
- Deactivate options target dependend. · 01354123
  Bernhard Schommer authored 9 years ago
  01354123
Jun 22, 2016
- Stricter control of permissions in memory injections and extensions · fb44646e
  Xavier Leroy authored 9 years ago
  fb44646e
- Update in preparation for release 2.7 · 9b31f673
  Xavier Leroy authored 9 years ago
  
  9b31f673
- Improved handling of "rotate left" and "rotate right" operators · f849a03b
  Xavier Leroy authored 9 years ago
  f849a03b
- Driveraux.mli: fix documentation comment · 076e8fb1
  Xavier Leroy authored 9 years ago
  
  076e8fb1
Jun 21, 2016
- Remove code that will is deprecated in ocaml 4.03 · 7237ccb6
  Bernhard Schommer authored 9 years ago
  7237ccb6
- Pass the updated env through elab_expr. · 8f444dec
  Bernhard Schommer authored 9 years ago
  8f444dec
Jun 07, 2016
- fix '__builtin_annot_val' to '__builtin_annot_intval', such that CompCert can... · 3c4f1377
  Michael Schmidt authored 9 years ago
  3c4f1377
May 28, 2016
- Fixed warning 45 for ExportClight.ml. · 35041fb0
  Bernhard Schommer authored 9 years ago
  
  35041fb0
May 27, 2016
- Merge pull request #101 from fpottier/comment · bd5bcadf
  Bernhard Schommer authored 9 years ago
  bd5bcadf
- Fixed a comment. · acaf3211
  François Pottier authored 9 years ago
  
  acaf3211
- Merge pull request #99 from AbsInt/register-pairs · 5087ec78
  Xavier Leroy authored 9 years ago
  5087ec78
- Merge pull request #100 from AbsInt/driver-split · b45cdb9d
  Xavier Leroy authored 9 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 9 years ago
  
  8d3dbd36
- configure: regression on Menhir's minimal version · 4e2fb826
  Xavier Leroy authored 9 years ago
  
  4e2fb826
May 17, 2016
- Introduce register pairs to describe calling conventions more precisely · 82f9d1f9
  Xavier Leroy authored 9 years ago
  82f9d1f9