aboutsummaryrefslogtreecommitdiffstats
Commit message (Expand)AuthorAgeFilesLines
* Compile with value analysisdev-initial-blocksYann Herklotz2020-06-217-41/+125
* Factor out addressing checks, check signed range.James Pollard2020-06-211-10/+17
* Lea op now checks alignment.James Pollard2020-06-211-12/+15
* Finish structure of Aindexed2scaled ILoad proof.James Pollard2020-06-202-14/+177
* Working on proof.James Pollard2020-06-191-10/+86
* Enforce stack size alignment to fix proof.James Pollard2020-06-183-10/+22
* Tidy up proof.James Pollard2020-06-182-13/+16
* Finish AInStack proof with minor assertions.James Pollard2020-06-181-32/+21
* Fix up ILoad proof.James Pollard2020-06-181-95/+58
* Fix array semantics behaviour for undefined values.James Pollard2020-06-181-1/+1
* Fix Inop proof to work with new array semantics.James Pollard2020-06-172-7/+44
* Some (very) useful lemmas about arrays.James Pollard2020-06-173-7/+139
* Use NBAs for loads and stores.James Pollard2020-06-172-4/+4
* Fix array semantics merge granularity.James Pollard2020-06-174-30/+87
* Array semantics now uses dependent Array type.James Pollard2020-06-145-49/+50
* Move some standard tactics to Coquplib.James Pollard2020-06-141-0/+10
* Add a basic length-indexed list type.James Pollard2020-06-131-0/+123
* Merge branch 'develop' into arrays-proofJames Pollard2020-06-123-4/+27
|\
| * Update matrix and use 32 bitYann Herklotz2020-06-123-12/+14
| * Add matrix testYann Herklotz2020-06-121-0/+21
* | Fix broken proof.James Pollard2020-06-121-4/+4
* | Merge branch 'master' into arrays-proofJames Pollard2020-06-121-4/+6
|\|
| * Merge pull request #7 from p0llard/hotfixYann Herklotz2020-06-121-4/+6
| |\
| | * Fix addressing bug.James Pollard2020-06-121-4/+6
| |/
* | Merge branch 'master' into arrays-proofJames Pollard2020-06-1234-1046/+19571
|\|
| * Add declaration of loadsYann Herklotz2020-06-122-4/+6
| * Merge branch 'master' of github.com:ymherklotz/CoqUpYann Herklotz2020-06-1215-0/+19189
| |\
| | * Merge pull request #6 from ymherklotz/branch_jcYann Herklotz2020-06-1215-0/+19189
| | |\
| | | * fixed my grammarJianyi Cheng2020-06-121-2/+2
| | | * Adding benchmarks to branch_jcJianyi Cheng2020-06-1215-0/+19189
| | |/
| * / Fix declaring function arguments correctlyYann Herklotz2020-06-123-12/+69
| |/
| * Add function call testYann Herklotz2020-06-121-0/+10
| * Update compcert to always inline functionsYann Herklotz2020-06-121-0/+0
| * Fix main functionYann Herklotz2020-06-121-17/+3
| * Add array to testYann Herklotz2020-06-122-1/+5
| * Fix printing of Verilog with new datatypesYann Herklotz2020-06-122-17/+27
| * Remove Verilog proofsYann Herklotz2020-06-123-133/+10
| * Declare all registers properly in HTLYann Herklotz2020-06-123-51/+95
| * Remove extraction of simulatorYann Herklotz2020-06-121-2/+2
| * Fix top level invocation to translate through HTLYann Herklotz2020-06-122-4/+8
| * Remove Test.vYann Herklotz2020-06-121-99/+0
| * Generate Verilog from HTLYann Herklotz2020-06-122-713/+154
| * Merge pull request #5 from p0llard/arrays-proofYann Herklotz2020-06-107-351/+643
| |\
* | | Some work on store proof.James Pollard2020-06-121-11/+38
* | | Rough outline of stack address proofJames Pollard2020-06-113-34/+109
* | | Working on proof.James Pollard2020-06-115-47/+156
| |/ |/|
* | Start fixing proofJames Pollard2020-06-091-94/+116
* | Fix automation tactic for modified constructorJames Pollard2020-06-091-2/+4
* | Start extending HTL proof to cover arrays.James Pollard2020-06-091-18/+31
* | Merge branch 'develop' into arrays-proofJames Pollard2020-06-098-56/+1160
|\|
generated by cgit (git 2.34.1) at 2024-05-21 19:54:42 +0000