|
|
@2498
|
8 years |
mckinna |
Refactor:
Typedefs object_code and costlabel_map lifted out from …
|
|
|
@2497
|
8 years |
mckinna |
Simplified dependencies on ASM; knock-on from changes in ASM/*.ma
|
|
|
@2496
|
8 years |
garnier |
Some tentative work on the simulation proof for expressions, in order …
|
|
|
@2495
|
8 years |
piccolo |
continuing lineariseProof
|
|
|
@2494
|
8 years |
mckinna |
Removed BJC's axiomatisation of rtlabs_to_rtl, now that …
|
|
|
@2493
|
8 years |
mckinna |
Change in cst_well_defd to fix previously broken defn of …
|
|
|
@2492
|
8 years |
campbell |
Reduce axiomatisation in compiler.ma.
|
|
|
@2491
|
8 years |
tranquil |
fixed wrt change of list member definition
|
|
|
@2490
|
8 years |
tranquil |
switched back to Byte immediate (instead of beval ones)
propagated …
|
|
|
@2489
|
8 years |
campbell |
Conjecture some Clight/Cminor? simulation results.
|
|
|
@2488
|
8 years |
garnier |
glitch fixed
|
|
|
@2487
|
8 years |
campbell |
Set up "after_n_steps" to enforce an invariant on states.
|
|
|
@2486
|
8 years |
campbell |
First go at a generalised version of measurable.
|
|
|
@2485
|
8 years |
campbell |
Sketch of Clight/Cminor? callstate simulation
|
|
|
@2484
|
8 years |
piccolo |
fixed Traces and semantics
added commutation record (not yet finished) …
|
|
|
@2483
|
8 years |
garnier |
Memory injections for Clight to Cminor, partially axiomatized.
|
|
|
@2482
|
8 years |
campbell |
Note about front-end simulations
|
|
|
@2481
|
8 years |
piccolo |
corrected some inconsistencies
fixed some of lineariseProof
|
|
|
@2480
|
8 years |
mulligan |
Some more changes.
|
|
|
@2479
|
8 years |
mulligan |
A small amount of rewriting as i didn't like the original introduction …
|
|
|
@2478
|
8 years |
tranquil |
unified is_internal_function_of_program and is_internal_function
|
|
|
@2477
|
8 years |
tranquil |
status_simulation reformulated
definition of joint_classify split up …
|
|
|
@2476
|
8 years |
piccolo |
fixed commutation lemmas in lineariseProof
started proof of main …
|
|
|
@2475
|
8 years |
campbell |
Get compiler.ma and correctness.ma checking again. Note that the …
|
|
|
@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 …
|
|
|
@2472
|
8 years |
campbell |
Misc clight->cminor notes.
|
|
|
@2471
|
8 years |
campbell |
Tame global environments a little.
|
|
|
@2470
|
8 years |
tranquil |
completely separated program counters from code pointers in joint …
|
|
|
@2469
|
8 years |
campbell |
Fix up opaque type errors from recent changes.
|
|
|
@2468
|
8 years |
garnier |
Floats are gone from the front-end. Some trace amount might remain in …
|
|
|
@2467
|
8 years |
piccolo |
LINEARISE PROOF MODIFIED NOT YED FIXED
|
|
|
@2466
|
8 years |
campbell |
Show how global environments in clight to cminor pass match up.
|
|
|
@2465
|
8 years |
campbell |
Remove obsolete comment (runtime functions should be implemented later …
|
|
|
@2464
|
8 years |
piccolo |
adapted lineariseProof to new semantics
|
|
|
@2463
|
8 years |
tranquil |
swapped back call_rel and ret_rel…
|
|
|
@2462
|
8 years |
tranquil |
separated in back end values program counters from code pointers …
|
|
|
@2461
|
8 years |
campbell |
First cut of inductive structured traces diagrams.
|
|
|
@2460
|
8 years |
campbell |
Rest of variable characterisation.
|
|
|
@2459
|
8 years |
campbell |
Syntax update
|
|
|
@2458
|
8 years |
campbell |
Clight to Cminor allocates stack variables to disjoint regions within …
|
|
|
@2457
|
8 years |
tranquil |
rewritten function handling in joint
swapped call_rel with ret_rel in …
|
|
|
@2456
|
8 years |
boender |
- added simple proof
|
|
|
@2455
|
8 years |
campbell |
Dump rough notes on RTLabs structured traces existence proof.
|
|
|
@2454
|
8 years |
campbell |
More misc notes on clight->cminor.
|
|
|
@2453
|
8 years |
tranquil |
come changes in monad notation to
* avoid pretty printed monsters
* …
|
|
|
@2452
|
8 years |
piccolo |
Completed commutation lemmas of fetch_statement
|
|
|
@2451
|
8 years |
mulligan |
Structured traces paper for Brian as per e-mail conversation yesterday.
|
|
|
@2450
|
8 years |
garnier |
Minor typo
|
|
|
@2449
|
8 years |
garnier |
Documentation added.
|
|
|
@2448
|
8 years |
garnier |
Comitting current state of switch removal.
|
|
|
@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). …
|
|
|
@2444
|
8 years |
campbell |
Some inversion lemmas for after_n_steps for dealing with >1 source …
|
|
|
@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.
|
|
|
@2441
|
8 years |
garnier |
Moved general stuff on memories from switchRemoval to MemProperties?, …
|
|
|
@2440
|
8 years |
piccolo |
fixed range_strong and linearise
(commit by Paolo, he's to blame in case)
|
|
|
@2439
|
8 years |
campbell |
Get a proper reverse mapping of function blocks to identifiers by …
|
|
|
@2438
|
8 years |
garnier |
Sync of the w.i.p. for switch removal.
|
|
|
@2437
|
8 years |
tranquil |
generalised calls to calls with pointers
|
|
|
@2436
|
8 years |
tranquil |
small changes
|
|
|
@2435
|
8 years |
tranquil |
new back end operations
|
|
|
@2434
|
8 years |
campbell |
Misc notes.
|
|
|
@2433
|
8 years |
campbell |
Tidy up Clight pointer comparison.
|
|
|
@2432
|
8 years |
campbell |
Remove off-the-end pointers from front end ops.
|
|
|
@2431
|
8 years |
campbell |
Fix in matita-out branch too.
|
|
|
@2430
|
8 years |
campbell |
Fix casting for conditionals in CompCert?-derived C parser.
|
|
|
@2429
|
8 years |
garnier |
Restrict semantics of pointer comparison to what CompCert? does - i.e. …
|
|
|
@2428
|
8 years |
campbell |
Tighten requirements on switch statements in Clight to only give …
|
|
|
@2427
|
8 years |
mulligan |
More work on explanation.
|
|
|
@2426
|
8 years |
boender |
- updated stacksize to reflect new developments, completed proof
- …
|
|
|
@2425
|
8 years |
mulligan |
Garrigue's stuff completely added to the paper. Need to explain the …
|
|
|
@2424
|
8 years |
mulligan |
Changes to the file including making a start on incorporating …
|
|
|
@2423
|
8 years |
tranquil |
as_classifier predicate → as_classify function
as_call predicate from …
|
|
|
@2422
|
8 years |
tranquil |
adapted joint to cl_call f
|
|
|
@2421
|
8 years |
tranquil |
added simulation of flat prefix, and comments to explain the code
|
|
|
@2420
|
8 years |
campbell |
Tidy away generic results about folds on positive/identifier maps.
|
|
|
@2419
|
8 years |
mulligan |
Some initial work.
|
|
|
@2418
|
8 years |
campbell |
Add a checking function for the uniqueness of cost labels in RTLabs …
|
|
|
@2417
|
8 years |
boender |
- reverted changes to StructuredTraces? (shouldn't have been committed …
|
|
|
@2416
|
8 years |
mulligan |
Some more minor changes
|
|
|
@2415
|
8 years |
campbell |
Add the ability to map blocks to symbols in preparation for stack space.
|
|
|
@2414
|
8 years |
mulligan |
Added bib file, done a little bit of rearrangement.
|
|
|
@2413
|
8 years |
tranquil |
* tal_rel corrected to include cases where tal_base_call \approx …
|
|
|
@2412
|
8 years |
campbell |
Tidy up measurable definition a bit more.
|
|
|
@2411
|
8 years |
sacerdot |
Extensible records implemented via option type.
One axiom left.
|
|
|
@2410
|
8 years |
mulligan |
Changes to Section 2.
|
|
|
@2409
|
8 years |
mulligan |
Some text about algebraic data types and their limitations. Needs to …
|
|
|
@2408
|
8 years |
sacerdot |
…
|
|
|
@2407
|
8 years |
campbell |
Sigh, continue in for loops was broken too.
|
|
|
@2406
|
8 years |
sacerdot |
Elimination principle committed.
|
|
|
@2405
|
8 years |
sacerdot |
Type of elimination principle generated + more lemmas.
|
|
|
@2404
|
8 years |
sacerdot |
Example finished.
|
|
|
@2403
|
8 years |
sacerdot |
More work, example almost finished up to recursive type.
|
|
|
@2402
|
8 years |
sacerdot |
Progress on parametric types.
|
|
|
@2401
|
8 years |
mulligan |
For Jaap's delight.
|
|
|
@2400
|
8 years |
sacerdot |
Some tests.
|
|
|
@2399
|
8 years |
campbell |
Fill in some details about the statement of correctness.
|
|
|