aboutsummaryrefslogtreecommitdiffstats
Commit message (Expand)AuthorAgeFilesLines
...
| | * | | | configure: support Coq 8.12.2Xavier Leroy2020-12-241-2/+2
| | * | | | Configure the correct archiver to build runtime/libcompcert.aXavier Leroy2020-12-242-2/+8
| | * | | | x86 32 bits: ABI non-conformance for functions returning structs/unionsXavier Leroy2020-12-111-1/+1
* | | | | | omega -> liaDavid Monniaux2021-06-062-26/+28
| |_|/ / / |/| | | |
* | | | | for making the dockerDavid Monniaux2021-05-114-0/+3
* | | | | for pruning the dockerDavid Monniaux2021-05-111-1/+2
* | | | | pruning the imageDavid Monniaux2021-05-111-0/+4
* | | | | adjust to compile for various archDavid Monniaux2021-05-111-3/+3
* | | | | progress being madeDavid Monniaux2021-05-101-2/+15
* | | | | build for aarch64David Monniaux2021-05-101-1/+4
* | | | | dockerfilesDavid Monniaux2021-05-102-8/+9
* | | | | dockerfile for buildingDavid Monniaux2021-05-101-0/+8
* | | | | Increasing required OCaml version (Pervasives <-> Stdlib module renaming)Cyril SIX2021-05-041-2/+2
* | | | | for OCaml 4.13David Monniaux2021-04-301-1/+1
* | | | | Compatibilité Coq 8.13David Monniaux2021-04-285-8/+3
* | | | | add auxfileDavid Monniaux2021-04-271-0/+17
* | | | | Merge branch 'kvx-work' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCer...Léo Gourdin2021-04-2218-566/+370
|\ \ \ \ \
| * | | | | fix broken link in index-kvx.htmlSylvain Boulmé2021-04-161-1/+1
| | |_|_|/ | |/| | |
| * | | | Merge remote-tracking branch 'origin/manuscript' into kvx-worksubmission_OOPSLA2021_AARCH64_KVXCyril SIX2021-04-135-525/+173
| |\ \ \ \
| | * | | | CleaningCyril SIX2021-04-021-2/+1
| | * | | | More efficientCyril SIX2021-04-021-8/+12
| | * | | | Outermost loop detection worksCyril SIX2021-04-021-9/+10
| | * | | | Getting all loop bodiesCyril SIX2021-04-022-2/+50
| | * | | | get_loop_headers simplification (using the new get_loop_backedges)Cyril SIX2021-04-021-39/+7
| | * | | | Simple backedge detection (modified code from get_loop_headers)Cyril SIX2021-04-023-0/+57
| | * | | | Big simplification of get_loop_infoCyril SIX2021-03-311-111/+16
| | * | | | Simplification of the Linearize heuristic (same result functionally)Cyril SIX2021-03-301-216/+6
| | * | | | Simplifications on Linearize - details belowCyril SIX2021-03-291-205/+79
| | * | | | Code simplification of get_path_map (no functionality change)Cyril SIX2021-01-261-14/+16
| * | | | | Adding more precise heuristic measuresCyril SIX2021-04-131-2/+62
| * | | | | Adding overpredictsCyril SIX2021-04-131-3/+6
| * | | | | Recording of prediction stats with COMPCERT_PROFILING_STATS environment flagCyril SIX2021-04-131-33/+93
| * | | | | Adding distinction between kvx-cos and kvx-mbr (for trapping loads)Cyril SIX2021-04-137-4/+22
| * | | | | rm spurious filesDavid Monniaux2021-04-1239-1705/+0
| * | | | | test profilingDavid Monniaux2021-04-1242-0/+1720
| * | | | | collision of registersDavid Monniaux2021-04-122-3/+3
* | | | | | moving my testsLéo Gourdin2021-04-2226-157/+0
|/ / / / /
* | | | | removing unusued proof lineLéo Gourdin2021-04-091-1/+0
* | | | | adding missing xorimm expLéo Gourdin2021-04-092-0/+77
* | | | | Merge branch 'riscv-work' into kvx-workLéo Gourdin2021-04-0921-1514/+2642
|\ \ \ \ \
| * | | | | Remove flagsLéo Gourdin2021-04-094-10/+3
| * | | | | Removing expansions from AsmgenLéo Gourdin2021-04-096-1401/+49
| | |_|_|/ | |/| | |
| * | | | Removing addptrofs draft, next will be mergingLéo Gourdin2021-04-099-254/+104
| * | | | bugfixLéo Gourdin2021-04-082-2/+3
| * | | | Important commit on expansions' mini CSE, and a draft for addptrofsLéo Gourdin2021-04-0613-762/+1081
| * | | | a more general way to manage special registers before introducing SPLéo Gourdin2021-03-308-560/+593
| * | | | Now a more general way to perform imm operationsLéo Gourdin2021-03-309-38/+68
| * | | | Refactoring the mayundef OP to be more general...Léo Gourdin2021-03-305-201/+191
| * | | | bugfix and printOpLéo Gourdin2021-03-262-19/+29
| * | | | fix admitLéo Gourdin2021-03-261-2/+1
generated by cgit (git 2.34.1) at 2024-07-12 01:40:27 +0000