From ae5f96895dfd7454d1a3cb8770d0a180b956acda Mon Sep 17 00:00:00 2001
From: Josh Berdine <jjb@microsoft.com>
Date: Mon, 3 Dec 2012 03:51:04 +0000
Subject: [PATCH] Change to avoid relying on sed supporting disjunction or
escaped control characters
---
src/api/ml/add_error_checking.V3.sed | 2 +-
src/api/ml/add_error_checking.sed | 81 ++++++++++++++++++----------
src/api/ml/build.sed | 2 +-
3 files changed, 56 insertions(+), 29 deletions(-)
diff --git a/src/api/ml/add_error_checking.V3.sed b/src/api/ml/add_error_checking.V3.sed
index 170ca2d6b..7ec725b77 100644
--- a/src/api/ml/add_error_checking.V3.sed
+++ b/src/api/ml/add_error_checking.V3.sed
@@ -1,2 +1,2 @@
# Customize error handling for contexts created in ML:
-s/Z3_API Z3_mk_context\(_rc\|\)(\(.*\))/Z3_API Z3_mk_context\1(\2) quote(dealloc,\"Z3_set_error_handler(_res, caml_z3_error_handler);\")/g
+s/Z3_API Z3_mk_context(\(.*\))/Z3_API Z3_mk_context(\1) quote(dealloc,\"Z3_set_error_handler(_res, caml_z3_error_handler);\")/g
diff --git a/src/api/ml/add_error_checking.sed b/src/api/ml/add_error_checking.sed
index ede3275e1..71c06b9e4 100644
--- a/src/api/ml/add_error_checking.sed
+++ b/src/api/ml/add_error_checking.sed
@@ -3,14 +3,19 @@
# Add error checking epilogue for all Z3_API functions that accept two Z3_contexts
:begincc
-# add epilogue for two Z3_context parameters
-s/Z3_API \(.*\)(\(.*\)Z3_context \([a-zA-Z]*\)\(.*\)Z3_context \([a-zA-Z]*\)\([^a-zA-Z].*\|\))\(;\|\)[ ]*$/Z3_API \1(\2Z3_context \3\4Z3_context \5\6) quote(dealloc,\"check_error_code(\3);\")\7/g
-
-# if a match was found, done with all Z3_contexts and Z3_theorys
+# add epilogue for two Z3_context parameters and if a match was found, done with all Z3_contexts and Z3_theorys so jump to endt
+s/Z3_API \(.*\)(\(.*\)Z3_context \([a-zA-Z]*\)\(.*\)Z3_context \([a-zA-Z]*\)\([^a-zA-Z].*\));[ ]*$/Z3_API \1(\2Z3_context \3\4Z3_context \5\6) quote(dealloc,\"check_error_code(\3);\");/g
+t endt
+s/Z3_API \(.*\)(\(.*\)Z3_context \([a-zA-Z]*\)\(.*\)Z3_context \([a-zA-Z]*\));[ ]*$/Z3_API \1(\2Z3_context \3\4Z3_context \5) quote(dealloc,\"check_error_code(\3);\");/g
+t endt
+s/Z3_API \(.*\)(\(.*\)Z3_context \([a-zA-Z]*\)\(.*\)Z3_context \([a-zA-Z]*\)\([^a-zA-Z].*\))[ ]*$/Z3_API \1(\2Z3_context \3\4Z3_context \5\6) quote(dealloc,\"check_error_code(\3);\")/g
+t endt
+s/Z3_API \(.*\)(\(.*\)Z3_context \([a-zA-Z]*\)\(.*\)Z3_context \([a-zA-Z]*\))[ ]*$/Z3_API \1(\2Z3_context \3\4Z3_context \5) quote(dealloc,\"check_error_code(\3);\")/g
t endt
# if complete prototype, done with two Z3_contexts
-/Z3_API .*(.*)\(;\|\)[ ]*$/b endcc
+/Z3_API .*(.*);[ ]*$/b endcc
+/Z3_API .*(.*)[ ]*$/b endcc
# if incomplete prototype
/Z3_API .*(.*/{
@@ -18,10 +23,14 @@ t endt
# read another line
N
- # add epilogue for two Z3_context parameters
- s/Z3_API \(.*\)(\(.*\)Z3_context \([a-zA-Z]*\)\(.*\)Z3_context \([a-zA-Z]*\)\([^a-zA-Z].*\|\))\(;\|\)[ ]*$/Z3_API \1(\2Z3_context \3\4Z3_context \5\6) quote(dealloc,\"check_error_code(\3); check_error_code(\5);\")\7/g
-
- # if a match was found, done with all Z3_contexts and Z3_theorys
+ # add epilogue for two Z3_context parameters and if a match was found, done with all Z3_contexts and Z3_theorys so jump to endt
+ s/Z3_API \(.*\)(\(.*\)Z3_context \([a-zA-Z]*\)\(.*\)Z3_context \([a-zA-Z]*\)\([^a-zA-Z].*\));[ ]*$/Z3_API \1(\2Z3_context \3\4Z3_context \5\6) quote(dealloc,\"check_error_code(\3); check_error_code(\5);\");/g
+ t endt
+ s/Z3_API \(.*\)(\(.*\)Z3_context \([a-zA-Z]*\)\(.*\)Z3_context \([a-zA-Z]*\));[ ]*$/Z3_API \1(\2Z3_context \3\4Z3_context \5) quote(dealloc,\"check_error_code(\3); check_error_code(\5);\");/g
+ t endt
+ s/Z3_API \(.*\)(\(.*\)Z3_context \([a-zA-Z]*\)\(.*\)Z3_context \([a-zA-Z]*\)\([^a-zA-Z].*\))[ ]*$/Z3_API \1(\2Z3_context \3\4Z3_context \5\6) quote(dealloc,\"check_error_code(\3); check_error_code(\5);\")/g
+ t endt
+ s/Z3_API \(.*\)(\(.*\)Z3_context \([a-zA-Z]*\)\(.*\)Z3_context \([a-zA-Z]*\))[ ]*$/Z3_API \1(\2Z3_context \3\4Z3_context \5) quote(dealloc,\"check_error_code(\3); check_error_code(\5);\")/g
t endt
# else keep looking for two Z3_contexts
@@ -31,14 +40,19 @@ t endt
# Add error checking epilogue for all Z3_API functions that accept one Z3_context
:beginc
-# add epilogue for one Z3_context parameter
-s/Z3_API \(.*\)(\(.*\)Z3_context \([a-zA-Z]*\)\([^a-zA-Z].*\|\))\(;\|\)[ ]*$/Z3_API \1(\2Z3_context \3\4) quote(dealloc,\"check_error_code(\3);\")\5/g
-
-# if a match was found, done with all Z3_contexts and Z3_theorys
+# add epilogue for one Z3_context parameter and if a match was found, done with all Z3_contexts and Z3_theorys so jump to endt
+s/Z3_API \(.*\)(\(.*\)Z3_context \([a-zA-Z]*\)\([^a-zA-Z].*\));[ ]*$/Z3_API \1(\2Z3_context \3\4) quote(dealloc,\"check_error_code(\3);\");/g
+t endt
+s/Z3_API \(.*\)(\(.*\)Z3_context \([a-zA-Z]*\));[ ]*$/Z3_API \1(\2Z3_context \3) quote(dealloc,\"check_error_code(\3);\");/g
+t endt
+s/Z3_API \(.*\)(\(.*\)Z3_context \([a-zA-Z]*\)\([^a-zA-Z].*\)[ ]*$/Z3_API \1(\2Z3_context \3\4) quote(dealloc,\"check_error_code(\3);\")/g
+t endt
+s/Z3_API \(.*\)(\(.*\)Z3_context \([a-zA-Z]*\))[ ]*$/Z3_API \1(\2Z3_context \3) quote(dealloc,\"check_error_code(\3);\")/g
t endt
# if complete prototype, done with all Z3_contexts
-/Z3_API .*(.*)\(;\|\)[ ]*$/b endc
+/Z3_API .*(.*);[ ]*$/b endc
+/Z3_API .*(.*)[ ]*$/b endc
# if incomplete prototype
/Z3_API .*(.*/{
@@ -46,10 +60,14 @@ t endt
# read another line
N
- # add epilogue for one Z3_context parameter
- s/Z3_API \(.*\)(\(.*\)Z3_context \([a-zA-Z]*\)\([^a-zA-Z].*\|\))\(;\|\)[ ]*$/Z3_API \1(\2Z3_context \3\4) quote(dealloc,\"check_error_code(\3);\")\5/g
-
- # if a match was found, done with all Z3_contexts and Z3_theorys
+ # add epilogue for one Z3_context parameter and if a match was found, done with all Z3_contexts and Z3_theorys so jump to endt
+ s/Z3_API \(.*\)(\(.*\)Z3_context \([a-zA-Z]*\)\([^a-zA-Z].*\));[ ]*$/Z3_API \1(\2Z3_context \3\4) quote(dealloc,\"check_error_code(\3);\");/g
+ t endt
+ s/Z3_API \(.*\)(\(.*\)Z3_context \([a-zA-Z]*\));[ ]*$/Z3_API \1(\2Z3_context \3) quote(dealloc,\"check_error_code(\3);\");/g
+ t endt
+ s/Z3_API \(.*\)(\(.*\)Z3_context \([a-zA-Z]*\)\([^a-zA-Z].*\))[ ]*$/Z3_API \1(\2Z3_context \3\4) quote(dealloc,\"check_error_code(\3);\")/g
+ t endt
+ s/Z3_API \(.*\)(\(.*\)Z3_context \([a-zA-Z]*\))[ ]*$/Z3_API \1(\2Z3_context \3) quote(dealloc,\"check_error_code(\3);\")/g
t endt
# else keep looking for one Z3_context
@@ -60,24 +78,33 @@ t endt
# Add error checking epilogue for all Z3_API functions that accept a Z3_theory
:begint
-# add epilogue for one Z3_theory parameter
-s/Z3_API \(.*\)(\(.*\)Z3_theory \([a-zA-Z]*\)\([^a-zA-Z].*\|\))\(;\|\)[ ]*$/Z3_API \1(\2Z3_theory \3\4) quote(dealloc,\"check_error_code(Z3_theory_get_context(\3));\")\5/g
-
-# if a match was found, done with all Z3_contexts and Z3_theorys
+# add epilogue for one Z3_theory parameter and if a match was found, done with all Z3_contexts and Z3_theorys so jump to endt
+s/Z3_API \(.*\)(\(.*\)Z3_theory \([a-zA-Z]*\)\([^a-zA-Z].*\));[ ]*$/Z3_API \1(\2Z3_theory \3\4) quote(dealloc,\"check_error_code(Z3_theory_get_context(\3));\");/g
+t endt
+s/Z3_API \(.*\)(\(.*\)Z3_theory \([a-zA-Z]*\));[ ]*$/Z3_API \1(\2Z3_theory \3) quote(dealloc,\"check_error_code(Z3_theory_get_context(\3));\");/g
+t endt
+s/Z3_API \(.*\)(\(.*\)Z3_theory \([a-zA-Z]*\)\([^a-zA-Z].*\))[ ]*$/Z3_API \1(\2Z3_theory \3\4) quote(dealloc,\"check_error_code(Z3_theory_get_context(\3));\")/g
+t endt
+s/Z3_API \(.*\)(\(.*\)Z3_theory \([a-zA-Z]*\))[ ]*$/Z3_API \1(\2Z3_theory \3) quote(dealloc,\"check_error_code(Z3_theory_get_context(\3));\")/g
t endt
# if complete prototype, done with all Z3_theorys
-/Z3_API .*(.*)\(;\|\)[ ]*$/b endt
+/Z3_API .*(.*);[ ]*$/b endt
+/Z3_API .*(.*)[ ]*$/b endt
/Z3_API .*(.*/{
# read another line
N
- # add epilogue for one Z3_theory parameter
- s/Z3_API \(.*\)(\(.*\)Z3_theory \([a-zA-Z]*\)\([^a-zA-Z].*\|\))\(;\|\)[ ]*$/Z3_API \1(\2Z3_theory \3\4) quote(dealloc,\"check_error_code(Z3_theory_get_context(\3));\")\5/g
-
- # if a match was found, done with all Z3_theorys
+ # add epilogue for one Z3_theory parameter and if a match was found, done with all Z3_contexts and Z3_theorys so jump to endt
+ s/Z3_API \(.*\)(\(.*\)Z3_theory \([a-zA-Z]*\)\([^a-zA-Z].*\));[ ]*$/Z3_API \1(\2Z3_theory \3\4) quote(dealloc,\"check_error_code(Z3_theory_get_context(\3));\");/g
+ t endt
+ s/Z3_API \(.*\)(\(.*\)Z3_theory \([a-zA-Z]*\));[ ]*$/Z3_API \1(\2Z3_theory \3) quote(dealloc,\"check_error_code(Z3_theory_get_context(\3));\");/g
+ t endt
+ s/Z3_API \(.*\)(\(.*\)Z3_theory \([a-zA-Z]*\)\([^a-zA-Z].*\))[ ]*$/Z3_API \1(\2Z3_theory \3\4) quote(dealloc,\"check_error_code(Z3_theory_get_context(\3));\")/g
+ t endt
+ s/Z3_API \(.*\)(\(.*\)Z3_theory \([a-zA-Z]*\))[ ]*$/Z3_API \1(\2Z3_theory \3) quote(dealloc,\"check_error_code(Z3_theory_get_context(\3));\")/g
t endt
# else keep looking for one Z3_theory
diff --git a/src/api/ml/build.sed b/src/api/ml/build.sed
index d53a13713..c7d1fc804 100644
--- a/src/api/ml/build.sed
+++ b/src/api/ml/build.sed
@@ -43,7 +43,7 @@ s/\\ / /g
s/\\c \([^ .,:]*\)/[\1]/g
# '#Z3_' -> 'Z3.'
-s/#Z3_\([^ \n\.\t,)]*\)/{!Z3.\1}/g
+s/#Z3_\([^ \.,) ]*\)/{!Z3.\1}/g
# '/*@}*/' -> ''
s/\/\*@{\*\///g