Timeline
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.
Aug 26, 2011:
- 8:06 PM Changeset [1122] by
- Internal function call implemented too.
- 8:00 PM Changeset [1121] by
- External function calls implemented (but look at the new comment on …
- 7:41 PM Changeset [1120] by
- All operations implemented.
- 7:38 PM Changeset [1119] by
- Type for evaluation of opaccs fixed (maybe wrongly: should it return …
- 7:08 PM Changeset [1118] by
- All derivatives of St_const implemented (up to axioms to match the two …
- 6:47 PM Changeset [1117] by
- More operations implemented.
- 6:47 PM Changeset [1116] by
- Some comments.
- 6:47 PM Changeset [1115] by
- Some comments.
- 1:01 PM Changeset [1114] by
- some more operations implemented
- 12:40 PM Changeset [1113] by
- Semantics (interpreter) of RTL. The file does not compile yet. I am …
Aug 24, 2011:
- 7:08 PM Changeset [1112] by
- got lin > asm stuff working
- 6:47 PM Changeset [1111] by
- minor change: marked some possibly dodgy (and very complex) code
- 6:45 PM Changeset [1110] by
- changes to get ltl to lin pass to work properly
- 5:12 PM Changeset [1109] by
- Update branch.
- 3:04 PM Changeset [1108] by
- changes to get ertltoltli to compile
- 2:43 PM Changeset [1107] by
- got rtl-ertl pass working again
- 2:23 PM Changeset [1106] by
- changes necessary to get RTLabs->RTL to compile
Aug 10, 2011:
- 5:17 PM Changeset [1105] by
- Show that RTLabs graphs are closed on branch (i.e., all labels in …
- 5:17 PM Changeset [1104] by
- A little more tidying.
Note: See TracTimeline
for information about the timeline view.
