|
|
@728
|
10 years |
mulligan |
Changes from last two days.
|
|
|
@727
|
10 years |
campbell |
Enough fixes to let an RTLabs program run.
|
|
|
@726
|
10 years |
campbell |
Change identifiers to Words in Clight and RTLabs semantics.
|
|
|
@725
|
10 years |
campbell |
Do some light manual disambiguation to make Clight examples go through …
|
|
|
@724
|
10 years |
campbell |
More tractable version of bitvector_of_nat / nat_of_bitvector.
|
|
|
@723
|
10 years |
mulligan |
Added dependent type internalising the invariant that LIN function …
|
|
|
@722
|
10 years |
mulligan |
Committing changes from today. Several files do not typecheck.
|
|
|
@721
|
10 years |
mulligan |
Added diary of changes to project files.
|
|
|
@720
|
10 years |
campbell |
Sort out cost labels.
|
|
|
@719
|
10 years |
mulligan |
Added missing assembly file ported to matita.
|
|
|
@718
|
10 years |
campbell |
Add an AST type (i.e., intermediate language type) for pointers.
|
|
|
@717
|
10 years |
campbell |
Clean up Clight examples; better temporary definition of multiply.
|
|
|
@716
|
10 years |
mulligan |
Finished translating LTL statements to LIN statements. Need to …
|
|
|
@715
|
10 years |
mulligan |
Restored rev from Util as it appears that list reversal is not a part …
|
|
|
@714
|
10 years |
mulligan |
Work on translation from LTL to LIN.
|
|
|
@713
|
10 years |
mulligan |
Commit of initial LTL files.
|
|
|
@712
|
10 years |
mulligan |
Changes to get things to typecheck.
|
|
|
@711
|
10 years |
sacerdot |
…
|
|
|
@710
|
10 years |
campbell |
Start of way to import RTLabs from prototype compiler.
|
|
|
@709
|
10 years |
sacerdot |
Notations should NOT be redefined. Just add a new interpretation.
|
|
|
@708
|
10 years |
campbell |
Use a more normalize-friendly definition of clight_exec to make the …
|
|
|
@707
|
10 years |
campbell |
Remove old branch, which was merged after the move to src.
|
|
|
@706
|
10 years |
sacerdot |
Fixed (reference to basics/pairs was dandling).
|
|
|
@705
|
10 years |
sacerdot |
Ported to new library (notation).
|
|
|
@704
|
10 years |
sacerdot |
Minor speedup in one theorem (less automation).
|
|
|
@703
|
10 years |
sacerdot |
lib is now the default standard library (after commit 11216 in …
|
|
|
@702
|
10 years |
campbell |
Refine small-step executable semantics abstraction a little.
Some …
|
|
|
@701
|
10 years |
sacerdot |
New version.
|
|
|
@700
|
10 years |
campbell |
Get Clight semantics going again (except for problems CexecEquiv? that …
|
|
|
@699
|
10 years |
mulligan |
More or less finished formalisation of LIN.
|
|
|
@698
|
10 years |
mulligan |
Commit with changes to files to get our files to typecheck.
|
|
|
@697
|
10 years |
campbell |
Merge Clight branch of vectors and friends.
Start making stuff build.
|
|
|
@696
|
10 years |
mulligan |
Added missing I8051 file and completed most of LIN formalisation.
|
|
|
@695
|
10 years |
campbell |
Rearrange Clight files a bit - will try to make them work again soon…
|
|
|
@694
|
10 years |
campbell |
Start moving Clight into common directory.
|
|
|
@693
|
10 years |
campbell |
Separate out whole program executions from the clight semantics and …
|
|
|
@692
|
10 years |
mulligan |
Deleted files.
|
|
|
@691
|
10 years |
mulligan |
More movement of files within the repository.
|
|
|
@690
|
10 years |
mulligan |
Moved new matita files into correct place.
|
|
|
@689
|
10 years |
mulligan |
Got rid of old Matita development files.
|
|
|
@688
|
10 years |
mulligan |
Fixed local conflicts. Restructured svn repository.
|
|
|
@687
|
10 years |
mulligan |
Renamed to enforce consistency of filenames
|
|
|
@686
|
10 years |
mulligan |
Most of LIN completed.
|
|
|
@685
|
10 years |
ayache |
Bug fix in LINToASM (wrong conditional translation) in 8051 branch.
|
|
|
@684
|
10 years |
sacerdot |
Moved into Presentations.
|
|
|
@683
|
10 years |
mulligan |
Changes from working on my PC.
|
|
|
@682
|
10 years |
sacerdot |
…
|
|
|
@681
|
10 years |
sacerdot |
…
|
|
|
@680
|
10 years |
sacerdot |
8051-memoryspace-branch from Brian moved from D2.3 (that does not …
|
|
|
@679
|
10 years |
sacerdot |
The one in D2.2/8051 is more up to date. Committing this one was a …
|
|
|
@678
|
10 years |
amadio |
WP-rob update
|
|
|
@677
|
10 years |
campbell |
Use better titles for T3.2/3.3.
|
|
|
@676
|
10 years |
sacerdot |
…
|
|
|
@675
|
10 years |
sacerdot |
…
|
|
|
@674
|
10 years |
sacerdot |
…
|
|
|
@673
|
10 years |
regisgia |
* Cosmetics.
|
|
|
@672
|
10 years |
regisgia |
* Slides shuffling.
|
|
|
@671
|
10 years |
mulligan |
Finished demo script for tomorrow.
|
|
|
@670
|
10 years |
regisgia |
* New version of the video.
|
|
|
@669
|
10 years |
mulligan |
Fixed man months
|
|
|
@668
|
10 years |
mulligan |
small changes
|
|
|
@667
|
10 years |
mulligan |
Changes to presentation that claudio wanted
|
|
|
@666
|
10 years |
amadio |
WP-roberto update
|
|
|
@665
|
10 years |
sacerdot |
…
|
|
|
@664
|
10 years |
mulligan |
Changed output of Intel HEX files so we no longer have those …
|
|
|
@663
|
10 years |
regisgia |
* Video of prototype demonstration.
|
|
|
@662
|
10 years |
regisgia |
New version of the slides.
|
|
|
@661
|
10 years |
sacerdot |
Renaming.
|
|
|
@660
|
10 years |
sacerdot |
Final draft version.
|
|
|
@659
|
10 years |
sacerdot |
Draft version completed.
|
|
|
@658
|
10 years |
sacerdot |
…
|
|
|
@657
|
10 years |
campbell |
Mention cost labels in D3.1 summary slide.
|
|
|
@656
|
10 years |
amadio |
rob updated
|
|
|
@655
|
10 years |
regisgia |
* Slides from Yann.
|
|
|
@654
|
10 years |
sacerdot |
In progress
|
|
|
@653
|
10 years |
sacerdot |
New version, still a draft.
|
|
|
@652
|
10 years |
sacerdot |
Still unfinished.
|
|
|
@651
|
10 years |
campbell |
Small additions to WP3 slides.
|
|
|
@650
|
10 years |
mulligan |
Completed presentation slides by mentioning man hours used
|
|
|
@649
|
10 years |
mulligan |
Reworked presentation.
|
|
|
@648
|
10 years |
campbell |
Oops, wrong bitvector negation.
|
|
|
@647
|
10 years |
campbell |
Minor WP3 edits.
|
|
|
@646
|
10 years |
mulligan |
Got Search.ma working with Matita emulator.
|
|
|
@645
|
10 years |
ayache |
Pretty output in D2.2.
|
|
|
@644
|
10 years |
mulligan |
Committed files for demo on Friday. Binary search works with O'Caml …
|
|
|
@643
|
10 years |
ayache |
Bug fix in ASMCosts in D2.2.
|
|
|
@642
|
10 years |
ayache |
Added the review example in D2.2 (8051/tests/review1/)
|
|
|
@641
|
10 years |
ayache |
Improvement in the code of the cost computation in D2.2.
|
|
|
@640
|
10 years |
ayache |
Hex output not too long for mcu anymore. Readable output added.
|
|
|
@639
|
10 years |
campbell |
Preliminary work on RTLabs semantics
Will move to somewhere more …
|
|
|
@638
|
10 years |
campbell |
Switch to more conservative definitions in preparation for review. …
|
|
|
@637
|
10 years |
campbell |
First draft of WP3 slides.
|
|
|
@636
|
10 years |
campbell |
A few definitions that will be useful for some preliminary rtlabs …
|
|
|
@635
|
10 years |
campbell |
Some commentary.
|
|
|
@634
|
10 years |
ayache |
Bug fix in ASMCosts in D2.2.
|
|
|
@633
|
10 years |
amadio |
wp2 revised
|
|
|
@632
|
10 years |
ayache |
Small change in ASMCosts.
|
|
|
@631
|
10 years |
ayache |
Some bugs fixed in D2.2.
|
|
|
@630
|
10 years |
ayache |
Paris update in D2.2.
|
|
|
@629
|
10 years |
mulligan |
Fixed some slides: added description of WP4.1
|
|
|