|
|
|
@488
|
10 years |
campbell |
Some missing equality constants used by destruct.
|
|
|
|
@487
|
10 years |
campbell |
Port Clight semantics to the new-new matita syntax.
|
|
|
|
@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 …
|
|
|
|
@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
|
|
|
|
@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.
|
|
|
|
@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.
|
|
|
|
@417
|
10 years |
campbell |
Minor typo.
|
|
|
|
@416
|
10 years |
campbell |
Fix printing of switch statements as matita terms.
|
|
|
|
@415
|
10 years |
campbell |
A couple of amusing examples.
|
|
|
|
@413
|
10 years |
campbell |
Add example of executing C semantics.
|
|
|
|
@412
|
10 years |
campbell |
Add example of animation.
|
|
|
|
@411
|
10 years |
campbell |
Note associativity of IOMonad, subject to extensionality.
|
|
|
|
@409
|
10 years |
campbell |
Update a couple of examples; put support for animation in its own file.
|
|
|
|
@408
|
10 years |
campbell |
Add missing diagram.
|
|
|
|
@407
|
10 years |
campbell |
Mention version of compcert used.
|
|
|
|
@406
|
10 years |
campbell |
Move description of 8051 memory model out of C semantics.
|
|
|
|
@405
|
10 years |
campbell |
Move C semantics to the appropriate deliverable directory.
|
|
|
|
@402
|
10 years |
campbell |
Revise D3.1, add notes on files.
|
|
|
|
@393
|
10 years |
campbell |
A few more details in D3.1.
|
|
|
|
@381
|
10 years |
campbell |
Some d3.1 work.
|
|
|
|
@335
|
10 years |
campbell |
Quick pass through 3.1 text.
|
|
|
|
@207
|
10 years |
campbell |
Add memory extensions and rework parts of D3.1.
|
|
|
|
@197
|
10 years |
campbell |
Add some first draft text for 3.1.
|
