|
|
|
@547
|
9 years |
campbell |
Add missing file.
|
|
|
|
@535
|
9 years |
campbell |
Minimal integration of bitvectors into Clight semantics
- does a …
|
|
|
|
@534
|
9 years |
campbell |
Fix a couple of bugs with branched 4.1 stuff.
|
|
|
|
@533
|
9 years |
campbell |
Make stuff from D4.1 work with my copy of matita.
|
|
|
|
@531
|
9 years |
campbell |
Create temporary branch of D4.1 matita development to help integrate …
|
|
|
|
@502
|
9 years |
campbell |
Fix not on nulls on Clight.
|
|
|
|
@500
|
9 years |
campbell |
Use dependent pointer type to ensure that the representation is always …
|
|
|
|
@499
|
9 years |
campbell |
pointer_compat is a little more natural if it takes that block rather …
|
|
|
|
@498
|
9 years |
campbell |
Make block type a little more abstract; remove knowledge about the old …
|
|
|
|
@497
|
9 years |
campbell |
Remove bogus pointer compatibility case.
|
|
|
|
@496
|
9 years |
campbell |
First pass at moving regions to block type.
|
|
|
|
@488
|
9 years |
campbell |
Some missing equality constants used by destruct.
|
|
|
|
@487
|
9 years |
campbell |
Port Clight semantics to the new-new matita syntax.
|
|
|
|
@485
|
9 years |
campbell |
Fix treatment of pointers in initialisation data, a little like later …
|
|
|
|
@484
|
9 years |
campbell |
Separate out null values from integer zeros.
|
|
|
|
@483
|
9 years |
campbell |
Use pointer-specific "chunks" of memory for pointer loads and stores, …
|
|
|
|
@482
|
9 years |
campbell |
Note the purpose of the region in a pointer value.
|
|
|
|
@481
|
9 years |
campbell |
Tcomp_ptr should take the memory region and use that to calculate its size.
|
|
|
|
@480
|
9 years |
campbell |
"memory_space" to "region" replacement to match ocaml code
|
|
|
|
@479
|
9 years |
campbell |
Test of linked list insertion sort.
|
|
|
|
@478
|
9 years |
campbell |
Prevent clashes between names in AST and other parts of the …
|
|
|
|
@474
|
9 years |
campbell |
Reduce "include"s to reduce compilation time.
(Will be undone when …
|
|
|
|
@473
|
9 years |
campbell |
Track changes in nlibrary list-theory.ma -> list.ma
|
|
|
|
@469
|
9 years |
campbell |
Update work-in-progress file to match current development.
|
|
|
|
@468
|
9 years |
campbell |
Missing changes to completeness proof for function pointer type fix.
|
|
|
|
@467
|
9 years |
campbell |
Update some of the commented-out parts of Globalenvs for testing.
|
|
|
|
@458
|
9 years |
campbell |
Add a few more pointer tests.
|
|
|
|
@457
|
9 years |
campbell |
Correct checking of function pointers.
|
|
|
|
@456
|
9 years |
campbell |
Add 24bit initialisation data for null generic pointers.
|
|
|
|
@417
|
9 years |
campbell |
Minor typo.
|
|
|
|
@416
|
9 years |
campbell |
Fix printing of switch statements as matita terms.
|
|
|
|
@415
|
9 years |
campbell |
A couple of amusing examples.
|
|
|
|
@413
|
9 years |
campbell |
Add example of executing C semantics.
|
|
|
|
@412
|
9 years |
campbell |
Add example of animation.
|
|
|
|
@411
|
9 years |
campbell |
Note associativity of IOMonad, subject to extensionality.
|
|
|
|
@409
|
9 years |
campbell |
Update a couple of examples; put support for animation in its own file.
|
|
|
|
@408
|
9 years |
campbell |
Add missing diagram.
|
|
|
|
@407
|
9 years |
campbell |
Mention version of compcert used.
|
|
|
|
@406
|
9 years |
campbell |
Move description of 8051 memory model out of C semantics.
|
|
|
|
@405
|
9 years |
campbell |
Move C semantics to the appropriate deliverable directory.
|
|
|
|
@402
|
9 years |
campbell |
Revise D3.1, add notes on files.
|
|
|
|
@393
|
9 years |
campbell |
A few more details in D3.1.
|
|
|
|
@381
|
9 years |
campbell |
Some d3.1 work.
|
|
|
|
@335
|
9 years |
campbell |
Quick pass through 3.1 text.
|
|
|
|
@207
|
9 years |
campbell |
Add memory extensions and rework parts of D3.1.
|
|
|
|
@197
|
9 years |
campbell |
Add some first draft text for 3.1.
|
