Thomas Sewell
4fd43512bb
WIP on handling array assertions. Up to Retype_C.
...
This is quite a lot of work in the end. I've had to gut most of
Retype_C along the way. Nearly done there.
2015-12-02 09:06:06 +11:00
Thomas Sewell
6fa0909124
Partial progress on using array assertions.
2015-12-02 09:05:04 +11:00
Matthew Fernandez
d9154d00af
crefine: Remove a find_theorems invocation.
2015-11-25 10:29:22 +11:00
Joel Beeren
457a55a831
add arch_tcb object to C, rename aep -> ntfn
2015-11-20 16:02:13 +11:00
Thomas Sewell
7c3a06a8d7
Minor adjustments caused by Strengthen changes.
2015-10-29 11:27:54 +11:00
Rafal Kolanski
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
Rafal Kolanski
930a2ff179
priority-bitmap: Update Haskell->C refinement
...
(modulo clz_spec locale problem)
2015-10-20 23:52:07 +11:00
Joel Beeren
d0693fc7d5
fix CRefine after libseL4 NotificationObject terminology update
2015-10-14 14:00:27 +11:00
Ramana Kumar
0fb88ea01c
Merge branch 'master' into aep-merge
...
This commit should at least remove merge conflict markers, and the idea
is that at least refine, crefine, drefine, and infoflow (with sorrys)
build. Subsequent commits may be required to fix build issues that I
have not picked up.
2015-09-10 17:06:45 +10:00
Ramana Kumar
d88a931ec7
history squashed patch for aep-binding
2015-09-02 15:43:39 +10:00
Thomas Sewell
af86632985
Fix remaining sorries in crefine.
2015-07-16 14:44:56 +10:00
Thomas Sewell
e9180d5cb5
Repair refine/crefine for WCET annotations.
2015-07-14 14:23:29 +10:00
Thomas Sewell
ca4391881c
WIP on WCET annotations.
2015-07-14 14:23:29 +10:00
Gerwin Klein
eea646c84a
crefine: 2015 update up to Tcb_C
2015-05-18 09:11:43 +10:00
Gerwin Klein
12fa86863a
fewer warnings
2015-05-16 19:52:49 +10:00
David Greenaway
03b1952aaa
crefine: Port CRefine to Isabelle 2014.
2014-09-11 16:57:59 +10:00
Thomas Sewell
9b01fada15
Refine working.
2014-08-11 18:51:04 +10:00
Thomas Sewell
fc6e57716a
Proof updates, working as far as AInvs.
2014-08-11 14:50:56 +10:00
Gerwin Klein
154da63715
remove old levity and taint-mode comments
2014-07-22 18:10:28 +02:00
Gerwin Klein
50dda7708c
comment cleanup
2014-07-22 18:10:20 +02:00
Gerwin Klein
2a03e81df4
Import release snapshot.
2014-07-14 21:32:44 +02:00