TESTS: add tests for gcc-like attributes

Author: sipma

chc/app/CGlobalDeclarations.py

@@ -767,7 +767,8 @@ def f(n: ET.Element, r: IndexedTableValue) -> None:
                 continue
             if len(self.varinfo_storage_classes[vid]) > 1:
                 chklogger.logger.warning(
-                    "Multiple storage classes for variable %d", vid)
+                    "Multiple storage classes for variable %d: %s",
+                    vid, ", ".join(self.varinfo_storage_classes[vid]))
                 continue
             else:
                 storageclass = list(self.varinfo_storage_classes[vid])[0]

chc/cmdline/c_file/cfileutil.py

@@ -358,6 +358,7 @@ def cfile_run_file(args: argparse.Namespace) -> NoReturn:
     copen: bool = args.open
     jsonoutput: bool = args.json
     outputfile: Optional[str] = args.output
+    verbose: bool = args.verbose
     loglevel: str = args.loglevel
     logfilename: Optional[str] = args.logfilename
     logfilemode: str = args.logfilemode
@@ -451,7 +452,7 @@ def cfile_run_file(args: argparse.Namespace) -> NoReturn:
     capp.initialize_single_file(cfilename)
     cfile = capp.get_cfile()
 
-    am = AnalysisManager(capp)
+    am = AnalysisManager(capp, verbose=verbose)
 
     am.create_file_primary_proofobligations(cfilename)
     am.reset_tables(cfile)

chc/cmdline/chkc

@@ -749,6 +749,9 @@ def parse() -> argparse.Namespace:
     cfilerun.add_argument(
         "--output", "-o",
         help="name of outputfile (without extension)")
+    cfilerun.add_argument(
+        "--verbose", "-v",
+        action="store_true")
     cfilerun.add_argument(
         "--loglevel", "-log",
         choices=UL.LogLevel.options(),

tests/attributes/test_access.c

@@ -0,0 +1,33 @@
+/* test access attribute */
+
+void f_no_attr(int *p, int len);
+
+/* the access attribute specifies that the first argument must be able to
+   be read, with a minimum size specified by the second argument. */
+void f_attr(int *p, int len)  __attribute__((__access__ (read_only, 1, 2)));
+
+
+void test_no_attr() {
+  int buffer[12];
+
+  f_no_attr(buffer, 12);
+  f_no_attr(buffer, 20);
+}
+
+
+/* should show violation for the second call */
+void test_attr() {
+  int buffer[12];
+
+  f_attr(buffer, 12);
+  f_attr(buffer, 20);
+}
+
+
+int main(int argc, char **argv) {
+
+  test_no_attr();
+  test_attr();
+
+  return 0;
+}

tests/attributes/test_gvar_inequality.c

@@ -0,0 +1,45 @@
+/* tests the inequality attributes for global variables:
+   - chkc_le
+   - chkc_lt
+   - chkc_ge
+   - chkc_gt
+
+   These attributes can be used to enforce a global bounds on the value
+   of a global variable; they will generate proof obligations and can be
+   used in the discharge of other proof obligations.
+*/
+
+#define BUFSIZE 12
+
+int g_no_attr;
+
+int g_attr
+__attribute__ ((__chkc_lt__ (BUFSIZE))) __attribute__ ((__chkc_ge__ (0)));
+
+int buffer[BUFSIZE];
+
+
+void test_no_attr() {
+
+  buffer[g_no_attr] = 0;
+}
+
+
+/* attributes are used to discharge the index-lower and index-upper-bound
+   proof obligations. */
+void test_attr() {
+
+  buffer[g_attr] = 0;
+}
+
+
+int main(int argc, char **argv) {
+
+  g_no_attr = 10;
+  g_attr = 10;
+
+  test_no_attr();
+  test_attr();
+
+  return 0;
+}

tests/attributes/test_gvar_nonnull.c

@@ -0,0 +1,28 @@
+/* test of the chkc_not_null attribute on the value of a global variable */
+
+extern int *g_no_attr;
+
+extern int *g_attr __attribute__ ((__chkc_not_null__));
+
+void f(int *p) __attribute__ ((__nonnull__ (1)));
+
+
+void test_no_attr() {
+
+  f(g_no_attr);
+}
+
+
+void test_attr() {
+
+  f(g_attr);
+}
+
+
+int main(int argc, char **argv) {
+
+  test_no_attr();
+  test_attr();
+
+  return 0;
+}

tests/attributes/test_malloc.c

@@ -0,0 +1,51 @@
+/* test_malloc attribute
+
+   The malloc attribute allows discharge of the allocation-base proof
+   obligation for free.
+
+   Note: this test should show the discharge of the no-overlap requirement
+   for memcpy. It does not do so yet.
+*/
+
+void *f_no_attr(int len);
+
+void *f_attr(int len) __attribute__ ((__malloc__));
+
+void *memcpy(void *dst, const void *src, int len);
+
+
+void test_no_attr() {
+
+  char *p = (char *) f_no_attr(10);
+  char *q = (char *) f_no_attr(10);
+
+  if (p && q) {
+    memcpy(q, p, 10);
+  }
+
+  free(p);
+  free(q);
+}
+
+
+void test_attr() {
+
+  char *p = (char *) f_attr(10);
+  char *q = (char *) f_attr(10);
+
+  if (p && q) {
+    memcpy(q, p, 10);
+  }
+
+  free(p);
+  free(q);
+}
+
+
+int main(int argc, char **argv) {
+
+  test_no_attr();
+  test_attr();
+
+  return 0;
+}

tests/attributes/test_nonnull.c

@@ -0,0 +1,41 @@
+/* test attribute nonnull */
+
+void f_no_attr(int *p);
+
+void f_attr(int *p)  __attribute__ ((__nonnull__ (1)));
+
+void *malloc(int len);
+
+
+void test_no_attr() {
+  int buffer[12];
+
+  f_no_attr(buffer);
+
+  int *p = malloc(12);
+
+  f_no_attr(p);
+}
+
+
+/* Adds two proof obligation for not-null, one of which can be discharged
+   against the data type, the other one is open, because malloc may return
+   NULL. */
+void test_attr() {
+  int buffer[12];
+
+  f_attr(buffer);
+
+  int *p = malloc(12);
+
+  f_attr(p);
+}
+
+
+int main(int argc, char **argv) {
+
+  test_no_attr();
+  test_attr();
+
+  return 0;
+}

tests/attributes/test_preserves_all_memory.c

@@ -0,0 +1,34 @@
+/* test chkc_preserves_all_memory attribute
+
+   can be used to discharge proof obligations that memory has not been freed
+*/
+
+int f_no_attr(void *p);
+
+int f_attr(void *p) __attribute__ ((__chkc_preserves_all_memory__));
+
+void *malloc(int len);
+
+
+void test_no_attr() {
+
+  void *p = malloc(10);
+
+  f_no_attr(p);
+  f_no_attr(p);
+
+  return 0;
+}
+
+
+/* the valid-mem proof obligation is discharged based on the guarantee that
+   the first call to f_attr does not free p. */
+void test_attr() {
+
+  void *p = malloc(10);
+
+  f_attr(p);
+  f_attr(p);
+
+  return 0;
+}

tests/attributes/test_preserves_memory.c

@@ -0,0 +1,34 @@
+/* test chkc_preserves_memory attribute
+
+   can be used to discharge proof obligations that memory has not been freed
+
+   Note: does not yet work.
+*/
+
+int f_no_attr(void *p);
+
+int f_attr(void *p) __attribute__ ((__chkc_preserves_memory__ (1)));
+
+void *malloc(int len);
+
+
+void test_no_attr() {
+
+  void *p = malloc(10);
+
+  f_no_attr(p);
+  f_no_attr(p);
+
+  return 0;
+}
+
+
+void test_attr() {
+
+  void *p = malloc(10);
+
+  f_attr(p);
+  f_attr(p);
+
+  return 0;
+}