|
|
@1920
|
8 years |
campbell |
Most of the labelling simulation. Still need to sort out switch …
|
|
|
@1918
|
8 years |
tranquil |
using listb.ma now
|
|
|
@1917
|
8 years |
tranquil |
predicate for unrepeating traces, fused final_abstract_status with …
|
|
|
@1908
|
8 years |
fguidi |
notation fixup following last commit of matita
we shifted the levels …
|
|
|
@1902
|
8 years |
mulligan |
Reverted needless changes to StructuredTraces?
|
|
|
@1901
|
8 years |
mulligan |
Slight changes to StructuredTraces?: should not change too much
|
|
|
@1882
|
8 years |
tranquil |
big update, alas incomplete:
joint changed a bit, and all BE languages …
|
|
|
@1881
|
8 years |
campbell |
Resurrect version of exec_up_to which shows the final state.
|
|
|
@1880
|
8 years |
campbell |
Show that RTLabs flat traces are determined by their starting state, …
|
|
|
@1878
|
8 years |
campbell |
Enforce typing of constants in front-end, plus binops for RTLabs.
|
|
|
@1876
|
8 years |
campbell |
Update Cexec soundness proof.
Change finishes_with predicate to …
|
|
|
@1874
|
8 years |
campbell |
First cut at using back-end memory model throughout.
Note the …
|
|
|
@1873
|
8 years |
campbell |
Fix up earlier front-end value conversion work.
|
|
|
@1872
|
8 years |
campbell |
Make binary operations in Cminor/RTLabs properly typed.
A few extra …
|
|
|
@1812
|
8 years |
campbell |
Provide a combined type for terminating and non-terminating structured …
|
|
|
@1808
|
8 years |
campbell |
Create a Prop version of the non-terminating structured traces so that …
|
|
|
@1806
|
8 years |
campbell |
Show that we could construct RTLabs non-terminating structured traces …
|
|
|
@1783
|
8 years |
campbell |
Remove junk from non-terminating structured traces.
|
|
|
@1709
|
8 years |
mulligan |
Changes to the execution of the MOVC instruction
|
|
|
@1658
|
8 years |
mulligan |
asm costs changes from today
|
|
|
@1654
|
8 years |
campbell |
Corrections to structured trace definitions (see the mailing list). …
|
|
|
@1652
|
8 years |
campbell |
Forgot to apply 1583 to non-terminating case.
|
|
|
@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
|
8 years |
sacerdot |
1) Major refactoring: proofs moved where they should be.
2) New …
|
|
|
@963
|
8 years |
campbell |
Extra debugging aid for animation of semantics.
|
|
|