|
|
@1647
|
8 years |
tranquil |
* corrected some notation problems
* adapted Cligth with slight …
|
|
|
@1640
|
8 years |
tranquil |
* finished fork of semantics.ma
* unification of Errors under the …
|
|
|
@1635
|
8 years |
tranquil |
* lists with binders and monads
* Joint.ma and other temprarily …
|
|
|
@1631
|
8 years |
campbell |
Use fact that type environments in Cminor have distinct variables to …
|
|
|
@1627
|
8 years |
campbell |
Add some notions of freshness, and start using them for temporary …
|
|
|
@1626
|
8 years |
campbell |
Add extra type safety in front end. NB: critical freshness parts …
|
|
|
@1609
|
8 years |
boender |
- added alias to ASM/BitVectorTrie
- removed double include from …
|
|
|
@1608
|
8 years |
sacerdot |
Porting to new library still in progress.
|
|
|
@1601
|
8 years |
sacerdot |
Files ported to new version of the standard library.
|
|
|
@1599
|
8 years |
sacerdot |
Start of merging of stuff into the standard library of Matita.
|
|
|
@1598
|
8 years |
mulligan |
changes over the last couple of days
|
|
|
@1583
|
8 years |
campbell |
More on RTLabs structured traces.
Fixed mistake in structure trace …
|
|
|
@1574
|
8 years |
campbell |
A little more progress on traces on RTLabs.
|
|
|
@1566
|
8 years |
campbell |
Pacify changes to destruct tactic.
|
|
|
@1562
|
8 years |
mulligan |
new version of assembly, fixed conflict in positivemap.ma, changed …
|
|
|
@1555
|
8 years |
boender |
- changes to assembly
- added lookup to PositiveMap?
- lightly changed …
|
|
|
@1551
|
8 years |
campbell |
Functions to translate between back-end and front-end values.
|
|
|
@1545
|
8 years |
campbell |
Use pointer record in front-end.
|
|
|
@1544
|
8 years |
sacerdot |
StructuredTraces? inhabited for object code.
|
|
|
@1536
|
8 years |
campbell |
Use predicates throughout the structured traces.
|
|
|
@1535
|
8 years |
campbell |
Make RTLabs semantics use knowledge that the next instruction always …
|
|
|
@1532
|
8 years |
campbell |
Remove jump classification from structured traces.
|
|
|
@1531
|
8 years |
campbell |
A notion of abstract structured traces.
|
|
|
@1523
|
8 years |
campbell |
Separate out positive and Z definitions from extralib.ma.
Minor syntax …
|
|
|
@1516
|
8 years |
sacerdot |
Ported to syntax of Matita 0.99.1.
|
|
|
@1515
|
8 years |
campbell |
Add type of maps on positive binary numbers, and use them for …
|
|
|
@1512
|
8 years |
campbell |
Shorten proof of goal that solves now.
|
|
|
@1510
|
8 years |
sacerdot |
All files ported to new dependent inversion.
|
|
|
@1480
|
8 years |
sacerdot |
Proof changed (to use new automation).
BUG FOUND: automation fails if …
|
|
|
@1465
|
8 years |
sacerdot |
Dead code removed.
|
|
|
@1410
|
8 years |
campbell |
Remove a few old workarounds.
|
|
|
@1401
|
8 years |
ricciott |
Changes concerning the new behavior of destruct.
|
|
|
@1395
|
8 years |
sacerdot |
1) New versions of pointer_of_beval/beval_of_pointer with a stricter …
|
|
|
@1369
|
8 years |
campbell |
Put type information into front-end unary ops.
Slight change to …
|
|
|
@1368
|
8 years |
sacerdot |
A bug in the clear tactic makes the previous (correct) commit wrong. …
|
|
|
@1367
|
8 years |
sacerdot |
Proof improvement, still somehow a bit slow.
|
|
|
@1355
|
8 years |
sacerdot |
monadic fold_lefti added
|
|
|
@1353
|
8 years |
sacerdot |
This commit is made necessary by the last Matita change.
Inclusion is …
|
|
|
@1351
|
8 years |
campbell |
Tidy up some loose ends from the invariants branch merge.
|
|
|
@1350
|
8 years |
sacerdot |
Porting to latest destruct tactic.
Note: the tactics has a few …
|
|
|
@1347
|
8 years |
campbell |
Remove obsolete definitions.
|
|
|
@1339
|
8 years |
sacerdot |
Automation is now stronger.
|
|
|
@1316
|
8 years |
campbell |
Merge in id-lookup-branch to trunk.
|
|
|
@1268
|
8 years |
sacerdot |
1) AST/Identifier.ma no longer used, utilities/IdentifierTools no …
|
|
|
@1253
|
8 years |
mulligan |
uses.ma finished
|
|
|
@1233
|
8 years |
sacerdot |
1) Ported to Brian's new dependent type for fullexec
2) Universe level …
|
|
|
@1231
|
8 years |
campbell |
Change SmallstepExec? so that states can depend on global information. …
|
|
|
@1225
|
8 years |
campbell |
Missing ; in proof
|
|
|
@1224
|
8 years |
sacerdot |
Type of programs in common/AST made more dependent.
In particular, the …
|
|
|
@1215
|
8 years |
sacerdot |
1) Added shifting directly on pointers
2) More temporary axioms closed.
|
|
|
@1214
|
8 years |
sacerdot |
res_to_opt function added to common/Errors and used in joint/semantics …
|
|
|
@1213
|
8 years |
sacerdot |
1) New values (joint/BEValues.ma) and memory model for the back-ends
…
|
|
|
@1181
|
8 years |
mulligan |
changed smallstep exec in order to remove matita bug (superposition.ml …
|
|
|
@1139
|
8 years |
campbell |
Shift init_data out of generic program record so that it only appears …
|
|
|
@1129
|
8 years |
mulligan |
removed conversions between Register and register
|
|
|
@1125
|
8 years |
sacerdot |
Monadic mfold_left2 added.
|
|
|
@1092
|
8 years |
campbell |
Some minor definitions for identifiers and lists.
|
|
|
@1082
|
8 years |
mulligan |
work from today on ertl -> ltl pass
|
|
|
@1080
|
8 years |
mulligan |
more added
|
|
|
@1077
|
8 years |
mulligan |
ack, dependent types are scary
|
|
|
@1072
|
8 years |
campbell |
Use not equals form of showing entry/exit labels.
|
|
|
@1070
|
8 years |
campbell |
Show that entry and exit labels are in the RTLabs graph.
|
|
|
@1068
|
8 years |
mulligan |
rtlabs translation complete subject to axioms
|
|
|
@1064
|
8 years |
mulligan |
changes from today, nearly complete rtlabs translation pass
|
|
|
@1060
|
8 years |
mulligan |
work from this morning and yesterday
|
|
|
@1059
|
8 years |
mulligan |
work from today, bit of a mess at the moment
|
|
|
@1058
|
8 years |
campbell |
Evict CompCert? Maps interface in favour of BitVectorTries?.
|
|
|
@1057
|
8 years |
mulligan |
changes from today
|
|
|
@1056
|
8 years |
campbell |
Switch to delayed identifier error scheme.
|
|
|
@1055
|
8 years |
mulligan |
changes to how identifiers are generated
|
|
|
@1053
|
8 years |
mulligan |
changes
|
|
|
@1052
|
8 years |
mulligan |
removed offsets after reading cerco mailing list
|
|
|
@1049
|
8 years |
mulligan |
more stuff added
|
|
|
@1047
|
8 years |
mulligan |
more work from today
|
|
|
@1046
|
8 years |
mulligan |
syntax of rtlabs was wrong: cast not const. more added to rtlabs --> …
|
|
|
@1045
|
8 years |
mulligan |
resolved conflict in rtlabs
|
|
|
@985
|
9 years |
sacerdot |
1) Major refactoring: proofs moved where they should be.
2) New …
|
|
|
@963
|
9 years |
campbell |
Extra debugging aid for animation of semantics.
|
|
|
@962
|
9 years |
campbell |
Casts should use source type's signedness, not the target's.
|
|
|
@961
|
9 years |
campbell |
Use precise bitvector sizes throughout the front end, rather than …
|
|
|
@891
|
9 years |
campbell |
Revise proofs affected by recent matita change.
|
|
|
@889
|
9 years |
sacerdot |
Minor changes because of the new, weaker (but much faster) delift.
|
|
|
@882
|
9 years |
campbell |
Fix up fragile proofs for current version of matita.
|
|
|
@881
|
9 years |
campbell |
Sort out regions in Cminor to fix Clight to Cminor translation of Ederef.
|
|
|
@880
|
9 years |
campbell |
Add type information into Cminor.
As a result, the Clight to Cminor …
|
|
|
@879
|
9 years |
campbell |
Refine "AST" types to include size/signedness information.
|
|
|
@849
|
9 years |
sacerdot |
…
|
|
|
@816
|
9 years |
campbell |
Clight to Cminor compilation, modulo switch statements, temporary …
|
|
|
@797
|
9 years |
campbell |
Add error messages wherever the error monad is used.
Sticks to …
|
|
|
@795
|
9 years |
mulligan |
Changes from this morning.
|
|
|
@793
|
9 years |
mulligan |
Work from today on rtlabs -> rtl pass.
|
|
|
@790
|
9 years |
campbell |
A little tidying: get rid of requirement for jmeq in Mem.ma, remove …
|
|
|
@789
|
9 years |
mulligan |
More work on rtlabs -> rtl pass.
|
|
|
@782
|
9 years |
mulligan |
More work on rtl-ertl pass from today, plus resolved conflict.
|
|
|
@781
|
9 years |
campbell |
Implement labelling pass for Clight.
|
|
|
@779
|
9 years |
campbell |
Add merging of tries and identifier sets (based on Dominic's earlier …
|
|
|
@777
|
9 years |
mulligan |
Lots of work on RTL to ERTL pass from today.
|
|
|
@774
|
9 years |
campbell |
Separate out the different forms of addition and subtraction in the …
|
|
|
@764
|
9 years |
campbell |
Start Cminor to RTLabs phase.
Includes some syntax for matching …
|
|
|
@761
|
9 years |
campbell |
Enforce the use of declared identifiers/registers in Cminor/RTLabs.
|
|
|