From 231552ece5df843aebd8d8c501fd510db4d916c3 Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.maroneze@cea.fr>
Date: Tue, 17 Nov 2020 18:59:24 +0100
Subject: [PATCH] [tests] add tests for audit mode
---
tests/value/audit-in.json | 76 +++++++++++++++++++++++++++++
tests/value/audit.c | 10 ++++
tests/value/audit_included.h | 1 +
tests/value/oracle/audit-out.json | 76 +++++++++++++++++++++++++++++
tests/value/oracle/audit.res.oracle | 29 +++++++++++
5 files changed, 192 insertions(+)
create mode 100644 tests/value/audit-in.json
create mode 100644 tests/value/audit.c
create mode 100644 tests/value/audit_included.h
create mode 100644 tests/value/oracle/audit-out.json
create mode 100644 tests/value/oracle/audit.res.oracle
diff --git a/tests/value/audit-in.json b/tests/value/audit-in.json
new file mode 100644
index 00000000000..fc5e7af0541
--- /dev/null
+++ b/tests/value/audit-in.json
@@ -0,0 +1,76 @@
+{
+ "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
diff --git a/tests/value/audit.c b/tests/value/audit.c
new file mode 100644
index 00000000000..952edfab1ee
--- /dev/null
+++ b/tests/value/audit.c
@@ -0,0 +1,10 @@
+/* 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
+}
diff --git a/tests/value/audit_included.h b/tests/value/audit_included.h
new file mode 100644
index 00000000000..0db378b820a
--- /dev/null
+++ b/tests/value/audit_included.h
@@ -0,0 +1 @@
+// This file is included by audit.i
diff --git a/tests/value/oracle/audit-out.json b/tests/value/oracle/audit-out.json
new file mode 100644
index 00000000000..e12d53d0b0e
--- /dev/null
+++ b/tests/value/oracle/audit-out.json
@@ -0,0 +1,76 @@
+{
+ "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"
+ }
+}
diff --git a/tests/value/oracle/audit.res.oracle b/tests/value/oracle/audit.res.oracle
new file mode 100644
index 00000000000..c599da1fc5f
--- /dev/null
+++ b/tests/value/oracle/audit.res.oracle
@@ -0,0 +1,29 @@
+[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
--
GitLab