Context Navigation

Timeline

17:45 Changeset [502] by campbell: Fix not on nulls on Clight.
17:35 Changeset [501] by mulligan: more changes
16:45 Changeset [500] by campbell: Use dependent pointer type to ensure that the representation is always …
16:45 Changeset [499] by campbell: pointer_compat is a little more natural if it takes that block rather than …
16:45 Changeset [498] by campbell: Make block type a little more abstract; remove knowledge about the old …
16:45 Changeset [497] by campbell: Remove bogus pointer compatibility case.
16:45 Changeset [496] by campbell: First pass at moving regions to block type.
15:16 Changeset [495] by mulligan: more added
12:11 Changeset [494] by mulligan: more added
11:40 Changeset [493] by mulligan: incorporated some text from the eu report that needs to be pared down
10:22 Changeset [492] by mulligan: Initial commit of outline of prospective itp-2011 paper.

15:28 Changeset [491] by mulligan: Initial commit of (part)-formalisation of LIN intermediate language.

18:22 Changeset [490] by campbell: Update syntax of Matita Clight term printer.
18:22 Changeset [489] by campbell: Pointer fixes for the temporary version of the compiler that can output …
11:58 Changeset [488] by campbell: Some missing equality constants used by destruct.
11:49 Changeset [487] by campbell: Port Clight semantics to the new-new matita syntax.

11:36 PublicationVenues edited by mulligan: (diff)
11:12 PublicationVenues edited by mulligan: (diff)
11:08 PublicationVenues edited by mulligan: (diff)
10:50 PublicationVenues created by mulligan: Initial creation
10:47 WikiStart edited by mulligan: Added a section on potential publication venues. (diff)

12:41 Changeset [485] by campbell: Fix treatment of pointers in initialisation data, a little like later …

14:41 Changeset [484] by campbell: Separate out null values from integer zeros.
14:41 Changeset [483] by campbell: Use pointer-specific "chunks" of memory for pointer loads and stores, in …
14:41 Changeset [482] by campbell: Note the purpose of the region in a pointer value.

18:22 Changeset [481] by campbell: Tcomp_ptr should take the memory region and use that to calculate its …
17:30 Changeset [480] by campbell: "memory_space" to "region" replacement to match ocaml code
17:30 Changeset [479] by campbell: Test of linked list insertion sort.
17:30 Changeset [478] by campbell: Prevent clashes between names in AST and other parts of the development. …

14:57 Changeset [477] by mulligan: Added file for LIN.
14:37 Changeset [476] by mulligan: Commiting directory for formalization of intermediate compiler languages.
10:48 Ticket #1 (O'Caml emulator lacks export to Intel HEX) closed by mulligan: fixed
10:47 Changeset [475] by mulligan: Matita interpreter ported to latest version of matita (the one with the …

14:31 Changeset [474] by campbell: Reduce "include"s to reduce compilation time. (Will be undone when moving …
14:31 Changeset [473] by campbell: Track changes in nlibrary list-theory.ma -> list.ma
11:08 Changeset [472] by mulligan: More changes to debug and testing files to get them to work with the …
10:19 Changeset [471] by mulligan: Deleted (now) superfluous custom library files in favour of using Matita …
10:18 Changeset [470] by mulligan: Finished moving development over to standard library.
10:02 Changeset [469] by campbell: Update work-in-progress file to match current development.
10:02 Changeset [468] by campbell: Missing changes to completeness proof for function pointer type fix.
10:02 Changeset [467] by campbell: Update some of the commented-out parts of Globalenvs for testing.

18:46 Changeset [466] by mulligan: Most of execute_1 checked. Need to fix negations, though, in rest in …
18:10 Changeset [465] by mulligan: Moved over to standard library.
13:35 Changeset [464] by mulligan: Fixed strange bug/typo in BitVectorTrie?.ma
13:33 Changeset [463] by mulligan: Fixed DoTest? so that it doesn't take an hour to typecheck.
13:32 Changeset [462] by mulligan: Added bitvector arithmetic for Brian.

18:23 Changeset [461] by campbell: Handle null pointer constants properly for generic pointers (introducing a …
18:23 Changeset [460] by campbell: Port memory spaces changes to latest prototype compiler.
17:22 Changeset [459] by campbell: Create branch of the prototype compiler for memory space support
15:16 Changeset [458] by campbell: Add a few more pointer tests.
15:06 Changeset [457] by campbell: Correct checking of function pointers.
11:45 Changeset [456] by campbell: Add 24bit initialisation data for null generic pointers.
10:58 Changeset [455] by mulligan: Merge commit.

19:23 Changeset [454] by sacerdot: CSC + Nicolas + Dominic: 1) back-porting of changes by Nicolas from the …

17:01 Changeset [452] by mulligan: Added function to interface.
16:54 Changeset [451] by mulligan: Removed more debugging stuff from Test.ml.
16:54 Changeset [450] by mulligan: Comment added for Nicolas.
16:51 Changeset [449] by mulligan: Removed debugging code from Test.ml.
16:49 Changeset [448] by mulligan: Got Intel HEX format exportation working.
15:30 Changeset [447] by mulligan: Checksum seems to be working now on most lines, barring three? Weird bug.
14:14 Changeset [446] by mulligan: Checksum calculation added. Seems to still be buggy.
13:33 Changeset [445] by mulligan: Debugging hex output. Seems mcu8051 really doesn't like what's been spat …

14:19 Changeset [444] by mulligan: Got Test.native to compile. Added functions for exporting intel hex …
11:35 Changeset [443] by mulligan: Wrote exportation code. Need to test it.
10:54 Changeset [442] by mulligan: Partial implementation of Nicolas' requested feature (extraction of …

15:22 Changeset [441] by mulligan: Fixed bug in PUSH spotted by Nicolas.
14:13 Ticket #1 (O'Caml emulator lacks export to Intel HEX) created by mulligan: The O'Caml emulator lacks a function to dump code memory to an Intel HEX …

Note: See TracTimeline for information about the timeline view.