aboutsummaryrefslogtreecommitdiffstats
path: root/backend/CSE2proof.v
Commit message (Expand)AuthorAgeFilesLines
* Porting the BTL non-trap loads approach to RTLLéo Gourdin2021-11-021-191/+191
* Replacing default notrap load value by Vundef everywherecsix-PhDCyril SIX2021-06-181-2/+2
* Adding copyrightsCyril SIX2020-05-041-0/+12
* forward moves into store sourceDavid Monniaux2020-04-201-1/+4
* refine the rules for builtinsDavid Monniaux2020-04-161-4/+19
* progress on CSE2 builtinsDavid Monniaux2020-04-161-5/+15
* forgot an 'Admitted'David Monniaux2020-03-311-1/+1
* Merge remote-tracking branch 'origin/mppa-work' into mppa-cse2David Monniaux2020-03-111-1/+4
|\
| * remet is_trivial_op dans CSE2David Monniaux2020-03-111-1/+4
* | same version as in dm-cse2David Monniaux2020-03-031-24/+24
|/
* fixed CSE2 for mppa_k1cDavid Monniaux2020-03-031-668/+160
|\
| * CSE2 alias analysis for Risc-VDavid Monniaux2020-03-031-1/+1
| * moved away x86-dependent partsDavid Monniaux2020-03-031-38/+0
| * modularize proofDavid Monniaux2020-03-031-29/+10
| * may_overlap_soundDavid Monniaux2020-03-031-0/+38
| * starting to move x86 stuff to x86David Monniaux2020-03-031-201/+1
| * offsets in globals for x86David Monniaux2020-03-031-1/+78
| * globals alias analysis for x86David Monniaux2020-03-031-10/+57
| * with indexed/indexed alias analysis for x86David Monniaux2020-03-031-2/+2
| * 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-021-13/+19
| * works on x86 x86_64David Monniaux2020-03-021-29/+47
| * playing with offsetsDavid Monniaux2020-03-021-1/+67
* | Merge branch 'mppa-cse2' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCe...David Monniaux2020-03-031-78/+430
|\ \
| * | CSE2 with NOTRAPDavid Monniaux2020-02-031-91/+184
| * | NOTRAP in CSE2: progressDavid Monniaux2020-02-031-31/+259
| * | Merge branch 'dm-cse2' of /home/monniaux/progs/CompCert/dm-cse2 into mppa-cse2David Monniaux2020-02-031-18/+18
| |\|
| * | Merge branch 'dm-cse2' of /home/monniaux/progs/CompCert/dm-cse2 into mppa-cse2David Monniaux2020-02-031-0/+8
| |\ \
| * | | Merge branch 'dm-cse2' of /home/monniaux/progs/CompCert into mppa-cs2David Monniaux2020-01-281-65/+96
* | | | CSE2 now uses is_trivial_opDavid Monniaux2020-02-271-2/+21
* | | | 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-051-0/+32
* | | | wellformedness for reg begins; simplifiedDavid Monniaux2020-02-041-12/+9
* | | | wellformedness for reg beginsDavid Monniaux2020-02-041-0/+53
* | | | kill memory focusedDavid Monniaux2020-02-041-19/+45
* | | | invariant guaranteedDavid Monniaux2020-02-041-3/+53
* | | | wellformedness for memoryDavid Monniaux2020-02-041-13/+152
* | | | begin well formednessDavid Monniaux2020-02-041-0/+98
* | | | stuff information into a recordDavid Monniaux2020-02-041-20/+30
| |_|/ |/| |
* | | another version of proof that allows Vundef in loaded valuesDavid Monniaux2020-02-031-18/+18
| |/ |/|
* | commentsDavid Monniaux2020-02-031-0/+8
|/
* with loads too ?David Monniaux2020-01-281-6/+67
* load_soundDavid Monniaux2020-01-281-0/+96
* find_load_soundDavid Monniaux2020-01-281-4/+92
generated by cgit (git 2.34.1) at 2024-05-09 09:02:44 +0000