| #
6b9912c4 |
|
16-Oct-2017 |
Pang Luo <Pang.Luo@data61.csiro.au> |
manually adjust non-obvious cases of tab to space replacement
|
| #
184d6b70 |
|
09-Oct-2017 |
Matthew Brecknell <Matthew.Brecknell@data61.csiro.au> |
remove most tab characters
|
| #
796887d9 |
|
11-Jul-2017 |
Alejandro Gomez-Londono <alejandro.gomez@nicta.com.au> |
Removes all trailing whitespaces
|
| #
6ad456ca |
|
30-May-2016 |
Thomas Sewell <Thomas.Sewell@nicta.com.au> |
SELFOUR-444: Adjust Haskell, new ghost data.
The new ghost data is saved in the design spec when Untyped caps
are modified and will be used by CRefine.
|
| #
56b226a6 |
|
05-May-2016 |
Matthew Brecknell <Matthew.Brecknell@nicta.com.au> |
arch_split: CRefine: use requalify instead of shadow
|
| #
9ceed1eb |
|
03-May-2016 |
Daniel Matichuk <daniel.matichuk@nicta.com.au> |
arch_split: fix proofs after removing shadow and unqualify commands and adding fix for crunch. Checks up to DPolicy.
|
| #
1d20b393 |
|
26-Apr-2016 |
Daniel Matichuk <daniel.matichuk@nicta.com.au> |
arch_split: replaced sublocale with global_naming
|
| #
72337faa |
|
31-Mar-2016 |
Daniel Matichuk <daniel.matichuk@nicta.com.au> |
arch_split: added namespacing to ExecSpec
|
| #
fad2c6aa |
|
11-Jan-2016 |
Daniel Matichuk <daniel.matichuk@nicta.com.au> |
paramatrised abstract and haskell specs over L4V_ARCH
Haskell translator was modified to support multiple translations
of the haskell, with different build parameters.
|
| #
2a9d3022 |
|
20-Aug-2015 |
Rafal Kolanski <rafal.kolanski@nicta.com.au> |
priority-bitmap: Update abstract->Haskell refinement
Added word_log2 and word_clz (inline for now, will migrate them out to
lib later).
Proved most important properties of word_log2 and some basic
count leading zeros properties (word_clz). The former were painful.
Thanks to Thomas, we have a nice tactic for dealing with complicated
obj_at' predicates in conclusion: normalise_obj_at'
|
| #
ca439188 |
|
21-May-2015 |
Thomas Sewell <Thomas.Sewell@nicta.com.au> |
WIP on WCET annotations.
|
| #
12fa8686 |
|
16-May-2015 |
Gerwin Klein <gerwin.klein@nicta.com.au> |
fewer warnings
|
| #
2a03e81d |
|
14-Jul-2014 |
Gerwin Klein <gerwin.klein@nicta.com.au> |
Import release snapshot.
|