muen/tau0.git
2019-07-05 Adrian-Ken... Add explicit proof target master
2019-07-05 Adrian-Ken... Add Arcanist project file
2019-07-05 Adrian-Ken... Move test files to data directory
2019-07-05 Johannes OsterholzerImplement README comments
2019-07-05 Johannes OsterholzerREADME: Assorted minor changes
2019-07-05 Johannes OsterholzerREADME: Make subsection 'Invariant Preservation' clearer
2019-07-05 Johannes OsterholzerREADME: Update section 'Compilation'
2019-07-05 Johannes OsterholzerREADME: Explain why memory region tables are not unmapped
2019-07-05 Johannes OsterholzerDebug: Add explicit elaboration pragma
2019-07-05 Johannes OsterholzerFurther streamline naming of device domain XML commands
2019-07-05 Reto BuerkiPartially include test.xml in README
2019-07-05 Reto BuerkiMinor cleanup in test.xml
2019-07-05 Reto BuerkiEnable exception backtraces
2019-07-05 Reto BuerkiIncrease config constants
2019-07-05 Reto BuerkiDebug: Init log-level from Command_Line getter
2019-07-05 Reto BuerkiImplement log-level command line handling
2019-07-05 Reto BuerkiAdd log message before command processing
2019-07-05 Reto BuerkiSet default log-level to Notice
2019-07-05 Reto BuerkiSet some log messages to Notice log-level
2019-07-05 Reto BuerkiOutput error log messages on command failure
2019-07-05 Reto BuerkiMove Current_Level variable to Debug spec
2019-07-05 Reto BuerkiAdd new Notice loglevel
2019-07-05 Reto BuerkiSet Exec_Dir to bin
2019-07-05 Reto BuerkiUse obj as Object_Dir
2019-07-05 Reto BuerkiWrap calls with $(E) wrapper
2019-07-05 Reto BuerkiRemove generated directory in clean target
2019-07-05 Reto BuerkiDrop obsolete resolve.xsl file
2019-07-05 Reto BuerkiUse RESOLVE_XSL variable from Muen Makeconf
2019-07-05 Reto BuerkiDrop obsolete xml2ada script
2019-07-05 Reto BuerkiUse XML2ADA variable from Muen Makeconf
2019-07-05 Reto BuerkiUse BUILD_OPTS variable in BUILD target
2019-07-05 Reto BuerkiInclude Muen Makeconf
2019-07-05 Adrian-Ken... Move Active flag of EPT PTEs to bit 52
2019-07-05 Adrian-Ken... Minor optimization to XML.Command_Size
2019-07-05 Reto BuerkiIncrease Max_IRQs_Per_Subject from 8 to 48
2019-07-05 Reto BuerkiIncrease Max_Devices_Per_Subject from 8 to 16
2019-07-05 Reto BuerkiIncrease Max_IRQs_Per_Device to 36
2019-07-05 Johannes OsterholzerData.Processors: Check that APIC IDs are pairwise distinct
2019-07-05 Johannes OsterholzerCommand_Line: Remove parameter 'cpu-count'
2019-07-05 Johannes OsterholzerAmend test.xml
2019-07-05 Johannes OsterholzerImplement command Add_Processor
2019-07-05 Johannes OsterholzerUse Data.Processors
2019-07-05 Johannes OsterholzerRemove outdated FIXME
2019-07-05 Johannes OsterholzerAmend test.xml
2019-07-05 Johannes OsterholzerAdd parameter 'Level' to command 'Create_Device_Domain'
2019-07-05 Johannes OsterholzerAmend test.xml
2019-07-05 Johannes OsterholzerAdd parameter 'ID' to command 'Create_Device_Domain'
2019-07-05 Johannes OsterholzerCommands.Write_Image: Limit warnings pragma
2019-07-05 Johannes OsterholzerFix whitespace and alignment
2019-07-05 Reto BuerkiSet non-zero exit status on command failure
2019-07-05 Reto BuerkiFix warnings reported by -gnatyt
2019-07-05 Reto BuerkiEnable -gnatyt switch
2019-07-05 Reto BuerkiFix alignment in tau0.gpr file
2019-07-05 Johannes OsterholzerXML.*.Map_Pages: Honor value of parameter Base_Offset
2019-07-05 Johannes OsterholzerAdd XML commands 'mapDevicePagesSubject' and 'mapDevice...
2019-07-05 Johannes OsterholzerUse buffering in Files.Read_Word64
2019-07-05 Johannes OsterholzerBounded_Table: Add postcondition for Model
2019-07-05 Johannes OsterholzerCommand_Stream.XML: Set explicit range for Index_Type
2019-07-05 Johannes OsterholzerFile.Read_Word64: Pad with zeroes
2019-07-05 Johannes OsterholzerAdd XML commands 'mapPagesKernel' and 'mapPagesDeviceDo...
2019-07-05 Johannes OsterholzerTypes.Page_Table.EPT: Set IPAT only for leaf page tables
2019-07-05 Johannes OsterholzerTypes.Page_Table: Set caching type only for leaf page...
2019-07-05 Johannes OsterholzerAdd_Mapping: Supply caching type of memory regions...
2019-07-05 Johannes OsterholzerCommand_Stream: Use File.Read_Word64
2019-07-05 Johannes OsterholzerImplement Files.Read_Word64
2019-07-05 Johannes Osterholzertest.xml: Fix tabs
2019-07-05 Johannes Osterholzertest.xml: Specify page access rights
2019-07-05 Johannes OsterholzerSupply page access rights in commands 'mapDevicePage*'
2019-07-05 Johannes OsterholzerAdapt test.xml to changed command names
2019-07-05 Adrian-Ken... Streamline naming of device domain XML commands
2019-07-05 Johannes OsterholzerAmend test.xml with examples for '*_Pages_*' commands
2019-07-05 Johannes OsterholzerAdd and process XML command 'mapPagesSubject'
2019-07-05 Johannes OsterholzerAdd and process XML command 'activatePagesMR'
2019-07-05 Johannes OsterholzerAdd and process XML commands 'appendPages*'
2019-07-05 Johannes OsterholzerAdd and process XML command 'clearPages'
2019-07-05 Johannes OsterholzerCommand_Stream: Generate commands from XML node lazily
2019-07-05 Johannes OsterholzerData.Devices.Writers: Rectify postcondition
2019-07-05 Johannes OsterholzerAdd ghost function 'Page.Within (Address, Base, Length)'
2019-07-05 Johannes OsterholzerRemove unused Proof_In 'Typization_State'
2019-07-05 Johannes OsterholzerData.Memory.Paging: Fix inferred global annotations
2019-07-05 Johannes OsterholzerRename package 'Verification' to 'Page', add function...
2019-07-05 Johannes OsterholzerData.Memory.Paging: Prove preservation of Roots.Invariant
2019-07-05 Johannes OsterholzerAdd axiom Full_Typization_Page
2019-07-05 Johannes OsterholzerData.Memory.Paging: Add assertion to facilitate proof
2019-07-05 Johannes OsterholzerData.Roots: Add Lemma_Invariant
2019-07-05 Johannes OsterholzerData.Memory.Add_*_Block: Add invariant to contract
2019-07-05 Johannes OsterholzerData.Memory.VTd_IOMMU: Fix incorrect contract
2019-07-05 Johannes OsterholzerCommands.Setup: Add Roots.Invariant to contracts
2019-07-05 Johannes OsterholzerData.Memory_Region_Table: Shorten postcondition
2019-07-05 Johannes OsterholzerData.Roots.Writers: Strengthen some postconditions
2019-07-05 Johannes OsterholzerCommands.Devices: Add Data.Roots.Invariant to contracts
2019-07-05 Johannes OsterholzerData.Devices.Writers: Add Data.Roots.Invariant to contracts
2019-07-05 Johannes OsterholzerData.Roots: Add Invariant_Tau0_State
2019-07-05 Johannes OsterholzerCommands: Add Memory_Region_Table.Invariant to contracts
2019-07-05 Johannes OsterholzerData.Roots.Writers: Apply Memory_Region_Table.Lemma_Inv...
2019-07-05 Johannes OsterholzerMemory.Paging: State Memory_Region_Table.Invariant
2019-07-05 Johannes OsterholzerMemory_Region_Table: Add 'Lemma_Invariant'
2019-07-05 Johannes OsterholzerMemory.Paging: Honour out-parameter 'Success' in contracts
2019-07-05 Johannes OsterholzerMove VTd_Tables_Valid to Data.Roots
2019-07-05 Johannes OsterholzerRoots.Writers.Assign_Device: Fix proof
next