|
|
|
@2677
|
8 years |
campbell |
Retain the pointer for the function called in front-end call states
so …
|
|
|
|
@2428
|
8 years |
campbell |
Tighten requirements on switch statements in Clight to only give …
|
|
|
|
@2391
|
8 years |
campbell |
Revert "Put the post-loop cost label into the Clight while statement …
|
|
|
|
@2353
|
8 years |
campbell |
Put the post-loop cost label into the Clight while statement to get …
|
|
|
|
@1713
|
9 years |
campbell |
Add a distinguished final state to the front-end languages to match up …
|
|
|
|
@1605
|
9 years |
sacerdot |
Porting to last standard library of Matita.
|
|
|
|
@1566
|
9 years |
campbell |
Pacify changes to destruct tactic.
|
|
|
|
@1521
|
9 years |
sacerdot |
Syntax change in Matita: change what where => change where what.
|
|
|
|
@1516
|
9 years |
sacerdot |
Ported to syntax of Matita 0.99.1.
|
|
|
|
@1510
|
9 years |
sacerdot |
All files ported to new dependent inversion.
|
|
|
|
@1352
|
9 years |
sacerdot |
This commit is made necessary by the last Matita change.
Inclusion is …
|
|
|
|
@1350
|
9 years |
sacerdot |
Porting to latest destruct tactic.
Note: the tactics has a few …
|
|
|
|
@1344
|
9 years |
sacerdot |
Ported to new destruct.
|
|
|
|
@1244
|
9 years |
campbell |
Sort out Clight semantics equivalence proof for new SmallstepExec?.
|
|
|
|
@1216
|
9 years |
campbell |
Update Clight semantics equivalence proof to match changes in …
|
|
|
|
@961
|
10 years |
campbell |
Use precise bitvector sizes throughout the front end, rather than …
|
|
|
|
@891
|
10 years |
campbell |
Revise proofs affected by recent matita change.
|
|
|
|
@798
|
10 years |
campbell |
Fix usual matita tactic mistake.
|
|
|
|
@797
|
10 years |
campbell |
Add error messages wherever the error monad is used.
Sticks to …
|
|
|
|
@732
|
10 years |
campbell |
Fixups for CexecEquiv? due to earlier changes in SmallstepExec?.ma
|
|
|
|
@708
|
10 years |
campbell |
Use a more normalize-friendly definition of clight_exec to make the …
|
|
|
|
@702
|
10 years |
campbell |
Refine small-step executable semantics abstraction a little.
Some …
|
|
|
|
@700
|
10 years |
campbell |
Get Clight semantics going again (except for problems CexecEquiv? that …
|
|
|
|
@694
|
10 years |
campbell |
Start moving Clight into common directory.
|
|
copied from Deliverables/D3.1/C-semantics/CexecEquiv.ma:
|
|
|
|
@487
|
10 years |
campbell |
Port Clight semantics to the new-new matita syntax.
|
