aboutsummaryrefslogtreecommitdiffstats
path: root/kvx
Commit message (Expand)AuthorAgeFilesLines
* fix kvxv3.8+ssa_aarch64_postpassssaDavid Monniaux2021-01-101-4/+5
* one problem in this file (admitted)David Monniaux2021-01-101-1/+1
* fix for SSADavid Monniaux2021-01-101-3/+3
* fix for KVXDavid Monniaux2021-01-101-307/+19
* Merge remote-tracking branch 'origin/kvx-work' into kvx-work-ssaDavid Monniaux2021-01-0848-8232/+261
|\
| * update kvxSylvain Boulmé2021-01-074-98/+45
| * Merge branch 'kvx-work' into aarch64-peepholeSylvain Boulmé2020-12-1711-53/+57
| |\
| | * upgrade kvx backend to coq.8.12.2Sylvain Boulmé2020-12-165-33/+41
| | * Fixing test/regression for KVXv3.8_kvxCyril SIX2020-12-074-2/+16
| | * Merge branch 'kvx-work' into kvx-work-merge3.8Cyril SIX2020-12-0426-3325/+159
| | |\
| | | * Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepassCyril SIX2020-12-011-1/+0
| | | |\
| | * | | Fixing compilation for KVXCyril SIX2020-12-041-0/+3
| | * | | still issues with FR in kvxDavid Monniaux2020-12-033-27/+26
| | * | | some fixes for KVXDavid Monniaux2020-12-032-6/+0
| | * | | Merge branch 'master' (Absint 3.8) into kvx-work-merge3.8David Monniaux2020-11-182-11/+0
| * | | | Merge branch 'kvx-test-prepass' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy...David Monniaux2020-11-2736-9674/+117
| |\ \ \ \ | | | |/ / | | |/| |
| | * | | Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepassDavid Monniaux2020-11-242-12/+22
| | |\ \ \
| | * | | | new OpWeightsDavid Monniaux2020-10-222-0/+25
| | * | | | Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepassDavid Monniaux2020-10-182-7/+16
| | |\ \ \ \ | | | | |/ / | | | |/| |
| | * | | | update op_valid_pointer_eq proof on the KVXSylvain Boulmé2020-10-171-22/+4
| | * | | | fixing the move of the verified prepass scheduler into scheduling/ directorySylvain Boulmé2020-10-171-872/+0
| | * | | | Merge remote-tracking branch 'origin/kvx-test-prepass' into mppa-RTLpathSE-verifCyril SIX2020-10-1655-11464/+859
| | |\ \ \ \
| | | * | | | so that all architectures compileDavid Monniaux2020-10-021-0/+1
| | | * | | | non pipelined units = none on KVXDavid Monniaux2020-09-301-1/+3
| | | * | | | Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepassDavid Monniaux2020-09-2923-769/+765
| | | |\ \ \ \
| | | * \ \ \ \ Merge remote-tracking branch 'origin/kvx-work-riscV' into kvx-test-prepassDavid Monniaux2020-09-221-14/+0
| | | |\ \ \ \ \
| | | | * | | | | reflect changesDavid Monniaux2020-09-221-14/+0
| | | * | | | | | Merge remote-tracking branch 'origin/kvx-work-riscV' into kvx-test-prepassDavid Monniaux2020-09-212-272/+1
| | | |\| | | | |
| | | | * | | | | moved some "total" value domain functions to a central locationDavid Monniaux2020-09-211-271/+0
| | | * | | | | | just missing OpWeights for AARCH64David Monniaux2020-09-1614-9446/+0
| | | * | | | | | starting to move common filesDavid Monniaux2020-09-1616-1651/+0
| | | * | | | | | Merge branch 'mppa-RTLpathSE-verif-hash-junk' of gricad-gitlab.univ-grenoble-...David Monniaux2020-09-1012-222/+230
| | | |\ \ \ \ \ \
| | | | * \ \ \ \ \ Merge remote-tracking branch 'origin/kvx-work' into mppa-RTLpathSE-verif-hash...David Monniaux2020-09-056-75/+117
| | | | |\ \ \ \ \ \
| | | * | | | | | | | use with_destructorDavid Monniaux2020-09-102-20/+29
| | * | | | | | | | | removing useless opt_simuSylvain Boulmé2020-10-133-36/+25
| | * | | | | | | | | refactoring of RTLpathSE_impl.v (split with _simu_specs)Sylvain Boulmé2020-10-135-3911/+2086
| | * | | | | | | | | remove the last tiny issue!Sylvain Boulmé2020-10-121-10/+3
| | * | | | | | | | | simpl hsstate_simu_core_correctSylvain Boulmé2020-10-121-3/+1
| | * | | | | | | | | fix one issue by generalizing RTLpathSE_theory.sstate_simuSylvain Boulmé2020-10-122-9/+18
| | * | | | | | | | | move issue from hsexec_correct to hsstate_simu_core_correctSylvain Boulmé2020-10-121-14/+19
| | * | | | | | | | | most of the proof is done ! two (small ?) issues remain...Sylvain Boulmé2020-10-121-30/+83
| | * | | | | | | | | oops: forget to save before compile/commit/pushSylvain Boulmé2020-10-121-2/+5
| | * | | | | | | | | end of merge with Cyril's proofSylvain Boulmé2020-10-122-59/+227
| | * | | | | | | | | starting to merge with Cyril's proofSylvain Boulmé2020-10-111-48/+773
| | * | | | | | | | | hconsing: full proof of hsiexec_path_correctSylvain Boulmé2020-10-102-42/+71
| | * | | | | | | | | progress on hslocal_set_sreg_correctSylvain Boulmé2020-10-101-37/+53
| | * | | | | | | | | progress on hsexec_inst_correct_dynSylvain Boulmé2020-10-101-39/+140
| | * | | | | | | | | hconsing: red_PTree_set_correctSylvain Boulmé2020-10-091-0/+11
| | * | | | | | | | | hconsing: root_happly_correct + simplify_correct DONESylvain Boulmé2020-10-094-15/+145
| | * | | | | | | | | prove the kvx-test-prepass fix (commit 0e4186b8f)Sylvain Boulmé2020-10-081-14/+58
generated by cgit (git 2.34.1) at 2024-06-02 14:06:30 +0000