[tests] add tests for audit mode

tests/value/audit-in.json

+{
+  "sources": {
+    "tests/value/audit.c": "4574f9d5090319c57dab0c9cb81fda32",
+    "tests/value/audit_included.h": "6164442da331e54680e25ff2fe1ba74e"
+  },
+  "kernel": {
+    "warning-categories": {
+      "enabled": [
+        "*", "CERT", "CERT:EXP", "CERT:EXP:46", "CERT:MSC", "CERT:MSC:38",
+        "acsl-extension", "annot", "annot:missing-spec", "annot-error",
+        "audit", "check", "check:volatile", "cmdline", "ghost",
+        "ghost:bad-use", "inline", "linker",
+        "linker:drop-conflicting-unused", "parser",
+        "parser:conditional-feature", "pp", "pp:compilation-db", "typing",
+        "typing:implicit-conv-void-ptr",
+        "typing:implicit-function-declaration",
+        "typing:incompatible-pointer-types",
+        "typing:incompatible-types-call", "typing:inconsistent-specifier",
+        "typing:int-conversion", "typing:no-proto"
+      ],
+      "disabled": [
+        "CERT:EXP:10", "acsl-float-compare", "ghost:already-ghost",
+        "parser:decimal-float", "transient-block"
+      ]
+    }
+  },
+  "eva": {
+    "correctness-parameters": {
+      "-absolute-valid-range": "",
+      "-eva-all-rounding-modes-constants": "false",
+      "-eva-alloc-returns-null": "true",
+      "-eva-builtin": "",
+      "-eva-builtins-auto": "true",
+      "-eva-context-depth": "2",
+      "-eva-context-valid-pointers": "false",
+      "-eva-context-width": "2",
+      "-eva-ignore-recursive-calls": "false",
+      "-eva-initialization-padding-globals": "yes",
+      "-eva-initialized-locals": "false",
+      "-eva-new-initial-state": "0",
+      "-eva-reduce-on-logic-alarms": "false",
+      "-eva-undefined-pointer-comparison-propagate-all": "false",
+      "-eva-use-spec": "",
+      "-eva-warn-copy-indeterminate": "",
+      "-eva-warn-pointer-subtraction": "true",
+      "-eva-warn-signed-converted-downcast": "false",
+      "-eva-warn-undefined-pointer-comparison": "pointer",
+      "-initialized-padding-locals": "true",
+      "-lib-entry": "false",
+      "-main": "main",
+      "-safe-arrays": "true",
+      "-unspecified-access": "false",
+      "-warn-invalid-bool": "true",
+      "-warn-invalid-pointer": "false",
+      "-warn-left-shift-negative": "true",
+      "-warn-pointer-downcast": "true",
+      "-warn-right-shift-negative": "false",
+      "-warn-signed-downcast": "false",
+      "-warn-signed-overflow": "true",
+      "-warn-special-float": "non-finite",
+      "-warn-unsigned-downcast": "false",
+      "-warn-unsigned-overflow": "false"
+    },
+    "warning-categories": {
+      "enabled": [
+        "*", "alarm", "builtins", "builtins:missing-spec",
+        "builtins:override", "experimental", "libc", "libc:unsupported-spec",
+        "locals-escaping", "malloc", "malloc:imprecise", "signed-overflow"
+      ],
+      "disabled": [
+        "garbled-mix", "invalid-assigns", "loop-unroll", "malloc:weak",
+        "missing-loop-unroll", "missing-loop-unroll:for"
+      ]
+    }
+  }
+}
\ No newline at end of file

tests/value/audit.c

+/* run.config
+   LOG: audit-out.json
+   STDOPT: #"-audit-check @PTEST_DIR@/audit-in.json -audit-prepare @PTEST_DIR@/result/audit-out.json"
+*/
+
+#include "audit_included.h"
+
+void main() {
+  float f = 2.1; // to trigger a syntactic warning
+}

tests/value/audit_included.h

+// This file is included by audit.i

tests/value/oracle/audit-out.json

+{
+  "eva": {
+    "correctness-parameters": {
+      "-absolute-valid-range": "",
+      "-eva-all-rounding-modes-constants": "false",
+      "-eva-alloc-returns-null": "true",
+      "-eva-builtin": "",
+      "-eva-builtins-auto": "true",
+      "-eva-context-depth": "2",
+      "-eva-context-valid-pointers": "false",
+      "-eva-context-width": "2",
+      "-eva-ignore-recursive-calls": "false",
+      "-eva-initialization-padding-globals": "yes",
+      "-eva-initialized-locals": "false",
+      "-eva-new-initial-state": "0",
+      "-eva-reduce-on-logic-alarms": "false",
+      "-eva-undefined-pointer-comparison-propagate-all": "false",
+      "-eva-use-spec": "",
+      "-eva-warn-copy-indeterminate": "",
+      "-eva-warn-pointer-subtraction": "true",
+      "-eva-warn-signed-converted-downcast": "false",
+      "-eva-warn-undefined-pointer-comparison": "pointer",
+      "-initialized-padding-locals": "true",
+      "-lib-entry": "false",
+      "-main": "main",
+      "-safe-arrays": "true",
+      "-unspecified-access": "false",
+      "-warn-invalid-bool": "true",
+      "-warn-invalid-pointer": "false",
+      "-warn-left-shift-negative": "true",
+      "-warn-pointer-downcast": "true",
+      "-warn-right-shift-negative": "false",
+      "-warn-signed-downcast": "false",
+      "-warn-signed-overflow": "true",
+      "-warn-special-float": "non-finite",
+      "-warn-unsigned-downcast": "false",
+      "-warn-unsigned-overflow": "false"
+    },
+    "warning-categories": {
+      "enabled": [
+        "*", "alarm", "builtins", "builtins:missing-spec",
+        "builtins:override", "experimental", "libc", "libc:unsupported-spec",
+        "locals-escaping", "malloc", "malloc:imprecise", "signed-overflow"
+      ],
+      "disabled": [
+        "garbled-mix", "invalid-assigns", "loop-unroll", "malloc:weak",
+        "missing-loop-unroll", "missing-loop-unroll:for"
+      ]
+    }
+  },
+  "kernel": {
+    "warning-categories": {
+      "enabled": [
+        "*", "CERT", "CERT:EXP", "CERT:EXP:46", "CERT:MSC", "CERT:MSC:38",
+        "acsl-extension", "annot", "annot:missing-spec", "annot:multi-from",
+        "annot-error", "audit", "check", "check:volatile", "cmdline",
+        "ghost", "ghost:bad-use", "inline", "linker",
+        "linker:drop-conflicting-unused", "parser",
+        "parser:conditional-feature", "pp", "pp:compilation-db", "typing",
+        "typing:implicit-conv-void-ptr",
+        "typing:implicit-function-declaration",
+        "typing:incompatible-pointer-types",
+        "typing:incompatible-types-call", "typing:inconsistent-specifier",
+        "typing:int-conversion", "typing:no-proto"
+      ],
+      "disabled": [
+        "CERT:EXP:10", "acsl-float-compare", "ghost:already-ghost",
+        "parser:decimal-float", "transient-block"
+      ]
+    }
+  },
+  "sources": {
+    "tests/value/audit.c": "d91c35d6c3eb02ede2ca2bdf92fda63d",
+    "tests/value/audit_included.h": "6164442da331e54680e25ff2fe1ba74e"
+  }
+}

tests/value/oracle/audit.res.oracle

+[kernel:audit] Warning: 
+  different hashes for tests/value/audit.c: got d91c35d6c3eb02ede2ca2bdf92fda63d, expected 4574f9d5090319c57dab0c9cb81fda32
+[kernel] Audit: sources list written to: tests/value/result/audit-out.json
+[kernel] Parsing tests/value/audit.c (with preprocessing)
+[kernel:parser:decimal-float] tests/value/audit.c:9: Warning: 
+  Floating-point constant 2.1 is not represented exactly. Will use 0x1.0cccccccccccdp1.
+  (warn-once: no further messages from category 'parser:decimal-float' will be emitted)
+[eva] Analyzing a complete application starting at main
+[eva] Computing initial state
+[eva] Initial state computed
+[eva:initial-state] Values of globals at initialization
+  
+[eva] Recording results for main
+[eva] done for function main
+[eva] ====== VALUES COMPUTED ======
+[eva:final-states] Values at end of function main:
+  f ∈ {2.09999990463}
+[from] Computing for function main
+[from] Done for function main
+[from] ====== DEPENDENCIES COMPUTED ======
+  These dependencies hold at termination for the executions that terminate:
+[from] Function main:
+  NO EFFECTS
+[from] ====== END OF DEPENDENCIES ======
+[inout] Out (internal) for function main:
+    f
+[inout] Inputs for function main:
+    \nothing
+[kernel] Wrote: tests/value/result/audit-out.json