- 20bf593 ext2: Rename Inode_Extents -> Inline_Extents by Nico Huber · 11 months ago
- 7e7d149 ext2: Restore Size attribute, keep it along Object_Size by Nico Huber · 11 months ago
- b735a1d ext2: Relax initialization in Read() by Nico Huber · 11 months ago
- 4210fcc isofs: Assist proofs by Nico Huber · 11 months ago
- f9ab868 FILO: Check overflow when converting unsigned to signed by Nico Huber · 11 months ago
- 32f1927 FILO: Fix pre-coditions of Read_LE16/32 by Nico Huber · 11 months ago
- 995779c FILO: Pack buffers (for safe unchecked conversions) by Nico Huber · 11 months ago
- dccd234 vfs mock: Proble nullfs last by Nico Huber · 11 months ago
- a6d6315 Add NullFS by Thomas Heijligen · 11 months ago
- cc960f2 Start ISO9660 support by Nico Huber · 11 months ago
- b50290f ext2: Drop redundant initialization (Blockdev.Read handles it now) by Nico Huber · 11 months ago
- b18c2cc Add awful script to test ext2 filesystems by Nico Huber · 11 months ago
- bc6d631 Add alternative main() for a simple `cat' program by Nico Huber · 11 months ago
- e5855e9 vfs mock: Allow paths without leading / by Nico Huber · 11 months ago
- 566c886 ext2: Allow to open `root' as a subdirectory by Nico Huber · 11 months ago
- 75e20b5 ext2: Ignore physical 0 pointers in ext2 block map by Nico Huber · 11 months ago
- ea1de11 ext2: Cache physical location of current content block by Nico Huber · 11 months ago
- 4f366b3 ext2: Support gaps in extents for sparse files by Nico Huber · 11 months ago
- 767608d ext2: Ensure the directory walk progresses by Nico Huber · 11 months ago
- 29e1ba2 ext2: Check maximum extent length by Nico Huber · 11 months ago
- bc4f7e9 ext2: Fix typo in extent-header magic by Nico Huber · 11 months ago
- d55fa51 main: Use `z' format modifier by Nico Huber · 11 months ago
- 3603eaa nullfs: Use constants where possible by Nico Huber · 11 months ago
- 6fb3854 Justify warnings about unnecessary checks in 64-bit builds by Nico Huber · 11 months ago
- be9ca52 Drop redundant with/use clauses by Nico Huber · 11 months ago
- 6bef924 ext2: Simplify block cache by Nico Huber · 11 months ago
- 43af31f ext2: Only read interesting part of the superblock by Nico Huber · 11 months ago
- d7001cf Add some file-dumping tests by Nico Huber · 11 months ago
- f646c8e main(): Initialize options struct by Nico Huber · 11 months ago
- 9775da2 main(): Call adainit()/adafinal() by Nico Huber · 11 months ago
- fcd5f0e Hook ext2fs up in vfs.c by Nico Huber · 11 months ago
- 4331448 FILO.FS.VFS: Close currently open file before opening new one by Nico Huber · 11 months ago
- f01abce FILO.Blockdev.Read: Call devread() (not devopen()) by Nico Huber · 11 months ago
- a68ee40 Fix devread(): fread() returns the number of elements, not bytes by Nico Huber · 11 months ago
- a0b1178 gprbuild: Move output to build/ by Nico Huber · 11 months ago
- 936a9d8 Fixup :/ due to wrong signature by Thomas Heijligen · 11 months ago
- 68ed36e Blockdev: Buffer needs only to be of type out by Thomas Heijligen · 11 months ago
- 53df785 ext2: Somewhat finish proofs by Nico Huber · 12 months ago
- e5d7c0e ext2: Re-work file-name version of Open() to ease proving by Nico Huber · 12 months ago
- fe26032 ext2: Use unnecessarily big range type to ease proving by Nico Huber · 12 months ago
- eb01207 ext2: Finish round of proofs for inode version of Open() by Nico Huber · 12 months ago
- 7eb5692 ext2: Factor inode-group deserialization out by Nico Huber · 12 months ago
- 71f9ca0 ext2: Factor inode deserialization out by Nico Huber · 12 months ago
- 925326e ext2: Adjust inode version of Open() to ease proof by Nico Huber · 12 months ago
- 39f086c ext2: Restrict range of First_Data_Block by Nico Huber · 12 months ago
- ecafb8f ext2: Pre-compute Inodes_Per_Block & Desc_Per_Block by Nico Huber · 12 months ago
- 1db9193 ext2: Adjust Extent_Block_Map() to ease proof by Nico Huber · 12 months ago
- 52f4c8d ext2: Further split our state record by Nico Huber · 12 months ago
- 96a0b0e ext2: Help proof of extent lookup by Nico Huber · 12 months ago
- 6710c0e ext2: Fix binary extent search and help proof by Nico Huber · 12 months ago
- 5a042fd ext2: Adapt to satisfy some checks by Nico Huber · 12 months ago
- 700a411 ext2: Introduce State.Block_Size by Nico Huber · 12 months ago
- 3da2147 VFS: Satisfy GNATprove and No_Secondary_Stack by Nico Huber · 1 year ago
- 89d0594 ext2: Add missing default value for Inode.I by Nico Huber · 1 year ago
- 21d4202 Implement Ext2.Open() by Nico Huber · 1 year ago
- b1cb2d3 Re-invent FS.VFS.Open() by Nico Huber · 1 year ago
- 549a1b8 Drop `File_Len` from VFS.Read() by Nico Huber · 1 year ago
- d3644be Implement Ext2.Read() by Nico Huber · 1 year ago
- 022e226 ext2: Read inode type and length by Nico Huber · 1 year ago
- 7403a54 ext2: Rename Inode.Extents => Inode.Inline by Nico Huber · 1 year ago
- 1f3825e Disable SPARK_Mode for use of 'Address by Nico Huber · 1 year ago
- 2217322 Work around gnatprove trouble with >64-bit range type by Nico Huber · 1 year ago
- cdc0351 ext2: Implement Open() for an inode by number by Nico Huber · 1 year ago
- 57dfbfb ext2: Distinguish physical (always valid) and logical (per file) cached blocks by Nico Huber · 1 year ago
- f83364a Implement Is_Space() by Nico Huber · 1 year ago
- 33f6d95 ext2: Better organize per inode info by Nico Huber · 1 year ago
- 77a04d7 ext2: Make Feature_64Bit more strict by Nico Huber · 1 year ago
- cd1d5f7 Tune ext2 types by Nico Huber · 1 year ago
- 0496d89 Add Is_Power_Of_2 functions by Nico Huber · 1 year ago
- c4c7a5e ext2: Fix off-by-one by Nico Huber · 1 year ago
- fffc8c1 Implement Extent_Block_Map for ext4 extents by Nico Huber · 1 year ago
- 68c8693 ext2: Extract Cache_FSBlock procedure by Nico Huber · 1 year ago
- fe89712 ext2: Use a more generic cache index by Nico Huber · 1 year ago
- 6623c98 First version of Ext2_Block_Map by Nico Huber · 1 year ago
- 9072090 Fix Read_LE16/32 for array slices by Nico Huber · 1 year ago
- f5d99d0 Implement Ext2.Read_FSBlock by Nico Huber · 1 year ago
- 7f61349 Use BLOCK_SIZE by Nico Huber · 1 year ago
- a529660 Prepare Blockdev for 32-bit longs by Nico Huber · 1 year ago
- 9c04187 Introduce Blockdev_Length/_Offset by Nico Huber · 1 year ago
- 481ff84 Move shared types into FILO package by Nico Huber · 1 year ago
- 5182037 Add NullFS by Thomas Heijligen · 1 year, 1 month ago
- 5c43abc Move fs-filo to filo-fs by Thomas Heijligen · 1 year, 1 month ago
- a968f6f add Ada wrapper for C_devread by Thomas Heijligen · 1 year, 1 month ago
- 26f7183 FS.FILO.Ext2: Fill Mount() procedure by Nico Huber · 1 year, 1 month ago
- 8ec45a1 FS.FILO.Ext2: Export C functions by Nico Huber · 1 year, 1 month ago
- 2f4d597 VFS: add <> to generics by Thomas Heijligen · 1 year, 1 month ago
- 57d3a85 FS.FILO.Ext2: Update stubs by Nico Huber · 1 year, 1 month ago
- 3e72282 FS.FILO: Add Partition_Offset type by Nico Huber · 1 year, 1 month ago
- cd6b7ec FS: Add pre-conditions for deserialization functions by Nico Huber · 1 year, 1 month ago
- f983931 FS.FILO: Allow File_Offset of full File_Length by Nico Huber · 1 year, 1 month ago
- 3ec689d nix: add -U option to gnatprove by Thomas Heijligen · 1 year, 1 month ago
- 691220d FS.FILO.VFS: Move `Convention => C` to spec by Nico Huber · 1 year, 1 month ago
- 51f6041 Make VFS wrapper state aware by Nico Huber · 1 year, 1 month ago
- 75d1ff3 vfs: Add filo like vfs layer by Thomas Heijligen · 1 year, 1 month ago
- dc1a84b blockdev: Add missing partition functions by Thomas Heijligen · 1 year, 1 month ago
- 98417fc Add Read_LE16/32 and types by Nico Huber · 1 year, 1 month ago
- 1d7727f Add stub for FS.FILO.Ext2 by Nico Huber · 1 year, 1 month ago
- d49cb12 Move SPARK_Mode => Off into body by Thomas Heijligen · 1 year, 1 month ago
- b00b316 Use getopt for program parameters by Thomas Heijligen · 1 year, 1 month ago
- 3a5cd8c FS.FILO: Add access to globals by Nico Huber · 1 year, 1 month ago