Changes between Version 5 and Version 6 of C Interface

Timestamp:

02/15/10 13:41:24 (16 years ago)

Author:

Stephen Siegel

Comment:

--

C Interface

@@ -33 +33 @@
 == Abstract Functions ==
 
+== Example ==
+Here is a program that adds the elements in a file.  The commandline argument is the filename.   Inputs are the filename, the contents of the file, and the parameter B which is an upper bound on the number of elements that will be read.  Output is to stdout.
+
+How do we annotate this file in such a way that it does not interfere with compilation, but provides all the information we need to build a TASS model?
+
+
+{{{
+#include<stdio.h>
+#include<assert.h>
+/*@ _TASS_input {B>0} */
+#define B 3
+
+double sum = 0.0;
+
+/* arguments to main are inputs */
+int main(int argc, char* argv[]) {
+  char *filename;
+  double result = 0.0;
+  FILE *fp;
+  double tmp;
+  int i = 0;
+
+  if (argc != 2) {
+    printf("Usage: realadder filename\
+");
+    fflush(stdout);
+    return 1;
+  }
+  filename = argv[1];
+  fp = fopen(filename, "r");
+  assert(fp);
+  while (1) {
+    /*@ _TASS_corresponds spec@label */
+    int more = fscanf(fp, "%lf", &tmp);
+
+    /*@ _TASS_assume(tmp>=0.0) */
+    if (more == EOF) break;
+    i++;
+    if (i>B) {
+      printf("Too many numbers!  Limit is %d.\
+", B);
+      fflush(stdout);
+      return 2;
+    }
+    sum += tmp;
+  }
+  printf("The sum is %lf\
+", sum);
+  fclose(fp);
+  return 0;
+}
+}}}
+
+Idea: the result of fscanf can be represented as a symbolic function.  In other words, add functions:
+{{{
+_TASS_read_int(string filename, int position)
+_TASS_read_real(string filename, int position)
+}}}
+Or something like that.
+
+
+
+Questions:
+* do we need to add char (and string?) datatypes to TASS?
+