df519ffd25
avoid `make` warning, remove SimplExportOnly from HEAPS
...
Make ignores the HEAPS rule for SimplExportOnly anyhow (as it should).
2015-11-20 16:02:14 +11:00
be0ebaa139
ignore generated autoconf.h
2015-11-20 16:02:14 +11:00
ac632c5aaa
Wait -> Recv: update proofs
2015-11-20 16:02:14 +11:00
00bfafe2f5
Wait -> Recv: update specs
2015-11-20 16:02:14 +11:00
8fb2dc2b15
Wait -> Recv: haskell update
2015-11-20 16:02:13 +11:00
3af6a6b0da
added timing methods
2015-11-20 16:02:13 +11:00
457a55a831
add arch_tcb object to C, rename aep -> ntfn
2015-11-20 16:02:13 +11:00
ac9c3bb1a3
Remove sorry on clz_spec (C parser changes allow it to be proved now).
...
(with some magic from Thomas)
2015-11-20 15:58:15 +11:00
2f39375ee4
Modifies proofs partially working
...
At the moment, if there is a specification and DONT_TRANSLATE, the
automatic proofs only work if the specification is that no globals are
modified.
Work on JIRA VER-464
2015-11-19 11:27:05 +11:00
27a12b871c
Translate spec-only fns with new guarded_spec_body const
...
As per discussion in JIRA VER-464 issue.
Still to try to prove modifies theorems for such functions
automatically.
2015-11-19 09:58:36 +11:00
05c6abc751
removed unused (and outdated) constants
2015-11-13 15:24:36 +11:00
50ad3aba60
Delete trailing whitespace in jiraver464.thy
2015-11-12 16:40:04 +11:00
4e4bbc8267
Handle kernel's halt def/spec
...
Halt no longer gets an automatic modifies proof.
2015-11-12 16:40:04 +11:00
a2cc6ab301
Added wp_del and simp_del arguments to crunch.
2015-11-12 12:23:04 +11:00
dac491360f
Allow some DONT_TRANSLATES to have modifies proofs
...
In particular, if the only specification attached is the MODIFIES line,
then the automatic machinery will cope with proving the modifies result.
So, now rule out those with DONT_TRANSLATE and at least one fnspec.
2015-11-12 10:43:50 +11:00
7bd543ad76
Modifies proofs never tried for DONT_TRANSLATES
2015-11-12 10:14:45 +11:00
bbdf7c792c
Deal with compiler warnings in isa_termstypes.ML
...
Removes a bunch of unused code.
2015-11-12 10:01:25 +11:00
6a5ae1f8e6
Delete trailing whitespace in mlyacc sources
2015-11-12 09:53:29 +11:00
c126813667
Get clz definition to parse (JIRA VER-464).
...
It's added to the 464 regression test.
2015-11-12 09:51:57 +11:00
55c6cca7fb
lib: add term_pat: ML antiquotation for pattern matching on terms.
2015-11-11 18:57:46 +11:00
efede274df
Better RelSpec bodies for DONT_TRANSLATE functions
...
DONT_TRANSLATE functions must have MODIFIES clauses for this to work at
the moment.
2015-11-11 16:40:00 +11:00
7916a7751a
Define RelSpec bodies for DONT_TRANSLATE functions.
...
Work for JIRA VER-464
2015-11-10 17:14:08 +11:00
6f4b0f3e37
Work on JIRA VER-464
...
Breaks existing dont_translate test-case.
2015-11-09 14:55:47 +11:00
fe3045f798
Remove Isabelle warnings in ML
2015-11-09 14:55:47 +11:00
7f664edf13
One more fix for strengthen change.
2015-11-02 16:02:03 +11:00
314a46ee6f
One last fix, hopefully.
2015-11-02 10:52:06 +11:00
bdd8819f50
More minor adjustments.
2015-10-30 12:22:55 +11:00
7c3a06a8d7
Minor adjustments caused by Strengthen changes.
2015-10-29 11:27:54 +11:00
cb6234a718
Move strengthen rules to Strengthen; adjust WPBang.
2015-10-29 11:27:54 +11:00
aab5d41436
Facelift Strengthen; introduce WPBang.
...
Give Strengthen its own theory and a much more robust and general
implementation. However take away its ability to do elimination, maybe
to be restored.
Introduce a new theory, WPBang, for applying wp safe rules, with possible
attribute wp! (attribute yet to be implemented).
Still testing out both adjustments.
2015-10-29 11:27:54 +11:00
1ad00aa1ae
misc/regression/memusage.py: work around psutil API changes
...
Closes #5
2015-10-28 18:49:55 +11:00
b1cd097849
Eisbach_WP: Added wp_drop_imp and wp_strong_drop_imp
2015-10-26 15:39:15 +11:00
040c6be903
Eisbach_WP: extra "end"
2015-10-26 15:39:15 +11:00
6ba1095d66
Eisbach_WP: Renamed WPU to WPI and changed the default behaviour to be safe (not ever dropping antecedents)
2015-10-26 15:39:15 +11:00
7393799ab2
autocorres: restore simplifier tracing functionality.
2015-10-26 14:18:10 +11:00
e9257ae5b0
lib: Many helpers about `fold op ++`.
2015-10-23 11:54:04 +11:00
36c5cb6860
lib: Another CAmkES helper lemma.
2015-10-23 11:36:39 +11:00
693d6f63e0
Revert 64af29ab33
...
Still don't know what went wrong, but works now.
2015-10-22 08:15:23 +11:00
d3f3acb9fc
Fix up CRefine after seL4_NBWait merge.
2015-10-22 07:45:49 +11:00
d51402a5a2
Merge remote-tracking branch 'verification/master' into priority-bitmap
...
(seL4_NBWait)
2015-10-21 16:23:01 +11:00
c94b27b7ae
priority-bitmap: clean up CRefine
...
Cleaned up proof of tcbSchedDequeue_ccorres' (still ugly)
2015-10-21 16:22:11 +11:00
e403eb8f0a
poll: added non blocking sync wait
2015-10-21 14:24:49 +11:00
d6f7579be7
poll: Added new syscall for polling async endpoints (non-blocking wait)
2015-10-21 14:24:49 +11:00
6f8cdae201
priority-bitmap: clean up Refine (i.e. "FIXME RAF")
2015-10-21 13:38:29 +11:00
64af29ab33
c-parser: fix duplicate fact decl in testfiles/dc_20081211.thy
...
Why this is suddenly a problem now, when there hasn't been a change to
this file in years is completely unclear. Nonetheless, I need a green
build.
The error was:
*** Duplicate fact declaration "dc_20081211.dc_20081211.test_modifies"
vs. "dc_20081211.dc_20081211.test_modifies" (line 42 of
"~/repos/v/l4v/tools/c-parser/testfiles/dc_20081211.thy")
*** At command "lemma" (line 42 of
"~/repos/v/l4v/tools/c-parser/testfiles/dc_20081211.thy")
2015-10-21 12:00:15 +11:00
fa261e2c9c
autocorres: fix "no \citation" bibtex error
2015-10-21 11:58:13 +11:00
c1eb235105
Merge 'verification/master' into priority-bitmap
...
Green build except for:
CParserTest (WTF Duplicate fact declaration "dc_20081211.dc_20081211.test_modifies")
AutoCorresSEL4 (waiting on result)
There is still a carefully managed sorry in Schedule_R, waiting on the C
parser FNSPEC+DONT_TRANSLATE fix.
2015-10-21 06:19:20 +11:00
fca34f4a7f
priority-bitmap: TEMPORARY SORRY FOR JIRA VER-464
...
In Schedule_C:
(**** FIXME FIXME FIXME ***)
(* As per JIRA VER-464, the C Parser does not handle
DONT_TRANSLATE+MODIFIES+FNSPEC correctly. This is the spec given in util.h
in seL4 for clz. We do not get that spec back at present.
In order to have a working build until the C parser is fixed, we sorry this
proof. My apologies.
*)
2015-10-20 23:52:14 +11:00
71ff4d274a
c-parser: add packed_type instance for 2D arrays
...
I finally got it down into a form that Isabelle accepts, and without
even having to add spurious axioms.
2015-10-20 23:52:14 +11:00
3230d601ae
priority-bitmap: Update InfoflowC
2015-10-20 23:52:14 +11:00
Gerwin Klein
Daniel Matichuk
Joel Beeren
Rafal Kolanski
Michael Norrish
Corey Lewis
Japheth Lim
Thomas Sewell
Corey Richardson
Matthew Fernandez