mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-28 11:25:51 +00:00
Code Activity

Change to avoid relying on sed supporting disjunction or escaped control characters

Browse source
This commit is contained in:
Josh Berdine 2012-12-03 03:51:04 +00:00 • committed by Leonardo de Moura
parent 4ec4151e82
commit ae5f96895d
3 changed files with 56 additions and 29 deletions
Download patch file Download diff file Expand all files Collapse all files

81
src/api/ml/add_error_checking.sed
View file

@ -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