|
|
|
@2722
|
8 years |
campbell |
It's easier to keep the real function identifier in front-end …
|
|
|
|
@2677
|
8 years |
campbell |
Retain the pointer for the function called in front-end call states
so …
|
|
|
|
@2608
|
8 years |
garnier |
Regions are no more stored in blocks. block_region now tests the id, …
|
|
|
|
@2588
|
8 years |
garnier |
modified Cexec/Csem? semantics:
. force andbool and orbool types to be …
|
|
|
|
@2468
|
8 years |
garnier |
Floats are gone from the front-end. Some trace amount might remain in …
|
|
|
|
@2428
|
8 years |
campbell |
Tighten requirements on switch statements in Clight to only give …
|
|
|
|
@2391
|
9 years |
campbell |
Revert "Put the post-loop cost label into the Clight while statement …
|
|
|
|
@2353
|
9 years |
campbell |
Put the post-loop cost label into the Clight while statement to get …
|
|
|
|
@2176
|
9 years |
campbell |
Remove memory spaces other than XData and Code; simplify pointers as a …
|
|
|
|
@2106
|
9 years |
campbell |
Fix up a couple of proofs broken by recent changes.
|
|
|
|
@2019
|
9 years |
campbell |
Split out special induction principle for Clight from soundness file. …
|
|
|
|
@1988
|
9 years |
campbell |
Abstraction of the memory contents in the memory models is no longer …
|
|
|
|
@1876
|
9 years |
campbell |
Update Cexec soundness proof.
Change finishes_with predicate to …
|
|
|
|
@1713
|
9 years |
campbell |
Add a distinguished final state to the front-end languages to match up …
|
|
|
|
@1672
|
9 years |
campbell |
Matita now generates a couple of inversion lemmas that were manually …
|
|
|
|
@1647
|
9 years |
tranquil |
* corrected some notation problems
* adapted Cligth with slight …
|
|
|
|
@1545
|
9 years |
campbell |
Use pointer record in front-end.
|
|
|
|
@1516
|
9 years |
sacerdot |
Ported to syntax of Matita 0.99.1.
|
|
|
|
@1510
|
9 years |
sacerdot |
All files ported to new dependent inversion.
|
|
|
|
@1410
|
10 years |
campbell |
Remove a few old workarounds.
|
|
|
|
@1350
|
10 years |
sacerdot |
Porting to latest destruct tactic.
Note: the tactics has a few …
|
|
|
|
@1342
|
10 years |
sacerdot |
The new auto is much more powerful.
|
|
|
|
@1336
|
10 years |
sacerdot |
Ported to new Matita destruct/inversion.
One lemma fails at qed. …
|
|
|
|
@1244
|
10 years |
campbell |
Sort out Clight semantics equivalence proof for new SmallstepExec?.
|
|
|
|
@1224
|
10 years |
sacerdot |
Type of programs in common/AST made more dependent.
In particular, the …
|
|
|
|
@1139
|
10 years |
campbell |
Shift init_data out of generic program record so that it only appears …
|
|
|
|
@1058
|
10 years |
campbell |
Evict CompCert? Maps interface in favour of BitVectorTries?.
|
|
|
|
@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.
|
|
|
|
@882
|
10 years |
campbell |
Fix up fragile proofs for current version of matita.
|
|
|
|
@879
|
10 years |
campbell |
Refine "AST" types to include size/signedness information.
|
|
|
|
@797
|
10 years |
campbell |
Add error messages wherever the error monad is used.
Sticks to …
|
|
|
|
@744
|
10 years |
campbell |
Evict Coq-style integers from common/Integers.ma.
Make more bitvector …
|
|
|
|
@708
|
10 years |
campbell |
Use a more normalize-friendly definition of clight_exec to make the …
|
|
|
|
@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/CexecSound.ma:
|
|
|
|
@500
|
10 years |
campbell |
Use dependent pointer type to ensure that the representation is always …
|
