Commits · fb44646eb7308c1dd6a44b85415528982083200b · CertiCompil / Chamois-Arsene · GitLab

Snippets Groups Projects

Le runner partagé sera indisponible toute la journée du mercredi 9 juillet.

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
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
- fix typo in comment · 470f207e
  Michael Schmidt authored 9 years ago
  
  470f207e
- fix typo 'clinker_option' in configure for OSX · abc067fe
  Michael Schmidt authored 9 years ago
  
  abc067fe
May 07, 2016
- ValueAnalysis: use ZTrees instead of ZMaps for abstracting contents of memory blocks · 3f98769c
  Xavier Leroy authored 9 years ago
  3f98769c
Apr 27, 2016
- Revise the Stacking pass and its proof to make it easier to adapt to 64-bit architectures · 5978342d
  Xavier Leroy authored 9 years ago
  5978342d
Apr 25, 2016
- bug 18004, fix file extensions for dparse option · cf3f9615
  Michael Schmidt authored 9 years ago
  
  cf3f9615
- Enabled Werror via command line option. · d2c668e9
  Bernhard Schommer authored 9 years ago
  d2c668e9
Apr 09, 2016
- */TargetPrinter.ml: wrong comment attached to Init_float32 constants · e3a336fc
  Xavier Leroy authored 9 years ago
  e3a336fc
Apr 06, 2016
- Also enable warnings for doc generator. · 4f8ba5f0
  Bernhard Schommer authored 9 years ago
  
  4f8ba5f0
- Added iso646 header for alternate spellings. · 41b17255
  Bernhard Schommer authored 9 years ago
  41b17255
- Check for type compatibility when initializing TInt arrays with wide strings (§6.7.8), bug 18000 · ebaac507
  Michael Schmidt authored 9 years ago
  
  ebaac507
- Check for type compatibility when initializing TInt arrays with wide strings (§6.7.8), bug 18000 · 2ed2dcee
  Michael Schmidt authored 9 years ago
  
  2ed2dcee
Apr 05, 2016
- Revert initialization check, bug 18000 · ce248e4d
  Michael Schmidt authored 9 years ago
  
  ce248e4d
- Match type size with size of wchar_t when initializing TInt arrays with wide strings, bug 18000 · 567ed782
  Michael Schmidt authored 9 years ago
  
  567ed782
- Catch initialization of arrays with single expressions, bug 18000 · d891d704
  Michael Schmidt authored 9 years ago
  
  d891d704
- Catch initialization of arrays with single expressions, bug 18000 · 5c88ca36
  Michael Schmidt authored 9 years ago
  
  5c88ca36