aboutsummaryrefslogtreecommitdiffstats
Commit message (Collapse)AuthorAgeFilesLines
* 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
| | | | progress
* sem_rel_b_geDavid Monniaux2020-01-281-18/+77
|
* CSE2 split in two filesDavid Monniaux2020-01-283-827/+838
|
* 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 __builtin_nop from list of x86 builtins.Bernhard Schommer2020-01-031-3/+0
|
* Revert "Remove `__builtin_nop` for some architectures. (#208)"Bernhard Schommer2020-01-0314-3/+33
| | | | This reverts commit 4dfcd7d4be18e8bc437ca170782212aa06635a95.
* Added error for unknown builtin functions. (#208)Bernhard Schommer2019-12-211-1/+6
| | | | | | | | | Previously, using an unknown builtin function was treated like any other call to an undeclared function: a warning was emitted, and an error occurred at link-time. With this commit, using an unknown builtin function is an error, like in Clang.
* Remove `__builtin_nop` for some architectures. (#208)Bernhard Schommer2019-12-2114-33/+3
| | | | | | | The `__builtin_nop` function is documented only for PowerPC. It was added to the other architectures by copy paste, but has no known uses. So, remove `__builtin_nop` from all architectures but PowerPC.
* The SP register has dwarf register number 31.Bernhard Schommer2019-12-111-1/+1
|
* 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.
* Added dwarf register numbers for aarch64Bernhard Schommer2019-11-281-3/+18
|
* Added back unused_ais_parameter warning.Bernhard Schommer2019-11-261-0/+1
|
* Simplified diagnostics module.Bernhard Schommer2019-11-251-118/+41
| | | | | | | Instead of constructing four different lists for maintaining the state of the warnings only one list is now used. This list contains the name of the warning and a boolean indicating whether this option should be active by default. The rest is computed from this list.
* Remove no longer needed file PrintLTLinBernhard Schommer2019-11-121-115/+0
|
* Use `intuition idtac` instead of `intuition` (#321)Vincent Laporte2019-11-121-1/+1
| | | | A stronger `intuition` in the near future would break this use of `intuition`.
* Raise minimal required versions for OCaml and Coq (#203)Bernhard Schommer2019-10-311-9/+4
| | | At least OCaml 4.05 is now required as well as Coq 8.8.
generated by cgit (git 2.34.1) at 2024-07-07 00:21:02 +0000