Initial code release

17 files changed, 162 insertions, 0 deletions

diff --git a/examples/program_analysis/paper_demos/api1.after.txt b/examples/program_analysis/paper_demos/api1.after.txt
new file mode 100644
index 0000000..d4f6957
--- /dev/null
+++ b/examples/program_analysis/paper_demos/api1.after.txt
@@ -0,0 +1,14 @@
+#include <stdio.h>
+#include "cam.h"
+
+#define BUFFER_SIZE (1024 * 1024)
+char buffer[BUFFER_SIZE];
+
+void try_record_video() {
+    int result = cam_record_video(buffer, BUFFER_SIZE);
+    if (result == -4) {
+        printf("Could not record video.\n");
+    } else {
+        printf("Recording video worked!\n");
+    }
+}
diff --git a/examples/program_analysis/paper_demos/api1.before.txt b/examples/program_analysis/paper_demos/api1.before.txt
new file mode 100644
index 0000000..0703da3
--- /dev/null
+++ b/examples/program_analysis/paper_demos/api1.before.txt
@@ -0,0 +1,14 @@
+#include <stdio.h>
+#include "cam.h"
+
+#define BUFFER_SIZE (1024 * 1024)
+char buffer[BUFFER_SIZE];
+
+void try_record_video() {
+    int result = cam_record_video(buffer, BUFFER_SIZE, RES_AUTO);
+    if (result == -1) {
+        printf("Could not record video.\n");
+    } else {
+        printf("Recording video worked!\n");
+    }
+}
diff --git a/examples/program_analysis/paper_demos/api2.after.txt b/examples/program_analysis/paper_demos/api2.after.txt
new file mode 100644
index 0000000..340e681
--- /dev/null
+++ b/examples/program_analysis/paper_demos/api2.after.txt
@@ -0,0 +1,14 @@
+#include <stdio.h>
+#include "cam.h"
+
+#define BUFFER_SIZE (1024 * 1024)
+char buffer[BUFFER_SIZE];
+
+void try_record_audio() {
+    int result = cam_record_audio(buffer, BUFFER_SIZE);
+    if (result == -2) {
+        printf("Could not record audio.\n");
+    } else {
+        printf("Recorded audio!\n");
+    }
+}
diff --git a/examples/program_analysis/paper_demos/api2.before.txt b/examples/program_analysis/paper_demos/api2.before.txt
new file mode 100644
index 0000000..f74c538
--- /dev/null
+++ b/examples/program_analysis/paper_demos/api2.before.txt
@@ -0,0 +1,14 @@
+#include <stdio.h>
+#include "cam.h"
+
+#define BUFFER_SIZE (1024 * 1024)
+char buffer[BUFFER_SIZE];
+
+void try_record_audio() {
+    int result = cam_record_audio(buffer, BUFFER_SIZE, RES_AUTO);
+    if (result == -5) {
+        printf("Could not record audio.\n");
+    } else {
+        printf("Recorded audio!\n");
+    }
+}
diff --git a/examples/program_analysis/paper_demos/api3.after.txt b/examples/program_analysis/paper_demos/api3.after.txt
new file mode 100644
index 0000000..e69de29
--- /dev/null
+++ b/examples/program_analysis/paper_demos/api3.after.txt
diff --git a/examples/program_analysis/paper_demos/api3.before.txt b/examples/program_analysis/paper_demos/api3.before.txt
new file mode 100644
index 0000000..cb8d731
--- /dev/null
+++ b/examples/program_analysis/paper_demos/api3.before.txt
@@ -0,0 +1,14 @@
+#include <stdio.h>
+#include "cam.h"
+
+#define BUFFER_SIZE (1024)
+char buffer[BUFFER_SIZE];
+
+void try_record_still() {
+    int result = cam_record_frame(buffer, BUFFER_SIZE, RES_AUTO);
+    if (result == -3) {
+        printf("Could not record audio.\n");
+    } else {
+        printf("Recorded audio!\n");
+    }
+}
diff --git a/examples/program_analysis/paper_demos/bash.txt b/examples/program_analysis/paper_demos/bash.txt
new file mode 100644
index 0000000..083401c
--- /dev/null
+++ b/examples/program_analysis/paper_demos/bash.txt
@@ -0,0 +1,17 @@
+int cd_builtin (list) WORD_LIST *list; /*@\color{red}{//B1} @*/
+{
+  char *dirname, *cdpath, *path, *temp;
+...
+
+struct builtin static_shell_builtins[] = {
+...
+  { "cd", cd_builtin, ... }, /*@\color{red}{//B2} @*/
+...
+struct builtin *shell_builtins = static_shell_builtins; /*@\color{red}{//B3} @*/
+
+struct builtin * builtin_address_internal
+    (name, disabled_okay)
+    char *name; int disabled_okay; { /*@\color{red}{//B4} @*/
+...
+      j = shell_builtins[mid].name[0] - name[0];
+...
diff --git a/examples/program_analysis/paper_demos/docs.after.txt b/examples/program_analysis/paper_demos/docs.after.txt
new file mode 100644
index 0000000..e162420
--- /dev/null
+++ b/examples/program_analysis/paper_demos/docs.after.txt
@@ -0,0 +1,9 @@
+# CameraLib v2.0
+### `cam_record_video(buffer, buffer_size)`
+Records video from the main camera into `buffer` until `buffer_size` bytes are reached. On error returns -4.
+
+### `cam_record_audio(buffer, buffer_size)`
+Uses the main camera's microphone to record audio into `buffer` until `buffer_size` bytes have been recorded. On error returns -2.
+
+### `cam_record_frame(buffer, buffer_size)`
+Uses the main camera to record a single image to `buffer`. Automatically sets the resolution to fit in `buffer_size`. On failure returns -6.
diff --git a/examples/program_analysis/paper_demos/docs.before.txt b/examples/program_analysis/paper_demos/docs.before.txt
new file mode 100644
index 0000000..1f10feb
--- /dev/null
+++ b/examples/program_analysis/paper_demos/docs.before.txt
@@ -0,0 +1,9 @@
+# CameraLib v1.0
+### `cam_record_video(buffer, buffer_size, resolution)`
+Records video from the main camera into `buffer` until `buffer_size` bytes are reached. On error returns -1.
+
+### `cam_record_audio(buffer, buffer_size, resolution)`
+Uses the main camera's microphone to record audio into `buffer` until `buffer_size` bytes have been recorded. On error returns -5.
+
+### `cam_record_frame(buffer, buffer_size, resolution)`
+Uses the main camera to record a single image to `buffer`. Automatically sets the resolution to fit in `buffer_size`. On failure returns -3.
diff --git a/examples/program_analysis/paper_demos/fish.txt b/examples/program_analysis/paper_demos/fish.txt
new file mode 100644
index 0000000..2b933f0
--- /dev/null
+++ b/examples/program_analysis/paper_demos/fish.txt
@@ -0,0 +1,13 @@
+int builtin_cd(parser_t &parser, io_streams_t &streams, wchar_t **argv) { /*@\color{red}{//F1} @*/
+    const wchar_t *cmd = argv[0];
+    int argc = builtin_count_args(argv);
+...
+
+static const builtin_data_t builtin_datas[] = {
+...
+    {L"cd", &builtin_cd, ...}, /*@\color{red}{//F2} @*/
+...
+
+static const builtin_data_t *builtin_lookup(const wcstring &name) { /*@\color{red}{//F3} @*/
+    const builtin_data_t *array_end = builtin_datas + BUILTIN_COUNT;
+...
diff --git a/examples/program_analysis/paper_demos/gemm1.after.txt b/examples/program_analysis/paper_demos/gemm1.after.txt
new file mode 100644
index 0000000..5d49a4c
--- /dev/null
+++ b/examples/program_analysis/paper_demos/gemm1.after.txt
@@ -0,0 +1,6 @@
+assert(k > 0);
+int outer = k * 100;
+int inner = k * 10;
+read_mat(outer, inner, &A);
+read_mat(inner, outer, &B);
+gemm_skinny(A, B, &C, outer, inner, outer);
diff --git a/examples/program_analysis/paper_demos/gemm1.before.txt b/examples/program_analysis/paper_demos/gemm1.before.txt
new file mode 100644
index 0000000..5ff9d2b
--- /dev/null
+++ b/examples/program_analysis/paper_demos/gemm1.before.txt
@@ -0,0 +1,6 @@
+assert(k > 0);
+int outer = k * 100;
+int inner = k * 10;
+read_mat(outer, inner, &A);
+read_mat(inner, outer, &B);
+gemm_large(A, B, &C, outer, inner, outer);
diff --git a/examples/program_analysis/paper_demos/gemm2.after.txt b/examples/program_analysis/paper_demos/gemm2.after.txt
new file mode 100644
index 0000000..19bb8aa
--- /dev/null
+++ b/examples/program_analysis/paper_demos/gemm2.after.txt
@@ -0,0 +1,10 @@
+assert(k > 1);
+int outer = k, A_cols = k / 2;
+read_mat(outer, A_cols, &A);
+read_mat(A_cols, outer, &B);
+while (!done(A, B)) {
+    read_row(&A);
+    read_col(&B);
+    outer++;
+}
+gemm_skinny(A, B, &C, outer, A_cols, outer);
diff --git a/examples/program_analysis/paper_demos/gemm2.before.txt b/examples/program_analysis/paper_demos/gemm2.before.txt
new file mode 100644
index 0000000..6e0ab1c
--- /dev/null
+++ b/examples/program_analysis/paper_demos/gemm2.before.txt
@@ -0,0 +1,10 @@
+assert(k > 1);
+int outer = k, A_cols = k / 2;
+read_mat(outer, A_cols, &A);
+read_mat(A_cols, outer, &B);
+while (!done(A, B)) {
+    read_row(&A);
+    read_col(&B);
+    outer++;
+}
+gemm_large(A, B, &C, outer, A_cols, outer);
diff --git a/examples/program_analysis/paper_demos/gemm3.after.txt b/examples/program_analysis/paper_demos/gemm3.after.txt
new file mode 100644
index 0000000..e69de29
--- /dev/null
+++ b/examples/program_analysis/paper_demos/gemm3.after.txt
diff --git a/examples/program_analysis/paper_demos/gemm3.before.txt b/examples/program_analysis/paper_demos/gemm3.before.txt
new file mode 100644
index 0000000..3cd1072
--- /dev/null
+++ b/examples/program_analysis/paper_demos/gemm3.before.txt
@@ -0,0 +1,6 @@
+assert(k > 5);
+int AB_rowcol = k;
+int inner = k * k;
+read_mat(AB_rowcol, inner, &A);
+read_mat(inner, AB_rowcol, &B);
+gemm_large(A, B, &C, AB_rowcol, inner, AB_rowcol);
diff --git a/examples/program_analysis/paper_demos/gemm4.bad.txt b/examples/program_analysis/paper_demos/gemm4.bad.txt
new file mode 100644
index 0000000..a57dc33
--- /dev/null
+++ b/examples/program_analysis/paper_demos/gemm4.bad.txt
@@ -0,0 +1,6 @@
+assert(k > 0);
+int outer = k * 10;
+int inner = k * 10;
+read_mat(outer, inner, &A);
+read_mat(inner, outer, &B);
+gemm_large(A, B, &C);