aboutsummaryrefslogtreecommitdiffstats
path: root/backend
Commit message (Expand)AuthorAgeFilesLines
* invariant guaranteedDavid Monniaux2020-02-042-4/+56
* wellformedness for memoryDavid Monniaux2020-02-042-17/+158
* begin well formednessDavid Monniaux2020-02-042-15/+130
* stuff information into a recordDavid Monniaux2020-02-042-46/+63
* another version of proof that allows Vundef in loaded valuesDavid Monniaux2020-02-031-18/+18
* commentsDavid Monniaux2020-02-032-0/+14
* with loads too ?David Monniaux2020-01-282-8/+119
* load_soundDavid Monniaux2020-01-281-0/+96
* find_load_soundDavid Monniaux2020-01-281-4/+92
* begin adding loadsDavid Monniaux2020-01-281-2/+7
* much better - seems to eliminate CSE not containing loadsDavid Monniaux2020-01-282-2/+18
* still buggyDavid Monniaux2020-01-282-56/+95
* connected (just a silly problem)David Monniaux2020-01-281-2/+8
* CSE2 now works for expressionsDavid Monniaux2020-01-282-47/+69
* now going back to opDavid Monniaux2020-01-281-45/+6
* reworkDavid Monniaux2020-01-281-20/+49
* sem_rel_b_geDavid Monniaux2020-01-281-61/+152
* sem_rel_b_geDavid Monniaux2020-01-281-18/+77
* CSE2 split in two filesDavid Monniaux2020-01-282-827/+837
* progressDavid Monniaux2020-01-271-0/+467
* use in transformationDavid Monniaux2020-01-271-3/+21
* find_op_soundDavid Monniaux2020-01-271-1/+110
* goes to the end but does not find available opsDavid Monniaux2020-01-271-13/+5
* simpler definitionsDavid Monniaux2020-01-271-41/+24
* static analysis doneDavid Monniaux2020-01-271-20/+7
* kill_mem_soundDavid Monniaux2020-01-271-8/+59
* renamed kill_reg into kill_memDavid Monniaux2020-01-271-11/+11
* gen_oper_soundDavid Monniaux2020-01-271-1/+37
* oper_soundDavid Monniaux2020-01-271-0/+27
* oper1_soundDavid Monniaux2020-01-271-1/+10
* arg replaceDavid Monniaux2020-01-271-1/+87
* move soundDavid Monniaux2020-01-271-19/+85
* begin proving stuffDavid Monniaux2020-01-271-0/+436
* Remove no longer needed file PrintLTLinBernhard Schommer2019-11-121-115/+0
* Make explicit the use of hints from OrderedType (#316)Vincent Laporte2019-10-022-8/+8
* Reworked json export.Bernhard Schommer2019-09-123-29/+37
* Fix compile for architectures other than AArch64 (#192)Bernhard Schommer2019-08-171-2/+2
* AArch64 portXavier Leroy2019-08-087-37/+97
* Asmgenproof0: add predicate exec_straight0Xavier Leroy2019-08-071-0/+26
* Coq 8.10 compatibility: make explicit the "core" hint databaseXavier Leroy2019-08-071-2/+0
* Improve CSE for known built-in functionsXavier Leroy2019-07-172-7/+14
* Perform constant propagation for known built-in functionsXavier Leroy2019-07-174-16/+168
* Give formal semantics to some built-in functions and run-time functionsXavier Leroy2019-07-173-112/+231
* Compatibility with OCaml 4.08 (#302)Xavier Leroy2019-07-086-7/+6
* Rename option `-ffavor-branchless` into `-Obranchless`Xavier Leroy2019-07-051-3/+3
* Extended asm: print register names according to their typesXavier Leroy2019-06-171-9/+14
* Cminortyping: relax typechecking of function callsXavier Leroy2019-06-061-12/+15
* If-conversion optimizationXavier Leroy2019-06-064-72/+584
* Type inference and type checking for CminorXavier Leroy2019-06-061-0/+797
* Fix misspellings in messages, man pages, and commentsXavier Leroy2019-05-314-5/+5
generated by cgit (git 2.34.1) at 2024-07-02 09:40:39 +0000