source: src/ASM @ 927

Name Size Rev Age Author Last Change
../
CPP2011 927   9 years mulligan changes
Arithmetic.ma 10.6 KB ​ 744   9 years campbell Evict Coq-style integers from common/Integers.ma. Make more bitvector …
ASM.ma 8.7 KB ​ 832   9 years mulligan work from today
Assembly.ma 36.1 KB ​ 922   9 years mulligan changes to get assemblyproof to compile
AssemblyProof.ma 59.6 KB ​ 926   9 years sacerdot Main theorem false because of ticks :-(
BitVector.ma 4.2 KB ​ 868   9 years mulligan more changes
BitVectorTrie.ma 4.1 KB ​ 782   9 years mulligan More work on rtl-ertl pass from today, plus resolved conflict.
BitVectorZ.ma 4.0 KB ​ 891   9 years campbell Revise proofs affected by recent matita change.
Char.ma 76 bytes ​ 697   9 years campbell Merge Clight branch of vectors and friends. Start making stuff build.
Fetch.ma 22.0 KB ​ 895   9 years sacerdot Fetch function fixed: alla AJMPS were ACALL (and the other way around) …
I8051.ma 135.3 KB ​ 777   9 years mulligan Lots of work on RTL to ERTL pass from today.
Interpret.ma 28.7 KB ​ 910   9 years mulligan removed bug in execute_1_pseudoinstruction
README 641 bytes ​ 431   9 years mulligan - README updated - Test and DoTest? fixed to work on assembly_program - …
Status.ma 36.1 KB ​ 911   9 years sacerdot Type of set_code_memory generalized.
String.ma 84 bytes ​ 698   9 years mulligan Commit with changes to files to get our files to typecheck.
Util.ma 8.7 KB ​ 907   9 years boender - added quadruples to Util - start of implementation of new jump …
Vector.ma 16.5 KB ​ 889   9 years sacerdot Minor changes because of the new, weaker (but much faster) delift.
Note: See TracBrowser for help on using the repository browser.