Thomas Sewell
|
b5f796184a
|
Repair spec/refine, I think.
|
2015-07-15 17:25:47 +10:00 |
|
Thomas Sewell
|
ca4391881c
|
WIP on WCET annotations.
|
2015-07-14 14:23:29 +10:00 |
Gerwin Klein
|
cfec9ea0db
|
Merge branch 'master' into 2015
|
2015-05-28 11:45:13 +10:00 |
Joel Beeren
|
002cf370bb
|
Updated proof with new fastpath changes removing setCurrentASID and armv_contextSwitch_fp
|
2015-05-28 11:30:22 +10:00 |
|
Gerwin Klein
|
12fa86863a
|
fewer warnings
|
2015-05-16 19:52:49 +10:00 |
|
Gerwin Klein
|
0c67e0bfa1
|
2015 update for Refine
|
2015-05-12 17:17:31 +02: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 |