Commit Graph

8 Commits

Author SHA1 Message Date
Alejandro Gomez-Londono 0a31fa7fe4 Remove spec-check test and scripts 2017-05-12 12:50:55 +10:00
Alejandro Gomez-Londono 41f200d5b3 design: Update Makefiles + tests.xml to auto-generate the design spec
* It runs the haskell-translator as a dependency, eliminating the
      need for "run haskell translator" commits.
2017-05-12 12:50:49 +10:00
Rafal Kolanski 7e13fb9e91 cspec: move to ARM subdirectory
Configure to build with L4V_ARCH=ARM
2017-03-30 18:20:24 +11:00
Matthew Brecknell c1574f1f32 cspec: build: avoid re-entering isabelle via dash-0.5.8 2016-02-17 11:04:20 +11:00
Daniel Matichuk fad2c6aae9 paramatrised abstract and haskell specs over L4V_ARCH
Haskell translator was modified to support multiple translations
of the haskell, with different build parameters.
2016-01-13 12:01:40 +11:00
Japheth Lim d92666bc30 regression: remove forceful build options from CSpec makefiles. They don't seem to be needed. 2016-01-07 18:39:50 +11: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
Gerwin Klein 2a03e81df4 Import release snapshot. 2014-07-14 21:32:44 +02:00