aboutsummaryrefslogtreecommitdiffstats
Commit message (Expand)AuthorAgeFilesLines
* simplifying the translation, external calls + cfi_step on builtinsSylvain Boulmé2020-04-153-197/+128
* Adjust comment to reflect progress on cfi_stepJustus Fasse2020-04-121-24/+0
* Add exec_MBjumptable to PseudoAsmblock.cfi_stepJustus Fasse2020-04-122-1/+26
* Add exec_MBcond_false to PseudoAsmblock.cfi_stepJustus Fasse2020-04-122-1/+11
* Add exec_MBcond_true to PseudoAsmblock.cfi_stepJustus Fasse2020-04-122-4/+24
* Add exec_MBtailcall to PseudoAsmblock.cfi_stepJustus Fasse2020-04-102-11/+16
* exit_step_simulation: finish MBgoto caseJustus Fasse2020-04-081-1/+3
* Merge branch 'PseudoAsmblock' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/C...Justus Fasse2020-04-061-12/+6
|\
| * with a little help of [your] friend[].Sylvain Boulmé2020-04-061-12/+6
* | exit_step_simulation: finish MBcall caseJustus Fasse2020-04-061-4/+5
|/
* Progress on match_states of exit_step_simulationJustus Fasse2020-04-031-4/+22
* Modest progress in exit_step_simulationJustus Fasse2020-03-301-1/+40
* Adjust basic_step_simulation proofJustus Fasse2020-03-271-9/+6
* easy case of exit_step_simulationSylvain Boulmé2020-03-231-0/+6
* suggestion of exit_step_simulation lemmaSylvain Boulmé2020-03-231-29/+31
* Stuck on next step of `inst_step_simulation`Justus Fasse2020-03-191-3/+23
* Finish proof for basic_step_simulationJustus Fasse2020-03-121-8/+29
* Continuation of basic_step_simulationJustus Fasse2020-03-121-1/+38
* Live proving demonstration by Sylvain.Justus Fasse2020-03-121-1/+55
* fix copy-paste error from PseudoAsmproofSylvain Boulmé2020-03-111-1/+1
* move PseudoAsmblock proof in a separate fileSylvain Boulmé2020-03-113-324/+792
* starting the PseudoAsmblock proofSylvain Boulmé2020-03-091-7/+102
* Merge branch 'mppa-work' into PseudoAsmblockSylvain Boulmé2020-03-096-7/+15
|\
| * removing more coq8.10 warningsSylvain Boulmé2020-03-094-2/+10
| * removing some coqc 8.10 warningsSylvain Boulmé2020-03-092-5/+5
* | start PseudoAsmblockSylvain Boulmé2020-03-093-1/+550
|/
* removing warnings on hints in coreSylvain Boulmé2020-03-0711-42/+39
* fix for ppcDavid Monniaux2020-03-031-14/+22
* try to get it to compileDavid Monniaux2020-03-031-0/+1
* forgot k1CDavid Monniaux2020-03-032-0/+147
* fixes for risc-VDavid Monniaux2020-03-031-1/+1
* fix for aarch64David Monniaux2020-03-031-11/+9
* ported to armDavid Monniaux2020-03-031-9/+6
* ported for ppcDavid Monniaux2020-03-031-22/+17
* fix for risc-VDavid Monniaux2020-03-031-9/+7
* adjust for x86David Monniaux2020-03-031-44/+35
* fixed CSE2 for mppa_k1cDavid Monniaux2020-03-0324-843/+1266
|\
| * CSE2 with alias analysisDavid Monniaux2020-03-031-0/+20
| * CSE2 for powerpcDavid Monniaux2020-03-032-0/+152
| * aarch64David Monniaux2020-03-032-0/+150
| * CSE2 for ARMDavid Monniaux2020-03-031-0/+132
| * better 32/64-bit handlingDavid Monniaux2020-03-032-26/+51
| * CSE2 alias analysis for Risc-VDavid Monniaux2020-03-036-30/+158
| * moved away x86-dependent partsDavid Monniaux2020-03-032-38/+46
| * modularize proofDavid Monniaux2020-03-031-29/+10
| * may_overlap_soundDavid Monniaux2020-03-031-0/+38
| * starting to move x86 stuff to x86David Monniaux2020-03-032-201/+216
| * offsets in globals for x86David Monniaux2020-03-032-2/+82
| * globals alias analysis for x86David Monniaux2020-03-033-10/+67
| * with indexed/indexed alias analysis for x86David Monniaux2020-03-033-4/+32
generated by cgit (git 2.34.1) at 2024-07-14 03:17:51 +0000