kai-e.github.io/misc/PVS/ARMbuild/0001-Fix-C-errors-for-the-SBCL-based-ARM-Mac-build.patch at main · kai-e/kai-e.github.io · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
From 405c987f9be67e3c46f1a435d3ed5e3601b35405 Mon Sep 17 00:00:00 2001
From: Kai Engelhardt <k.e@acm.org>
Date: Sat, 1 Apr 2023 01:39:16 +1100
Subject: [PATCH] Fix C errors for the SBCL-based ARM Mac build

---
 src/BDD/bdd/utils/hash.h | 2 +-
 src/BDD/bdd_table.c      | 6 +++---
 src/BDD/mu_interface.h   | 2 +-
 src/BDD/mu_table.c       | 4 ++--
 4 files changed, 7 insertions(+), 7 deletions(-)

diff --git a/src/BDD/bdd/utils/hash.h b/src/BDD/bdd/utils/hash.h
index dba841d7..9bf9a538 100644
--- a/src/BDD/bdd/utils/hash.h
+++ b/src/BDD/bdd/utils/hash.h
@@ -71,7 +71,7 @@ typedef struct HASHTAB {
   int nr_rehashes;		/* nr. rehashes */
   int primes_index;		/* curr. index in primes[] table */
 #ifdef ALLOW_REHASH
-  void (*rehash_function) ();	/* function called when non-NULL */
+  void (*rehash_function) (int, int);	/* function called when non-NULL */
 				/* to process change of entry */
 				/* when rehashing in process. */
 				/* Rehashing might happen upon lookup with */
diff --git a/src/BDD/bdd_table.c b/src/BDD/bdd_table.c
index 68dc135e..ff3cc504 100644
--- a/src/BDD/bdd_table.c
+++ b/src/BDD/bdd_table.c
@@ -98,9 +98,9 @@ BDDPTR bdd___bdd_create_var_after (BDDPTR v) {return bdd_create_var_after (v);}
 BDDPTR bdd___bdd_create_var_last (void) {return bdd_create_var_last ();}

 void bdd___bdd_print (FILE *fp, BDDPTR f, char *s)
-  {return bdd_print (fp, f, s);}
+  {bdd_print (fp, f, s);}

-void bdd___bdd_quit (void) {return bdd_quit ();}
+void bdd___bdd_quit (void) {bdd_quit ();}

 int bdd___bdd_nodes_alive (void) {return bdd_nodes_alive ();}

@@ -166,7 +166,7 @@ BDDPTR bdd___bdd_subst_par_list (BDD_LIST f_list, BDD_LIST vars, BDDPTR g)
 {return (BDDPTR) bdd_subst_par_list (f_list, vars, g);}

 void bdd___bdd_free_vec (BDDPTR *f_vec, int size)
-  {return bdd_free_vec (f_vec, size);}
+  {bdd_free_vec (f_vec, size);}

 const char* bdd___bdd_get_output_string (int idx) {
   return (char*) bdd_get_output_string (idx);
diff --git a/src/BDD/mu_interface.h b/src/BDD/mu_interface.h
index 62fd0c20..b80edf1d 100644
--- a/src/BDD/mu_interface.h
+++ b/src/BDD/mu_interface.h
@@ -25,7 +25,7 @@ extern Term mu_mk_g_fixed_point (int relvar, Term fml1);
 extern Term mu_mk_rel_var_ (char *name);
 extern Formula mu_check_mk_bool_var (char *name);
 extern const char* get_mu_bool_var_name (int bdd_idx);
-extern LIST empty_list ();
+extern LIST empty_list (void);
 extern void pvs_mu_print_formula (Formula fml);
 extern void pvs_mu_print_term (Term t);

diff --git a/src/BDD/mu_table.c b/src/BDD/mu_table.c
index eb244ec3..dd49736e 100644
--- a/src/BDD/mu_table.c
+++ b/src/BDD/mu_table.c
@@ -80,13 +80,13 @@ Term mu___mu_mk_equiv_term (Term fml1, Term fml2)
 Term mu___mu_mk_implies_term (Term fml1, Term fml2)
   {return (Term) mu_mk_implies_term (fml1, fml2);}

-char* mu___get_mu_bool_var_name (bdd_idx)
+char* mu___get_mu_bool_var_name (int bdd_idx)
   {return (char *) get_mu_bool_var_name (bdd_idx);}

 LIST mu___append_cont(void *p, LIST list)
   {return (LIST) append_cont (p, list);}

-LIST mu___empty_list () {return (LIST) empty_list ();}
+LIST mu___empty_list (void) {return (LIST) empty_list ();}

 int mu___set_mu_warnings (int flag) {return set_mu_warnings (flag);}

--
2.37.1 (Apple Git-137.1)