aboutsummaryrefslogtreecommitdiffstats
path: root/kvx
Commit message (Expand)AuthorAgeFilesLines
* 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
| |\
| | * pointer_eq copiedDavid Monniaux2020-11-251-0/+20
| * | Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepassDavid Monniaux2020-11-242-12/+22
| |\|
| | * correction bug #223 sur KVXDavid Monniaux2020-11-232-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
| * | | | | | | Merge branch 'mppa-RTLpathSE-verif_Op_mem-irrel' into mppa-RTLpathSE-xverifSylvain Boulmé2020-10-081-30/+29
| |\ \ \ \ \ \ \
| | * | | | | | | prove the trick of simplify (as implemented in RTLpathSE_impl_junk)Sylvain Boulmé2020-08-271-18/+6
| | * | | | | | | prove that Mem.valid is preserved by symbolic execution of RTLpathSylvain Boulmé2020-08-271-12/+22
| * | | | | | | | Restart the proof with cherry-pick from Cyril and commit 0e4186b8fSylvain Boulmé2020-10-082-1795/+433
| * | | | | | | | update from kvx-test-prepass (commit 0e4186b8f)Sylvain Boulmé2020-10-081-4/+10
| * | | | | | | | Some theorem was wrongCyril SIX2020-09-301-4/+18
| * | | | | | | | Proof of hsok_local_set_sregCyril SIX2020-09-301-4/+25
| * | | | | | | | Some more progressCyril SIX2020-09-291-2/+33
| * | | | | | | | Bit of progressCyril SIX2020-09-291-6/+40
| * | | | | | | | Proof of simplify_correctCyril SIX2020-09-281-45/+101
| * | | | | | | | A bit of new Ltac and renamingCyril SIX2020-09-211-23/+70
generated by cgit (git 2.34.1) at 2024-06-02 11:47:40 +0000