aboutsummaryrefslogtreecommitdiffstats
Commit message (Collapse)AuthorAgeFilesLines
...
| * | | we still have issues with call stacksDavid Monniaux2020-01-092-15/+51
| | | |
| * | | moving forward with proofsDavid Monniaux2020-01-092-5/+20
| | | |
| * | | proof for jumptableDavid Monniaux2020-01-091-1/+17
| | | |
| * | | more proofsDavid Monniaux2020-01-091-1/+18
| | | |
| * | | fix bug and forward in proofsDavid Monniaux2020-01-092-2/+18
| | | |
| * | | some more proofDavid Monniaux2020-01-091-3/+53
| | | |
| * | | moving forward with proofsDavid Monniaux2020-01-091-1/+59
| | | |
| * | | fix bug in xfer functionDavid Monniaux2020-01-091-1/+2
| | | |
| * | | progressing in proofsDavid Monniaux2020-01-082-12/+101
| | | |
| * | | moving forward in proofsDavid Monniaux2020-01-081-2/+19
| | | |
| * | | correct semantics for bottomDavid Monniaux2020-01-082-14/+45
| | | |
| * | | progressing towards a proofDavid Monniaux2020-01-082-47/+150
| | | |
| * | | bogus proofDavid Monniaux2020-01-081-0/+141
| | | |
| * | | add an exampleDavid Monniaux2020-01-081-0/+18
| | | |
| * | | connect forward-moves to compilerDavid Monniaux2020-01-086-6/+23
| | | |
| * | | I *think* the transformation is now doneDavid Monniaux2020-01-081-2/+57
| | | |
| * | | transfer functionDavid Monniaux2020-01-081-1/+44
| | | |
| * | | more on semilattices (ADD_BOTTOM)David Monniaux2020-01-081-4/+114
| | | |
| * | | continue implementing semilatticeDavid Monniaux2020-01-081-7/+65
| | | |
| * | | begin latticeDavid Monniaux2020-01-081-0/+57
| |/ /
| * | swap load and store at disjoint offsetsDavid Monniaux2019-12-161-1/+53
| | |
| * | swap stores at disjoint offsetsDavid Monniaux2019-12-161-16/+30
| | |
| * | Merge branch 'master' of https://github.com/AbsInt/CompCert into mppa-workDavid Monniaux2019-12-161-1/+1
| |\|
| | * The SP register has dwarf register number 31.Bernhard Schommer2019-12-111-1/+1
| | |
| * | comment out theorem that cannot be provedDavid Monniaux2019-12-141-29/+33
| | |
| * | store_store_otherDavid Monniaux2019-12-131-1/+84
| | |
| * | progress in chunksDavid Monniaux2019-12-131-45/+9
| | |
| * | swap writes in memoryDavid Monniaux2019-12-131-0/+43
| | |
| * | set_disjointDavid Monniaux2019-12-131-0/+49
| | |
| * | some subgoal was provedDavid Monniaux2019-12-121-6/+61
| | |
| * | begin overlap proofsDavid Monniaux2019-12-111-0/+43
| | |
* | | Fixing is_empty functionCyril SIX2020-01-221-3/+3
| | |
* | | Branch duplication implementationCyril SIX2020-01-221-12/+94
| | |
* | | Set up the groundbase for doing the duplicationCyril SIX2020-01-171-4/+14
| | |
* | | Removed unnecessary .mli file (provoked compilation problems)Cyril SIX2020-01-171-12/+0
| | |
* | | Adding more debug elementsCyril SIX2020-01-151-1/+9
| | |
* | | Typo in printfCyril SIX2020-01-131-1/+1
| | |
* | | Opcode heuristic done for K1cCyril SIX2019-12-163-3/+33
| | |
* | | Stub for opcode heuristicCyril SIX2019-12-163-4/+16
| | |
* | | Fixing loop heuristic for the way CompCert handles loopsCyril SIX2019-12-111-11/+19
| | |
* | | Implemented call, return, store and loop heuristicsCyril SIX2019-12-111-2/+55
| | |
* | | Function to look ahead unconditionallyCyril SIX2019-12-111-0/+12
| | |
* | | Loop headers detection works!Cyril SIX2019-12-111-3/+17
| | |
* | | Dominators approach not working well ==> opting for visit approachCyril SIX2019-12-101-23/+73
| | |
* | | Calcul de dominateurs a l'air de marcherCyril SIX2019-12-101-88/+144
| | |
* | | Merge remote-tracking branch 'refs/remotes/origin/mppa-duplicate-oracle' ↵Cyril SIX2019-12-0924-292/+162
|\ \ \ | | | | | | | | | | | | into mppa-duplicate-oracle
| * | | Merge remote-tracking branch 'origin/mppa-work-upstream-merge' into ↵David Monniaux2019-12-0924-292/+162
| |\| | | | | | | | | | | | | | mppa-duplicate-oracle
| | * | Merge branch 'master' of https://github.com/AbsInt/CompCert into ↵David Monniaux2019-12-097-124/+74
| | |\| | | | | | | | | | | | | mppa-work-upstream-merge
| | | * Allow Coq 8.10.2.Bernhard Schommer2019-12-031-1/+1
| | | |
| | | * Fix for AArch64 alignment problem (#206)Bernhard Schommer2019-11-284-2/+13
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | In addressing modes for load and store instructions, the offset must be a multiple of the memory size being accessed. When accessing global variables, this may not be the case if the alignment of the variable is less than its size. Errors occur at link time. This PR extends the check for a representable offset for the addressing of global variables to also check whether the variable is correctly aligned. Only if both conditions are met can we generate the short sequence Padrp / ADadr. Otherwise we go through the generic loadsymbol sequence.
generated by cgit (git 2.34.1) at 2024-07-08 05:24:26 +0000