Timeline
Oct 26, 2011:
- 7:45 PM Changeset [1468] by
- * implemented constant propagation * implementing partial redundancy …
- 5:25 PM Changeset [1467] by
- small change, adding entry and exit labels into the internal function, …
- 5:08 PM Changeset [1466] by
- erasure for graph based joint languages almost complete
- 2:07 PM Changeset [1465] by
- Dead code removed.
Oct 25, 2011:
- 7:12 PM Changeset [1464] by
- Use unification hints to simplify the graph monotonicity proofs.
- 5:33 PM Changeset [1463] by
- added erasure for lin
- 4:11 PM Changeset [1462] by
- Added D5.1: Frama-C plug-in and Lustre wrapper. D2.2 (8051) has been …
Oct 24, 2011:
- 5:56 PM Changeset [1461] by
- rewrote erasure for assembly programs
- 4:53 PM Changeset [1460] by
- most of cost label erasure for assembly language complete, with one …
- 2:34 PM Changeset [1459] by
- - moved stronger occurs_exactly_once lemma to its proper place in …
- 11:44 AM Changeset [1458] by
- added skeleton file for erasure function for joint languages
Oct 23, 2011:
- 10:15 PM Changeset [1457] by
- Bug fixed: when calling an internal function, the pc block is now set …
- 6:37 PM Changeset [1456] by
- changed type of pointer_of_label in report
- 5:51 PM Changeset [1455] by
- ratios changed
- 4:28 PM Changeset [1454] by
- removed mention of axiomatised code in LIN/semantics.ma
Oct 22, 2011:
- 4:26 AM Changeset [1453] by
- …
- 4:26 AM Changeset [1452] by
- Bug fixed: labels MUST be represented as pointers whose block is the …
- 4:18 AM Changeset [1451] by
- 1. All axioms in LIN/semantics.ma closed 2. succ_pc and …
Oct 21, 2011:
- 10:37 PM Changeset [1450] by
- Disambiguation problem avoided.
- 6:45 PM Changeset [1449] by
- finished d4.3
- 6:33 PM Changeset [1448] by
- finished columns in d4.2 report
- 6:30 PM Changeset [1447] by
- changes to columns in tables
- 6:21 PM Changeset [1446] by
- …
- 6:19 PM Changeset [1445] by
- o'caml sizes done for first table
- 6:12 PM Changeset [1444] by
- * expression simplification finished
- 6:08 PM Changeset [1443] by
- sizes added
- 6:00 PM Changeset [1442] by
- changes fixing wrong deletion of conflicts
- 5:51 PM Changeset [1441] by
- small change
- 5:50 PM Changeset [1440] by
- ratios fixed
- 5:47 PM Changeset [1439] by
- …
- 5:36 PM Changeset [1438] by
- changed claudio's english, added bib file
- 5:30 PM Changeset [1437] by
- …
- 5:27 PM Changeset [1436] by
- …
- 5:24 PM Changeset [1435] by
- More on dependent types. One citation is missing.
- 4:45 PM Changeset [1434] by
- chages to typesetting and some wording changes
- 2:02 PM Changeset [1433] by
- * added infrastructure to add same-language transformations along the …
Oct 20, 2011:
- 4:21 PM Changeset [1432] by
- finished d4.2 report
- 3:57 PM Changeset [1431] by
- Back-end todo (in Italian only, sorry...)
- 3:55 PM Changeset [1430] by
- Bug fixed: push/pop must work on the isp (now added). Note: the sp is …
- 3:55 PM Changeset [1429] by
- Useless and removed.
- 3:32 PM Changeset [1428] by
- finished d4.3 report
- 3:07 PM Changeset [1427] by
- more added to d4.3 report
- 2:08 PM Changeset [1426] by
- removed axiom
- 11:12 AM Changeset [1425] by
- changes to the fixpoint calculation in ertl
Oct 19, 2011:
- 7:17 PM Changeset [1424] by
- 1. fold function over BitVectorTries? moved from ERTLToLTL to …
- 6:05 PM Changeset [1423] by
- - spill no longer used - BUG IN Interference: generating the destruct …
- 6:05 PM Changeset [1422] by
- corrected a small bug
- 5:59 PM Changeset [1421] by
- first draft of peeling optimization: * a framework for heuristics has …
- 5:50 PM Changeset [1420] by
- more changes
- 5:25 PM Changeset [1419] by
- All axioms closed.
- 5:11 PM Changeset [1418] by
- correct ratios for semantics calculated
- 5:10 PM Changeset [1417] by
- - proved that jumps always increase - this should make termination easy
- 4:43 PM Changeset [1416] by
- Maps from hardware registers to beval now implemented in ASM/I8051 (in …
- 4:22 PM Changeset [1415] by
- 1. hwreg_store/retrieve no longer returns a res (but it is still …
- 4:03 PM Changeset [1414] by
- more added
- 2:54 PM Changeset [1413] by
- a lot more added, including updated parameters based on csc's recent submit
- 2:22 PM Changeset [1412] by
- Tailcalls (via ids or pointers) to internal functions implemented. …
- 1:39 PM Changeset [1411] by
- 1. sem_params2 splitted into sem_params1 + sem_params2 to take out the …
- 11:54 AM Changeset [1410] by
- Remove a few old workarounds.
- 11:30 AM Changeset [1409] by
- added more to appendix discussing code
- 11:30 AM Changeset [1408] by
- 1. Added joint/BEGlobalenvs that is a modification of …
- 11:17 AM Changeset [1407] by
- almost finished
Oct 18, 2011:
- 4:25 PM Changeset [1406] by
- a little more
- 4:19 PM Changeset [1405] by
- yet more added. apparently there's more parameters than i ever …
- 3:39 PM Changeset [1404] by
- - reworked + added - added an axiom to arithmetic, but should be provable
- 3:12 PM Changeset [1403] by
- more added
- 1:30 PM Changeset [1402] by
- more added
- 12:39 PM Changeset [1401] by
- Changes concerning the new behavior of destruct.
- 12:14 PM Changeset [1400] by
- more added on parameters
- 11:38 AM Changeset [1399] by
- more work on parameters
Oct 17, 2011:
- 8:20 PM Changeset [1398] by
- more work on parameters
- 6:37 PM Changeset [1397] by
- more changes, talking about parameters
- 5:43 PM Changeset [1396] by
- Proof obligation closed.
- 5:41 PM Changeset [1395] by
- 1) New versions of pointer_of_beval/beval_of_pointer with a stricter …
- 4:50 PM Changeset [1394] by
- reconfiguring of tables, and recalculation of ratios
- 3:50 PM Changeset [1393] by
- - added invariant for policy trie to assembly - change (syntax only) …
- 2:08 PM Changeset [1392] by
- fiddling with Cminor: elimination of loops, blocks and exits
- 1:09 PM Changeset [1391] by
- more added
- 11:43 AM Changeset [1390] by
- All fetch_result implementations have been factorized out, leaving …
- 11:23 AM Changeset [1389] by
- One more axiom closed.
- 10:54 AM Changeset [1388] by
- fetch_result implemented for ERTL. This required a different …
- 2:01 AM Changeset [1387] by
- Further simplification *params1 no longer used.
- 1:58 AM Changeset [1386] by
- Structure of semantic parameters simplified.
- 1:40 AM Changeset [1385] by
- 1. fetch_result and pop_frame now takes the genv in input 2. …
Oct 16, 2011:
- 7:42 PM Changeset [1384] by
- * fetch_ra taken out of pop_frame again since it is used uniformly and …
Oct 15, 2011:
- 12:13 AM Changeset [1383] by
- Potential bug fixed and bug found: the way pointers and labels are put …
Oct 14, 2011:
- 10:50 PM Changeset [1382] by
- - succ_pc generalized to return a res (necessary for LIN semantics) - …
- 10:29 PM Changeset [1381] by
- Old commented out code removed.
- 10:25 PM Changeset [1380] by
- LTL and LIN semantics factorized out in joint_LTL_LIN_semantics.ma. …
- 7:44 PM Changeset [1379] by
- Invariant on LIN code removed. In Paris it was decided that a simpler …
- 7:32 PM Changeset [1378] by
- New file LIN/joint_LTL_LIN.ma to factorize out the syntactic …
- 7:22 PM Changeset [1377] by
- pop_frame now incorporates the fetch_result (that made sense only for …
- 5:55 PM Changeset [1376] by
- Stack deallocation for RTL implemented in pop_frame.
- 5:43 PM Changeset [1375] by
- changes, fixing typos etc
- 3:51 PM Changeset [1374] by
- added note about cfgs
- 3:51 PM Changeset [1373] by
- changes to file based on claudio's suggestions
- 2:48 PM Changeset [1372] by
- save_frame now takes the stacksize to allow RTL to allocate the stack frame
- 1:42 PM Changeset [1371] by
- save_frame changed to accept also the formal/actual argument pairs, …
- 10:56 AM Changeset [1370] by
- D3.3: Added a subsection on the SmallstepExec?.ma definitions, plus a …
- 10:56 AM Changeset [1369] by
- Put type information into front-end unary ops. Slight change to …
Oct 13, 2011:
- 6:11 PM Changeset [1368] by
- A bug in the clear tactic makes the previous (correct) commit wrong. …
- 5:48 PM Changeset [1367] by
- Proof improvement, still somehow a bit slow.
- 11:33 AM Changeset [1366] by
- added connections with other languages to d4.3 report, also fixed …
- 11:30 AM Changeset [1365] by
- changed description of task in 4.2 report. added outline and …
- 11:11 AM Changeset [1364] by
- finished the report on d4.2. starting d4.3 report
Oct 12, 2011:
- 9:11 PM Changeset [1363] by
- - done stuff with create_label_trie
- 5:54 PM Changeset [1362] by
- d4-2 report almost complete
- 11:52 AM Changeset [1361] by
- more changes
- 11:47 AM Changeset [1360] by
- added more on use of dependent types, and also discussing the …
Oct 11, 2011:
- 6:00 PM Changeset [1359] by
- 1. more work on the RTL semantics 2. changes to joint/semantics to …
- 5:48 PM Changeset [1358] by
- got rtlabs to rtl compiling, foldi_strong needs examining
- 5:42 PM Changeset [1357] by
- * changed implementation of constant indexings with extensible arrays …
- 5:33 PM Changeset [1356] by
- deleted redundant directory. added outlines for both reports, and …
- 3:32 PM Changeset [1355] by
- monadic fold_lefti added
- 2:38 PM Changeset [1354] by
- One axiom closed.
- 12:45 PM Changeset [1353] by
- This commit is made necessary by the last Matita change. Inclusion is …
- 12:45 PM Changeset [1352] by
- This commit is made necessary by the last Matita change. Inclusion is …
- 12:24 PM Changeset [1351] by
- Tidy up some loose ends from the invariants branch merge.
- 2:27 AM Changeset [1350] by
- Porting to latest destruct tactic. Note: the tactics has a few …
Oct 10, 2011:
- 11:32 PM Changeset [1349] by
- * work on LIN completed * small implementation of extensible arrays
- 10:40 PM Changeset [1348] by
- …
- 7:22 PM Changeset [1347] by
- Remove obsolete definitions.
- 6:18 PM Changeset [1346] by
- Minor corrections and a paragraph of context in the abstract to …
- 5:50 PM Changeset [1345] by
- work on ERTL and LTL completed
- 5:47 PM Changeset [1344] by
- Ported to new destruct.
- 5:27 PM Changeset [1343] by
- fixed some bugs in the translation
- 5:16 PM Changeset [1342] by
- The new auto is much more powerful.
- 4:38 PM Changeset [1341] by
- Empty directory removed.
- 4:34 PM Changeset [1340] by
- work on RTLabs and RTL completed
- 4:10 PM Changeset [1339] by
- Automation is now stronger.
- 4:05 PM Changeset [1338] by
- Automation is now stronger.
- 4:03 PM Changeset [1337] by
- Automation is now stronger.
- 3:54 PM Changeset [1336] by
- Ported to new Matita destruct/inversion. One lemma fails at qed. …
- 3:54 PM Changeset [1335] by
- Ported to new Matita stdlib.
- 2:17 PM Changeset [1334] by
- work on Cminor completed
- 12:53 PM Changeset [1333] by
- Avoid using the name of the construction of jmeq.
- 12:41 PM Changeset [1332] by
- Summation example updated (needs computational K).
- 10:21 AM Changeset [1331] by
- some changes, but i now have two contradictory proof obligations.
Oct 7, 2011:
- 6:39 PM Changeset [1330] by
- Evict obsolete file.
- 6:19 PM Changeset [1329] by
- 1. Definition of addresses moved to BEMem 2. Basic functions on …
- 5:47 PM Changeset [1328] by
- * bug in ClightUtilities?.find_max_depth_lbld fixed * single-entry loop …
- 4:15 PM Changeset [1327] by
- More progress in the implementation of the ERTL specific statements. …
- 3:48 PM Changeset [1326] by
- Code improved (now it uses the high level functions from …
- 3:45 PM Changeset [1325] by
- finished implementing the translate constant function
- 3:32 PM Changeset [1324] by
- The semantics of extended statements must also consider the label …
- 3:26 PM Changeset [1323] by
- Reduce number of notations for destructive let on pairs to one.
- 2:59 PM Changeset [1322] by
- address => stack_address
- 2:37 PM Changeset [1321] by
- No longer/never implemented files removed.
- 2:17 PM Changeset [1320] by
- Frame operations implemented.
- 1:48 PM Changeset [1319] by
- indexing branch is compiling again: * clight interpreter updated * …
- 1:48 PM Changeset [1318] by
- Frame management implemented.
- 12:28 PM Changeset [1317] by
- Fix listings in D3.2/D3.3.
- 12:26 PM Changeset [1316] by
- Merge in id-lookup-branch to trunk.
- 11:12 AM Changeset [1315] by
- another move for the same reason. got rtlabs > rtl compiling again by …
- 11:03 AM Changeset [1314] by
- name changes so that bash tab completion actually works with some …
Oct 6, 2011:
- 10:55 PM Changeset [1313] by
- (E)RTL semantics ported to new data type for save/pop frame (but not …
- 10:35 PM Changeset [1312] by
- Type of frame operations (pop_frame/save_frame) generalized to take in …
- 6:45 PM Changeset [1311] by
- Merge trunk to invariants branch, sorting out the handling of …
- 6:31 PM Changeset [1310] by
- * finished changes on annotator * implementing indexes in interpreter
- 6:09 PM Changeset [1309] by
- - refounded JEP
- 5:27 PM Changeset [1308] by
- changes to translate_cst
- 2:08 PM Changeset [1307] by
- adding translate_cst
- 11:19 AM Changeset [1306] by
- small changes to rtlabs. what axioms remain look hard to close. need …
- 11:07 AM Changeset [1305] by
- added indexes to loop constructors. Branch does not compile atm
- 1:24 AM Changeset [1304] by
- Work in progress.
- 12:16 AM Changeset [1303] by
- 1. LTL/semantics.ma added (work in progress) 2. init_locals fixed to …
Oct 5, 2011:
- 11:36 PM Changeset [1302] by
- ERTL/semantics.ma ported to joint/SemanticUtils (in progress)
- 11:35 PM Changeset [1301] by
- Axioms re-grouped according to their use.
- 10:43 PM Changeset [1300] by
- More (graph) axioms implemented. Look at the comments marked with XXX …
- 9:53 PM Changeset [1299] by
- Functions from RTL/semantics.ma generalized to work on every graph …
- 9:41 PM Changeset [1298] by
- - fetch_statement now takes in input the globalenv - fetch_statement …
- 6:04 PM Changeset [1297] by
- changed representation of indexings to a nameless one implemented with …
- 5:53 PM Changeset [1296] by
- changes
- 4:15 PM Changeset [1295] by
- More progress.
- 3:19 PM Changeset [1294] by
- RTL semantics: porting to joint semantics started.
- 2:47 PM Changeset [1293] by
- finished rtl abs to rtl transformation subject to closing some axioms …
- 11:15 AM Changeset [1292] by
- more added to rtlabs translation
- 10:20 AM Changeset [1291] by
- Started branch of untrusted compiler with indexed labels * added …
Oct 4, 2011:
- 2:00 AM Changeset [1290] by
- One more function ported to new Joint.
- 1:57 AM Changeset [1289] by
- semantics ported to latest Joint version
Oct 3, 2011:
- 5:33 PM Changeset [1288] by
- more added to rtlabs to rtl pass
- 4:55 PM Changeset [1287] by
- about 3/4 of the way through rtlabs to rtl now
- 4:07 PM Changeset [1286] by
- more changes to the rtl abs to rtl pass
- 3:08 PM Changeset [1285] by
- more implementation on maps, final push to get rtl abs to rtl working
- 8:35 AM Changeset [1284] by
- Bugs fixed: fresh_label changes the label universe, but this was not …
Sep 30, 2011:
- 3:12 AM Changeset [1283] by
- Bad programming practice removed: change_label is no longer required …
Sep 28, 2011:
- 11:50 PM Changeset [1282] by
- Cosmetic change: names of joint statements/instructions shortened and …
- 11:08 PM Changeset [1281] by
- Porting of all transformation to the joint syntax practically …
- 2:43 AM Changeset [1280] by
- Some progress in the porting of RTLAbstoRTL to the joint syntax: 1) …
- 2:41 AM Changeset [1279] by
- Bug fixed in definition of ltb.
Sep 27, 2011:
- 9:57 AM Changeset [1278] by
- oppargs requires two more arguments. RTLtoERTL to be fixed since it …
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.
Note: See TracTimeline
for information about the timeline view.
