Keeping cpp script for the moment.

Signed-off-by: Achim D. Brucker <adbrucker@0x5f.org>

misc/scripts/cpp

@@ -0,0 +1,17 @@
+#!/bin/bash
+#
+# Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
+#
+# SPDX-License-Identifier: BSD-2-Clause
+#
+
+#
+# Wrapper for clang C preprocessor on MacOS
+#
+export L4CPP="-DTARGET=ARM -DTARGET_ARM -DPLATFORM=Sabre -DPLATFORM_Sabre"
+
+if [[ "$OSTYPE" == "darwin"* ]]; then
+    llvm-gcc -Wno-invalid-pp-token -E -x c $@
+else
+    cpp -Wno-invalid-pp-token -E -x c $@
+fi

tools/c-parser/calculate_state.ML

@@ -480,8 +480,12 @@ fun mk_thy_types cse install thy = let
 
   val thy = List.foldl rcddecls_phase0 thy sorted_structs
 
+  val abs_outfilnameN = (if Path.is_absolute (Path.explode outfilnameN)
+                            then outfilnameN
+                            else (Path.implode o Path.expand)
+                                   (Path.append (Resources.master_directory thy) (Path.explode outfilnameN)))
   (* Yuck, sorry *)
-  val _ = gen_umm_types_file cse outfilnameN
+  val _ = gen_umm_types_file cse abs_outfilnameN
 
   val arrays = List.filter (fn (_, sz) => sz <> 0)
                            (Binaryset.listItems (get_array_mentions cse))

tools/c-parser/isar_install.ML

@@ -145,7 +145,9 @@ fun get_Csyntax thy s = let
   val cpp_option =
       case Config.get_global thy cpp_path of
           "" => NONE
-        | s => SOME s
+        | s => SOME (if Path.is_absolute (Path.explode s)
+                     then s
+                     else Path.implode (Path.append (Resources.master_directory thy) (Path.explode s)))
   val cpp_error_count = Config.get_global thy report_cpp_errors
   val (ast0, _) =
       StrictCParser.parse