|
|
@2908
|
8 years |
sacerdot |
Bug fixed by hand, they will be fixed automatically by the new extraction.
|
|
|
@2907
|
8 years |
sacerdot |
1. a few bugs fixed
2. as_return implemented for ASM & OC
|
|
|
@2906
|
8 years |
sacerdot |
Bug fixed.
|
|
|
@2905
|
8 years |
sacerdot |
Semantics of ASM in place (up to return values and function call …
|
|
|
@2904
|
8 years |
sacerdot |
1. Algorithm modified by hand to make it run faster.
The trusted …
|
|
|
@2903
|
8 years |
sacerdot |
Extracted again.
|
|
|
@2902
|
8 years |
sacerdot |
Quick hack to allow printing of OC code. It will be automatically …
|
|
|
@2901
|
8 years |
sacerdot |
1. backendPrinter renamed to printer
2. Clight printing branched into …
|
|
|
@2900
|
8 years |
sacerdot |
Flushing to understand where it is slow.
|
|
|
@2899
|
8 years |
sacerdot |
1. some renaming ASM_xxx to OC_xxx
2. ASM_pre_classified_system …
|
|
|
@2898
|
8 years |
piccolo |
1) simplification of cond and seq case for StatusSimulationHelper? …
|
|
|
@2897
|
8 years |
campbell |
Minor tidying.
|
|
|
@2896
|
8 years |
campbell |
Complete part of measurable to structured subtraces proof that
shows …
|
|
|
@2895
|
8 years |
campbell |
Match up function id from RTLabs Callstate with shadow stack,
use in …
|
|
|
@2894
|
8 years |
campbell |
Some progress on showing that the change to structured traces …
|
|
|
@2893
|
8 years |
campbell |
Add tlr_unrepeating.
|
|
|
@2892
|
8 years |
campbell |
Add cost hypotheses.
|
|
|
@2891
|
8 years |
piccolo |
added precondition on seq statement and tested correct in the …
|
|
|
@2890
|
8 years |
sacerdot |
Exported again, now the execution is correct up to LIN for a simple …
|
|
|
@2889
|
8 years |
sacerdot |
It works very nice!
|
|
|
@2888
|
8 years |
tranquil |
backtracked some partial changes
|
|
|
@2887
|
8 years |
tranquil |
Corrected bug where eliminable statements where not eliminated. …
|
|
|
@2886
|
8 years |
piccolo |
partial commit
|
|
|
@2885
|
8 years |
sacerdot |
Hint at how to change everything.
|
|
|
@2884
|
8 years |
sacerdot |
Debugging print added.
|
|
|
@2883
|
8 years |
piccolo |
partial commit
|
|
|
@2882
|
8 years |
sacerdot |
…
|
|
|
@2881
|
8 years |
sacerdot |
…
|
|
|
@2880
|
8 years |
sacerdot |
…
|
|
|
@2879
|
8 years |
tranquil |
changed coercion from list of joint_seq to blocks to a more efficient one
|
|
|
@2878
|
8 years |
tranquil |
backtracked some changes that were not ready for commit
|
|
|
@2877
|
8 years |
garnier |
Correction of a bug in my former bug correction.
|
|
|
@2876
|
8 years |
tranquil |
corrected another endianess bug in joint_semantics. Switched some …
|
|
|
@2875
|
8 years |
sacerdot |
Pretty printing of object code integrated too.
A couple of axioms make …
|
|
|
@2874
|
8 years |
sacerdot |
Syntax fixed: ./cerco [-exec] filename annotationoption
|
|
|
@2873
|
8 years |
sacerdot |
Extracted again.
|
|
|
@2872
|
8 years |
tassi |
Fix list of distributed files so that the debian package can be built
|
|
|
@2871
|
8 years |
tranquil |
op2 evaluation on beval's rendered oblivious to carry bit when …
|
|
|
@2870
|
8 years |
sacerdot |
Proof fixed.
|
|
|
@2869
|
8 years |
tranquil |
some reorganization of definitions, and a new taaf_append_taaf
|
|
|
@2868
|
8 years |
sacerdot |
Pretty printing of ERTL and ERTLptr code.
|
|
|
@2867
|
8 years |
sacerdot |
New extraction after indianess bug fixes by Paolo.
|
|
|
@2866
|
8 years |
tranquil |
corrected two bugs of the translation: constant translation used wrong …
|
|
|
@2865
|
8 years |
sacerdot |
…
|
|
|
@2864
|
8 years |
sacerdot |
I must have drunk yesterday: all RTL passes are printed correctly; the …
|
|
|
@2863
|
8 years |
piccolo |
Added new invariant to good_if
Generalized version of cond case for …
|
|
|
@2862
|
8 years |
sacerdot |
Repaired, a reverse was enough.
|
|
|
@2861
|
8 years |
mckinna |
PROVISIONAL commit:
Unintentional list reversal cause final step of …
|
|
|
@2860
|
8 years |
sacerdot |
RTL printing, core dumps ATM
|
|
|
@2859
|
8 years |
sacerdot |
Pretty printing improved (now it always starts the visit from lbl 1).
|
|
|
@2858
|
8 years |
sacerdot |
Trying to pretty print the code graph in visit order.
Slightly bugged …
|
|
|
@2857
|
8 years |
garnier |
CL to CM: some invariants strengthened.
|
|
|
@2856
|
8 years |
sacerdot |
Pretty printing of LTL almost finished.
|
|
|
@2855
|
8 years |
piccolo |
little bug fixed in TranslateUtils?.
|
|
|
@2854
|
8 years |
sacerdot |
Pretty printing of the LTL program.
|
|
|
@2853
|
8 years |
sacerdot |
Pretty printing of line/label numbers.
|
|
|
@2852
|
8 years |
mckinna |
Interim commit to re-establish well-typedness after all the recent …
|
|
|
@2851
|
8 years |
piccolo |
partial commit
|
|
|
@2850
|
8 years |
garnier |
Progress on CL to CM. Some more cases closed modulo some critical …
|
|
|
@2849
|
8 years |
piccolo |
partial commit
|
|
|
@2848
|
8 years |
sacerdot |
The pretty printer for LTL.
|
|
|
@2847
|
8 years |
sacerdot |
…
|
|
|
@2846
|
8 years |
sacerdot |
Pretty printing of joint programs.
|
|
|
@2845
|
8 years |
piccolo |
ERTLptr to LTL correctness proof started
|
|
|
@2844
|
8 years |
piccolo |
Stupid bug fixed
|
|
|
@2843
|
8 years |
piccolo |
1) Fixed a litte bug in Joint.ma
2) ERTL to ERTLptr correctness proof …
|
|
|
@2842
|
8 years |
sacerdot |
The compiler can now show all back-end traces too (assembly and object …
|
|
|
@2841
|
8 years |
sacerdot |
The compiler now computes also the stack cost for every intermediate …
|
|
|
@2840
|
8 years |
campbell |
Remove irrelevant stuff from RTLabs_partial_traces
|
|
|
@2839
|
8 years |
campbell |
Basic structure of RTLabs measurable to structured traces results.
|
|
|
@2838
|
8 years |
garnier |
Closing some more cases
|
|
|
@2837
|
8 years |
tranquil |
* filled in evaluation of LTL/LIN's extended instrucitons
|
|
|
@2836
|
8 years |
sacerdot |
…
|
|
|
@2835
|
8 years |
sacerdot |
Included Uses.ma which is required by the untrusted code.
The …
|
|
|
@2834
|
8 years |
sacerdot |
Execution integrated in the compiler, as it was in the prototype. …
|
|
|
@2833
|
8 years |
sacerdot |
…
|
|
|
@2832
|
8 years |
sacerdot |
Added abstraction in front of cases daemon for code extraction.
|
|
|
@2831
|
8 years |
sacerdot |
…
|
|
|
@2830
|
8 years |
sacerdot |
Added abstractions in front of cases daemon for code extraction.
|
|
|
@2829
|
8 years |
sacerdot |
Semantics files committed.
|
|
|
@2828
|
8 years |
sacerdot |
1. New semantics.ma file that puts together all semantics.
It …
|
|
|
@2827
|
8 years |
sacerdot |
Everything extracted again.
|
|
|
@2826
|
8 years |
sacerdot |
New error messages.
|
|
|
@2825
|
8 years |
garnier |
Progress, Clight to Cminor
|
|
|
@2824
|
8 years |
tranquil |
* moved sum on lists notation to extranat
* used sum on lists to …
|
|
|
@2823
|
8 years |
tranquil |
* corrected bug in ERTL semantics (both delframe and newframe did the …
|
|
|
@2822
|
8 years |
garnier |
A consitent proof state for Clight to Cminor, with some progress (and …
|
|
|
@2821
|
8 years |
tranquil |
* implemented preclassified system for joint (in joint/joint_fullexec.ma)
|
|
|
@2820
|
8 years |
sacerdot |
Proof obligation closed.
|
|
|
@2819
|
8 years |
sacerdot |
Proof obligation closed.
|
|
|
@2818
|
8 years |
sacerdot |
"Repaired", using non computational daemons.
|
|
|
@2817
|
8 years |
sacerdot |
Repaired after Paolo's commit.
|
|
|
@2816
|
8 years |
sacerdot |
Repaired after Paolo's commit.
|
|
|
@2815
|
8 years |
sacerdot |
exec superseded by exec_all
|
|
|
@2814
|
8 years |
sacerdot |
frontend superseded by execute_all
|
|
|
@2813
|
8 years |
sacerdot |
RTLabs now printed too
|
|
|
@2812
|
8 years |
sacerdot |
Pre-classified system for RTLabs.
|
|
|
@2811
|
8 years |
sacerdot |
Pre-classified system for RTLabs.
|
|
|
@2810
|
8 years |
sacerdot |
Cminor semantics exported.
|
|
|
@2809
|
8 years |
sacerdot |
…
|
|
|