|
|
|
@2474
|
8 years |
tranquil |
changed form of a statement
|
|
|
|
@2473
|
8 years |
tranquil |
put some generic stuff we need in the back end in extraGlobalenvs …
|
|
|
|
@2470
|
8 years |
tranquil |
completely separated program counters from code pointers in joint …
|
|
|
|
@2467
|
8 years |
piccolo |
LINEARISE PROOF MODIFIED NOT YED FIXED
|
|
|
|
@2464
|
8 years |
piccolo |
adapted lineariseProof to new semantics
|
|
|
|
@2462
|
8 years |
tranquil |
separated in back end values program counters from code pointers …
|
|
|
|
@2457
|
8 years |
tranquil |
rewritten function handling in joint
swapped call_rel with ret_rel in …
|
|
|
|
@2456
|
8 years |
boender |
- added simple proof
|
|
|
|
@2452
|
8 years |
piccolo |
Completed commutation lemmas of fetch_statement
|
|
|
|
@2447
|
8 years |
piccolo |
All axioms opened so far and that must be closed here have been
closed.
|
|
|
|
@2446
|
8 years |
piccolo |
Fetch commutation proof reduced to one simple (?) lemma.
|
|
|
|
@2445
|
8 years |
piccolo |
1. sigma function axiomatically defined (together with
its spec). …
|
|
|
|
@2443
|
8 years |
tranquil |
changed joint's stack pointer and internal stack
|
|
|
|
@2442
|
8 years |
piccolo |
Traces repaired. (By Paolo)
Statement of lineariseProof in place.
|
|
|
|
@2440
|
8 years |
piccolo |
fixed range_strong and linearise
(commit by Paolo, he's to blame in case)
|
|
|
|
@2437
|
8 years |
tranquil |
generalised calls to calls with pointers
|
|
|
|
@2426
|
8 years |
boender |
- updated stacksize to reflect new developments, completed proof
- …
|
|
|
|
@2422
|
8 years |
tranquil |
adapted joint to cl_call f
|
|
|
|
@2417
|
8 years |
boender |
- reverted changes to StructuredTraces? (shouldn't have been committed …
|
|
|
|
@2398
|
8 years |
boender |
- committed start of stacksize
|
|
|
|
@2324
|
8 years |
tranquil |
semantics of blocks: function to produce trace from execution of …
|
|
|
|
@2286
|
8 years |
tranquil |
Big update!
* merge of all _paolo variants
* reorganised some depends …
|
|
|
|
@2233
|
9 years |
tranquil |
* completed update of ERTL semantics
* some minor changes in joint …
|
|
|
|
@2217
|
9 years |
tranquil |
* collapsed step_params, unserialized_params, funct_params and …
|
|
|
|
@2214
|
9 years |
tranquil |
* changed order of parameters of joint_internal_function and genv in …
|
|
|
|
@2208
|
9 years |
tranquil |
* moving some code around
* changed immediates to hold beval in …
|
|
|
|
@2200
|
9 years |
tranquil |
* updated joint semantics: generation of linear and graph semantics
* …
|
|
|
|
@2186
|
9 years |
tranquil |
updated joint semantics
|
|
|
|
@2185
|
9 years |
campbell |
Use bitvectors for offsets.
|
|
|
|
@2182
|
9 years |
tranquil |
updated linearisation pass
|
|
|
|
@2176
|
9 years |
campbell |
Remove memory spaces other than XData and Code; simplify pointers as a …
|
|
|
|
@2162
|
9 years |
tranquil |
* yet another correction to joint
* added functions adding prologues …
|
|
|
|
@2155
|
9 years |
tranquil |
updates to blocks and RTLabs to RTL translation (which sidesteps …
|
|
|
|
@2103
|
9 years |
campbell |
Make transform_*program take a more general transformation to make …
|
|
|
|
@2043
|
9 years |
sacerdot |
Broken code commented out.
|
|
|
|
@2042
|
9 years |
sacerdot |
Repaired (Type => DeqSet?)
|
|
|
|
@1999
|
9 years |
campbell |
Make back-end use the main global envs.
|
|
|
|
@1995
|
9 years |
campbell |
Overall compiler definition; bits and pieces to
make everything happy(ish).
|
|
|
|
@1993
|
9 years |
campbell |
Make front-end memory model only depend on the general definitions by …
|
|
|
|
@1988
|
9 years |
campbell |
Abstraction of the memory contents in the memory models is no longer …
|
|
|
|
@1987
|
9 years |
campbell |
Move BEValues to common to reflect their use in the memory model for …
|
|
|
|
@1976
|
9 years |
tranquil |
* monads: just changed some defs, which had to be propagated in some …
|
|
|
|
@1949
|
9 years |
tranquil |
* lemma trace rel to eq flatten trace
* some more properties of …
|
|
|
|
@1908
|
9 years |
fguidi |
notation fixup following last commit of matita
we shifted the levels …
|
|
|
|
@1882
|
9 years |
tranquil |
big update, alas incomplete:
joint changed a bit, and all BE languages …
|
|
|
|
@1874
|
9 years |
campbell |
First cut at using back-end memory model throughout.
Note the …
|
|
|
|
@1709
|
9 years |
mulligan |
Changes to the execution of the MOVC instruction
|
|
|
|
@1644
|
9 years |
tranquil |
minor changes
|
|
|
|
@1643
|
9 years |
tranquil |
* some changes in everything
* separated extensions in sequential and …
|
|
|
|
@1641
|
9 years |
tranquil |
* semanticsUtils_paolo.ma contains code to generate both graph and …
|
|
|
|
@1640
|
9 years |
tranquil |
* finished fork of semantics.ma
* unification of Errors under the …
|
|
|
|
@1635
|
9 years |
tranquil |
* lists with binders and monads
* Joint.ma and other temprarily …
|
|
|
|
@1601
|
9 years |
sacerdot |
Files ported to new version of the standard library.
|
|
|
|
@1599
|
9 years |
sacerdot |
Start of merging of stuff into the standard library of Matita.
|
|
|
|
@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.
|
|
|
|
@1515
|
9 years |
campbell |
Add type of maps on positive binary numbers, and use them for …
|
|
|
|
@1472
|
9 years |
mulligan |
moved proof utils to erasure.ma
|
|
|
|
@1471
|
9 years |
mulligan |
finished erasure and generalised so as to work on arbitrary joint programs
|
|
|
|
@1470
|
9 years |
mulligan |
finished, pretty ugly though as matita's disambiguation is a …
|
|
|
|
@1469
|
9 years |
mulligan |
finished new relabelling for graphs subject to one axiom closed
|
|
|
|
@1467
|
9 years |
mulligan |
small change, adding entry and exit labels into the internal function, …
|
|
|
|
@1466
|
9 years |
mulligan |
erasure for graph based joint languages almost complete
|
|
|
|
@1463
|
9 years |
mulligan |
added erasure for lin
|
|
|
|
@1458
|
9 years |
mulligan |
added skeleton file for erasure function for joint languages
|
|
|
|
@1457
|
9 years |
sacerdot |
Bug fixed: when calling an internal function, the pc block is now set …
|
|
|
|
@1452
|
9 years |
sacerdot |
Bug fixed: labels MUST be represented as pointers whose block is the …
|
|
|
|
@1451
|
9 years |
sacerdot |
1. All axioms in LIN/semantics.ma closed
2. succ_pc and …
|
|
|
|
@1430
|
9 years |
sacerdot |
Bug fixed: push/pop must work on the isp (now added).
Note: the sp is …
|
|
|
|
@1419
|
9 years |
sacerdot |
All axioms closed.
|
|
|
|
@1416
|
9 years |
sacerdot |
Maps from hardware registers to beval now implemented in ASM/I8051 (in …
|
|
|
|
@1415
|
9 years |
sacerdot |
1. hwreg_store/retrieve no longer returns a res (but it is still …
|
|
|
|
@1411
|
9 years |
sacerdot |
1. sem_params2 splitted into sem_params1 + sem_params2 to take out the …
|
|
|
|
@1408
|
9 years |
sacerdot |
1. Added joint/BEGlobalenvs that is a modification of …
|
|
|
|
@1395
|
9 years |
sacerdot |
1) New versions of pointer_of_beval/beval_of_pointer with a stricter …
|
|
|
|
@1390
|
9 years |
sacerdot |
All fetch_result implementations have been factorized out, leaving …
|
|
|
|
@1387
|
9 years |
sacerdot |
Further simplification *params1 no longer used.
|
|
|
|
@1386
|
9 years |
sacerdot |
Structure of semantic parameters simplified.
|
|
|
|
@1385
|
9 years |
sacerdot |
1. fetch_result and pop_frame now takes the genv in input
2. …
|
|
|
|
@1384
|
9 years |
sacerdot |
* fetch_ra taken out of pop_frame again since it is used uniformly and …
|
|
|
|
@1383
|
9 years |
sacerdot |
Potential bug fixed and bug found: the way pointers and labels are put …
|
|
|
|
@1382
|
9 years |
sacerdot |
- succ_pc generalized to return a res (necessary for LIN semantics)
- …
|
|
|
|
@1380
|
9 years |
sacerdot |
LTL and LIN semantics factorized out in joint_LTL_LIN_semantics.ma. …
|
|
|
|
@1377
|
9 years |
sacerdot |
pop_frame now incorporates the fetch_result (that made sense only for …
|
|
|
|
@1376
|
9 years |
sacerdot |
Stack deallocation for RTL implemented in pop_frame.
|
|
|
|
@1372
|
9 years |
sacerdot |
save_frame now takes the stacksize to allow RTL to allocate the stack frame
|
|
|
|
@1371
|
9 years |
sacerdot |
save_frame changed to accept also the formal/actual argument pairs, …
|
|
|
|
@1359
|
9 years |
sacerdot |
1. more work on the RTL semantics
2. changes to joint/semantics to …
|
|
|
|
@1352
|
9 years |
sacerdot |
This commit is made necessary by the last Matita change.
Inclusion is …
|
|
|
|
@1329
|
9 years |
sacerdot |
1. Definition of addresses moved to BEMem
2. Basic functions on …
|
|
|
|
@1324
|
9 years |
sacerdot |
The semantics of extended statements must also consider the label …
|
|
|
|
@1312
|
9 years |
sacerdot |
Type of frame operations (pop_frame/save_frame) generalized to take in …
|
|
|
|
@1303
|
9 years |
sacerdot |
1. LTL/semantics.ma added (work in progress)
2. init_locals fixed to …
|
|
|
|
@1302
|
9 years |
sacerdot |
ERTL/semantics.ma ported to joint/SemanticUtils (in progress)
|
|
|
|
@1300
|
9 years |
sacerdot |
More (graph) axioms implemented. Look at the comments marked with XXX …
|
|
|
|
@1299
|
9 years |
sacerdot |
Functions from RTL/semantics.ma generalized to work on every graph …
|
|
|
|
@1298
|
9 years |
sacerdot |
- fetch_statement now takes in input the globalenv
- fetch_statement …
|
|
|
|
@1294
|
9 years |
sacerdot |
RTL semantics: porting to joint semantics started.
|
|
|
|
@1289
|
9 years |
sacerdot |
semantics ported to latest Joint version
|
|
|
|
@1284
|
9 years |
sacerdot |
Bugs fixed: fresh_label changes the label universe, but this was not …
|
|
|
|
