aboutsummaryrefslogtreecommitdiffstats
Commit message (Expand)AuthorAgeFilesLines
* streamlined lattice codeDavid Monniaux2020-03-054-144/+17
* begin CSE3David Monniaux2020-03-051-0/+76
* HashedSet with extractionDavid Monniaux2020-03-051-0/+6
* HashedSet with module typesDavid Monniaux2020-03-051-0/+115
* move lattice stuff where it belongsDavid Monniaux2020-03-054-0/+1446
* fix for ppcDavid Monniaux2020-03-031-14/+22
* try to get it to compileDavid Monniaux2020-03-031-0/+1
* forgot k1CDavid Monniaux2020-03-032-0/+147
* fixes for risc-VDavid Monniaux2020-03-031-1/+1
* fix for aarch64David Monniaux2020-03-031-11/+9
* ported to armDavid Monniaux2020-03-031-9/+6
* ported for ppcDavid Monniaux2020-03-031-22/+17
* fix for risc-VDavid Monniaux2020-03-031-9/+7
* adjust for x86David Monniaux2020-03-031-44/+35
* fixed CSE2 for mppa_k1cDavid Monniaux2020-03-0324-843/+1266
|\
| * CSE2 with alias analysisDavid Monniaux2020-03-031-0/+20
| * CSE2 for powerpcDavid Monniaux2020-03-032-0/+152
| * aarch64David Monniaux2020-03-032-0/+150
| * CSE2 for ARMDavid Monniaux2020-03-031-0/+132
| * better 32/64-bit handlingDavid Monniaux2020-03-032-26/+51
| * CSE2 alias analysis for Risc-VDavid Monniaux2020-03-036-30/+158
| * moved away x86-dependent partsDavid Monniaux2020-03-032-38/+46
| * modularize proofDavid Monniaux2020-03-031-29/+10
| * may_overlap_soundDavid Monniaux2020-03-031-0/+38
| * starting to move x86 stuff to x86David Monniaux2020-03-032-201/+216
| * offsets in globals for x86David Monniaux2020-03-032-2/+82
| * globals alias analysis for x86David Monniaux2020-03-033-10/+67
| * with indexed/indexed alias analysis for x86David Monniaux2020-03-033-4/+32
| * kill_store_soundDavid Monniaux2020-03-021-10/+25
| * kill_store1_soundDavid Monniaux2020-03-021-3/+41
| * load_store_awayDavid Monniaux2020-03-021-1/+2
| * swap predicateDavid Monniaux2020-03-022-13/+27
| * works on x86 x86_64David Monniaux2020-03-021-29/+47
| * playing with offsetsDavid Monniaux2020-03-021-1/+67
| * Merge branch 'master' of https://github.com/AbsInt/CompCert into dm-cse2-naiveDavid Monniaux2020-03-0269-1230/+1104
| |\
| | * Define the semantics of `free(NULL)`, continuedXavier Leroy2020-03-021-1/+1
| | * Define the semantics of `free(NULL)` (#226)Xavier Leroy2020-03-022-43/+74
| | * Weaker ec_readonly condition over external calls (#225)Xavier Leroy2020-03-022-18/+35
| | * Documentation comment for single_passed_as_singleXavier Leroy2020-03-021-1/+2
| | * In strict PPC ABI mode, pass single FP on stack in double FP formatXavier Leroy2020-03-021-2/+2
| | * Define IRC.class_of_type for types Tany32, Tany64Xavier Leroy2020-03-021-1/+2
| | * Make single arg alignment depend on toolchain.Bernhard Schommer2020-03-023-3/+20
| * | loadv_storev_sameDavid Monniaux2020-03-021-0/+18
* | | Merge branch 'mppa-cse2' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCe...David Monniaux2020-03-032176-666/+596149
|\ \ \
| * \ \ Merge remote-tracking branch 'origin/mppa-work' into mppa-cse2David Monniaux2020-02-1451-456/+2436
| |\ \ \
| | * | | Added option -ftracelinearize which linearizes based on ifnot branchesCyril SIX2020-02-124-4/+59
| | * | | Moving some arch specific theorems from PSproof to AsmblockpropsCyril SIX2020-02-112-219/+218
| | * | | Moving Asmblockgenproof0 to mppa_k1c/lib/Cyril SIX2020-02-101-0/+0
| | * | | Removing from Asmblockgenproof0 architecture specific definitionsCyril SIX2020-02-109-130/+153
| | * | | Moved some theoremsCyril SIX2020-02-104-113/+101
generated by cgit (git 2.34.1) at 2024-07-06 15:21:29 +0000