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, 32 insertions, 0 deletions

diff --git a/test/ccured_olden/tsp/tsp.h b/test/ccured_olden/tsp/tsp.h
new file mode 100644
index 00000000..8d928891
--- /dev/null
+++ b/test/ccured_olden/tsp/tsp.h
@@ -0,0 +1,32 @@
+typedef struct tree {
+  int sz;
+  double x,y;
+  struct tree *left, *right;
+  /*struct tree *next, *prev;*/
+  struct tree *next /*{95}*/, *prev /*{95}*/;
+} *Tree;
+
+/* Builds a 2D tree of n nodes in specified range with dir as primary 
+   axis (0 for x, 1 for y) */
+Tree build_tree(int n,int dir,int lo,int num_proc,double min_x,
+                double max_x,double min_y,double max_y);
+/* Compute TSP for the tree t -- use conquer for problems <= sz */
+Tree tsp(Tree t, int sz, int nproc);
+
+#ifdef PLAIN
+#include <time.h>
+#define local
+#define mymalloc malloc
+#define CMMD_node_timer_clear(x)  (void)0
+#define TIMESTART(clk) {clk=(double)clock();}
+#define TIMESTOP(clk) {clk=1000000.0 * ((double)clock()-(clk))/CLOCKS_PER_SEC;}
+extern double wallclock;
+#define timer_start(x) TIMESTART(wallclock)
+#define timer_stop(x) TIMESTOP(wallclock)
+#define timer_elapsed(x) (wallclock / 1000.0)
+#define chatting printf
+#define NOTEST() (void)0
+#define RETEST() (void)0
+#define LOCAL(x) x
+#define mymalloc malloc
+#endif