Timeline



Aug 30, 2011:

6:55 PM Changeset [1153] by campbell
Merge trunk into branch.
5:43 PM Changeset [1152] by mulligan
more added
4:56 PM Changeset [1151] by sacerdot
Only new_/del_frame and framesize left.
4:23 PM Changeset [1150] by sacerdot
Push/pop implemented.
4:22 PM Changeset [1149] by mulligan
changes to get everything type checking again after changing names of …
4:14 PM Changeset [1148] by sacerdot
Function call/return finished (up to retrieving parameters from the …
4:09 PM Changeset [1147] by campbell
Remove some obsolete commented out code, update a couple of comments.
4:07 PM Changeset [1146] by sacerdot
More progress: function call/return almost completed.
4:02 PM Changeset [1145] by mulligan
changed naming in i8051 of classes of registers to make them consistent
3:53 PM Changeset [1144] by mulligan
added build.ma file. matita bug found
3:39 PM Changeset [1143] by sacerdot
Added one important observation (not implemented yet).
3:33 PM Changeset [1142] by sacerdot
More progress.
3:33 PM Changeset [1141] by sacerdot
Comment (about a bug) added.
2:23 PM Changeset [1140] by sacerdot
More instructions implemented.
12:47 PM Changeset [1139] by campbell
Shift init_data out of generic program record so that it only appears …
12:08 PM Changeset [1138] by mulligan
merged ertl_st_opaccs_a and ertl_st_opaccs_b into each other

Aug 29, 2011:

6:27 PM Changeset [1137] by sacerdot
More progress.
6:01 PM Changeset [1136] by mulligan
fixed ertl pass
5:45 PM Changeset [1135] by campbell
Add invariants to Cminor semantics to rule out some failures.
5:45 PM Changeset [1134] by campbell
Extra results for non-failing map updates.
5:45 PM Changeset [1133] by campbell
Add missing utilities files
5:30 PM Changeset [1132] by mulligan
reunified ltl and lin instruction type, removing lifting in ltl and …
5:19 PM Changeset [1131] by mulligan
changes to syntax of ertl: removed ertl_st_addr_l and ertl_st_addr_h …
5:11 PM Changeset [1130] by sacerdot
File in progress (copied from RTL). All instructions considered up to …
4:34 PM Changeset [1129] by mulligan
removed conversions between Register and register
4:27 PM Changeset [1128] by mulligan
fixed ERTLtoLTLI so it type checks again
3:30 PM Changeset [1127] by mulligan
interference graphs axiomatised, more added to ertl
3:07 PM Changeset [1126] by sacerdot
Semantics completed up to initial state creation.
3:07 PM Changeset [1125] by sacerdot
Monadic mfold_left2 added.
2:42 PM Changeset [1124] by mulligan
finished off liveness analysis by axiomatising properties
2:34 PM Changeset [1123] by sacerdot
Added comment about missing alignment of data in memory.

Aug 26, 2011:

8:06 PM Changeset [1122] by sacerdot
Internal function call implemented too.
8:00 PM Changeset [1121] by sacerdot
External function calls implemented (but look at the new comment on …
7:41 PM Changeset [1120] by sacerdot
All operations implemented.
7:38 PM Changeset [1119] by sacerdot
Type for evaluation of opaccs fixed (maybe wrongly: should it return …
7:08 PM Changeset [1118] by sacerdot
All derivatives of St_const implemented (up to axioms to match the two …
6:47 PM Changeset [1117] by sacerdot
More operations implemented.
6:47 PM Changeset [1116] by sacerdot
Some comments.
6:47 PM Changeset [1115] by sacerdot
Some comments.
1:01 PM Changeset [1114] by sacerdot
some more operations implemented
12:40 PM Changeset [1113] by sacerdot
Semantics (interpreter) of RTL. The file does not compile yet. I am …

Aug 24, 2011:

7:08 PM Changeset [1112] by mulligan
got lin > asm stuff working
6:47 PM Changeset [1111] by mulligan
minor change: marked some possibly dodgy (and very complex) code
6:45 PM Changeset [1110] by mulligan
changes to get ltl to lin pass to work properly
5:12 PM Changeset [1109] by campbell
Update branch.
3:04 PM Changeset [1108] by mulligan
changes to get ertltoltli to compile
2:43 PM Changeset [1107] by mulligan
got rtl-ertl pass working again
2:23 PM Changeset [1106] by mulligan
changes necessary to get RTLabs->RTL to compile

Aug 10, 2011:

5:17 PM Changeset [1105] by campbell
Show that RTLabs graphs are closed on branch (i.e., all labels in …
5:17 PM Changeset [1104] by campbell
A little more tidying.

Aug 5, 2011:

1:47 PM Changeset [1103] by boender
- reverted to old policy

Aug 4, 2011:

1:55 PM Changeset [1102] by campbell
Tidy up branch

Aug 3, 2011:

5:18 PM Changeset [1101] by campbell
Label preservation in Cminor initialisation and RTLabs translation on …
5:18 PM Changeset [1100] by campbell
Finally show that labels in generated Cminor programs are properly …
4:17 PM Changeset [1099] by ayache
Bug fix in Deliverables/D2.2/8051: cast simplification.
2:48 PM Changeset [1098] by campbell
Merge branch with trunk
1:04 PM Changeset [1097] by campbell
Checkpoint labels work on branch again.
1:04 PM Changeset [1096] by campbell
Checkpoint part way through adding proper C label checking to the branch.
1:04 PM Changeset [1095] by campbell
Make add_exprs total (on branch).
Note: See TracTimeline for information about the timeline view.