summaryrefslogtreecommitdiffstats
path: root/src/common.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/common.h')
-rw-r--r--src/common.h32
1 files changed, 25 insertions, 7 deletions
diff --git a/src/common.h b/src/common.h
index aeecaf5..886d4dd 100644
--- a/src/common.h
+++ b/src/common.h
@@ -111,6 +111,7 @@ struct efi_guid_s
#define PMAC_FWDRIVER 5
#define PMAC_SWAP 0x82
#define PMAC_LINUX 0x83
+#define PMAC_BEOS 0xEB
#define PMAC_HFS 0xAF
#define PMAC_MAP 6
#define PMAC_PATCHES 7
@@ -232,6 +233,9 @@ struct efi_guid_s
#define GPT_ENT_TYPE_SOLARIS_RESERVED5 \
((const efi_guid_t){le32(0x6a8d2ac7),le16(0x1dd2),le16(0x11b2),0x96,0xa6,{0x08,0x00,0x20,0x73,0x66,0x31}})
+#define GPT_ENT_TYPE_BEOS_BFS \
+ ((const efi_guid_t){le32(0x42465331),le16(0x3ba3),le16(0x10f1),0x80,0x2a,{0x48,0x61,0x69,0x6b,0x75,0x21}})
+
#define TESTDISK_O_RDONLY 00
#define TESTDISK_O_RDWR 02
#define TESTDISK_O_DIRECT 040000
@@ -363,7 +367,7 @@ struct arch_fnct_struct
int (*write_MBR_code)(disk_t *disk);
void (*set_prev_status)(const disk_t *disk, partition_t *partition);
void (*set_next_status)(const disk_t *disk, partition_t *partition);
- int (*test_structure)(list_part_t *list_part);
+ int (*test_structure)(const list_part_t *list_part);
unsigned int (*get_part_type)(const partition_t *partition);
int (*set_part_type)(partition_t *partition, unsigned int part_type);
void (*init_structure)(const disk_t *disk,list_part_t *list_part, const int verbose);
@@ -472,6 +476,10 @@ void set_part_name(partition_t *partition, const char *src, const unsigned int m
@*/
void set_part_name_chomp(partition_t *partition, const unsigned char *src, const unsigned int max_size);
+/*@
+ @ requires valid_read_string(str);
+ @ ensures \result == \null || valid_read_string(\result);
+ @*/
char* strip_dup(char* str);
/*@ assigns \nothing; */
@@ -570,21 +578,31 @@ struct tm *localtime_r(const time_t *timep, struct tm *result);
/*@
@ requires \valid(current_cmd);
- @ requires valid_string(*current_cmd);
- @ requires valid_read_string((char *)*cmd);
+ @ requires valid_read_string(*current_cmd);
+ @ requires valid_read_string(cmd);
+ @ requires \separated(cmd+(..), current_cmd);
+ @ requires strlen(cmd) == n;
+ @ assigns *current_cmd;
+ @ assigns \result \from indirect:(*current_cmd)[0 .. n-1], indirect:cmd[0 ..n-1], indirect:n;
+ @ ensures valid_read_string(*current_cmd);
+ @ ensures \result == 0 ==> *current_cmd == \old(*current_cmd) + n;
+ @ ensures \result != 0 ==> *current_cmd == \old(*current_cmd);
@*/
- // requires strlen(cmd) == n;
-int check_command(char **current_cmd, const char *cmd, size_t n);
+int check_command(char **current_cmd, const char *cmd, const size_t n);
/*@
@ requires \valid(current_cmd);
- @ requires valid_string(*current_cmd);
+ @ requires valid_read_string(*current_cmd);
+ @ assigns *current_cmd;
+ @ ensures valid_read_string(*current_cmd);
@*/
void skip_comma_in_command(char **current_cmd);
/*@
@ requires \valid(current_cmd);
- @ requires valid_string(*current_cmd);
+ @ requires valid_read_string(*current_cmd);
+ @ assigns *current_cmd;
+ @ ensures valid_read_string(*current_cmd);
@*/
uint64_t get_int_from_command(char **current_cmd);
#ifdef __cplusplus