Ajout du banc de tests de CCured (Olden benchmark suite, cf.

CCured: type-safe retrofitting of legacy code, G.Necula et al.)

rapportCompcert_all.txt liste les erreurs produites par ccomp.



git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@121 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

1 files changed, 19 insertions, 0 deletions

diff --git a/test/ccured_olden/bh/normalize.pl b/test/ccured_olden/bh/normalize.pl
new file mode 100755
index 00000000..102d372f
--- /dev/null
+++ b/test/ccured_olden/bh/normalize.pl
@@ -0,0 +1,19 @@
+#!/usr/bin/perl -w
+# strip wallclock times from output so we can compare
+
+while ($line = <STDIN>) {
+  # I don't know if it's a problem, but we seem to get some difference
+  # about whether the 0's are positive or negative.. so let's change
+  # all occurrances of "-0.0000" to simply " 0.0000"
+  $line =~ s/-0\.0000/ 0.0000/g;
+
+  ($firstSix) = ($line =~ /^(\s+\S+\s+\S+\s+\S+\s+\S+\s+\S+\s+\S+)\s+\S+$/);
+  if ($firstSix) {
+    # only output the first 6 columns
+    print ("$firstSix\n");
+  }
+  else {
+    # no match; print whole line
+    print ($line);
+  }
+}