aboutsummaryrefslogtreecommitdiffstats
Commit message (Expand)AuthorAgeFilesLines
* CSE2 now uses is_trivial_opDavid Monniaux2020-02-272-3/+22
* Merge branch 'master' of https://github.com/AbsInt/CompCert into dm-cse2David Monniaux2020-02-2764-1168/+975
|\
| * Update the RISC-V calling conventions (#221)Xavier Leroy2020-02-262-137/+149
| * The type of a wide char constant is wchar_t. (#223)Bernhard Schommer2020-02-241-1/+2
| * Platform-independent implementation of Conventions.size_arguments (#222)Xavier Leroy2020-02-247-649/+68
| * AArch64: normalize function return values of small integer typeXavier Leroy2020-02-211-3/+11
| * Cosmetic: in OCaml code, write "open! Module" instead of "open !Module"Xavier Leroy2020-02-215-6/+6
| * Add interoperability test for functions returning small integer typesXavier Leroy2020-02-212-0/+23
| * Support re-normalization of values returned by function callsXavier Leroy2020-02-217-33/+174
| * Refine the type of function results in AST.signatureXavier Leroy2020-02-2143-286/+445
| * More precise determination of small data accesses (#220)Bernhard Schommer2020-02-201-3/+15
| * Support vertical tabs and treat them as whitespace (#218)Bernhard Schommer2020-02-181-1/+1
| * Take the sign into account for int to ptr cast.Bernhard Schommer2020-02-122-2/+3
| * Added base address if needed.Bernhard Schommer2020-02-063-33/+53
| * Compatibility with OCaml 4.10 (#214)Xavier Leroy2020-02-063-7/+7
| * Revised menhirLib autoconfiguration (#331)Xavier Leroy2020-02-053-5/+9
| * Support Coq 8.11.0 (#212)Xavier Leroy2020-02-054-2/+8
| * Incorrect computation of extra stack size for vararg calls in RISC-V (#213)Bernhard Schommer2020-02-051-2/+2
| * Reduce the checking time for the "decidable_equality_from" tacticxavier.leroy2020-01-301-4/+5
* | add hintDavid Monniaux2020-02-051-0/+1
* | wellformed_reg_kill_memDavid Monniaux2020-02-051-1/+17
* | rm useless admitted lemmaDavid Monniaux2020-02-051-5/+0
* | wellformed_reg_kill_reg simpliiedDavid Monniaux2020-02-051-8/+3
* | wellformed_reg_kill_regDavid Monniaux2020-02-051-0/+129
* | progress on wellformed regDavid Monniaux2020-02-053-13/+204
* | wellformedness for reg begins; simplifiedDavid Monniaux2020-02-041-12/+9
* | wellformedness for reg beginsDavid Monniaux2020-02-041-0/+53
* | kill memory focusedDavid Monniaux2020-02-042-20/+46
* | invariant guaranteedDavid Monniaux2020-02-042-4/+56
* | wellformedness for memoryDavid Monniaux2020-02-042-17/+158
* | begin well formednessDavid Monniaux2020-02-042-15/+130
* | gremove_tDavid Monniaux2020-02-041-0/+36
* | gcombine_nullDavid Monniaux2020-02-041-0/+13
* | gcombine_nullDavid Monniaux2020-02-041-1/+39
* | 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
* | forgot a "in *"David Monniaux2020-01-281-20/+1
* | 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-286-8/+51
* | 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
generated by cgit (git 2.34.1) at 2024-07-03 01:02:39 +0000