|
../
|
|
CPP2012-policy
|
|
2099
|
9 years
|
boender |
- added reference to Intel dev manual
|
|
CPP2012-asm
|
|
2327
|
8 years
|
mulligan |
Fixed typos in paper highlighted by referees. More substantial …
|
|
CPP2011
|
|
1033
|
10 years
|
sacerdot |
ispelled & submitted
|
|
AssemblyProofSplit.ma
|
119.7 KB
|
2516
|
8 years
|
mckinna |
removed typedefs; restored older versions; moved typedefs to …
|
|
BitVectorTrie.ma
|
26.6 KB
|
2767
|
8 years
|
mckinna |
WARNING: BIG commit, which pushes code_size_opt check into …
|
|
CodeMemory.ma
|
8.5 KB
|
2767
|
8 years
|
mckinna |
WARNING: BIG commit, which pushes code_size_opt check into …
|
|
README
|
641 bytes
|
431
|
10 years
|
mulligan |
- README updated
- Test and DoTest? fixed to work on assembly_program
- …
|
|
AbstractStatus.ma
|
2.0 KB
|
2899
|
8 years
|
sacerdot |
1. some renaming ASM_xxx to OC_xxx
2. ASM_pre_classified_system …
|
|
ASM.ma
|
38.7 KB
|
2999
|
8 years
|
sacerdot |
code_memory added to labelled_object_code to avoid recomputing it …
|
|
ASMCosts.ma
|
36.3 KB
|
2999
|
8 years
|
sacerdot |
code_memory added to labelled_object_code to avoid recomputing it …
|
|
ASMCostsSplit.ma
|
11.3 KB
|
2999
|
8 years
|
sacerdot |
code_memory added to labelled_object_code to avoid recomputing it …
|
|
Assembly.ma
|
58.5 KB
|
2999
|
8 years
|
sacerdot |
code_memory added to labelled_object_code to avoid recomputing it …
|
|
AssemblyProof.ma
|
54.1 KB
|
2899
|
8 years
|
sacerdot |
1. some renaming ASM_xxx to OC_xxx
2. ASM_pre_classified_system …
|
|
AssemblyProofSplitSplit.ma
|
15.4 KB
|
2899
|
8 years
|
sacerdot |
1. some renaming ASM_xxx to OC_xxx
2. ASM_pre_classified_system …
|
|
BitVector.ma
|
7.1 KB
|
2782
|
8 years
|
sacerdot |
1. Paolo's bv_of_nat/nat_of_bv in BitVector? used to work with the …
|
|
CostsProof.ma
|
31.2 KB
|
2999
|
8 years
|
sacerdot |
code_memory added to labelled_object_code to avoid recomputing it …
|
|
Fetch.ma
|
30.2 KB
|
2999
|
8 years
|
sacerdot |
code_memory added to labelled_object_code to avoid recomputing it …
|
|
FoldStuff.ma
|
1.7 KB
|
1600
|
9 years
|
sacerdot |
utilities and ASM ported to the new standard library
|
|
I8051.ma
|
4.6 KB
|
2645
|
8 years
|
sacerdot |
1. some broken back-end files repaires, several still to go
2. the …
|
|
I8051bis.ma
|
125 bytes
|
1415
|
9 years
|
sacerdot |
1. hwreg_store/retrieve no longer returns a res (but it is still …
|
|
Interpret2.ma
|
5.0 KB
|
2999
|
8 years
|
sacerdot |
code_memory added to labelled_object_code to avoid recomputing it …
|
|
Interpret.ma
|
60.3 KB
|
2906
|
8 years
|
sacerdot |
Bug fixed.
|
|
Policy.ma
|
35.4 KB
|
2771
|
8 years
|
sacerdot |
Some speed up in Policy.ma.
|
|
PolicyFront.ma
|
33.4 KB
|
2713
|
8 years
|
sacerdot |
PolicyFront?.ma repaired
|
|
PolicyStep.ma
|
59.8 KB
|
2714
|
8 years
|
sacerdot |
PolicyStep?.ma repaired
|
|
Status.ma
|
36.3 KB
|
2907
|
8 years
|
sacerdot |
1. a few bugs fixed
2. as_return implemented for ASM & OC
|
|
StatusProofs.ma
|
13.5 KB
|
2285
|
8 years
|
sacerdot |
1. duplicated code erased
2. POP case finished up to lemmas on …
|
|
StatusProofsSplit.ma
|
20.3 KB
|
2285
|
8 years
|
sacerdot |
1. duplicated code erased
2. POP case finished up to lemmas on …
|
|
Test.ma
|
92.8 KB
|
2284
|
8 years
|
sacerdot |
PUSH finished
|
|
Util.ma
|
41.5 KB
|
2700
|
8 years
|
sacerdot |
1. exponential function dropped in favour of standard library
2. …
|
|
UtilBranch.ma
|
2.4 KB
|
2702
|
8 years
|
sacerdot |
1. proof closed in ASM/UtilBranch
2. more passes integrated in the …
|
|
WellLabeled.ma
|
6.8 KB
|
2710
|
8 years
|
sacerdot |
ASMCosts.ma repaired
|
|
Arithmetic.ma
|
38.3 KB
|
2796
|
8 years
|
tranquil |
* added global notation for existence in Type[1] (\exists[1] x.P)
* in …
|
|
BitVectorZ.ma
|
4.3 KB
|
2200
|
9 years
|
tranquil |
* updated joint semantics: generation of linear and graph semantics
* …
|
|
Vector.ma
|
34.9 KB
|
2286
|
8 years
|
tranquil |
Big update!
* merge of all _paolo variants
* reorganised some depends …
|
