bug #398 test (bug was resolved last night), and a script to download all bug attachm...
authorMorgan Deters <mdeters@gmail.com>
Wed, 26 Sep 2012 16:42:40 +0000 (16:42 +0000)
committerMorgan Deters <mdeters@gmail.com>
Wed, 26 Sep 2012 16:42:40 +0000 (16:42 +0000)
contrib/get-bug-attachments [new file with mode: 0755]
test/regress/regress0/Makefile.am
test/regress/regress0/bug398.smt2 [new file with mode: 0644]

diff --git a/contrib/get-bug-attachments b/contrib/get-bug-attachments
new file mode 100755 (executable)
index 0000000..16af3c6
--- /dev/null
@@ -0,0 +1,75 @@
+#!/bin/bash
+#
+# get-bug-attachments
+# Morgan Deters <mdeters@cs.nyu.edu>
+# Wed, 26 Sep 2012 09:40:10 -0400
+#
+
+if [ $# -lt 1 ]; then
+  echo "usage: `basename $0` bugids.." >&2
+  exit 1
+fi
+
+while [ $# -gt 0 ]; do
+
+bugid="$1"
+shift
+
+function webcat {
+  if which wget &>/dev/null; then
+    wget -O - "$1"
+  elif which curl &>/dev/null; then
+    curl "$1"
+  else
+    echo "Please install wget or curl." >&2;
+    exit 1
+  fi
+}
+
+function webget {
+  if which wget &>/dev/null; then
+    tmpfile="$(mktemp)"
+    filename="$(wget -qS -O "$tmpfile" "$1" 2>&1 | grep 'Content-disposition: attachment' | sed 's,.*filename="\(.*\)".*,\1,')"
+    ext="$(echo "$filename" | sed 's,.*\.\(.*\),\1,')"
+    if [ -e "$2.$ext" ] && ! diff -q "$tmpfile" "$2.$ext" &>/dev/null; then
+      c=a
+      while [ -e "$2$c.$ext" ] && ! diff -q "$tmpfile" "$2$c.$ext" &>/dev/null; do
+        c=$(echo $c | tr a-y b-z)
+      done
+      mkdir -p "$(dirname "$2")"
+      mv "$tmpfile" "$2$c.$ext"
+      echo "$2$c.$ext"
+    else
+      mkdir -p "$(dirname "$2")"
+      mv "$tmpfile" "$2.$ext"
+      echo "$2.$ext"
+    fi
+  elif which curl &>/dev/null; then
+    mkdir -p "$(dirname "$2")"
+    curl "$1" >"$2"
+  else
+    echo "Please install wget or curl." >&2;
+    exit 1
+  fi
+}
+
+count=0
+for attachment in $(\
+  webcat "http://church.cims.nyu.edu/bugs/show_bug.cgi?id=$bugid" 2>/dev/null \
+  | grep ' href="attachment.cgi?id=[0-9][0-9]*' \
+  | sed 's,.* href="attachment.cgi?id=\([0-9][0-9]*\).*,\1,' \
+  | sort -nu); do
+
+  let count++
+  echo -n "Downloading attachment $attachment..."
+  webget "http://church.cims.nyu.edu/bugs/attachment.cgi?id=$attachment" "test/regress/regress0/bug$bugid"
+
+done
+
+if [ $count -eq 0 ]; then
+  echo "There are no bug testcase attachments for bug #$bugid."
+else
+  echo "Downloaded $count bug testcases for bug #$bugid."
+fi
+
+done
index 50527e51a7de54fbdcb9cd33d083e536be3e4ed8..ed12c447eccca72eb1bf59d2edce6db9845d8edd 100644 (file)
@@ -128,7 +128,8 @@ BUG_TESTS = \
        bug339.smt2 \
        bug365.smt2 \
        bug382.smt2 \
-       bug383.smt2
+       bug383.smt2 \
+       bug398.smt2
 
 TESTS =        $(SMT_TESTS) $(SMT2_TESTS) $(CVC_TESTS) $(TPTP_TESTS) $(BUG_TESTS)
 
diff --git a/test/regress/regress0/bug398.smt2 b/test/regress/regress0/bug398.smt2
new file mode 100644 (file)
index 0000000..0423d11
--- /dev/null
@@ -0,0 +1,3 @@
+% EXIT: 0
+(set-logic QF_LRA)
+(define-fun x () Real (+ 4 1))