Timeline
09/21/11:
- 22:22 Changeset [1245] by
- RTLtoERTL and LINToASM: porting to new Joint data type in progress. …
- 18:08 Changeset [1244] by
- Sort out Clight semantics equivalence proof for new SmallstepExec?.
- 17:53 Changeset [1243] by
- small changes
- 17:35 Changeset [1242] by
- Some clean-up.
- 17:28 Changeset [1241] by
- changes for claudio
- 17:24 Changeset [1240] by
- Ported to common definitions.
- 17:21 Changeset [1239] by
- RTLAbstoRTL ported to new datatypes. Note: RTL syntax/semantics is not …
- 16:25 Changeset [1238] by
- Update Cminor and RTLabs to fit SmallstepExec? changes.
- 15:58 Changeset [1237] by
- Wrong commit repaired.
- 15:56 Changeset [1236] by
- LTLToLin.ma completed (up to a couple of daemons used to provide dead …
- 12:14 Changeset [1235] by
- Some basic material for D3.2, but not yet finished.
- 12:14 Changeset [1234] by
- Add (rather brief) draft of D3.3.
- 11:57 Changeset [1233] by
- 1) Ported to Brian's new dependent type for fullexec 2) Universe level …
- 11:24 Changeset [1232] by
- big changes: got what was implemented in the ertl to ltl pass type …
09/20/11:
- 19:11 Changeset [1231] by
- Change SmallstepExec? so that states can depend on global information. Use …
- 15:56 Changeset [1230] by
- more changes
- 13:26 Changeset [1229] by
- changes
09/19/11:
- 16:52 Changeset [1228] by
- some more changes
- 12:57 Changeset [1227] by
- changes
09/16/11:
- 19:16 Changeset [1226] by
- Adjust pretty printers for change in program records, try a test of each.
- 18:48 Changeset [1225] by
- Missing ; in proof
- 18:39 Changeset [1224] by
- Type of programs in common/AST made more dependent. In particular, the …
- 17:15 Changeset [1223] by
- changes
- 11:02 Changeset [1222] by
- LTL fully ported to the joint syntax.
- 10:53 Changeset [1221] by
- Cleanup.
09/15/11:
- 18:05 Changeset [1220] by
- ERTL ported to the new joint syntax.
- 17:40 Changeset [1219] by
- a little more added
- 16:56 Changeset [1218] by
- a lot added to interference graph calculation
- 16:42 Changeset [1217] by
- Only one axiom left.
- 15:33 Changeset [1216] by
- Update Clight semantics equivalence proof to match changes in …
- 15:04 Changeset [1215] by
- 1) Added shifting directly on pointers 2) More temporary axioms closed.
- 14:27 Changeset [1214] by
- res_to_opt function added to common/Errors and used in joint/semantics to …
- 14:01 Changeset [1213] by
- 1) New values (joint/BEValues.ma) and memory model for the back-ends …
09/14/11:
- 17:03 Changeset [1212] by
- more added on interference graphs
- 16:14 Changeset [1211] by
- fixed interference file
- 16:04 Changeset [1210] by
- getting rid of typeclass-like records in favour of file-level axioms. …
09/13/11:
- 17:14 Changeset [1209] by
- more work on int. graphs
- 16:33 Changeset [1208] by
- added adts for sets, tables and priority sets in order to make life easier …
09/12/11:
- 16:20 Changeset [1207] by
- Second part of fixing temporaries in Clight to Cminor stage.
- 16:20 Changeset [1206] by
- First stage of fixing temporary generation in Clight/toCminor.ma.
09/10/11:
- 12:16 Changeset [1205] by
- typographical changes
- 12:13 Changeset [1204] by
- small change
- 12:09 Changeset [1203] by
- implemented referees comments
09/09/11:
- 11:48 Changeset [1202] by
- more changes, changed mention of atkey's jvm
- 11:27 Changeset [1201] by
- more changes to reduce length
- 11:03 Changeset [1200] by
- small changes and rewordings to decrease length
- 09:49 Changeset [1199] by
- got paper down to 15 and a half pages with nothing much added to document
09/08/11:
- 16:04 Changeset [1198] by
- Clight cast removal (NB: quite different from the prototype).
09/07/11:
- 12:10 Changeset [1197] by
- Merge trunk to branch.
09/06/11:
- 18:15 Changeset [1196] by
- some more changes, need some additional datastructures
- 17:20 Changeset [1195] by
- List find function.
- 17:20 Changeset [1194] by
- Remove old, commented out code.
- 15:49 Changeset [1193] by
- work on colouring algorithm halted as it can be axiomatised. now …
- 13:33 Changeset [1192] by
- some files that were missing / laying dormant on my computer
- 10:38 Changeset [1191] by
- ertl to ertl pass back where it was before the changes to joint
09/05/11:
- 17:53 Changeset [1190] by
- improved explanation of matita
- 17:23 Changeset [1189] by
- implemented some language fixes as spotted by the referees
- 17:14 Changeset [1188] by
- removed stray lines from uses.ma so that it at least typechecks
- 17:13 Changeset [1187] by
- fixed build.ma
- 17:08 Changeset [1186] by
- Spurious code removed. joint_fullexec implemented up to make_initial_state …
- 17:02 Changeset [1185] by
- ported liveness analysis to new code
- 14:55 Changeset [1184] by
- changed to llncs style and increased font size in code extracts
- 13:31 Changeset [1183] by
- removed parameterised label types in the three lowest level languages
- 13:23 Changeset [1182] by
- changes to semantics: removing parameterised "next" element in joint …
- 13:11 Changeset [1181] by
- changed smallstep exec in order to remove matita bug (superposition.ml on …
- 12:01 Changeset [1180] by
- lin to ltl pass complete
- 11:58 Changeset [1179] by
- changes to ertl, ltl and lin to use new notion of joint params. ertl to …
- 11:26 Changeset [1178] by
- fixed ertl.ma to use new version of joint params
09/04/11:
- 21:36 Changeset [1177] by
- Almost finished. Some functions still to be implemented, but I suspect …
09/03/11:
09/02/11:
- 17:58 Changeset [1175] by
- changes to ertl pass
- 16:09 Changeset [1174] by
- Semantics of most instructions completed.
- 15:33 Changeset [1173] by
- Unified semantics for ERTL/LTL/LIN (in progress). I hope to include RTL …
- 15:00 Changeset [1172] by
- ertltoltl.ma half complete
- 14:51 Changeset [1171] by
- changes made on claudio's request: changed order of nesting in the …
- 12:28 Changeset [1170] by
- changes to ertl > ltl pass
- 11:57 Changeset [1169] by
- JointRTLtoLIN moved to Joint
- 11:36 Changeset [1168] by
- Joint statements parameterized over a record.
- 10:35 Changeset [1167] by
- …
- 10:35 Changeset [1166] by
- moved joint ltl lin files into their own directory. more changes to ltl …
09/01/11:
- 17:18 Changeset [1165] by
- more changes
- 16:53 Changeset [1164] by
- ltl to lin working again, more changes to joint syntax
- 16:23 Changeset [1163] by
- even more streamlining and fixes to get things type checking
- 11:32 Changeset [1162] by
- changes committed to ertl semantics based on our new combined syntax for …
08/31/11:
- 18:24 Changeset [1161] by
- changes from today: merged ertl, ltl and lin into one datatype to simplify …
- 12:30 Changeset [1160] by
- changes to unfunctorised code in ertltoltl.ma
- 12:30 Changeset [1159] by
- - added 'nth' theorems - moved up \bot a bit
- 12:15 Changeset [1158] by
- Record patch needed to use matita pretty printers with acc.
- 12:15 Changeset [1157] by
- Update pretty printers and examples.
- 11:41 Changeset [1156] by
- ERTL semantics completed up to initialization and memory model.
- 11:26 Changeset [1155] by
- removed
- 11:26 Changeset [1154] by
- changes to ertl files: in process of removing ertltoltli.ma in favour or …
08/30/11:
- 18:55 Changeset [1153] by
- Merge trunk into branch.
- 17:43 Changeset [1152] by
- more added
- 16:56 Changeset [1151] by
- Only new_/del_frame and framesize left.
- 16:23 Changeset [1150] by
- Push/pop implemented.
- 16:22 Changeset [1149] by
- changes to get everything type checking again after changing names of …
- 16:14 Changeset [1148] by
- Function call/return finished (up to retrieving parameters from the stack …
- 16:09 Changeset [1147] by
- Remove some obsolete commented out code, update a couple of comments.
- 16:07 Changeset [1146] by
- More progress: function call/return almost completed.
- 16:02 Changeset [1145] by
- changed naming in i8051 of classes of registers to make them consistent
- 15:53 Changeset [1144] by
- added build.ma file. matita bug found
- 15:39 Changeset [1143] by
- Added one important observation (not implemented yet).
- 15:33 Changeset [1142] by
- More progress.
- 15:33 Changeset [1141] by
- Comment (about a bug) added.
- 14:23 Changeset [1140] by
- More instructions implemented.
- 12:47 Changeset [1139] by
- Shift init_data out of generic program record so that it only appears in …
- 12:08 Changeset [1138] by
- merged ertl_st_opaccs_a and ertl_st_opaccs_b into each other
08/29/11:
- 18:27 Changeset [1137] by
- More progress.
- 18:01 Changeset [1136] by
- fixed ertl pass
- 17:45 Changeset [1135] by
- Add invariants to Cminor semantics to rule out some failures.
- 17:45 Changeset [1134] by
- Extra results for non-failing map updates.
- 17:45 Changeset [1133] by
- Add missing utilities files
- 17:30 Changeset [1132] by
- reunified ltl and lin instruction type, removing lifting in ltl and lin …
- 17:19 Changeset [1131] by
- changes to syntax of ertl: removed ertl_st_addr_l and ertl_st_addr_h in …
- 17:11 Changeset [1130] by
- File in progress (copied from RTL). All instructions considered up to …
- 16:34 Changeset [1129] by
- removed conversions between Register and register
- 16:27 Changeset [1128] by
- fixed ERTLtoLTLI so it type checks again
- 15:30 Changeset [1127] by
- interference graphs axiomatised, more added to ertl
- 15:07 Changeset [1126] by
- Semantics completed up to initial state creation.
- 15:07 Changeset [1125] by
- Monadic mfold_left2 added.
- 14:42 Changeset [1124] by
- finished off liveness analysis by axiomatising properties
- 14:34 Changeset [1123] by
- Added comment about missing alignment of data in memory.
08/26/11:
- 20:06 Changeset [1122] by
- Internal function call implemented too.
- 20:00 Changeset [1121] by
- External function calls implemented (but look at the new comment on the …
- 19:41 Changeset [1120] by
- All operations implemented.
- 19:38 Changeset [1119] by
- Type for evaluation of opaccs fixed (maybe wrongly: should it return Byte …
- 19:08 Changeset [1118] by
- All derivatives of St_const implemented (up to axioms to match the two …
- 18:47 Changeset [1117] by
- More operations implemented.
- 18:47 Changeset [1116] by
- Some comments.
- 18:47 Changeset [1115] by
- Some comments.
- 13:01 Changeset [1114] by
- some more operations implemented
- 12:40 Changeset [1113] by
- Semantics (interpreter) of RTL. The file does not compile yet. I am …
08/24/11:
- 19:08 Changeset [1112] by
- got lin > asm stuff working
- 18:47 Changeset [1111] by
- minor change: marked some possibly dodgy (and very complex) code
- 18:45 Changeset [1110] by
- changes to get ltl to lin pass to work properly
- 17:12 Changeset [1109] by
- Update branch.
- 15:04 Changeset [1108] by
- changes to get ertltoltli to compile
- 14:43 Changeset [1107] by
- got rtl-ertl pass working again
- 14:23 Changeset [1106] by
- changes necessary to get RTLabs->RTL to compile
Note: See TracTimeline
for information about the timeline view.
