Commits · PLDI_2021_before_anonymization · CertiCompil / CompCert-KVX · GitLab

Snippets Groups Projects

Nov 09, 2020
- Merge remote-tracking branch 'origin/kvx-work-ssa' into kvx-test-prepass-ssa · 615644a4
  David Monniaux authored 4 years ago
  
  PLDI_2021_before_anonymization
  
  615644a4
- renumber before SSA · e8df8a3a
  David Monniaux authored 4 years ago
  
  e8df8a3a
Nov 07, 2020
- do not test with picosat · dabd9ab4
  David Monniaux authored 4 years ago
  
  dabd9ab4
- do not compile picosat on kvx · 28660d64
  David Monniaux authored 4 years ago
  
  28660d64
Nov 06, 2020
- Merge remote-tracking branch 'origin/kvx-work-ssa' into kvx-test-prepass-ssa · 755530c3
  David Monniaux authored 4 years ago
  
  755530c3
- Merge remote-tracking branch 'origin/kvx-work' into kvx-work-ssa · b9588e8f
  David Monniaux authored 4 years ago
  
  b9588e8f
- Merge remote-tracking branch 'origin/kvx-work-ssa' into kvx-test-prepass-ssa · 311be726
  David Monniaux authored 4 years ago
  
  311be726
- rm extra from regular run · 433a2661
  David Monniaux authored 4 years ago
  
  433a2661
Nov 05, 2020
- Merge remote-tracking branch 'origin/kvx-work-ssa' into kvx-test-prepass-ssa · 4312540c
  David Monniaux authored 4 years ago
  
  4312540c
- Merge remote-tracking branch 'compcertssa/issue1' into kvx-work-ssa · 28b52a3a
  David Monniaux authored 4 years ago
  
  fix picosat etc. SSA crashes
  28b52a3a
- add extra and picosat to the test files · 00a17c97
  EXT Delphine Demange authored 4 years ago
  
  00a17c97
- generalize entrypoint normalization checker + low-cost error messages · d426499c
  EXT Delphine Demange authored 4 years ago
  
  d426499c
- low-cost error messages · 2a6bc83a
  EXT Delphine Demange authored 4 years ago
  
  2a6bc83a
- low-cost error messages · ea755b0f
  EXT Delphine Demange authored 4 years ago
  
  ea755b0f
- ignoring picosat generated files · b58c3626
  EXT Delphine Demange authored 4 years ago
  
  b58c3626
- adding local makefile for ccomp, with ccomp flags · cb8e2938
  EXT Delphine Demange authored 4 years ago
  
  cb8e2938
- Adding proper makefile · 325f6000
  EXT Delphine Demange authored 4 years ago
  
  325f6000
- Adding picosat-965 · 6ec5b387
  EXT Delphine Demange authored 4 years ago
  
  6ec5b387
- Test program related to issue #1 · 618ec760
  EXT Delphine Demange authored 4 years ago
  
  618ec760
- Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepass-ssa · a956cef5
  David Monniaux authored 4 years ago
  
  a956cef5
- Fixing issue with loops having branches leading to goto backedge · 362bdda2
  Cyril SIX authored 4 years ago
  
  362bdda2
- Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepass-ssa · 0c8e8335
  David Monniaux authored 4 years ago
  
  0c8e8335
- Merge remote-tracking branch 'origin/kvx-work' into kvx-work-ssa · f83502f3
  David Monniaux authored 4 years ago
  
  f83502f3
Nov 04, 2020
- Fixing get_loop_headers + alternative get_inner_loops (commented, not active) · 160c4ae2
  Cyril SIX authored 4 years ago
  
  160c4ae2
- Merge branch 'kvx-work' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into kvx-work · 9b6758f4
  David Monniaux authored 4 years ago
  
  9b6758f4
- move loop rotate down · b7c2d3f6
  David Monniaux authored 4 years ago
  
  b7c2d3f6
- youtube link · 2ebe7e34
  Sylvain Boulmé authored 4 years ago
  
  2ebe7e34
- Revert "Embed the short video with subtitles..." · 07898190
  Sylvain Boulmé authored 4 years ago
  
  This reverts commit 2d01e962.
  07898190
- Embed the short video with subtitles... · 2d01e962
  Sylvain Boulmé authored 4 years ago
  
  2d01e962
- do not print "refining" unless asked · afbf8601
  David Monniaux authored 4 years ago
  
  afbf8601
- Merge remote-tracking branch 'origin/kvx-test-prepass' into kvx-test-prepass-ssa · e152b1c1
  David Monniaux authored 4 years ago
  
  e152b1c1
- Merge remote-tracking branch 'origin/kvx-work-ssa' into kvx-test-prepass-ssa · 97cf6e66
  David Monniaux authored 4 years ago
  
  97cf6e66
- Merge remote-tracking branch 'origin/kvx-work' into kvx-work-ssa · e475cffd
  David Monniaux authored 4 years ago
  
  e475cffd
- disable debug printing in scheduler · 0fe569d2
  David Monniaux authored 4 years ago
  
  0fe569d2
- Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepass · 1eaa5dad
  David Monniaux authored 4 years ago
  
  1eaa5dad
- do not print "updates" to nodes · decb2ce7
  David Monniaux authored 4 years ago
  
  decb2ce7
Nov 03, 2020
- Merge remote-tracking branch 'origin/kvx-test-prepass' into kvx-test-prepass-ssa · 92f91660
  David Monniaux authored 4 years ago
  
  92f91660
- Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepass · babf0034
  David Monniaux authored 4 years ago
  
  babf0034
- Merge remote-tracking branch 'origin/kvx-work' into kvx-work-ssa · c7db1353
  David Monniaux authored 4 years ago
  
  c7db1353
- refixcse3 · 025a1854
  David Monniaux authored 4 years ago
  
  025a1854