Thomas Sewell 13ad834ace Generated bitfield proofs: use hrs_mem_update. ... This is a technical change to the proof mode of the bitfield generator included in the seL4 source. The postconditions of the generated specifications of the *_ptr_set and *_ptr_new functions now describe the entire new heap via (new_heap = hrs_mem_update (...) old_heap). Previously they described the contents of various projections of the heap, which is less precise.		2016-11-01 16:18:02 +11:00
..
bf.vim	Release snapshot	2014-07-18 05:03:59 +10:00
bitfield_gen.py	Generated bitfield proofs: use hrs_mem_update.	2016-11-01 16:18:02 +11:00
changed.sh	Release snapshot	2014-07-18 05:03:59 +10:00
circular_includes.py	Replace circular includes perl script with python	2016-10-24 10:53:36 +11:00
cpp_gen.sh	Release snapshot	2014-07-18 05:03:59 +10:00
invocation_header_gen.py	update #ifdef to #if in auto generated files	2016-10-17 12:18:58 +11:00
lex.py	Release snapshot	2014-07-18 05:03:59 +10:00
syscall_header_gen.py	Debug: avoid syscall_names unsued Werror when debug mode is enabled	2016-10-20 09:06:57 +11:00
umm.py	tools: umm: python3 compat	2016-01-25 15:42:04 +11:00
xmllint.sh	Release snapshot	2014-07-18 05:03:59 +10:00
yacc.py	tools: yacc: fix broken python3 compatability hack	2016-01-25 15:56:15 +11:00