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