Make it compile
diff --git a/default.gpr b/default.gpr
index 7437fd5..96aed41 100644
--- a/default.gpr
+++ b/default.gpr
@@ -1,6 +1,6 @@
project Default is
-
- for Main use ("main");
+ for Languages use ("ada", "c");
+ for Main use ("main.c");
for Source_Dirs use ("src");
package Builder is
diff --git a/default.nix b/default.nix
index 6cb0bac..0ce641b 100644
--- a/default.nix
+++ b/default.nix
@@ -11,6 +11,7 @@
gprbuild
spark2014
z3
+ cppcheck
];
gprFile = "default.gpr";
diff --git a/src/fs.c b/src/blockdev.c
similarity index 64%
rename from src/fs.c
rename to src/blockdev.c
index 271662a..443efcd 100644
--- a/src/fs.c
+++ b/src/blockdev.c
@@ -1,9 +1,9 @@
#include <stdio.h>
-#include "fs.h"
+#include "blockdev.h"
-FILE* block_device = NULL
+FILE* block_device = NULL;
size_t device_size = 0;
@@ -13,15 +13,17 @@
if (!block_device) {
return 0;
}
- fseek(block_device, 0, SEEK_END)
+ fseek(block_device, 0, SEEK_END);
+ device_size = ftell(block_device);
return 1;
}
void devclose(void)
{
- if (block_device)
+ if (block_device) {
fclose(block_device);
+ }
block_device = NULL;
device_size = 0;
}
@@ -29,19 +31,22 @@
int devread(unsigned long sector, unsigned long byte_offset, unsigned long byte_len, void *buf)
{
if (!block_device) {
- fprintf(stdcerr, "devread: Device not open.\n");
+ fprintf(stderr, "devread: Device not open.\n");
return 0;
}
const unsigned long offset = sector * 512 + byte_offset;
- if (offset + byte_len > device_size)
- fprintf(stdcerr, "devread: Attempt to read beyond device.\n");
+ if (offset + byte_len > device_size) {
+ fprintf(stderr, "devread: Attempt to read beyond device.\n");
return 0;
}
- if fseek(block_device, sector * 512 + byte_offset, SEEK_SET);
+ if (fseek(block_device, sector * 512 + byte_offset, SEEK_SET) != 0) {
+ fprintf(stderr, "devread: Failed to set offset on device.\n");
+ return 0;
+ }
if (fread(buf, byte_len, 1, block_device) != byte_len) {
- fprintf(stdcerr, "devread: Failed to read from device.\n");
+ fprintf(stderr, "devread: Failed to read from device.\n");
return 0;
}
return 1;
@@ -58,5 +63,3 @@
//unsigned long file_size(void);
//void file_set_size(unsigned long size);
//void file_close(void);
-
-#endif /* FS_H */
diff --git a/src/blockdev.h b/src/blockdev.h
new file mode 100644
index 0000000..77256aa
--- /dev/null
+++ b/src/blockdev.h
@@ -0,0 +1,36 @@
+#ifndef BLOCKDEV_H
+#define BLOCKDEV_H
+
+/** devopen
+ * @param name Filename to be used as blockdevice
+ * @param reopen Unused, set NULL
+ * @return 1 on success, 0 on failure !CAUTION
+ */
+int devopen(const char *name, int *reopen);
+
+/** devclose
+ */
+void devclose(void);
+
+/** devread
+ * @param sector 512 byte sector of the block device
+ * @param byte_offset Offset in the block
+ * @param byte_len Buffer length
+ * @param buf Buffer
+ * @return 1 on sucess, 0 on failure !CAUTION
+ */
+int devread(unsigned long sector, unsigned long byte_offset,
+ unsigned long byte_len, void *buf);
+
+
+//void dev_set_partition(unsigned long start, unsigned long size);
+//void dev_get_partition(unsigned long *start, unsigned long *size);
+
+//int file_open(const char *filename);
+//int file_read(void *buf, unsigned long len);
+//unsigned long file_seek(unsigned long offset);
+//unsigned long file_size(void);
+//void file_set_size(unsigned long size);
+//void file_close(void);
+
+#endif /* BLOCKDEV_H */
diff --git a/src/fs-filo.adb b/src/fs-filo.adb
index 3280b34..591f321 100644
--- a/src/fs-filo.adb
+++ b/src/fs-filo.adb
@@ -1,21 +1,19 @@
package body FS.FILO is
procedure Read
- (Buffer : in out Buffer_Type;
- Offset : in Natural;
- Bytes_Read: out Natural)
+ (Buffer : in out Buffer_Type;
+ Offset : in Natural;
+ Success : out Boolean)
is
- Sector_Size : constant Natural := 512;
- Sector : constant Interfaces.C.unsigned_long := Offset / Sector_Size;
- Byte_Offset : constant Interfaces.C.unsigned_long := Offset rem Sector_Size;
- Byte_Len : constant Interfaces.C.unsigned_long := Buffer'Length;
+ --Sector_Size : constant Natural := 512;
+ --Sector : constant Interfaces.C.unsigned_long := Offset / Sector_Size;
+ --Byte_Offset : constant Interfaces.C.unsigned_long := Offset rem Sector_Size;
+ --Byte_Len : constant Interfaces.C.unsigned_long := Buffer'Length;
+ --function To_Bool(Item : Interfaces.C.int) return Bool is
+ -- (if Item = 0 then False else True);
begin
-
- Bytes_Read := C_devread
- (sector => Sector,
- byte_offset => Byte_Offset,
- byte_len => Byte_Len,
- buf => Buffer'Address);
+ null;
+ --Success := To_Bool (C_devread (Sector, Byte_Offset, Byte_Len, Buffer'Address));
end Read;
end FS.FILO;
diff --git a/src/fs-filo.ads b/src/fs-filo.ads
index 43b6cef..12132e3 100644
--- a/src/fs-filo.ads
+++ b/src/fs-filo.ads
@@ -1,4 +1,5 @@
with Interfaces.C;
+with System;
package FS.FILO is
@@ -13,12 +14,13 @@
(sector : Interfaces.C.unsigned_long;
byte_offset : Interfaces.C.unsigned_long;
byte_len : Interfaces.C.unsigned_long;
- buf : ... )
+ buf : System.Address)
return Interfaces.C.int
with
SPARK_Mode => Off,
Import => True,
- Conversion => C;
+ Convention => C,
+ External_Name => "devopen";
end FS.FILO;
diff --git a/src/fs.ads b/src/fs.ads
index 3ea5a69..4591a8a 100644
--- a/src/fs.ads
+++ b/src/fs.ads
@@ -1,5 +1,7 @@
+with Interfaces;
+
package FS is
- type Buffer is array (Natural range <>) of Unsigned_8;
+ type Buffer_Type is array (Natural range <>) of Interfaces.Unsigned_8;
end FS;
diff --git a/src/fs.h b/src/fs.h
deleted file mode 100644
index cf7f003..0000000
--- a/src/fs.h
+++ /dev/null
@@ -1,39 +0,0 @@
-#ifndef FS_H
-#define FS_H
-
-/** devopen
- * @param name Filename to be used as blockdevice
- * @param reopen Unused, set NULL
- * @return 1 on success, 0 on failure !CAUTION
- */
-int devopen(const char *name, int *reopen);
-
-/** devclose
- */
-void devclose(void);
-
-/** devread
- * @param sector 512 byte sector of the block device
- * @param byte_offset Offset in the block
- * @param byte_len Buffer length
- * @param buf Buffer
- * @return 1 on sucess, 0 on failure !CAUTION
- */
-int devread(unsigned long sector, unsigned long byte_offset,
- unsigned long byte_len, void *buf);
-
-
-
-
-
-void dev_set_partition(unsigned long start, unsigned long size);
-void dev_get_partition(unsigned long *start, unsigned long *size);
-
-int file_open(const char *filename);
-int file_read(void *buf, unsigned long len);
-unsigned long file_seek(unsigned long offset);
-unsigned long file_size(void);
-void file_set_size(unsigned long size);
-void file_close(void);
-
-#endif /* FS_H */
diff --git a/src/main.c b/src/main.c
index 91a40d7..5468842 100644
--- a/src/main.c
+++ b/src/main.c
@@ -1,15 +1,17 @@
#include <stdio.h>
+#include "blockdev.h"
+
int main(int argc, char* argv[])
{
if (argc != 2) {
- fprintf(stdcerr, "Use %s /path/to/filesystem\n", argv[0]);
+ fprintf(stderr, "Use %s /path/to/filesystem\n", argv[0]);
return -1;
}
if (devopen(argv[1], NULL) != 1) {
- fprintf(stdcerr, "Faild to open %s\n", argv[1]);
+ fprintf(stderr, "Faild to open %s\n", argv[1]);
return -1;
}