|
|
@2522
|
8 years |
sacerdot |
Generic stuff moved to infrastructure.
|
|
|
@2521
|
8 years |
sacerdot |
..
|
|
|
@2520
|
8 years |
sacerdot |
Now it is nice!
|
|
|
@2519
|
8 years |
mulligan |
To prevent conflicts
|
|
|
@2518
|
8 years |
sacerdot |
…
|
|
|
@2517
|
8 years |
sacerdot |
…
|
|
|
@2516
|
8 years |
mckinna |
removed typedefs; restored older versions; moved typedefs to …
|
|
|
@2515
|
8 years |
sacerdot |
…
|
|
|
@2514
|
8 years |
sacerdot |
All .ma files committed: some of them are just in-progress.
|
|
|
@2513
|
8 years |
mckinna |
Minor tweaks. Simplified dependencies again.
|
|
|
@2512
|
8 years |
mckinna |
Simplified dependencies on ASM, to allow rollback to when …
|
|
|
@2511
|
8 years |
campbell |
Conjecture main Cminor/RTLabs simulation results.
Add a few notes …
|
|
|
@2510
|
8 years |
garnier |
Some progress on the Cl -> Cm front
|
|
|
@2509
|
8 years |
campbell |
misc note
|
|
|
@2508
|
8 years |
mckinna |
more tweaks. compiler and correctness still build.
|
|
|
@2507
|
8 years |
piccolo |
finished pop case in commutation eval_Seq_no_pc
|
|
|
@2506
|
8 years |
campbell |
Use common definition of measurable.
|
|
|
@2505
|
8 years |
mckinna |
Cleaned up compiler.ma; some refactoring/additional code needed in …
|
|
|
@2504
|
8 years |
mckinna |
More refactoring to support the tidied up compiler.ma
|
|
|
@2503
|
8 years |
mckinna |
tidied up, with new auxiliary defns, some refactoring, some code …
|
|
|
@2502
|
8 years |
campbell |
Sketch a little about how measurable traces might work with RTLabs and …
|
|
|
@2501
|
8 years |
piccolo |
working on lineariseProof. Not yet finished.
|
|
|
@2500
|
8 years |
garnier |
Continuing work on simulation in Clight/Cminor?
|
|
|
@2499
|
8 years |
campbell |
Separate out the RTLabs abstract status record from the proofs about …
|
|
|
@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 …
|
|
|