|
|
@535
|
10 years |
campbell |
Minimal integration of bitvectors into Clight semantics
- does a …
|
|
|
@534
|
10 years |
campbell |
Fix a couple of bugs with branched 4.1 stuff.
|
|
|
@533
|
10 years |
campbell |
Make stuff from D4.1 work with my copy of matita.
|
|
|
@532
|
10 years |
mulligan |
after much faffing, top of minipages now align correctly
|
|
|
@531
|
10 years |
campbell |
Create temporary branch of D4.1 matita development to help integrate …
|
|
|
@530
|
10 years |
sacerdot |
8051/MIPS
|
|
|
@529
|
10 years |
mulligan |
wrote about cost labels
|
|
|
@528
|
10 years |
mulligan |
Removed all \begin{quote} .. \end{quote} around code snippets for …
|
|
|
@527
|
10 years |
mulligan |
added section on representation of integers
|
|
|
@526
|
10 years |
sacerdot |
Something to say in the comparison.
|
|
|
@525
|
10 years |
mulligan |
lots of changes
|
|
|
@524
|
10 years |
mulligan |
Finished discussion of anatomy of emulator
|
|
|
@523
|
10 years |
mulligan |
added a small reference to cost labels, along with a pointer to the …
|
|
|
@522
|
10 years |
mulligan |
completed changes to discussion on labels and pseudoinstructions
|
|
|
@521
|
10 years |
mulligan |
more changes
|
|
|
@520
|
10 years |
mulligan |
more changes
|
|
|
@519
|
10 years |
mulligan |
Footnote fixed
|
|
|
@518
|
10 years |
mulligan |
small changes
|
|
|
@517
|
10 years |
mulligan |
more added
|
|
|
@516
|
10 years |
mulligan |
Added section on Tries
|
|
|
@515
|
10 years |
mulligan |
finished tidying the introduction
|
|
|
@514
|
10 years |
mulligan |
more tidying
|
|
|
@513
|
10 years |
mulligan |
more changes to intro
|
|
|
@512
|
10 years |
mulligan |
tidy up of the intro
|
|
|
@511
|
10 years |
mulligan |
validation section complete
|
|
|
@510
|
10 years |
mulligan |
more added, talking about dependent types now
|
|
|
@509
|
10 years |
sacerdot |
Background.
|
|
|
@508
|
10 years |
mulligan |
Changes
|
|
|
@507
|
10 years |
mulligan |
A bit on labels and pseudo-instructions
|
|
|
@506
|
10 years |
mulligan |
a bit more added
|
|
|
@505
|
10 years |
mulligan |
finished sentence
|
|
|
@504
|
10 years |
mulligan |
work on intro committed following claudio's second e-mail
|
|
|
@503
|
10 years |
mulligan |
Added PNG files for claudio.
|
|
|
@502
|
10 years |
campbell |
Fix not on nulls on Clight.
|
|
|
@501
|
10 years |
mulligan |
more changes
|
|
|
@500
|
10 years |
campbell |
Use dependent pointer type to ensure that the representation is always …
|
|
|
@499
|
10 years |
campbell |
pointer_compat is a little more natural if it takes that block rather …
|
|
|
@498
|
10 years |
campbell |
Make block type a little more abstract; remove knowledge about the old …
|
|
|
@497
|
10 years |
campbell |
Remove bogus pointer compatibility case.
|
|
|
@496
|
10 years |
campbell |
First pass at moving regions to block type.
|
|
|
@495
|
10 years |
mulligan |
more added
|
|
|
@494
|
10 years |
mulligan |
more added
|
|
|
@493
|
10 years |
mulligan |
incorporated some text from the eu report that needs to be pared down
|
|
|
@492
|
10 years |
mulligan |
Initial commit of outline of prospective itp-2011 paper.
|
|
|
@491
|
10 years |
mulligan |
Initial commit of (part)-formalisation of LIN intermediate language.
|
|
|
@490
|
10 years |
campbell |
Update syntax of Matita Clight term printer.
|
|
|
@489
|
10 years |
campbell |
Pointer fixes for the temporary version of the compiler that can …
|
|
|
@488
|
10 years |
campbell |
Some missing equality constants used by destruct.
|
|
|
@487
|
10 years |
campbell |
Port Clight semantics to the new-new matita syntax.
|
|
|
@486
|
10 years |
ayache |
Deliverable D2.2
|
|
|
@485
|
10 years |
campbell |
Fix treatment of pointers in initialisation data, a little like later …
|
|
|
@484
|
10 years |
campbell |
Separate out null values from integer zeros.
|
|
|
@483
|
10 years |
campbell |
Use pointer-specific "chunks" of memory for pointer loads and stores, …
|
|
|
@482
|
10 years |
campbell |
Note the purpose of the region in a pointer value.
|
|
|
@481
|
10 years |
campbell |
Tcomp_ptr should take the memory region and use that to calculate its size.
|
|
|
@480
|
10 years |
campbell |
"memory_space" to "region" replacement to match ocaml code
|
|
|
@479
|
10 years |
campbell |
Test of linked list insertion sort.
|
|
|
@478
|
10 years |
campbell |
Prevent clashes between names in AST and other parts of the …
|
|
|
@477
|
10 years |
mulligan |
Added file for LIN.
|
|
|
@476
|
10 years |
mulligan |
Commiting directory for formalization of intermediate compiler languages.
|
|
|
@475
|
10 years |
mulligan |
Matita interpreter ported to latest version of matita (the one with …
|
|
|
@474
|
10 years |
campbell |
Reduce "include"s to reduce compilation time.
(Will be undone when …
|
|
|
@473
|
10 years |
campbell |
Track changes in nlibrary list-theory.ma -> list.ma
|
|
|
@472
|
10 years |
mulligan |
More changes to debug and testing files to get them to work with the …
|
|
|
@471
|
10 years |
mulligan |
Deleted (now) superfluous custom library files in favour of using …
|
|
|
@470
|
10 years |
mulligan |
Finished moving development over to standard library.
|
|
|
@469
|
10 years |
campbell |
Update work-in-progress file to match current development.
|
|
|
@468
|
10 years |
campbell |
Missing changes to completeness proof for function pointer type fix.
|
|
|
@467
|
10 years |
campbell |
Update some of the commented-out parts of Globalenvs for testing.
|
|
|
@466
|
10 years |
mulligan |
Most of execute_1 checked. Need to fix negations, though, in rest in …
|
|
|
@465
|
10 years |
mulligan |
Moved over to standard library.
|
|
|
@464
|
10 years |
mulligan |
Fixed strange bug/typo in BitVectorTrie?.ma
|
|
|
@463
|
10 years |
mulligan |
Fixed DoTest? so that it doesn't take an hour to typecheck.
|
|
|
@462
|
10 years |
mulligan |
Added bitvector arithmetic for Brian.
|
|
|
@461
|
10 years |
campbell |
Handle null pointer constants properly for generic pointers …
|
|
|
@460
|
10 years |
campbell |
Port memory spaces changes to latest prototype compiler.
|
|
|
@459
|
10 years |
campbell |
Create branch of the prototype compiler for memory space support
|
|
|
@458
|
10 years |
campbell |
Add a few more pointer tests.
|
|
|
@457
|
10 years |
campbell |
Correct checking of function pointers.
|
|
|
@456
|
10 years |
campbell |
Add 24bit initialisation data for null generic pointers.
|
|
|
@455
|
10 years |
mulligan |
Merge commit.
|
|
|
@454
|
10 years |
sacerdot |
CSC + Nicolas + Dominic:
1) back-porting of changes by Nicolas from …
|
|
|
@453
|
10 years |
ayache |
Import of the Paris's sources.
|
|
|
@452
|
10 years |
mulligan |
Added function to interface.
|
|
|
@451
|
10 years |
mulligan |
Removed more debugging stuff from Test.ml.
|
|
|
@450
|
10 years |
mulligan |
Comment added for Nicolas.
|
|
|
@449
|
10 years |
mulligan |
Removed debugging code from Test.ml.
|
|
|
@448
|
10 years |
mulligan |
Got Intel HEX format exportation working.
|
|
|
@447
|
10 years |
mulligan |
Checksum seems to be working now on most lines, barring three? Weird bug.
|
|
|
@446
|
10 years |
mulligan |
Checksum calculation added. Seems to still be buggy.
|
|
|
@445
|
10 years |
mulligan |
Debugging hex output. Seems mcu8051 really doesn't like what's been …
|
|
|
@444
|
10 years |
mulligan |
Got Test.native to compile. Added functions for exporting intel hex …
|
|
|
@443
|
10 years |
mulligan |
Wrote exportation code. Need to test it.
|
|
|
@442
|
10 years |
mulligan |
Partial implementation of Nicolas' requested feature (extraction of …
|
|
|
@441
|
10 years |
mulligan |
Fixed bug in PUSH spotted by Nicolas.
|
|
|
@440
|
10 years |
mulligan |
indentation changes by emacs
|
|
|
@439
|
10 years |
mulligan |
Changes to get everything to compile.
|
|
|
@438
|
10 years |
sacerdot |
Final version.
|
|
|
@437
|
10 years |
sacerdot |
1. new function assembly_unlabelled_program
2. the new function is now …
|
|
|
@436
|
10 years |
sacerdot |
…
|
|
|