Matthew Brecknell
70de40bcdd
autocorres-crefine: add AutoCorresCRefine image
2017-11-22 12:18:16 +11:00
Matthew Brecknell
079d5dec23
autocorres-crefine: make AutoCorres tools available in CRefine
2017-11-22 12:18:16 +11:00
Miki Tanaka
9bdb47e114
reintroduce Orphanage test (for ARM only)
...
- Orphanage files in the ARM_HYP and X64 directories are not tested at the moment
- once we finish proving them, we will remove the restriction to ARM
2017-10-24 13:49:21 +11:00
Joel Beeren
f05bc45d59
misc: clean up before merging x64
2017-08-11 11:49:18 +10:00
Joel Beeren
82863978bd
Merge branch 'master' into x64
2017-08-09 17:10:06 +10:00
Matthew Brecknell
3bbc1d0cb9
regression: remove redundant RefineOnly image
...
This was previously used to exclude Orphanage from the X64 regression.
Now that the Refine image excludes Orphange, RefineOnly is no longer
needed.
2017-08-09 17:02:49 +10:00
Joel Beeren
0685280906
misc: remove redundant skip_proofs flag for BaseRefine in proof/ROOT
2017-08-09 11:28:10 +10:00
Joel Beeren
2ce1bf3a25
misc: remove unnecessary theories from proof/ROOT
2017-08-08 16:13:38 +10:00
Joel Beeren
d9afe3f45c
run_tests: Adjust environment flags for build
...
*** ALERT: ANYONE USING SKIP_REFINE_PROOFS SHOULD CHANGE TO
SKIP_DUPLICATED_PROOFS IN ~/.isabelle/etc/settings!!! ***
Previously SKIP_REFINE_PROOFS was being used to skip duplicated Refine
and AInvs proofs when building CBaseRefine and InfoFlowC. This
conflicted with adding an option to actually skip building Refine proofs
(for example when trying to quickly build DBaseRefine).
After this change, we have the following SKIP_PROOFS flags:
* SKIP_AINVS_PROOFS: used to skip AInvs proofs (for example when
building Refine)
* SKIP_REFINE_PROOFS: used to skip Refine proofs (for example when
building DBaseRefine)
* SKIP_DUPLICATED_PROOFS: used to skip the rebuild of AInvs and
Refine when building forked images such as CBaseRefine and
InfoFlowC
In addition, the QUICK_AND_DIRTY flag for AInvs has been changed:
INVS_QUICK_AND_DIRTY -> AINVS_QUICK_AND_DIRTY
2017-08-08 16:11:20 +10:00
Joel Beeren
d1482e4ffa
misc: added skip proofs option for Refine
...
tags: [NO_PROOF]
2017-08-08 12:19:43 +10:00
Matthew Brecknell
238e8b307e
x64: merge master
2017-07-21 11:27:12 +10:00
Alejandro Gomez-Londono
796887d9b1
Removes all trailing whitespaces
2017-07-12 15:13:51 +10:00
Gerwin Klein
9f32001c78
arm-hyp: enable quick_and_dirty for snd CBaseRefine image
2017-06-19 14:32:35 +10:00
Rafal Kolanski
96c13859e0
proof/ROOT: add CREFINE_QUICK_AND_DIRTY flag
...
Use to build CRefine in quick_and_dirty mode.
2017-06-19 14:32:35 +10:00
Gerwin Klein
682dde4155
refine: add intermediate BaseRefine2 session for small machines
2017-06-19 14:32:29 +10:00
Gerwin Klein
09a02acc7b
arm-hyp proofs/ROOT: make it possible to skip proofs in BaseRefine
2017-06-19 14:32:28 +10:00
Gerwin Klein
740d606774
refine: closed the Orphanage
...
Not necessary for CRefine and better proved on the abstract spec now.
To be resurrected (on abstract) in the future.
2017-06-19 14:32:27 +10:00
Miki Tanaka
3d22990928
arm-hyp test: setup REFINE_QUICK_AND_DIRTY for Refine (to be squashed)
...
* fix the order of entries in the ROOT file
2017-06-19 14:32:25 +10:00
Miki Tanaka
e0b6d45db4
arm-hyp test: add BaseRefine to regression, set up REFINE_QUICK_AND_DIRETY for Refine
2017-06-19 14:32:23 +10:00
Miki Tanaka
2ae9147f02
arm-hyp test: default targets for arm-hyp, turn on quick_and_dirty for AInvs
2017-06-19 14:32:20 +10:00
Matthew Brecknell
23057ee017
x64 refine: add a RefineOnly image which skips Orphanage
2017-04-24 23:58:05 +10:00
Joel Beeren
3b8d91161b
x64: add RefineQD image with quick and dirty, without Orphanage
2017-04-21 14:33:21 +10:00
Joel Beeren
ead5678100
x64: add AInvsSP image for skipping over AInvs proofs
2017-04-05 15:42:48 +10:00
Rafal Kolanski
c41c7a97ca
update references from/to moved crefine, parametrise over L4V_ARCH
2017-03-31 16:13:41 +11:00
Joel Beeren
ee209a2455
x64: add quick-and-dirty BaseRefineQD image, doesnt import KernelInit
2017-03-14 17:59:08 +11:00
Joel Beeren
67daaea42a
x64: AInvs now done except ArchAInvsPre and KernelInit_AI
2017-03-14 13:16:14 +11:00
Matthew Brecknell
6ce6c97397
arch_split: DetSchedDomainTime_AI, DetSchedSchedule_AI for ARM
2017-03-09 12:10:44 +11:00
Rafal Kolanski
7657681fca
move refine/* to refine/ARM/*, parametrise over $L4V_ARCH
2017-01-30 12:22:22 +11:00
Joel Beeren
eb5badce92
l4v: Add intermediate image for InfoFlowC.
...
This allows one to skip the Access, InfoFlow proofs
when building InfoFlowC, hopefully allowing faster
turn arounds when doing maintenance.
2016-11-16 09:12:18 +11:00
Thomas Sewell
d765a64b81
SELFOUR-444: Haskell implementation, begin refine.
...
First attempt at a haskell implementation of preemptible retyping
and the refinement proof to abstract.
2016-11-02 11:19:08 +11:00
Gerwin Klein
445efb7c29
lib: closure for Word_Lib and own session
2016-05-16 21:11:40 +10:00
Japheth Lim
3144c4d847
Remove time limits from Isabelle ROOT files.
2016-02-29 14:52:37 +11:00
Thomas Sewell
ca4391881c
WIP on WCET annotations.
2015-07-14 14:23:29 +10:00
Gerwin Klein
f9e40c29db
cleanup: there already is a separate Bisim session
2015-04-19 10:24:42 +01:00
Daniel Matichuk
a221a52350
Added new proofcount tool to "tools" and removed old one from "lib".
...
Removed reference to old proof_counting from proof/ROOT and spec/ROOT
2015-02-11 17:46:34 +11:00
deang
77c600038f
infoflow: fixed and added Example_Valid_StateH to testing
...
Some of the noninterference results depend on executions at the haskell level starting at a valid initial state. This file demonstrates this condition being realised.
2014-11-18 17:39:17 +11:00
Thomas Sewell
f59767cdac
Slight fudges for Fastpath use with PIDE.
2014-09-18 20:12:43 +10:00
Thomas Sewell
41c0e994ad
Make SIMPL->Graph regression testable.
2014-09-05 19:10:03 +10:00
Gerwin Klein
f1d808c96a
integrate separation kernel config proofs
...
Hooked up into build system and regression test; added READMEs
2014-08-13 22:08:46 +10:00
Andrew Boyton
c060f715db
Add a top-level file for the capDL API proofs.
2014-07-24 19:56:24 +10:00
Gerwin Klein
2a03e81df4
Import release snapshot.
2014-07-14 21:32:44 +02:00