aboutsummaryrefslogtreecommitdiffstats
path: root/scheduling
Commit message (Collapse)AuthorAgeFilesLines
* finish verify_block and proofLéo Gourdin2021-05-051-21/+123
|
* advance in cfg checkerLéo Gourdin2021-05-051-1/+138
|
* clean deprecated commentsSylvain Boulmé2021-05-051-6/+1
|
* Factorize as suggested for call/tailcallLéo Gourdin2021-05-041-43/+43
|
* finishing proofs and cleanupLéo Gourdin2021-05-041-134/+48
|
* some advance and simplificationsLéo Gourdin2021-05-041-67/+71
|
* suggestions...Sylvain Boulmé2021-05-041-20/+70
|
* builtin case OK, call and tailcall started but not finishedLéo Gourdin2021-05-041-1/+29
|
* one example case on main proofLéo Gourdin2021-05-041-18/+20
|
* Some try in step_simulationLéo Gourdin2021-05-041-3/+20
|
* proof for Icond in iblock_istepLéo Gourdin2021-05-041-1/+31
|
* essai avec le cond_star_stepSylvain Boulmé2021-05-041-12/+45
|
* essaisSylvain Boulmé2021-05-031-16/+31
|
* some advanceLéo Gourdin2021-05-031-8/+39
|
* Merge branch 'BTL' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert ↵Sylvain Boulmé2021-05-031-35/+22
|\ | | | | | | into BTL
| * A better structure for inductive propLéo Gourdin2021-05-031-35/+25
| |
* | une autre suggestionSylvain Boulmé2021-05-031-0/+14
|/
* Trying a inductive predicate for BTL-RTL proofLéo Gourdin2021-05-031-10/+41
|
* more implem notes in BTLroadmapSylvain Boulmé2021-05-021-1/+8
|
* BTL roadmapSylvain Boulmé2021-05-021-0/+79
|
* debroussaillage et precisions...Sylvain Boulmé2021-05-012-23/+73
|
* BTLtoRTL: proof for internal/external/return statesLéo Gourdin2021-04-302-2/+27
|
* start the new "BTL" IR.Sylvain Boulmé2021-04-283-0/+725
|
* Merge remote-tracking branch 'origin/manuscript' into kvx-worksubmission_OOPSLA2021_AARCH64_KVXCyril SIX2021-04-131-14/+16
|\
| * Code simplification of get_path_map (no functionality change)Cyril SIX2021-01-261-14/+16
| |
* | Remove flagsLéo Gourdin2021-04-091-3/+1
| |
* | Important commit on expansions' mini CSE, and a draft for addptrofsLéo Gourdin2021-04-062-5/+2
| |
* | Remove first nop when doing expansionLéo Gourdin2021-03-211-0/+1
| |
* | Merge remote-tracking branch 'origin/riscv-work' into riscv-work-fpinit-stillexpLéo Gourdin2021-03-062-5/+5
|\ \
| * | Adding a mini CSE pass in the expansion oracleLéo Gourdin2021-03-062-4/+5
| | |
* | | Adding fp init expansionsLéo Gourdin2021-03-021-3/+3
| | |
* | | [Admitted checker] Oracle expansion for float/float32 constant initLéo Gourdin2021-03-022-4/+4
|/ /
* | fix ci ?Léo Gourdin2021-03-021-1/+1
| |
* | Try to save values in virtual registers during expansionLéo Gourdin2021-03-011-1/+1
| |
* | Proofs finished for expansionLéo Gourdin2021-03-011-22/+6
| |
* | Debugging fake values finishedLéo Gourdin2021-03-011-10/+19
| |
* | proof of fsval_proj_correctSylvain Boulmé2021-03-011-7/+27
| |
* | Merge remote-tracking branch 'origin/riscv-work-rules' into riscv-workLéo Gourdin2021-03-011-4/+4
|\ \
| * | bug fix ?Sylvain Boulmé2021-03-011-4/+4
| | |
* | | Proof of fsval condition cmp okLéo Gourdin2021-03-011-968/+18
| | |
* | | [Admitted checker] Some more proof, version with buggy addirw0Léo Gourdin2021-02-251-18/+2
| | |
* | | some more proof for fake hsval checker expansionsLéo Gourdin2021-02-251-324/+1
| | |
* | | [Intermediate] Adding fake hsval for Ccomp expansionLéo Gourdin2021-02-232-164/+68
| | |
* | | Fix importsLéo Gourdin2021-02-231-1/+1
| | |
* | | Merge remote-tracking branch 'origin/riscv-work-rules' into riscv-workLéo Gourdin2021-02-236-79/+202
|\| |
| * | Merge branch 'riscv-work-rules' of ↵Léo Gourdin2021-02-231-2/+52
| |\ \ | | | | | | | | | | | | gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into riscv-work-rules
| | * | add target_cbranch_expanseSylvain Boulmé2021-02-231-2/+52
| | | |
| * | | Separate target_op_simplify for riscVLéo Gourdin2021-02-231-19/+2
| |/ /
| * | fix commentsSylvain Boulmé2021-02-231-2/+5
| | |
| * | starting an interface for target rewriting rules.Sylvain Boulmé2021-02-231-9/+130
| | |
generated by cgit (git 2.34.1) at 2024-07-14 12:35:23 +0000