diff options
Diffstat (limited to 'test')
-rw-r--r-- | test/monniaux/profiling/compcert_profiling.dat | bin | 0 -> 96 bytes | |||
-rwxr-xr-x | test/monniaux/profiling/test_profiling | bin | 0 -> 14144 bytes | |||
-rw-r--r-- | test/monniaux/profiling/test_profiling.c | 15 |
3 files changed, 15 insertions, 0 deletions
diff --git a/test/monniaux/profiling/compcert_profiling.dat b/test/monniaux/profiling/compcert_profiling.dat Binary files differnew file mode 100644 index 00000000..fa57a995 --- /dev/null +++ b/test/monniaux/profiling/compcert_profiling.dat diff --git a/test/monniaux/profiling/test_profiling b/test/monniaux/profiling/test_profiling Binary files differnew file mode 100755 index 00000000..b530aae2 --- /dev/null +++ b/test/monniaux/profiling/test_profiling diff --git a/test/monniaux/profiling/test_profiling.c b/test/monniaux/profiling/test_profiling.c new file mode 100644 index 00000000..013b1d68 --- /dev/null +++ b/test/monniaux/profiling/test_profiling.c @@ -0,0 +1,15 @@ +#include <stdlib.h> +#include <stdio.h> + +int main(int argc, char **argv) { + if (argc < 2) return 1; + int i = atoi(argv[1]); + if (i > 0) { + printf("positive\n"); + } else if (i==0) { + printf("zero\n"); + } else { + printf("negative\n"); + } + return 0; +} |