Timeline
Sep 26, 2011:
- 6:58 PM Changeset [1277] by
- Runtime functions and conclusion for D3.2.
- 6:14 PM Changeset [1276] by
- Support for replacing operations with runtime support functions in …
- 6:07 PM Changeset [1275] by
- RTL ported to joint syntax, but: 1. bug discovered: opaccs should …
- 5:58 PM Changeset [1274] by
- starting removing axioms from adts and giving them proper implementations
- 5:57 PM Changeset [1273] by
- Remove generated file.
- 5:57 PM Changeset [1272] by
- Revert accidental commit.
- 4:24 PM Changeset [1271] by
- finished, kind of
- 3:59 PM Changeset [1270] by
- Making RTL syntax an instance of Joint.
- 3:06 PM Changeset [1269] by
- Useless include removed.
- 2:52 PM Changeset [1268] by
- 1) AST/Identifier.ma no longer used, utilities/IdentifierTools no …
- 12:41 PM Changeset [1267] by
- Other bits and pieces for D3.3.
- 12:09 PM Changeset [1266] by
- Added second projection.
- 11:29 AM Changeset [1265] by
- Revisions to D3.3.
Sep 23, 2011:
- 6:44 PM Changeset [1264] by
- Almost ported to new Joint syntax.
- 5:12 PM Changeset [1263] by
- changes
- 4:40 PM Changeset [1262] by
- RTLtoERTL ported to the joint syntax for ERTL. Now it is time to port …
- 4:17 PM Changeset [1261] by
- More of D3.2.
- 3:04 PM Changeset [1260] by
- commit for csc
- 11:49 AM Changeset [1259] by
- More progress towards new Joint data type.
- 1:47 AM Changeset [1258] by
- More progress towards porting to joint syntax.
Sep 22, 2011:
- 6:04 PM Changeset [1257] by
- More progress in porting to joint datatype.
- 6:03 PM Changeset [1256] by
- changes: added a mapi for graphs
- 4:23 PM Changeset [1255] by
- Major mistake fixed: op1 and op2 were assuming the source and dest …
- 4:16 PM Changeset [1254] by
- More progress towards porting of RTLtoERTL to joint syntax.
- 2:57 PM Changeset [1253] by
- uses.ma finished
- 2:49 PM Changeset [1252] by
- graph_params added to joint/Joint.ma, together with useful common …
- 2:29 PM Changeset [1251] by
- changes to get things compiling again after yet another CSC rearrangement!
- 12:02 PM Changeset [1250] by
- 1. Sigma types projections moved to utilities/extralib.ma 2. Extended …
- 11:41 AM Changeset [1249] by
- changes to get everything to typecheck again
- 10:13 AM Changeset [1248] by
- deleted files that do not compile in utilities, changed ertl.ma to use …
- 3:03 AM Changeset [1247] by
- Code (almost) ported to latest joint/Joint.ma datatype. I still need …
- 2:50 AM Changeset [1246] by
- Yet another change to Joint.ma to accomodate all passes. The concrete …
Sep 21, 2011:
- 10:22 PM Changeset [1245] by
- RTLtoERTL and LINToASM: porting to new Joint data type in progress. …
- 6:08 PM Changeset [1244] by
- Sort out Clight semantics equivalence proof for new SmallstepExec?.
- 5:53 PM Changeset [1243] by
- small changes
- 5:35 PM Changeset [1242] by
- Some clean-up.
- 5:28 PM Changeset [1241] by
- changes for claudio
- 5:24 PM Changeset [1240] by
- Ported to common definitions.
- 5:21 PM Changeset [1239] by
- RTLAbstoRTL ported to new datatypes. Note: RTL syntax/semantics is …
- 4:25 PM Changeset [1238] by
- Update Cminor and RTLabs to fit SmallstepExec? changes.
- 3:58 PM Changeset [1237] by
- Wrong commit repaired.
- 3:56 PM Changeset [1236] by
- LTLToLin.ma completed (up to a couple of daemons used to provide dead …
- 12:14 PM Changeset [1235] by
- Some basic material for D3.2, but not yet finished.
- 12:14 PM Changeset [1234] by
- Add (rather brief) draft of D3.3.
- 11:57 AM Changeset [1233] by
- 1) Ported to Brian's new dependent type for fullexec 2) Universe level …
- 11:24 AM Changeset [1232] by
- big changes: got what was implemented in the ertl to ltl pass type …
Sep 20, 2011:
- 7:11 PM Changeset [1231] by
- Change SmallstepExec? so that states can depend on global information. …
- 3:56 PM Changeset [1230] by
- more changes
- 1:26 PM Changeset [1229] by
- changes
Sep 19, 2011:
- 4:52 PM Changeset [1228] by
- some more changes
- 12:57 PM Changeset [1227] by
- changes
Sep 16, 2011:
- 7:16 PM Changeset [1226] by
- Adjust pretty printers for change in program records, try a test of each.
- 6:48 PM Changeset [1225] by
- Missing ; in proof
- 6:39 PM Changeset [1224] by
- Type of programs in common/AST made more dependent. In particular, the …
- 5:15 PM Changeset [1223] by
- changes
- 11:02 AM Changeset [1222] by
- LTL fully ported to the joint syntax.
- 10:53 AM Changeset [1221] by
- Cleanup.
Sep 15, 2011:
- 6:05 PM Changeset [1220] by
- ERTL ported to the new joint syntax.
- 5:40 PM Changeset [1219] by
- a little more added
- 4:56 PM Changeset [1218] by
- a lot added to interference graph calculation
- 4:42 PM Changeset [1217] by
- Only one axiom left.
- 3:33 PM Changeset [1216] by
- Update Clight semantics equivalence proof to match changes in …
- 3:04 PM Changeset [1215] by
- 1) Added shifting directly on pointers 2) More temporary axioms closed.
- 2:27 PM Changeset [1214] by
- res_to_opt function added to common/Errors and used in joint/semantics …
- 2:01 PM Changeset [1213] by
- 1) New values (joint/BEValues.ma) and memory model for the back-ends …
Sep 14, 2011:
- 5:03 PM Changeset [1212] by
- more added on interference graphs
- 4:14 PM Changeset [1211] by
- fixed interference file
- 4:04 PM Changeset [1210] by
- getting rid of typeclass-like records in favour of file-level axioms. …
Sep 13, 2011:
- 5:14 PM Changeset [1209] by
- more work on int. graphs
- 4:33 PM Changeset [1208] by
- added adts for sets, tables and priority sets in order to make life …
Sep 12, 2011:
- 4:20 PM Changeset [1207] by
- Second part of fixing temporaries in Clight to Cminor stage.
- 4:20 PM Changeset [1206] by
- First stage of fixing temporary generation in Clight/toCminor.ma.
Sep 10, 2011:
- 12:16 PM Changeset [1205] by
- typographical changes
- 12:13 PM Changeset [1204] by
- small change
- 12:09 PM Changeset [1203] by
- implemented referees comments
Sep 9, 2011:
- 11:48 AM Changeset [1202] by
- more changes, changed mention of atkey's jvm
- 11:27 AM Changeset [1201] by
- more changes to reduce length
- 11:03 AM Changeset [1200] by
- small changes and rewordings to decrease length
- 9:49 AM Changeset [1199] by
- got paper down to 15 and a half pages with nothing much added to document
Sep 8, 2011:
- 4:04 PM Changeset [1198] by
- Clight cast removal (NB: quite different from the prototype).
Sep 7, 2011:
- 12:10 PM Changeset [1197] by
- Merge trunk to branch.
Sep 6, 2011:
- 6:15 PM Changeset [1196] by
- some more changes, need some additional datastructures
- 5:20 PM Changeset [1195] by
- List find function.
- 5:20 PM Changeset [1194] by
- Remove old, commented out code.
- 3:49 PM Changeset [1193] by
- work on colouring algorithm halted as it can be axiomatised. now …
- 1:33 PM Changeset [1192] by
- some files that were missing / laying dormant on my computer
- 10:38 AM Changeset [1191] by
- ertl to ertl pass back where it was before the changes to joint
Sep 5, 2011:
- 5:53 PM Changeset [1190] by
- improved explanation of matita
- 5:23 PM Changeset [1189] by
- implemented some language fixes as spotted by the referees
- 5:14 PM Changeset [1188] by
- removed stray lines from uses.ma so that it at least typechecks
- 5:13 PM Changeset [1187] by
- fixed build.ma
- 5:08 PM Changeset [1186] by
- Spurious code removed. joint_fullexec implemented up to …
- 5:02 PM Changeset [1185] by
- ported liveness analysis to new code
- 2:55 PM Changeset [1184] by
- changed to llncs style and increased font size in code extracts
- 1:31 PM Changeset [1183] by
- removed parameterised label types in the three lowest level languages
- 1:23 PM Changeset [1182] by
- changes to semantics: removing parameterised "next" element in joint …
- 1:11 PM Changeset [1181] by
- changed smallstep exec in order to remove matita bug (superposition.ml …
- 12:01 PM Changeset [1180] by
- lin to ltl pass complete
- 11:58 AM Changeset [1179] by
- changes to ertl, ltl and lin to use new notion of joint params. ertl …
- 11:26 AM Changeset [1178] by
- fixed ertl.ma to use new version of joint params
Sep 4, 2011:
- 9:36 PM Changeset [1177] by
- Almost finished. Some functions still to be implemented, but I suspect …
Sep 3, 2011:
Sep 2, 2011:
- 5:58 PM Changeset [1175] by
- changes to ertl pass
- 4:09 PM Changeset [1174] by
- Semantics of most instructions completed.
- 3:33 PM Changeset [1173] by
- Unified semantics for ERTL/LTL/LIN (in progress). I hope to include …
- 3:00 PM Changeset [1172] by
- ertltoltl.ma half complete
- 2:51 PM Changeset [1171] by
- changes made on claudio's request: changed order of nesting in the …
- 12:28 PM Changeset [1170] by
- changes to ertl > ltl pass
- 11:57 AM Changeset [1169] by
- JointRTLtoLIN moved to Joint
- 11:36 AM Changeset [1168] by
- Joint statements parameterized over a record.
- 10:35 AM Changeset [1167] by
- …
- 10:35 AM Changeset [1166] by
- moved joint ltl lin files into their own directory. more changes to …
Sep 1, 2011:
- 5:18 PM Changeset [1165] by
- more changes
- 4:53 PM Changeset [1164] by
- ltl to lin working again, more changes to joint syntax
- 4:23 PM Changeset [1163] by
- even more streamlining and fixes to get things type checking
- 11:32 AM Changeset [1162] by
- changes committed to ertl semantics based on our new combined syntax …
Aug 31, 2011:
- 6:24 PM Changeset [1161] by
- changes from today: merged ertl, ltl and lin into one datatype to …
- 12:30 PM Changeset [1160] by
- changes to unfunctorised code in ertltoltl.ma
- 12:30 PM Changeset [1159] by
- - added 'nth' theorems - moved up \bot a bit
- 12:15 PM Changeset [1158] by
- Record patch needed to use matita pretty printers with acc.
- 12:15 PM Changeset [1157] by
- Update pretty printers and examples.
- 11:41 AM Changeset [1156] by
- ERTL semantics completed up to initialization and memory model.
- 11:26 AM Changeset [1155] by
- removed
- 11:26 AM Changeset [1154] by
- changes to ertl files: in process of removing ertltoltli.ma in favour …
Aug 30, 2011:
- 6:55 PM Changeset [1153] by
- Merge trunk into branch.
- 5:43 PM Changeset [1152] by
- more added
- 4:56 PM Changeset [1151] by
- Only new_/del_frame and framesize left.
- 4:23 PM Changeset [1150] by
- Push/pop implemented.
- 4:22 PM Changeset [1149] by
- changes to get everything type checking again after changing names of …
- 4:14 PM Changeset [1148] by
- Function call/return finished (up to retrieving parameters from the …
- 4:09 PM Changeset [1147] by
- Remove some obsolete commented out code, update a couple of comments.
- 4:07 PM Changeset [1146] by
- More progress: function call/return almost completed.
- 4:02 PM Changeset [1145] by
- changed naming in i8051 of classes of registers to make them consistent
- 3:53 PM Changeset [1144] by
- added build.ma file. matita bug found
- 3:39 PM Changeset [1143] by
- Added one important observation (not implemented yet).
- 3:33 PM Changeset [1142] by
- More progress.
- 3:33 PM Changeset [1141] by
- Comment (about a bug) added.
- 2:23 PM Changeset [1140] by
- More instructions implemented.
- 12:47 PM Changeset [1139] by
- Shift init_data out of generic program record so that it only appears …
- 12:08 PM Changeset [1138] by
- merged ertl_st_opaccs_a and ertl_st_opaccs_b into each other
Aug 29, 2011:
- 6:27 PM Changeset [1137] by
- More progress.
- 6:01 PM Changeset [1136] by
- fixed ertl pass
- 5:45 PM Changeset [1135] by
- Add invariants to Cminor semantics to rule out some failures.
- 5:45 PM Changeset [1134] by
- Extra results for non-failing map updates.
- 5:45 PM Changeset [1133] by
- Add missing utilities files
- 5:30 PM Changeset [1132] by
- reunified ltl and lin instruction type, removing lifting in ltl and …
- 5:19 PM Changeset [1131] by
- changes to syntax of ertl: removed ertl_st_addr_l and ertl_st_addr_h …
- 5:11 PM Changeset [1130] by
- File in progress (copied from RTL). All instructions considered up to …
- 4:34 PM Changeset [1129] by
- removed conversions between Register and register
- 4:27 PM Changeset [1128] by
- fixed ERTLtoLTLI so it type checks again
- 3:30 PM Changeset [1127] by
- interference graphs axiomatised, more added to ertl
- 3:07 PM Changeset [1126] by
- Semantics completed up to initial state creation.
- 3:07 PM Changeset [1125] by
- Monadic mfold_left2 added.
- 2:42 PM Changeset [1124] by
- finished off liveness analysis by axiomatising properties
- 2:34 PM Changeset [1123] by
- Added comment about missing alignment of data in memory.
Note: See TracTimeline
for information about the timeline view.
