source: src/joint

Revision Log Mode:


Legend:

Added
Modified
Copied or renamed
Diff Rev Age Author Log Message
(edit) @3262   7 years piccolo reverted status_simulation_utils
(edit) @3261   7 years piccolo reverted joint_semantics rtl_semantics and ltl_semantics
(edit) @3259   7 years piccolo changed ERTL semantics: 1) added manipulation of stack pointer …
(edit) @3154   7 years piccolo 1) changed block_of_call in order to prevent pre-main calls 2) …
(edit) @3145   7 years tranquil * removed sigma types from traces of intensional events * completed …
(edit) @3118   7 years piccolo 1) finished return case in StatusSimulationHelper? 2) started to write …
(edit) @3050   7 years piccolo 1) Added general commutation theorem for monads. 2) Added some …
(edit) @3042   7 years sacerdot Repaired.
(edit) @3041   7 years sacerdot Repaired
(edit) @3037   7 years tranquil * ADDRESS joint instruction now has also an offset * corrected call to …
(edit) @3014   7 years tranquil ERTL to ERTLptr pass suppressed (it introduced a bug in the later …
(edit) @2996   7 years sacerdot Printing of graphs now starts from the entry point.
(edit) @2991   7 years piccolo Fixed cond and seq case in StatusSimulationHelper? Added cost case in …
(edit) @2985   7 years sacerdot Order of printing of lines in LIN fixed again, truly this time. But I …
(edit) @2983   7 years sacerdot LIN code was printed in reverse order. But I have not really …
(edit) @2982   7 years sacerdot Pretty priting of LIN implemented.
(edit) @2980   7 years tranquil fixed b_graph_translate
(edit) @2973   7 years tranquil semanticUtils adapted to changes in TranslateUtils?
(edit) @2970   7 years tranquil now joint_if_entry can change when a preamble is added, so code points …
(edit) @2968   7 years sacerdot The initial status memory was not really initialized. Now it is.
(edit) @2967   7 years sacerdot Semantics changed so that a terminating joint program that returns an …
(edit) @2957   7 years tranquil fixed semantics_blocks
(edit) @2954   7 years tranquil resolved circular dependency for ERTLptr's semantics
(edit) @2952   7 years tranquil * corrected all back-end premains to not pass any arguments to the …
(edit) @2950   7 years sacerdot linearise repaired (did I do the right thing???)
(edit) @2946   7 years tranquil main novelties: * there is an in-built stack_usage nat in joint …
(edit) @2940   7 years sacerdot 1. StatusSimulationHelper? changed to allow to use status_rel that …
(edit) @2939   7 years sacerdot Major problem: in order to accomodate the ERTLptrToLTL proof pass, the …
(edit) @2932   7 years sacerdot Same comment as previous commit on this file: the previous commit was …
(edit) @2929   7 years sacerdot Bug fixed: the coercion mechanism made you think that the CALL case …
(edit) @2920   7 years sacerdot dos2unix-ed
(edit) @2898   7 years piccolo 1) simplification of cond and seq case for StatusSimulationHelper?
(edit) @2891   7 years piccolo added precondition on seq statement and tested correct in the …
(edit) @2886   7 years piccolo partial commit
(edit) @2885   7 years sacerdot Hint at how to change everything.
(edit) @2883   7 years piccolo partial commit
(edit) @2879   7 years tranquil changed coercion from list of joint_seq to blocks to a more efficient one
(edit) @2878   7 years tranquil backtracked some changes that were not ready for commit
(edit) @2876   7 years tranquil corrected another endianess bug in joint_semantics. Switched some …
(edit) @2869   7 years tranquil some reorganization of definitions, and a new taaf_append_taaf
(edit) @2865   7 years sacerdot
(edit) @2863   7 years piccolo Added new invariant to good_if Generalized version of cond case for …
(edit) @2859   7 years sacerdot Pretty printing improved (now it always starts the visit from lbl 1).
(edit) @2858   7 years sacerdot Trying to pretty print the code graph in visit order. Slightly bugged …
(edit) @2855   7 years piccolo little bug fixed in TranslateUtils?.
(edit) @2853   7 years sacerdot Pretty printing of line/label numbers.
(edit) @2851   7 years piccolo partial commit
(edit) @2847   7 years sacerdot
(edit) @2846   7 years sacerdot Pretty printing of joint programs.
(edit) @2843   7 years piccolo 1) Fixed a litte bug in Joint.ma 2) ERTL to ERTLptr correctness proof …
(edit) @2824   7 years tranquil * moved sum on lists notation to extranat * used sum on lists to …
(edit) @2823   7 years tranquil * corrected bug in ERTL semantics (both delframe and newframe did the …
(edit) @2821   7 years tranquil * implemented preclassified system for joint (in joint/joint_fullexec.ma)
(edit) @2817   7 years sacerdot Repaired after Paolo's commit.
(edit) @2816   7 years sacerdot Repaired after Paolo's commit.
(edit) @2808   7 years tranquil added local_stacksize to joint internal functions to accomodate for …
(edit) @2806   7 years tranquil new b_graph_translate obligations
(edit) @2796   7 years tranquil * added global notation for existence in Type[1] (\exists[1] x.P) * in …
(edit) @2785   7 years piccolo Traces.ma repaired
(edit) @2784   7 years sacerdot Repaired after Mauro's commit.
(edit) @2783   7 years piccolo modified joint_closed_internal_function definition (added condition on …
(edit) @2774   7 years sacerdot 1. the compiler now outputs both the stack cost model and the max …
(edit) @2760   7 years sacerdot 1. Many files repaired. 2. 3 new daemons: 2 in Assembly.ma, 1 in …
(edit) @2757   7 years tranquil many things are still broken, but there is a partial backtrack on …
(edit) @2755   7 years tranquil * changed primitives of abstract status (with stuf that is probably …
(edit) @2723   7 years campbell Library name typo fixed.
(edit) @2716   7 years sacerdot utilities/deqsets.ma => utilities/deqsets_extra.ma for extraction
(edit) @2712   7 years tranquil changed some fields of joint_internal_function's invariant fixed linearise
(edit) @2708   7 years tranquil fixed linearise and LINToASM LINToASM has now correct transformation …
(edit) @2702   7 years sacerdot 1. proof closed in ASM/UtilBranch 2. more passes integrated in the …
(edit) @2688   7 years tranquil * in Arithmeticcs.ma: commented include that breaks script in latest …
(edit) @2687   7 years tranquil * polished some interfaces
(edit) @2683   7 years tranquil proof of properties of b_graph_program_transform (with an open axiom)
(edit) @2681   7 years tranquil * improvements to the graph translation function * fixed passes up to LTL
(edit) @2675   7 years tranquil * a generic graph program transformation
(edit) @2674   7 years tranquil * another change in block definition * RTLabs -> RTL and ERTL -> …
(edit) @2666   7 years piccolo bug fixed in blocks.ma
(edit) @2661   7 years sacerdot stacksize "repaired" by "considering" tailcalls Some daemons added …
(edit) @2655   7 years tranquil new step in code semantic lemma
(edit) @2647   7 years sacerdot Stupid typo fixed.
(edit) @2645   7 years sacerdot 1. some broken back-end files repaires, several still to go 2. the …
(edit) @2642   7 years piccolo fixed joint/Traces after having posed block 0 to be Code
(edit) @2641   7 years piccolo defined dummy block code equals to 0
(edit) @2639   7 years sacerdot We are not going to prove erasure. Thus this becomes dead code.
(edit) @2638   7 years piccolo Back-end fixes for last Garnier's commit that removes the regions from …
(edit) @2601   7 years sacerdot Extraction to ocaml is now working, with a couple of bugs left. One …
(edit) @2599   7 years tranquil * map_opt and map on positive maps are now clean (erase empty …
(edit) @2595   7 years tranquil * dropped locals and exit from definition of joint_if_function * new …
(edit) @2592   7 years piccolo main lemma of ERTLptr in place
(edit) @2590   7 years piccolo added monad machineary for ERTL to ERTLptr translation eval_seq_no_pc …
(edit) @2570   7 years piccolo ERTLtoERTLptr in place
(edit) @2564   7 years piccolo ERTL fully repaired, useless part of return value of pop_ra removed.
(edit) @2562   7 years piccolo linearise modified
(edit) @2561   7 years tranquil * moved CALL as different case than joint_seq: lots of broken code now …
(edit) @2559   7 years piccolo lineariseProof finished
(edit) @2557   7 years tranquil minor modification of commented (for now) proof of correctness of …
(edit) @2556   7 years tranquil in joint semantics and traces: added a last popped calling address to …
(edit) @2555   7 years piccolo lemma eval_call_ok finished
(edit) @2553   7 years tranquil as_classify changed to a partial function added a status for tailcalls
(edit) @2551   7 years piccolo completed isFinal and fetchStatementSigmaCommute. Fixed exit …
Note: See TracRevisionLog for help on using the revision log.