source:

Revision Log Mode:


Legend:

Added
Modified
Copied or renamed
Diff Rev Age Author Log Message
(edit) @3094   7 years sacerdot Makefile with targets: byte opt clean
(edit) @3093   7 years sacerdot Makefile replaces build, targets: byte, opt, clean
(edit) @3092   7 years sacerdot No more references to Lustre stuff.
(edit) @3091   7 years sacerdot …
(edit) @3090   7 years tassi dist: take into account symlink
(edit) @3089   7 years sacerdot Symbolic link to the cparser
(edit) @3088   7 years sacerdot We now also generate the package for native code.
(edit) @3087   7 years tassi script to build tarpall
(edit) @3086   7 years sacerdot extracted is now in driver
(edit) @3085   7 years sacerdot extracted directory moved into driver to make debian packages more …
(edit) @3084   7 years amadio
(edit) @3083   7 years sacerdot The cost and stack* variables are now initialized with the cost of …
(edit) @3082   7 years mckinna Tidying up: the long comment about preamble/renamed_symbols in the …
(edit) @3081   7 years campbell Tidy up recent work a little.
(edit) @3080   7 years sacerdot New extraction.
(edit) @3079   7 years tranquil added printing of ERTL, LTL and LIN's ext_seq's.
(edit) @3078   7 years tranquil fixed change of Mov
(edit) @3077   7 years sacerdot New extraction.
(edit) @3076   7 years mckinna simplified include dependencies
(edit) @3075   7 years mckinna Apologies for late folding in of old changes which were left over from …
(edit) @3074   7 years campbell Put some kind of high level proof in for front-end.
(edit) @3073   7 years sacerdot New extraction, all tests pass.
(edit) @3072   7 years tranquil corrected a bug (translate_store was wrong)
(edit) @3071   7 years sacerdot …
(edit) @3070   7 years sacerdot Ext case of RTL implemented.
(edit) @3069   7 years sacerdot New extraction.
(edit) @3068   7 years sacerdot Debugging code removed.
(edit) @3067   7 years sacerdot New test that fails too.
(edit) @3066   7 years tranquil * implemented get_arg_16 for ACC_DPTR * LINToASM is now agnostic as to …
(edit) @3065   7 years sacerdot Efficiency of semantics of assembled improved: ticks_of was …
(edit) @3064   7 years sacerdot Efficiency of the semantics of assembly improved by avoiding the …
(edit) @3063   7 years campbell Remove measure function from FEMeasurable because we're not using it …
(edit) @3062   7 years sacerdot Bug fixed in the semantics of Mov: the offset was ignored. Now all …
(edit) @3061   7 years sacerdot New extraction.
(edit) @3060   7 years sacerdot Bug fixed in the semantics of JMP. The bug was due to a bug in the …
(edit) @3059   7 years sacerdot New extraction
(edit) @3058   7 years tranquil …
(edit) @3057   7 years tranquil lookup of function identifiers was not corrected with sigma
(edit) @3056   7 years tranquil fixed a merge gone wrong
(edit) @3055   7 years campbell Start getting partial Clight to Cminor proof in shape for …
(edit) @3054   7 years campbell Put missing typ check in; adjust proof because I did it a little …
(edit) @3053   7 years campbell Cast simplification preserves measurable subtraces.
(edit) @3052   7 years tranquil …
(edit) @3051   7 years tranquil fixed order of global initialization in LINToASM. For the moment …
(edit) @3050   7 years piccolo 1) Added general commutation theorem for monads. 2) Added some …
(edit) @3049   7 years campbell Globalenvs and initial states for cast simplification.
(edit) @3048   7 years campbell Improve dependency for cast simplification.
(edit) @3047   7 years campbell Switch removal and labelling combined.
(edit) @3046   7 years campbell Main part of combined switch removal and labelling proof.
(edit) @3045   7 years tranquil fixed what made test3 fail. However it involves a different notion of …
(edit) @3044   7 years campbell Start showing combination of switch removal and labelling is OK. Fix …
(edit) @3043   7 years sacerdot New major extraction that should have solved all remaining issues. As …
(edit) @3042   7 years sacerdot Repaired.
(edit) @3041   7 years sacerdot Repaired
(edit) @3040   7 years tranquil fixed LINToASM
(edit) @3039   7 years tranquil * merged and extended MovSuccessor? and Mov in one instruction (Mov dst …
(edit) @3038   7 years sacerdot Bug fixed: the stack_cost* variables must be declared before the …
(edit) @3037   7 years tranquil * ADDRESS joint instruction now has also an offset * corrected call to …
(edit) @3036   7 years garnier Fixing some problems, progress, etc
(edit) @3035   7 years mckinna Tweak: tidied up ?/\ldots Conceptual: better monadic threading of …
(edit) @3034   7 years sacerdot Bug fixed: COST instructions are now assembled as NOP to prevent the …
(edit) @3033   7 years sacerdot Bug fixed: sign_extension was extending according to the _second_ bit, …
(edit) @3032   7 years campbell Remind myself why ms_rel_normal is reasonable.
(edit) @3031   7 years campbell Tidy up RTLabs preclassified_system definitions.
(edit) @3030   7 years campbell Break up front-end for correctness proof. Use let rec to prevent …
(edit) @3029   7 years sacerdot New extraction after DPH/DPL bug fixing.
(edit) @3028   7 years sacerdot Bug fixed: 82 and 83 (intended to be the addresses of DPH/DPL) should …
(edit) @3027   7 years sacerdot Another output used by the plug-in.
(edit) @3026   7 years sacerdot With -a we now produce also the .cerco file required by the plug-in.
(edit) @3025   7 years sacerdot 1. two syntax errors in instrumented files fixed 2. the compiler now …
(edit) @3024   7 years sacerdot Bug fixed: set_flags was ignoring the cy and ov flags.
(edit) @3023   7 years sacerdot Typo fixed. It made all GOTOs jump to random positions in the ASM code.
(edit) @3022   7 years campbell Make a couple of tests monadic for easier inversion.
(edit) @3021   7 years campbell Replace clight_clock_after with a more sensible definition that uses …
(edit) @3020   7 years sacerdot - Options not used removed from the help/interface. - More compliance …
(edit) @3019   7 years sacerdot New extraction after ERTLptr abortion.
(edit) @3018   7 years sacerdot 1) some files repaired 2) all stuff related to the aborted pass …
(edit) @3017   7 years sacerdot Repaired.
(edit) @3016   7 years tranquil fixed after previous commit
(edit) @3015   7 years sacerdot Comment removed
(edit) @3014   7 years tranquil ERTL to ERTLptr pass suppressed (it introduced a bug in the later …
(edit) @3013   7 years sacerdot Temporary parsing files removed.
(edit) @3012   7 years sacerdot Debugging code removed after bug fixing.
(edit) @3011   7 years sacerdot New extraction.
(edit) @3010   7 years tranquil same bug as was in liveness is now fixed
(edit) @3009   7 years sacerdot New extraction.
(edit) @3008   7 years tranquil corrected bug where the address of pointer calls was not defined as used
(edit) @3007   7 years campbell Sketch out how Cminor to RTLabs correctness would fit into the …
(edit) @3006   7 years sacerdot New extraction, bugs fixed.
(edit) @3005   7 years sacerdot Beginning of making it fully compatible with untrusted one.
(edit) @3004   7 years tranquil fixed a bug where when doing an asymetrical op, cast initialization …
(edit) @3003   7 years sacerdot Correctness.ma "repaired"
(edit) @3002   7 years tranquil fixed previous commit
(edit) @3001   7 years sacerdot New extraction.
(edit) @3000   7 years tranquil added RTLabs printer
(edit) @2999   7 years sacerdot code_memory added to labelled_object_code to avoid recomputing it …
(edit) @2998   7 years sacerdot Test on conditional execution. Fails atm.
(edit) @2997   7 years sacerdot New extraction.
(edit) @2996   7 years sacerdot Printing of graphs now starts from the entry point.
(edit) @2995   7 years sacerdot The lIN_printer extracted.
Note: See TracRevisionLog for help on using the revision log.