diff --git a/src/plugins/e-acsl/Makefile.in b/src/plugins/e-acsl/Makefile.in
index cc38e19deb76fdce64b98022f26caca66c3329cb..cb5b3025bc2e633804e4a8128d6d40509d4a899e 100644
--- a/src/plugins/e-acsl/Makefile.in
+++ b/src/plugins/e-acsl/Makefile.in
@@ -183,8 +183,8 @@ PLUGIN_TESTS_DIRS := \
runtime \
bts \
gmp \
- no-main \
full-mmodel \
+ segment-only \
temporal \
special
@@ -203,6 +203,15 @@ E_ACSL_DEFAULT_TESTS: \
$(EACSL_PLUGIN_DIR)/tests/print.cmxs \
$(EACSL_PLUGIN_DIR)/tests/print.cmo
+$(EACSL_PLUGIN_DIR)/tests/test_config: \
+ $(EACSL_PLUGIN_DIR)/tests/test_config.in \
+ $(EACSL_PLUGIN_DIR)/Makefile
+ $(PRINT_MAKING) $@
+ $(SED) -e "s|@SEDCMD@|`which sed `|g" $< > $@
+
+tests:: $(EACSL_PLUGIN_DIR)/tests/ptests_config \
+ $(EACSL_PLUGIN_DIR)/tests/print.cmxs
+
clean::
for d in $(E_ACSL_EXTRA_DIRS); do \
$(RM) $$d/*~; \
@@ -284,7 +293,8 @@ EACSL_DOC_FILES = \
man/e-acsl-gcc.sh.1
EACSL_TEST_FILES = \
- tests/test_config.in tests/print.ml
+ tests/test_config.in \
+ tests/print.ml
# Test files without header management
EACSL_DISTRIB_TESTS = \
@@ -485,19 +495,6 @@ uninstall::
$(PRINT_RM) E-ACSL man pages
$(RM) $(MANDIR)/man1/e-acsl-gcc.sh.1
-####################
-# Testing (part 2) #
-####################
-
-ifeq (@MAY_RUN_TESTS@,yes)
-
-$(E_ACSL_DIR)/tests/test_config: $(E_ACSL_DIR)/tests/test_config.in \
- $(E_ACSL_DIR)/Makefile
- $(PRINT_MAKING) $@
- $(SED) -e "s|@SEDCMD@|`which sed `|g" $< > $@
-
-endif
-
#####################################
# Regenerating the Makefile on need #
#####################################
diff --git a/src/plugins/e-acsl/tests/bts/test_config b/src/plugins/e-acsl/tests/bts/test_config
deleted file mode 100644
index 1fb42e2f9122687547c8d809923862b7e1f27918..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/bts/test_config
+++ /dev/null
@@ -1,3 +0,0 @@
-LOG: gen_@PTEST_NAME@.c
-OPT: -variadic-no-translation -machdep gcc_x86_64 -check -e-acsl -then-last -load-script tests/print.cmxs -print -ocode tests/bts/result/gen_@PTEST_NAME@.c -kernel-verbose 0 -eva -eva-verbose 0
-EXEC: ./scripts/testrun.sh @PTEST_NAME@ bts "" "--frama-c=@frama-c@"
diff --git a/src/plugins/e-acsl/tests/builtin/test_config b/src/plugins/e-acsl/tests/builtin/test_config
index f20809dc6ea46914cb9ae5b1cca8160b6f1ebca5..5978357b4e5bba0940ff12302fdcd61c6d85eced 100644
--- a/src/plugins/e-acsl/tests/builtin/test_config
+++ b/src/plugins/e-acsl/tests/builtin/test_config
@@ -1,4 +1 @@
-LOG: gen_@PTEST_NAME@.c
-EXECNOW: gcc -c -I@PTEST_DIR@ -o @PTEST_DIR@/signalled.o @PTEST_DIR@/signalled.c
-OPT: -variadic-no-translation -kernel-warn-key CERT:MSC:38=inactive -machdep gcc_x86_64 -check -e-acsl -e-acsl-full-mmodel -e-acsl-replace-libc-functions -then-last -load-script tests/print.cmxs -print -ocode tests/builtin/result/gen_@PTEST_NAME@.c -kernel-verbose 0 -eva @EVA_OPTIONS@
-EXEC: ./scripts/testrun.sh @PTEST_NAME@ builtin "1" "--frama-c=@frama-c@ --full-mmodel --frama-c-extra -kernel-warn-key=CERT:MSC:38=inactive --libc-replacements --ld-flags @PTEST_DIR@/signalled.o"
+STDOPT: #"-e-acsl-replace-libc-functions"
diff --git a/src/plugins/e-acsl/tests/format/oracle/fprintf.res.oracle b/src/plugins/e-acsl/tests/format/oracle/fprintf.res.oracle
index e0fb28f138a99d5b723a372f59bf6e58f4b0bed1..891fe89fa286044fcb57f3b80561928b5756a9eb 100644
--- a/src/plugins/e-acsl/tests/format/oracle/fprintf.res.oracle
+++ b/src/plugins/e-acsl/tests/format/oracle/fprintf.res.oracle
@@ -15,6 +15,18 @@
[e-acsl] Warning: annotating undefined function `waitpid':
the generated program may miss memory instrumentation
if there are memory-related annotations.
+[kernel:annot:missing-spec] FRAMAC_SHARE/libc/stdio.h:165: Warning:
+ Neither code nor specification for function fprintf, generating default assigns from the prototype
+[kernel:annot:missing-spec] FRAMAC_SHARE/libc/stdio.h:169: Warning:
+ Neither code nor specification for function printf, generating default assigns from the prototype
+[kernel:annot:missing-spec] FRAMAC_SHARE/libc/stdio.h:171: Warning:
+ Neither code nor specification for function snprintf, generating default assigns from the prototype
+[kernel:annot:missing-spec] FRAMAC_SHARE/libc/stdio.h:173: Warning:
+ Neither code nor specification for function sprintf, generating default assigns from the prototype
+[kernel:annot:missing-spec] FRAMAC_SHARE/libc/stdio.h:369: Warning:
+ Neither code nor specification for function dprintf, generating default assigns from the prototype
+[kernel:annot:missing-spec] tests/format/fprintf.c:15: Warning:
+ Neither code nor specification for function fork, generating default assigns from the prototype
[e-acsl] FRAMAC_SHARE/libc/sys/wait.h:92: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
@@ -35,89 +47,38 @@
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
[e-acsl] translation done in project "e-acsl".
-[eva] Analyzing a complete application starting at main
-[eva] Computing initial state
-[eva] Initial state computed
-[eva:initial-state] Values of globals at initialization
- __e_acsl_init ∈ [--..--]
- __e_acsl_heap_allocation_size ∈ [--..--]
- __e_acsl_math_HUGE_VAL ∈ [-1.79769313486e+308 .. 1.79769313486e+308]
- __e_acsl_math_HUGE_VALF ∈ [-3.40282346639e+38 .. 3.40282346639e+38]
- __e_acsl_math_INFINITY ∈ [-1.79769313486e+308 .. 1.79769313486e+308]
- testno ∈ {0}
- __e_acsl_sound_verdict ∈ [--..--]
- __gen_e_acsl_literal_string ∈ {0}
- __gen_e_acsl_literal_string_2 ∈ {0}
- __gen_e_acsl_literal_string_3 ∈ {0}
- __gen_e_acsl_literal_string_4 ∈ {0}
- __gen_e_acsl_literal_string_5 ∈ {0}
- __gen_e_acsl_literal_string_6 ∈ {0}
- __gen_e_acsl_literal_string_7 ∈ {0}
- __gen_e_acsl_literal_string_8 ∈ {0}
- __gen_e_acsl_literal_string_9 ∈ {0}
- __gen_e_acsl_literal_string_10 ∈ {0}
- __gen_e_acsl_literal_string_11 ∈ {0}
- __gen_e_acsl_literal_string_12 ∈ {0}
- __gen_e_acsl_literal_string_13 ∈ {0}
- __gen_e_acsl_literal_string_14 ∈ {0}
- __gen_e_acsl_literal_string_15 ∈ {0}
- __gen_e_acsl_literal_string_16 ∈ {0}
- __gen_e_acsl_literal_string_17 ∈ {0}
- __gen_e_acsl_literal_string_18 ∈ {0}
- __gen_e_acsl_literal_string_19 ∈ {0}
- __gen_e_acsl_literal_string_20 ∈ {0}
- __gen_e_acsl_literal_string_21 ∈ {0}
- __gen_e_acsl_literal_string_22 ∈ {0}
- __gen_e_acsl_literal_string_23 ∈ {0}
- __gen_e_acsl_literal_string_24 ∈ {0}
- __gen_e_acsl_literal_string_25 ∈ {0}
- __gen_e_acsl_literal_string_26 ∈ {0}
- __gen_e_acsl_literal_string_27 ∈ {0}
- __gen_e_acsl_literal_string_28 ∈ {0}
- __gen_e_acsl_literal_string_29 ∈ {0}
- __gen_e_acsl_literal_string_30 ∈ {0}
- __gen_e_acsl_literal_string_31 ∈ {0}
-[eva] using specification for function __e_acsl_memory_init
-[eva] using specification for function __e_acsl_store_block
-[eva] using specification for function __e_acsl_full_init
-[eva] using specification for function __e_acsl_mark_readonly
-[eva] using specification for function fork
-[eva] using specification for function __e_acsl_builtin_fprintf
-[eva] using specification for function exit
-[eva] using specification for function __e_acsl_valid
-[eva] using specification for function __e_acsl_assert
-[eva] using specification for function waitpid
-[eva] using specification for function __e_acsl_initialized
+[kernel:annot:missing-spec] tests/format/fprintf.c:15: Warning:
+ Neither code nor specification for function __e_acsl_builtin_fprintf, generating default assigns from the prototype
[eva:alarm] FRAMAC_SHARE/libc/sys/wait.h:86: Warning:
function __e_acsl_assert: precondition got status unknown.
-[eva] using specification for function __e_acsl_delete_block
[eva:alarm] FRAMAC_SHARE/libc/sys/wait.h:86: Warning:
function __gen_e_acsl_waitpid: postcondition 'initialization,stat_loc_init_on_success' got status unknown.
[eva:alarm] tests/format/fprintf.c:15: Warning:
accessing uninitialized left-value. assert \initialized(&process_status);
-[eva] using specification for function __e_acsl_builtin_printf
+[kernel:annot:missing-spec] tests/format/signalled.h:12: Warning:
+ Neither code nor specification for function __e_acsl_builtin_printf, generating default assigns from the prototype
[eva:invalid-assigns] tests/format/fprintf.c:16:
Completely invalid destination for assigns clause *stream. Ignoring.
[eva:alarm] tests/format/fprintf.c:16: Warning:
accessing uninitialized left-value. assert \initialized(&process_status_0);
-[eva] using specification for function tmpfile
[eva:alarm] tests/format/fprintf.c:19: Warning:
accessing uninitialized left-value. assert \initialized(&process_status_1);
[eva:alarm] FRAMAC_SHARE/libc/stdio.h:94: Warning:
function __e_acsl_assert: precondition got status unknown.
-[eva] using specification for function fclose
[eva:alarm] tests/format/fprintf.c:21: Warning:
accessing uninitialized left-value. assert \initialized(&process_status_2);
[eva:invalid-assigns] tests/format/fprintf.c:22:
Completely invalid destination for assigns clause *stream. Ignoring.
[eva:alarm] tests/format/fprintf.c:22: Warning:
accessing uninitialized left-value. assert \initialized(&process_status_3);
-[eva] using specification for function __e_acsl_builtin_dprintf
+[kernel:annot:missing-spec] tests/format/fprintf.c:27: Warning:
+ Neither code nor specification for function __e_acsl_builtin_dprintf, generating default assigns from the prototype
[eva:alarm] tests/format/fprintf.c:27: Warning:
accessing uninitialized left-value. assert \initialized(&process_status_4);
[eva:alarm] tests/format/fprintf.c:28: Warning:
accessing uninitialized left-value. assert \initialized(&process_status_5);
-[eva] using specification for function __e_acsl_builtin_sprintf
+[kernel:annot:missing-spec] tests/format/fprintf.c:34: Warning:
+ Neither code nor specification for function __e_acsl_builtin_sprintf, generating default assigns from the prototype
[eva:alarm] tests/format/fprintf.c:34: Warning:
accessing uninitialized left-value. assert \initialized(&process_status_6);
[eva:alarm] tests/format/fprintf.c:35: Warning:
@@ -132,7 +93,8 @@
Completely invalid destination for assigns clause *(str + (0 ..)). Ignoring.
[eva:alarm] tests/format/fprintf.c:38: Warning:
accessing uninitialized left-value. assert \initialized(&process_status_10);
-[eva] using specification for function __e_acsl_builtin_snprintf
+[kernel:annot:missing-spec] tests/format/fprintf.c:41: Warning:
+ Neither code nor specification for function __e_acsl_builtin_snprintf, generating default assigns from the prototype
[eva:alarm] tests/format/fprintf.c:41: Warning:
accessing uninitialized left-value. assert \initialized(&process_status_11);
[eva:alarm] tests/format/fprintf.c:42: Warning:
@@ -151,5 +113,3 @@
Completely invalid destination for assigns clause *(str + (0 ..)). Ignoring.
[eva:alarm] tests/format/fprintf.c:46: Warning:
accessing uninitialized left-value. assert \initialized(&process_status_16);
-[eva] using specification for function __e_acsl_memory_clean
-[eva] done for function main
diff --git a/src/plugins/e-acsl/tests/format/oracle/gen_fprintf.c b/src/plugins/e-acsl/tests/format/oracle/gen_fprintf.c
index ec1141bf7af25720a0042f5ed437931880fe2641..1803d4e9f5eeb5593b30d3878f0241caf3fa9766 100644
--- a/src/plugins/e-acsl/tests/format/oracle/gen_fprintf.c
+++ b/src/plugins/e-acsl/tests/format/oracle/gen_fprintf.c
@@ -4,7 +4,6 @@
#include "stdlib.h"
#include "sys/time.h"
#include "sys/wait.h"
-char *__gen_e_acsl_literal_string_31;
char *__gen_e_acsl_literal_string_30;
char *__gen_e_acsl_literal_string_29;
char *__gen_e_acsl_literal_string_28;
@@ -13,28 +12,28 @@ char *__gen_e_acsl_literal_string_26;
char *__gen_e_acsl_literal_string_25;
char *__gen_e_acsl_literal_string_24;
char *__gen_e_acsl_literal_string_23;
-char *__gen_e_acsl_literal_string_21;
-char *__gen_e_acsl_literal_string_19;
-char *__gen_e_acsl_literal_string_16;
+char *__gen_e_acsl_literal_string_22;
+char *__gen_e_acsl_literal_string_20;
+char *__gen_e_acsl_literal_string_18;
char *__gen_e_acsl_literal_string_15;
char *__gen_e_acsl_literal_string_14;
char *__gen_e_acsl_literal_string_13;
char *__gen_e_acsl_literal_string_12;
-char *__gen_e_acsl_literal_string_9;
+char *__gen_e_acsl_literal_string_11;
char *__gen_e_acsl_literal_string_8;
-char *__gen_e_acsl_literal_string_10;
char *__gen_e_acsl_literal_string_7;
-char *__gen_e_acsl_literal_string_11;
+char *__gen_e_acsl_literal_string_9;
+char *__gen_e_acsl_literal_string_6;
+char *__gen_e_acsl_literal_string_10;
char *__gen_e_acsl_literal_string;
char *__gen_e_acsl_literal_string_2;
char *__gen_e_acsl_literal_string_3;
-char *__gen_e_acsl_literal_string_6;
char *__gen_e_acsl_literal_string_5;
char *__gen_e_acsl_literal_string_4;
-char *__gen_e_acsl_literal_string_22;
-char *__gen_e_acsl_literal_string_20;
-char *__gen_e_acsl_literal_string_18;
+char *__gen_e_acsl_literal_string_21;
+char *__gen_e_acsl_literal_string_19;
char *__gen_e_acsl_literal_string_17;
+char *__gen_e_acsl_literal_string_16;
extern int __e_acsl_sound_verdict;
/*@ assigns \result;
@@ -46,111 +45,111 @@ void __e_acsl_globals_init(void)
static char __e_acsl_already_run = 0;
if (! __e_acsl_already_run) {
__e_acsl_already_run = 1;
- __gen_e_acsl_literal_string_31 = "tests/format/fprintf.c:46";
- __e_acsl_store_block((void *)__gen_e_acsl_literal_string_31,
- sizeof("tests/format/fprintf.c:46"));
- __e_acsl_full_init((void *)__gen_e_acsl_literal_string_31);
- __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_31);
- __gen_e_acsl_literal_string_30 = "tests/format/fprintf.c:45";
+ __gen_e_acsl_literal_string_30 = "tests/format/fprintf.c:46";
__e_acsl_store_block((void *)__gen_e_acsl_literal_string_30,
- sizeof("tests/format/fprintf.c:45"));
+ sizeof("tests/format/fprintf.c:46"));
__e_acsl_full_init((void *)__gen_e_acsl_literal_string_30);
__e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_30);
- __gen_e_acsl_literal_string_29 = "tests/format/fprintf.c:44";
+ __gen_e_acsl_literal_string_29 = "tests/format/fprintf.c:45";
__e_acsl_store_block((void *)__gen_e_acsl_literal_string_29,
- sizeof("tests/format/fprintf.c:44"));
+ sizeof("tests/format/fprintf.c:45"));
__e_acsl_full_init((void *)__gen_e_acsl_literal_string_29);
__e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_29);
- __gen_e_acsl_literal_string_28 = "tests/format/fprintf.c:43";
+ __gen_e_acsl_literal_string_28 = "tests/format/fprintf.c:44";
__e_acsl_store_block((void *)__gen_e_acsl_literal_string_28,
- sizeof("tests/format/fprintf.c:43"));
+ sizeof("tests/format/fprintf.c:44"));
__e_acsl_full_init((void *)__gen_e_acsl_literal_string_28);
__e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_28);
- __gen_e_acsl_literal_string_27 = "tests/format/fprintf.c:42";
+ __gen_e_acsl_literal_string_27 = "tests/format/fprintf.c:43";
__e_acsl_store_block((void *)__gen_e_acsl_literal_string_27,
- sizeof("tests/format/fprintf.c:42"));
+ sizeof("tests/format/fprintf.c:43"));
__e_acsl_full_init((void *)__gen_e_acsl_literal_string_27);
__e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_27);
- __gen_e_acsl_literal_string_26 = "tests/format/fprintf.c:41";
+ __gen_e_acsl_literal_string_26 = "tests/format/fprintf.c:42";
__e_acsl_store_block((void *)__gen_e_acsl_literal_string_26,
- sizeof("tests/format/fprintf.c:41"));
+ sizeof("tests/format/fprintf.c:42"));
__e_acsl_full_init((void *)__gen_e_acsl_literal_string_26);
__e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_26);
- __gen_e_acsl_literal_string_25 = "tests/format/fprintf.c:38";
+ __gen_e_acsl_literal_string_25 = "tests/format/fprintf.c:41";
__e_acsl_store_block((void *)__gen_e_acsl_literal_string_25,
- sizeof("tests/format/fprintf.c:38"));
+ sizeof("tests/format/fprintf.c:41"));
__e_acsl_full_init((void *)__gen_e_acsl_literal_string_25);
__e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_25);
- __gen_e_acsl_literal_string_24 = "tests/format/fprintf.c:37";
+ __gen_e_acsl_literal_string_24 = "tests/format/fprintf.c:38";
__e_acsl_store_block((void *)__gen_e_acsl_literal_string_24,
- sizeof("tests/format/fprintf.c:37"));
+ sizeof("tests/format/fprintf.c:38"));
__e_acsl_full_init((void *)__gen_e_acsl_literal_string_24);
__e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_24);
- __gen_e_acsl_literal_string_23 = "tests/format/fprintf.c:36";
+ __gen_e_acsl_literal_string_23 = "tests/format/fprintf.c:37";
__e_acsl_store_block((void *)__gen_e_acsl_literal_string_23,
- sizeof("tests/format/fprintf.c:36"));
+ sizeof("tests/format/fprintf.c:37"));
__e_acsl_full_init((void *)__gen_e_acsl_literal_string_23);
__e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_23);
- __gen_e_acsl_literal_string_21 = "tests/format/fprintf.c:35";
- __e_acsl_store_block((void *)__gen_e_acsl_literal_string_21,
+ __gen_e_acsl_literal_string_22 = "tests/format/fprintf.c:36";
+ __e_acsl_store_block((void *)__gen_e_acsl_literal_string_22,
+ sizeof("tests/format/fprintf.c:36"));
+ __e_acsl_full_init((void *)__gen_e_acsl_literal_string_22);
+ __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_22);
+ __gen_e_acsl_literal_string_20 = "tests/format/fprintf.c:35";
+ __e_acsl_store_block((void *)__gen_e_acsl_literal_string_20,
sizeof("tests/format/fprintf.c:35"));
- __e_acsl_full_init((void *)__gen_e_acsl_literal_string_21);
- __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_21);
- __gen_e_acsl_literal_string_19 = "tests/format/fprintf.c:34";
- __e_acsl_store_block((void *)__gen_e_acsl_literal_string_19,
+ __e_acsl_full_init((void *)__gen_e_acsl_literal_string_20);
+ __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_20);
+ __gen_e_acsl_literal_string_18 = "tests/format/fprintf.c:34";
+ __e_acsl_store_block((void *)__gen_e_acsl_literal_string_18,
sizeof("tests/format/fprintf.c:34"));
- __e_acsl_full_init((void *)__gen_e_acsl_literal_string_19);
- __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_19);
- __gen_e_acsl_literal_string_16 = "tests/format/fprintf.c:28";
- __e_acsl_store_block((void *)__gen_e_acsl_literal_string_16,
- sizeof("tests/format/fprintf.c:28"));
- __e_acsl_full_init((void *)__gen_e_acsl_literal_string_16);
- __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_16);
- __gen_e_acsl_literal_string_15 = "tests/format/fprintf.c:27";
+ __e_acsl_full_init((void *)__gen_e_acsl_literal_string_18);
+ __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_18);
+ __gen_e_acsl_literal_string_15 = "tests/format/fprintf.c:28";
__e_acsl_store_block((void *)__gen_e_acsl_literal_string_15,
- sizeof("tests/format/fprintf.c:27"));
+ sizeof("tests/format/fprintf.c:28"));
__e_acsl_full_init((void *)__gen_e_acsl_literal_string_15);
__e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_15);
- __gen_e_acsl_literal_string_14 = "tests/format/fprintf.c:22";
+ __gen_e_acsl_literal_string_14 = "tests/format/fprintf.c:27";
__e_acsl_store_block((void *)__gen_e_acsl_literal_string_14,
- sizeof("tests/format/fprintf.c:22"));
+ sizeof("tests/format/fprintf.c:27"));
__e_acsl_full_init((void *)__gen_e_acsl_literal_string_14);
__e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_14);
- __gen_e_acsl_literal_string_13 = "tests/format/fprintf.c:21";
+ __gen_e_acsl_literal_string_13 = "tests/format/fprintf.c:22";
__e_acsl_store_block((void *)__gen_e_acsl_literal_string_13,
- sizeof("tests/format/fprintf.c:21"));
+ sizeof("tests/format/fprintf.c:22"));
__e_acsl_full_init((void *)__gen_e_acsl_literal_string_13);
__e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_13);
- __gen_e_acsl_literal_string_12 = "tests/format/fprintf.c:19";
+ __gen_e_acsl_literal_string_12 = "tests/format/fprintf.c:21";
__e_acsl_store_block((void *)__gen_e_acsl_literal_string_12,
- sizeof("tests/format/fprintf.c:19"));
+ sizeof("tests/format/fprintf.c:21"));
__e_acsl_full_init((void *)__gen_e_acsl_literal_string_12);
__e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_12);
- __gen_e_acsl_literal_string_9 = "tests/format/fprintf.c:16";
- __e_acsl_store_block((void *)__gen_e_acsl_literal_string_9,
- sizeof("tests/format/fprintf.c:16"));
- __e_acsl_full_init((void *)__gen_e_acsl_literal_string_9);
- __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_9);
- __gen_e_acsl_literal_string_8 = "tests/format/fprintf.c:15";
+ __gen_e_acsl_literal_string_11 = "tests/format/fprintf.c:19";
+ __e_acsl_store_block((void *)__gen_e_acsl_literal_string_11,
+ sizeof("tests/format/fprintf.c:19"));
+ __e_acsl_full_init((void *)__gen_e_acsl_literal_string_11);
+ __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_11);
+ __gen_e_acsl_literal_string_8 = "tests/format/fprintf.c:16";
__e_acsl_store_block((void *)__gen_e_acsl_literal_string_8,
- sizeof("tests/format/fprintf.c:15"));
+ sizeof("tests/format/fprintf.c:16"));
__e_acsl_full_init((void *)__gen_e_acsl_literal_string_8);
__e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_8);
- __gen_e_acsl_literal_string_10 = "foobar %s\n";
- __e_acsl_store_block((void *)__gen_e_acsl_literal_string_10,
- sizeof("foobar %s\n"));
- __e_acsl_full_init((void *)__gen_e_acsl_literal_string_10);
- __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_10);
- __gen_e_acsl_literal_string_7 = "foobar\n";
+ __gen_e_acsl_literal_string_7 = "tests/format/fprintf.c:15";
__e_acsl_store_block((void *)__gen_e_acsl_literal_string_7,
- sizeof("foobar\n"));
+ sizeof("tests/format/fprintf.c:15"));
__e_acsl_full_init((void *)__gen_e_acsl_literal_string_7);
__e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_7);
- __gen_e_acsl_literal_string_11 = "foobar";
- __e_acsl_store_block((void *)__gen_e_acsl_literal_string_11,
+ __gen_e_acsl_literal_string_9 = "foobar %s\n";
+ __e_acsl_store_block((void *)__gen_e_acsl_literal_string_9,
+ sizeof("foobar %s\n"));
+ __e_acsl_full_init((void *)__gen_e_acsl_literal_string_9);
+ __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_9);
+ __gen_e_acsl_literal_string_6 = "foobar\n";
+ __e_acsl_store_block((void *)__gen_e_acsl_literal_string_6,
+ sizeof("foobar\n"));
+ __e_acsl_full_init((void *)__gen_e_acsl_literal_string_6);
+ __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_6);
+ __gen_e_acsl_literal_string_10 = "foobar";
+ __e_acsl_store_block((void *)__gen_e_acsl_literal_string_10,
sizeof("foobar"));
- __e_acsl_full_init((void *)__gen_e_acsl_literal_string_11);
- __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_11);
+ __e_acsl_full_init((void *)__gen_e_acsl_literal_string_10);
+ __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_10);
__gen_e_acsl_literal_string = "TEST %d: ";
__e_acsl_store_block((void *)__gen_e_acsl_literal_string,
sizeof("TEST %d: "));
@@ -166,11 +165,6 @@ void __e_acsl_globals_init(void)
sizeof("OK: Expected execution at %s\n"));
__e_acsl_full_init((void *)__gen_e_acsl_literal_string_3);
__e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_3);
- __gen_e_acsl_literal_string_6 = "Hello world!";
- __e_acsl_store_block((void *)__gen_e_acsl_literal_string_6,
- sizeof("Hello world!"));
- __e_acsl_full_init((void *)__gen_e_acsl_literal_string_6);
- __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_6);
__gen_e_acsl_literal_string_5 = "FAIL: Unexpected signal at %s\n";
__e_acsl_store_block((void *)__gen_e_acsl_literal_string_5,
sizeof("FAIL: Unexpected signal at %s\n"));
@@ -181,56 +175,24 @@ void __e_acsl_globals_init(void)
sizeof("FAIL: Unexpected execution at %s\n"));
__e_acsl_full_init((void *)__gen_e_acsl_literal_string_4);
__e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_4);
- __gen_e_acsl_literal_string_22 = "123";
- __e_acsl_store_block((void *)__gen_e_acsl_literal_string_22,
+ __gen_e_acsl_literal_string_21 = "123";
+ __e_acsl_store_block((void *)__gen_e_acsl_literal_string_21,
sizeof("123"));
- __e_acsl_full_init((void *)__gen_e_acsl_literal_string_22);
- __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_22);
- __gen_e_acsl_literal_string_20 = "12";
- __e_acsl_store_block((void *)__gen_e_acsl_literal_string_20,sizeof("12"));
- __e_acsl_full_init((void *)__gen_e_acsl_literal_string_20);
- __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_20);
- __gen_e_acsl_literal_string_18 = "1";
- __e_acsl_store_block((void *)__gen_e_acsl_literal_string_18,sizeof("1"));
- __e_acsl_full_init((void *)__gen_e_acsl_literal_string_18);
- __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_18);
- __gen_e_acsl_literal_string_17 = "-%s-";
- __e_acsl_store_block((void *)__gen_e_acsl_literal_string_17,
- sizeof("-%s-"));
+ __e_acsl_full_init((void *)__gen_e_acsl_literal_string_21);
+ __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_21);
+ __gen_e_acsl_literal_string_19 = "12";
+ __e_acsl_store_block((void *)__gen_e_acsl_literal_string_19,sizeof("12"));
+ __e_acsl_full_init((void *)__gen_e_acsl_literal_string_19);
+ __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_19);
+ __gen_e_acsl_literal_string_17 = "1";
+ __e_acsl_store_block((void *)__gen_e_acsl_literal_string_17,sizeof("1"));
__e_acsl_full_init((void *)__gen_e_acsl_literal_string_17);
__e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_17);
- __e_acsl_store_block((void *)(& __gen_e_acsl_waitpid),(size_t)1);
- __e_acsl_full_init((void *)(& __gen_e_acsl_waitpid));
- __e_acsl_store_block((void *)(& __gen_e_acsl_fclose),(size_t)1);
- __e_acsl_full_init((void *)(& __gen_e_acsl_fclose));
- __e_acsl_store_block((void *)(& __gen_e_acsl_tmpfile),(size_t)1);
- __e_acsl_full_init((void *)(& __gen_e_acsl_tmpfile));
- __e_acsl_store_block((void *)(& __gen_e_acsl_exit),(size_t)1);
- __e_acsl_full_init((void *)(& __gen_e_acsl_exit));
- __e_acsl_store_block((void *)(& signal_eval),(size_t)1);
- __e_acsl_full_init((void *)(& signal_eval));
- __e_acsl_store_block((void *)(& testno),(size_t)4);
- __e_acsl_full_init((void *)(& testno));
- __e_acsl_store_block((void *)(& __fc_time),(size_t)4);
- __e_acsl_full_init((void *)(& __fc_time));
- __e_acsl_store_block((void *)(& __fc_p_sigaction),(size_t)8);
- __e_acsl_full_init((void *)(& __fc_p_sigaction));
- __e_acsl_store_block((void *)(sigaction),(size_t)2080);
- __e_acsl_full_init((void *)(& sigaction));
- __e_acsl_store_block((void *)(& __fc_p_fopen),(size_t)8);
- __e_acsl_full_init((void *)(& __fc_p_fopen));
- __e_acsl_store_block((void *)(__fc_fopen),(size_t)128);
- __e_acsl_full_init((void *)(& __fc_fopen));
- __e_acsl_store_block((void *)(& stdout),(size_t)8);
- __e_acsl_full_init((void *)(& stdout));
- __e_acsl_store_block((void *)(& __fc_p_random48_counter),(size_t)8);
- __e_acsl_full_init((void *)(& __fc_p_random48_counter));
- __e_acsl_store_block((void *)(random48_counter),(size_t)6);
- __e_acsl_full_init((void *)(& random48_counter));
- __e_acsl_store_block((void *)(& __fc_random48_init),(size_t)4);
- __e_acsl_full_init((void *)(& __fc_random48_init));
- __e_acsl_store_block((void *)(& __fc_rand_max),(size_t)8);
- __e_acsl_full_init((void *)(& __fc_rand_max));
+ __gen_e_acsl_literal_string_16 = "-%s-";
+ __e_acsl_store_block((void *)__gen_e_acsl_literal_string_16,
+ sizeof("-%s-"));
+ __e_acsl_full_init((void *)__gen_e_acsl_literal_string_16);
+ __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_16);
}
return;
}
@@ -242,18 +204,11 @@ int main(int argc, char const **argv)
char buf[5];
__e_acsl_memory_init(& argc,(char ***)(& argv),(size_t)8);
__e_acsl_globals_init();
- __e_acsl_store_block((void *)(buf),(size_t)5);
- __e_acsl_store_block((void *)(template),(size_t)256);
- __e_acsl_store_block((void *)(& __retres),(size_t)4);
- char *pstr = (char *)__gen_e_acsl_literal_string_6;
- __e_acsl_store_block((void *)(& pstr),(size_t)8);
- __e_acsl_full_init((void *)(& pstr));
+ char *pstr = (char *)"Hello world!";
{
pid_t pid = fork();
- __e_acsl_store_block((void *)(& pid),(size_t)4);
- __e_acsl_full_init((void *)(& pid));
if (! pid) {
- __e_acsl_builtin_fprintf("",stdout,__gen_e_acsl_literal_string_7);
+ __e_acsl_builtin_fprintf("",stdout,__gen_e_acsl_literal_string_6);
__gen_e_acsl_exit(0);
}
else {
@@ -261,17 +216,14 @@ int main(int argc, char const **argv)
__e_acsl_store_block((void *)(& process_status),(size_t)4);
__gen_e_acsl_waitpid(pid,& process_status,0);
/*@ assert Eva: initialization: \initialized(&process_status); */
- signal_eval(process_status,0,__gen_e_acsl_literal_string_8);
+ signal_eval(process_status,0,__gen_e_acsl_literal_string_7);
__e_acsl_delete_block((void *)(& process_status));
}
- __e_acsl_delete_block((void *)(& pid));
}
{
pid_t pid_0 = fork();
- __e_acsl_store_block((void *)(& pid_0),(size_t)4);
- __e_acsl_full_init((void *)(& pid_0));
if (! pid_0) {
- __e_acsl_builtin_fprintf("",(FILE *)0,__gen_e_acsl_literal_string_7);
+ __e_acsl_builtin_fprintf("",(FILE *)0,__gen_e_acsl_literal_string_6);
__gen_e_acsl_exit(0);
}
else {
@@ -279,10 +231,9 @@ int main(int argc, char const **argv)
__e_acsl_store_block((void *)(& process_status_0),(size_t)4);
__gen_e_acsl_waitpid(pid_0,& process_status_0,0);
/*@ assert Eva: initialization: \initialized(&process_status_0); */
- signal_eval(process_status_0,1,__gen_e_acsl_literal_string_9);
+ signal_eval(process_status_0,1,__gen_e_acsl_literal_string_8);
__e_acsl_delete_block((void *)(& process_status_0));
}
- __e_acsl_delete_block((void *)(& pid_0));
}
FILE *fh = __gen_e_acsl_tmpfile();
__e_acsl_store_block((void *)(& fh),(size_t)8);
@@ -290,11 +241,9 @@ int main(int argc, char const **argv)
if (fh) {
{
pid_t pid_1 = fork();
- __e_acsl_store_block((void *)(& pid_1),(size_t)4);
- __e_acsl_full_init((void *)(& pid_1));
if (! pid_1) {
- __e_acsl_builtin_fprintf("s",fh,__gen_e_acsl_literal_string_10,
- __gen_e_acsl_literal_string_11);
+ __e_acsl_builtin_fprintf("s",fh,__gen_e_acsl_literal_string_9,
+ __gen_e_acsl_literal_string_10);
__gen_e_acsl_exit(0);
}
else {
@@ -302,19 +251,16 @@ int main(int argc, char const **argv)
__e_acsl_store_block((void *)(& process_status_1),(size_t)4);
__gen_e_acsl_waitpid(pid_1,& process_status_1,0);
/*@ assert Eva: initialization: \initialized(&process_status_1); */
- signal_eval(process_status_1,0,__gen_e_acsl_literal_string_12);
+ signal_eval(process_status_1,0,__gen_e_acsl_literal_string_11);
__e_acsl_delete_block((void *)(& process_status_1));
}
- __e_acsl_delete_block((void *)(& pid_1));
}
__gen_e_acsl_fclose(fh);
{
pid_t pid_2 = fork();
- __e_acsl_store_block((void *)(& pid_2),(size_t)4);
- __e_acsl_full_init((void *)(& pid_2));
if (! pid_2) {
- __e_acsl_builtin_fprintf("s",fh,__gen_e_acsl_literal_string_10,
- __gen_e_acsl_literal_string_11);
+ __e_acsl_builtin_fprintf("s",fh,__gen_e_acsl_literal_string_9,
+ __gen_e_acsl_literal_string_10);
__gen_e_acsl_exit(0);
}
else {
@@ -322,19 +268,16 @@ int main(int argc, char const **argv)
__e_acsl_store_block((void *)(& process_status_2),(size_t)4);
__gen_e_acsl_waitpid(pid_2,& process_status_2,0);
/*@ assert Eva: initialization: \initialized(&process_status_2); */
- signal_eval(process_status_2,1,__gen_e_acsl_literal_string_13);
+ signal_eval(process_status_2,1,__gen_e_acsl_literal_string_12);
__e_acsl_delete_block((void *)(& process_status_2));
}
- __e_acsl_delete_block((void *)(& pid_2));
}
{
pid_t pid_3 = fork();
- __e_acsl_store_block((void *)(& pid_3),(size_t)4);
- __e_acsl_full_init((void *)(& pid_3));
if (! pid_3) {
__e_acsl_builtin_fprintf("s",(FILE *)(& argc),
- __gen_e_acsl_literal_string_10,
- __gen_e_acsl_literal_string_11);
+ __gen_e_acsl_literal_string_9,
+ __gen_e_acsl_literal_string_10);
__gen_e_acsl_exit(0);
}
else {
@@ -342,18 +285,15 @@ int main(int argc, char const **argv)
__e_acsl_store_block((void *)(& process_status_3),(size_t)4);
__gen_e_acsl_waitpid(pid_3,& process_status_3,0);
/*@ assert Eva: initialization: \initialized(&process_status_3); */
- signal_eval(process_status_3,1,__gen_e_acsl_literal_string_14);
+ signal_eval(process_status_3,1,__gen_e_acsl_literal_string_13);
__e_acsl_delete_block((void *)(& process_status_3));
}
- __e_acsl_delete_block((void *)(& pid_3));
}
}
{
pid_t pid_4 = fork();
- __e_acsl_store_block((void *)(& pid_4),(size_t)4);
- __e_acsl_full_init((void *)(& pid_4));
if (! pid_4) {
- __e_acsl_builtin_dprintf("",1,__gen_e_acsl_literal_string_7);
+ __e_acsl_builtin_dprintf("",1,__gen_e_acsl_literal_string_6);
__gen_e_acsl_exit(0);
}
else {
@@ -361,17 +301,14 @@ int main(int argc, char const **argv)
__e_acsl_store_block((void *)(& process_status_4),(size_t)4);
__gen_e_acsl_waitpid(pid_4,& process_status_4,0);
/*@ assert Eva: initialization: \initialized(&process_status_4); */
- signal_eval(process_status_4,0,__gen_e_acsl_literal_string_15);
+ signal_eval(process_status_4,0,__gen_e_acsl_literal_string_14);
__e_acsl_delete_block((void *)(& process_status_4));
}
- __e_acsl_delete_block((void *)(& pid_4));
}
{
pid_t pid_5 = fork();
- __e_acsl_store_block((void *)(& pid_5),(size_t)4);
- __e_acsl_full_init((void *)(& pid_5));
if (! pid_5) {
- __e_acsl_builtin_dprintf("",3,__gen_e_acsl_literal_string_7);
+ __e_acsl_builtin_dprintf("",3,__gen_e_acsl_literal_string_6);
__gen_e_acsl_exit(0);
}
else {
@@ -379,18 +316,15 @@ int main(int argc, char const **argv)
__e_acsl_store_block((void *)(& process_status_5),(size_t)4);
__gen_e_acsl_waitpid(pid_5,& process_status_5,0);
/*@ assert Eva: initialization: \initialized(&process_status_5); */
- signal_eval(process_status_5,1,__gen_e_acsl_literal_string_16);
+ signal_eval(process_status_5,1,__gen_e_acsl_literal_string_15);
__e_acsl_delete_block((void *)(& process_status_5));
}
- __e_acsl_delete_block((void *)(& pid_5));
}
{
pid_t pid_6 = fork();
- __e_acsl_store_block((void *)(& pid_6),(size_t)4);
- __e_acsl_full_init((void *)(& pid_6));
if (! pid_6) {
- __e_acsl_builtin_sprintf("s",buf,__gen_e_acsl_literal_string_17,
- __gen_e_acsl_literal_string_18);
+ __e_acsl_builtin_sprintf("s",buf,__gen_e_acsl_literal_string_16,
+ __gen_e_acsl_literal_string_17);
__gen_e_acsl_exit(0);
}
else {
@@ -398,18 +332,15 @@ int main(int argc, char const **argv)
__e_acsl_store_block((void *)(& process_status_6),(size_t)4);
__gen_e_acsl_waitpid(pid_6,& process_status_6,0);
/*@ assert Eva: initialization: \initialized(&process_status_6); */
- signal_eval(process_status_6,0,__gen_e_acsl_literal_string_19);
+ signal_eval(process_status_6,0,__gen_e_acsl_literal_string_18);
__e_acsl_delete_block((void *)(& process_status_6));
}
- __e_acsl_delete_block((void *)(& pid_6));
}
{
pid_t pid_7 = fork();
- __e_acsl_store_block((void *)(& pid_7),(size_t)4);
- __e_acsl_full_init((void *)(& pid_7));
if (! pid_7) {
- __e_acsl_builtin_sprintf("s",buf,__gen_e_acsl_literal_string_17,
- __gen_e_acsl_literal_string_20);
+ __e_acsl_builtin_sprintf("s",buf,__gen_e_acsl_literal_string_16,
+ __gen_e_acsl_literal_string_19);
__gen_e_acsl_exit(0);
}
else {
@@ -417,18 +348,15 @@ int main(int argc, char const **argv)
__e_acsl_store_block((void *)(& process_status_7),(size_t)4);
__gen_e_acsl_waitpid(pid_7,& process_status_7,0);
/*@ assert Eva: initialization: \initialized(&process_status_7); */
- signal_eval(process_status_7,0,__gen_e_acsl_literal_string_21);
+ signal_eval(process_status_7,0,__gen_e_acsl_literal_string_20);
__e_acsl_delete_block((void *)(& process_status_7));
}
- __e_acsl_delete_block((void *)(& pid_7));
}
{
pid_t pid_8 = fork();
- __e_acsl_store_block((void *)(& pid_8),(size_t)4);
- __e_acsl_full_init((void *)(& pid_8));
if (! pid_8) {
- __e_acsl_builtin_sprintf("s",buf,__gen_e_acsl_literal_string_17,
- __gen_e_acsl_literal_string_22);
+ __e_acsl_builtin_sprintf("s",buf,__gen_e_acsl_literal_string_16,
+ __gen_e_acsl_literal_string_21);
__gen_e_acsl_exit(0);
}
else {
@@ -436,18 +364,15 @@ int main(int argc, char const **argv)
__e_acsl_store_block((void *)(& process_status_8),(size_t)4);
__gen_e_acsl_waitpid(pid_8,& process_status_8,0);
/*@ assert Eva: initialization: \initialized(&process_status_8); */
- signal_eval(process_status_8,1,__gen_e_acsl_literal_string_23);
+ signal_eval(process_status_8,1,__gen_e_acsl_literal_string_22);
__e_acsl_delete_block((void *)(& process_status_8));
}
- __e_acsl_delete_block((void *)(& pid_8));
}
{
pid_t pid_9 = fork();
- __e_acsl_store_block((void *)(& pid_9),(size_t)4);
- __e_acsl_full_init((void *)(& pid_9));
if (! pid_9) {
- __e_acsl_builtin_sprintf("s",(char *)0,__gen_e_acsl_literal_string_17,
- __gen_e_acsl_literal_string_22);
+ __e_acsl_builtin_sprintf("s",(char *)0,__gen_e_acsl_literal_string_16,
+ __gen_e_acsl_literal_string_21);
__gen_e_acsl_exit(0);
}
else {
@@ -455,18 +380,15 @@ int main(int argc, char const **argv)
__e_acsl_store_block((void *)(& process_status_9),(size_t)4);
__gen_e_acsl_waitpid(pid_9,& process_status_9,0);
/*@ assert Eva: initialization: \initialized(&process_status_9); */
- signal_eval(process_status_9,1,__gen_e_acsl_literal_string_24);
+ signal_eval(process_status_9,1,__gen_e_acsl_literal_string_23);
__e_acsl_delete_block((void *)(& process_status_9));
}
- __e_acsl_delete_block((void *)(& pid_9));
}
{
pid_t pid_10 = fork();
- __e_acsl_store_block((void *)(& pid_10),(size_t)4);
- __e_acsl_full_init((void *)(& pid_10));
if (! pid_10) {
- __e_acsl_builtin_sprintf("s",pstr,__gen_e_acsl_literal_string_17,
- __gen_e_acsl_literal_string_22);
+ __e_acsl_builtin_sprintf("s",pstr,__gen_e_acsl_literal_string_16,
+ __gen_e_acsl_literal_string_21);
__gen_e_acsl_exit(0);
}
else {
@@ -474,19 +396,16 @@ int main(int argc, char const **argv)
__e_acsl_store_block((void *)(& process_status_10),(size_t)4);
__gen_e_acsl_waitpid(pid_10,& process_status_10,0);
/*@ assert Eva: initialization: \initialized(&process_status_10); */
- signal_eval(process_status_10,1,__gen_e_acsl_literal_string_25);
+ signal_eval(process_status_10,1,__gen_e_acsl_literal_string_24);
__e_acsl_delete_block((void *)(& process_status_10));
}
- __e_acsl_delete_block((void *)(& pid_10));
}
{
pid_t pid_11 = fork();
- __e_acsl_store_block((void *)(& pid_11),(size_t)4);
- __e_acsl_full_init((void *)(& pid_11));
if (! pid_11) {
__e_acsl_builtin_snprintf("s",buf,(unsigned long)4,
- __gen_e_acsl_literal_string_17,
- __gen_e_acsl_literal_string_22);
+ __gen_e_acsl_literal_string_16,
+ __gen_e_acsl_literal_string_21);
__gen_e_acsl_exit(0);
}
else {
@@ -494,19 +413,16 @@ int main(int argc, char const **argv)
__e_acsl_store_block((void *)(& process_status_11),(size_t)4);
__gen_e_acsl_waitpid(pid_11,& process_status_11,0);
/*@ assert Eva: initialization: \initialized(&process_status_11); */
- signal_eval(process_status_11,0,__gen_e_acsl_literal_string_26);
+ signal_eval(process_status_11,0,__gen_e_acsl_literal_string_25);
__e_acsl_delete_block((void *)(& process_status_11));
}
- __e_acsl_delete_block((void *)(& pid_11));
}
{
pid_t pid_12 = fork();
- __e_acsl_store_block((void *)(& pid_12),(size_t)4);
- __e_acsl_full_init((void *)(& pid_12));
if (! pid_12) {
__e_acsl_builtin_snprintf("s",buf,(unsigned long)5,
- __gen_e_acsl_literal_string_17,
- __gen_e_acsl_literal_string_22);
+ __gen_e_acsl_literal_string_16,
+ __gen_e_acsl_literal_string_21);
__gen_e_acsl_exit(0);
}
else {
@@ -514,19 +430,16 @@ int main(int argc, char const **argv)
__e_acsl_store_block((void *)(& process_status_12),(size_t)4);
__gen_e_acsl_waitpid(pid_12,& process_status_12,0);
/*@ assert Eva: initialization: \initialized(&process_status_12); */
- signal_eval(process_status_12,0,__gen_e_acsl_literal_string_27);
+ signal_eval(process_status_12,0,__gen_e_acsl_literal_string_26);
__e_acsl_delete_block((void *)(& process_status_12));
}
- __e_acsl_delete_block((void *)(& pid_12));
}
{
pid_t pid_13 = fork();
- __e_acsl_store_block((void *)(& pid_13),(size_t)4);
- __e_acsl_full_init((void *)(& pid_13));
if (! pid_13) {
__e_acsl_builtin_snprintf("s",pstr,(unsigned long)6,
- __gen_e_acsl_literal_string_17,
- __gen_e_acsl_literal_string_22);
+ __gen_e_acsl_literal_string_16,
+ __gen_e_acsl_literal_string_21);
__gen_e_acsl_exit(0);
}
else {
@@ -534,19 +447,16 @@ int main(int argc, char const **argv)
__e_acsl_store_block((void *)(& process_status_13),(size_t)4);
__gen_e_acsl_waitpid(pid_13,& process_status_13,0);
/*@ assert Eva: initialization: \initialized(&process_status_13); */
- signal_eval(process_status_13,1,__gen_e_acsl_literal_string_28);
+ signal_eval(process_status_13,1,__gen_e_acsl_literal_string_27);
__e_acsl_delete_block((void *)(& process_status_13));
}
- __e_acsl_delete_block((void *)(& pid_13));
}
{
pid_t pid_14 = fork();
- __e_acsl_store_block((void *)(& pid_14),(size_t)4);
- __e_acsl_full_init((void *)(& pid_14));
if (! pid_14) {
__e_acsl_builtin_snprintf("s",buf,(unsigned long)6,
- __gen_e_acsl_literal_string_17,
- __gen_e_acsl_literal_string_22);
+ __gen_e_acsl_literal_string_16,
+ __gen_e_acsl_literal_string_21);
__gen_e_acsl_exit(0);
}
else {
@@ -554,19 +464,16 @@ int main(int argc, char const **argv)
__e_acsl_store_block((void *)(& process_status_14),(size_t)4);
__gen_e_acsl_waitpid(pid_14,& process_status_14,0);
/*@ assert Eva: initialization: \initialized(&process_status_14); */
- signal_eval(process_status_14,1,__gen_e_acsl_literal_string_29);
+ signal_eval(process_status_14,1,__gen_e_acsl_literal_string_28);
__e_acsl_delete_block((void *)(& process_status_14));
}
- __e_acsl_delete_block((void *)(& pid_14));
}
{
pid_t pid_15 = fork();
- __e_acsl_store_block((void *)(& pid_15),(size_t)4);
- __e_acsl_full_init((void *)(& pid_15));
if (! pid_15) {
__e_acsl_builtin_snprintf("s",(char *)0,(unsigned long)6,
- __gen_e_acsl_literal_string_17,
- __gen_e_acsl_literal_string_22);
+ __gen_e_acsl_literal_string_16,
+ __gen_e_acsl_literal_string_21);
__gen_e_acsl_exit(0);
}
else {
@@ -574,19 +481,16 @@ int main(int argc, char const **argv)
__e_acsl_store_block((void *)(& process_status_15),(size_t)4);
__gen_e_acsl_waitpid(pid_15,& process_status_15,0);
/*@ assert Eva: initialization: \initialized(&process_status_15); */
- signal_eval(process_status_15,1,__gen_e_acsl_literal_string_30);
+ signal_eval(process_status_15,1,__gen_e_acsl_literal_string_29);
__e_acsl_delete_block((void *)(& process_status_15));
}
- __e_acsl_delete_block((void *)(& pid_15));
}
{
pid_t pid_16 = fork();
- __e_acsl_store_block((void *)(& pid_16),(size_t)4);
- __e_acsl_full_init((void *)(& pid_16));
if (! pid_16) {
__e_acsl_builtin_snprintf("s",(char *)0,(unsigned long)0,
- __gen_e_acsl_literal_string_17,
- __gen_e_acsl_literal_string_22);
+ __gen_e_acsl_literal_string_16,
+ __gen_e_acsl_literal_string_21);
__gen_e_acsl_exit(0);
}
else {
@@ -594,32 +498,12 @@ int main(int argc, char const **argv)
__e_acsl_store_block((void *)(& process_status_16),(size_t)4);
__gen_e_acsl_waitpid(pid_16,& process_status_16,0);
/*@ assert Eva: initialization: \initialized(&process_status_16); */
- signal_eval(process_status_16,0,__gen_e_acsl_literal_string_31);
+ signal_eval(process_status_16,0,__gen_e_acsl_literal_string_30);
__e_acsl_delete_block((void *)(& process_status_16));
}
- __e_acsl_delete_block((void *)(& pid_16));
}
- __e_acsl_full_init((void *)(& __retres));
__retres = 0;
- __e_acsl_delete_block((void *)(& argv));
- __e_acsl_delete_block((void *)(& argc));
- __e_acsl_delete_block((void *)(& signal_eval));
- __e_acsl_delete_block((void *)(& testno));
- __e_acsl_delete_block((void *)(& __fc_time));
- __e_acsl_delete_block((void *)(& __fc_p_sigaction));
- __e_acsl_delete_block((void *)(sigaction));
- __e_acsl_delete_block((void *)(& __fc_p_fopen));
- __e_acsl_delete_block((void *)(__fc_fopen));
- __e_acsl_delete_block((void *)(& stdout));
- __e_acsl_delete_block((void *)(& __fc_p_random48_counter));
- __e_acsl_delete_block((void *)(random48_counter));
- __e_acsl_delete_block((void *)(& __fc_random48_init));
- __e_acsl_delete_block((void *)(& __fc_rand_max));
- __e_acsl_delete_block((void *)(buf));
__e_acsl_delete_block((void *)(& fh));
- __e_acsl_delete_block((void *)(template));
- __e_acsl_delete_block((void *)(& pstr));
- __e_acsl_delete_block((void *)(& __retres));
__e_acsl_memory_clean();
return __retres;
}
diff --git a/src/plugins/e-acsl/tests/format/test_config b/src/plugins/e-acsl/tests/format/test_config
index 221c07ca9537a337420266c26d9370fbc2a1d519..eeaea353f8aafc1309b0f8b93ac86c545a2dd08a 100644
--- a/src/plugins/e-acsl/tests/format/test_config
+++ b/src/plugins/e-acsl/tests/format/test_config
@@ -1,3 +1 @@
-LOG: gen_@PTEST_NAME@.c
-OPT: -variadic-no-translation -machdep gcc_x86_64 -check -e-acsl -e-acsl-full-mmodel -e-acsl-validate-format-strings -kernel-warn-key=annot:missing-spec=inactive -then-last -load-script tests/print.cmxs -print -ocode tests/format/result/gen_@PTEST_NAME@.c -kernel-verbose 0 -eva @EVA_OPTIONS@
-EXEC: ./scripts/testrun.sh @PTEST_NAME@ format "1" "--frama-c=@frama-c@ --full-mmodel --validate-format-strings"
+STDOPT: #"-e-acsl-validate-format-strings"
diff --git a/src/plugins/e-acsl/tests/full-mmodel-only/test_config b/src/plugins/e-acsl/tests/full-mmodel-only/test_config
deleted file mode 100644
index 4ce37cb7b762b2f63b7c1e8cb1034519edf40d43..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/full-mmodel-only/test_config
+++ /dev/null
@@ -1,3 +0,0 @@
-EXEC: ./scripts/testrun.sh @PTEST_NAME@ full-mmodel-only "1" "--frama-c=@frama-c@ --full-mmodel"
-LOG: gen_@PTEST_NAME@.c
-OPT: -machdep gcc_x86_64 -check -e-acsl -e-acsl-full-mmodel -then-last -load-script tests/print.cmxs -print -ocode tests/full-mmodel-only/result/gen_@PTEST_NAME@.c -kernel-verbose 0 -eva @EVA_OPTIONS@
diff --git a/src/plugins/e-acsl/tests/full-mmodel/oracle/addrOf.res.oracle b/src/plugins/e-acsl/tests/full-mmodel/oracle/addrOf.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..efd026311297e55d8fefb674326118e6ece88624
--- /dev/null
+++ b/src/plugins/e-acsl/tests/full-mmodel/oracle/addrOf.res.oracle
@@ -0,0 +1,2 @@
+[e-acsl] beginning translation.
+[e-acsl] translation done in project "e-acsl".
diff --git a/src/plugins/e-acsl/tests/full-mmodel/oracle/gen_addrOf.c b/src/plugins/e-acsl/tests/full-mmodel/oracle/gen_addrOf.c
index 05cb6511ba08ed6fce4953414b0a3578544c1c77..3c2bad6f858c1f3248748229c2c4d76d1e06bc24 100644
--- a/src/plugins/e-acsl/tests/full-mmodel/oracle/gen_addrOf.c
+++ b/src/plugins/e-acsl/tests/full-mmodel/oracle/gen_addrOf.c
@@ -28,16 +28,53 @@ void f(void)
return;
}
+void __e_acsl_globals_init(void)
+{
+ static char __e_acsl_already_run = 0;
+ if (! __e_acsl_already_run) {
+ __e_acsl_already_run = 1;
+ __e_acsl_store_block((void *)(& f),(size_t)1);
+ __e_acsl_full_init((void *)(& f));
+ __e_acsl_store_block((void *)(& __fc_p_fopen),(size_t)8);
+ __e_acsl_full_init((void *)(& __fc_p_fopen));
+ __e_acsl_store_block((void *)(__fc_fopen),(size_t)128);
+ __e_acsl_full_init((void *)(& __fc_fopen));
+ __e_acsl_store_block((void *)(& __fc_p_random48_counter),(size_t)8);
+ __e_acsl_full_init((void *)(& __fc_p_random48_counter));
+ __e_acsl_store_block((void *)(random48_counter),(size_t)6);
+ __e_acsl_full_init((void *)(& random48_counter));
+ __e_acsl_store_block((void *)(& __fc_random48_init),(size_t)4);
+ __e_acsl_full_init((void *)(& __fc_random48_init));
+ __e_acsl_store_block((void *)(& __fc_rand_max),(size_t)8);
+ __e_acsl_full_init((void *)(& __fc_rand_max));
+ }
+ return;
+}
+
int main(void)
{
int __retres;
__e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
+ __e_acsl_globals_init();
+ __e_acsl_store_block((void *)(& __retres),(size_t)4);
int x = 0;
+ __e_acsl_store_block((void *)(& x),(size_t)4);
+ __e_acsl_full_init((void *)(& x));
f();
/*@ assert &x ≡ &x; */
__e_acsl_assert(& x == & x,(char *)"Assertion",(char *)"main",
(char *)"&x == &x",16);
+ __e_acsl_full_init((void *)(& __retres));
__retres = 0;
+ __e_acsl_delete_block((void *)(& f));
+ __e_acsl_delete_block((void *)(& __fc_p_fopen));
+ __e_acsl_delete_block((void *)(__fc_fopen));
+ __e_acsl_delete_block((void *)(& __fc_p_random48_counter));
+ __e_acsl_delete_block((void *)(random48_counter));
+ __e_acsl_delete_block((void *)(& __fc_random48_init));
+ __e_acsl_delete_block((void *)(& __fc_rand_max));
+ __e_acsl_delete_block((void *)(& x));
+ __e_acsl_delete_block((void *)(& __retres));
__e_acsl_memory_clean();
return __retres;
}
diff --git a/src/plugins/e-acsl/tests/full-mmodel/test_config b/src/plugins/e-acsl/tests/full-mmodel/test_config
index 81cf738d2711eb9ff4193db1d9be1a0186a6db97..82cdcaaa69d16cc0e2427322763c59b35a07268b 100644
--- a/src/plugins/e-acsl/tests/full-mmodel/test_config
+++ b/src/plugins/e-acsl/tests/full-mmodel/test_config
@@ -1,5 +1 @@
-LOG: gen_@PTEST_NAME@.c
-OPT: -machdep gcc_x86_64 -check -e-acsl -then-last -load-script tests/print.cmxs -print -ocode tests/full-mmodel/result/gen_@PTEST_NAME@.c -kernel-verbose 0 -eva @EVA_OPTIONS@
-EXEC: ./scripts/testrun.sh @PTEST_NAME@ full-mmodel "1" "--frama-c=@frama-c@ --full-mmodel"
-LOG: gen_@PTEST_NAME@2.c
-OPT: -machdep gcc_x86_64 -check -e-acsl -e-acsl-full-mmodel -then-last -load-script tests/print.cmxs -print -ocode tests/full-mmodel/result/gen_@PTEST_NAME@2.c -kernel-verbose 0 -eva @EVA_OPTIONS@
+STDOPT: #"-e-acsl-full-mmodel"
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/arith.res.oracle b/src/plugins/e-acsl/tests/gmp/oracle/arith.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..49ade870a7844d9509bb53480298afdbb248db8f
--- /dev/null
+++ b/src/plugins/e-acsl/tests/gmp/oracle/arith.res.oracle
@@ -0,0 +1,12 @@
+[e-acsl] beginning translation.
+[e-acsl] translation done in project "e-acsl".
+[eva:alarm] tests/gmp/arith.i:18: Warning:
+ function __e_acsl_assert: precondition got status unknown.
+[eva:alarm] tests/gmp/arith.i:34: Warning:
+ function __e_acsl_assert: precondition got status unknown.
+[eva:alarm] tests/gmp/arith.i:34: Warning:
+ signed overflow. assert -2147483648 ≤ 1 + __gen_e_acsl__7;
+[eva:alarm] tests/gmp/arith.i:34: Warning:
+ signed overflow. assert 1 + __gen_e_acsl__7 ≤ 2147483647;
+[eva:alarm] tests/gmp/arith.i:34: Warning:
+ function __e_acsl_assert: precondition got status unknown.
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/array.res.oracle b/src/plugins/e-acsl/tests/gmp/oracle/array.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..b53db5cdd350ef838d5b42096d6424237952ae6c
--- /dev/null
+++ b/src/plugins/e-acsl/tests/gmp/oracle/array.res.oracle
@@ -0,0 +1,8 @@
+[e-acsl] beginning translation.
+[e-acsl] translation done in project "e-acsl".
+[eva:alarm] tests/gmp/array.i:13: Warning: assertion got status unknown.
+[eva:alarm] tests/gmp/array.i:13: Warning:
+ function __e_acsl_assert: precondition got status unknown.
+[eva:alarm] tests/gmp/array.i:14: Warning: assertion got status unknown.
+[eva:alarm] tests/gmp/array.i:14: Warning:
+ function __e_acsl_assert: precondition got status unknown.
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/at.res.oracle b/src/plugins/e-acsl/tests/gmp/oracle/at.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..b3ea1b65fec9a4ea89a4c44746757e24a9b8e238
--- /dev/null
+++ b/src/plugins/e-acsl/tests/gmp/oracle/at.res.oracle
@@ -0,0 +1,9 @@
+[e-acsl] beginning translation.
+[e-acsl] translation done in project "e-acsl".
+[eva:alarm] tests/gmp/at.i:12: Warning: assertion got status unknown.
+[eva:alarm] tests/gmp/at.i:14: Warning: assertion got status unknown.
+[eva:alarm] tests/gmp/at.i:48: Warning: assertion got status unknown.
+[eva:alarm] tests/gmp/at.i:49: Warning: assertion got status unknown.
+[eva:alarm] tests/gmp/at.i:50: Warning: assertion got status unknown.
+[eva:alarm] tests/gmp/at.i:26: Warning: assertion got status unknown.
+[eva:alarm] tests/gmp/at.i:28: Warning: assertion got status unknown.
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/at_on-purely-logic-variables.res.oracle b/src/plugins/e-acsl/tests/gmp/oracle/at_on-purely-logic-variables.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..6f8dd058c2e23fd0660a2eb821892b29c5bb18d9
--- /dev/null
+++ b/src/plugins/e-acsl/tests/gmp/oracle/at_on-purely-logic-variables.res.oracle
@@ -0,0 +1,87 @@
+[e-acsl] beginning translation.
+[e-acsl] tests/gmp/at_on-purely-logic-variables.c:64: Warning:
+ E-ACSL construct
+ `\at on purely logic variables that needs to allocate too much memory (bigger than int_max bytes)'
+ is not yet supported.
+ Ignoring annotation.
+[e-acsl] tests/gmp/at_on-purely-logic-variables.c:65: Warning:
+ E-ACSL construct `\at with logic variable linked to C variable'
+ is not yet supported.
+ Ignoring annotation.
+[e-acsl] translation done in project "e-acsl".
+[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:28: Warning:
+ assertion got status unknown.
+[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:29: Warning:
+ assertion got status unknown.
+[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:29: Warning:
+ accessing uninitialized left-value.
+ assert \initialized(__gen_e_acsl_at_2 + (__gen_e_acsl_j - 2));
+[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:29: Warning:
+ function __e_acsl_assert: precondition got status unknown.
+[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:29: Warning:
+ function __e_acsl_assert: precondition got status unknown.
+[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:31: Warning:
+ assertion got status unknown.
+[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:33: Warning:
+ accessing uninitialized left-value.
+ assert
+ \initialized(__gen_e_acsl_at_3 +
+ ((__gen_e_acsl_u - 9) * 11 + ((__gen_e_acsl_v - -5) - 1)));
+[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:34: Warning:
+ function __e_acsl_assert: precondition got status unknown.
+[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:37: Warning:
+ assertion got status unknown.
+[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:41: Warning:
+ assertion got status unknown.
+[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:41: Warning:
+ accessing uninitialized left-value.
+ assert \initialized(__gen_e_acsl_at_5 + ((__gen_e_acsl_k_3 - -9) - 1));
+[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:41: Warning:
+ function __e_acsl_assert: precondition got status unknown.
+[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:41: Warning:
+ function __e_acsl_assert: precondition got status unknown.
+[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:43: Warning:
+ assertion got status unknown.
+[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:44: Warning:
+ accessing uninitialized left-value.
+ assert
+ \initialized(__gen_e_acsl_at_6 +
+ ((__gen_e_acsl_u_3 - 9) * 32 + ((__gen_e_acsl_v_3 - -5) - 1)));
+[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:45: Warning:
+ function __e_acsl_assert: precondition got status unknown.
+[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:7: Warning:
+ accessing uninitialized left-value.
+ assert \initialized(__gen_e_acsl_at + ((__gen_e_acsl_n - 1) - 1));
+[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:7: Warning:
+ accessing uninitialized left-value.
+ assert \initialized(__gen_e_acsl_at_2 + ((__gen_e_acsl_n - 1) - 1));
+[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:7: Warning:
+ function __e_acsl_assert: precondition got status unknown.
+[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:7: Warning:
+ function __e_acsl_assert: precondition got status unknown.
+[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:6: Warning:
+ function __gen_e_acsl_f: postcondition got status unknown.
+[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:8: Warning:
+ function __gen_e_acsl_f: postcondition got status unknown.
+[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:16: Warning:
+ assertion got status unknown.
+[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:16: Warning:
+ accessing uninitialized left-value.
+ assert \initialized(__gen_e_acsl_at + (__gen_e_acsl_w - 3));
+[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:16: Warning:
+ function __e_acsl_assert: precondition got status unknown.
+[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:16: Warning:
+ function __e_acsl_assert: precondition got status unknown.
+[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:54: Warning:
+ assertion got status unknown.
+[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:56: Warning:
+ accessing uninitialized left-value.
+ assert
+ \initialized(__gen_e_acsl_at_7 +
+ ((__gen_e_acsl_u_5 - 10) * 300 +
+ (((__gen_e_acsl_v_5 - -10) - 1) * 100 +
+ ((__gen_e_acsl_w - 100) - 1))));
+[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:63: Warning:
+ assertion got status unknown.
+[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:65: Warning:
+ assertion got status unknown.
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/cast.res.oracle b/src/plugins/e-acsl/tests/gmp/oracle/cast.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..91fde30486f7d9ecc718e9982b70a1434b27f74d
--- /dev/null
+++ b/src/plugins/e-acsl/tests/gmp/oracle/cast.res.oracle
@@ -0,0 +1,4 @@
+[e-acsl] beginning translation.
+[e-acsl] tests/gmp/cast.i:23: Warning:
+ E-ACSL construct `R to Int' is not yet supported. Ignoring annotation.
+[e-acsl] translation done in project "e-acsl".
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/comparison.res.oracle b/src/plugins/e-acsl/tests/gmp/oracle/comparison.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..efd026311297e55d8fefb674326118e6ece88624
--- /dev/null
+++ b/src/plugins/e-acsl/tests/gmp/oracle/comparison.res.oracle
@@ -0,0 +1,2 @@
+[e-acsl] beginning translation.
+[e-acsl] translation done in project "e-acsl".
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/functions.res.oracle b/src/plugins/e-acsl/tests/gmp/oracle/functions.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..0851deb0f638262317b79a3190c0f20c0b37761d
--- /dev/null
+++ b/src/plugins/e-acsl/tests/gmp/oracle/functions.res.oracle
@@ -0,0 +1,14 @@
+[e-acsl] beginning translation.
+[e-acsl] translation done in project "e-acsl".
+[eva:alarm] tests/gmp/functions.c:44: Warning:
+ function __e_acsl_assert: precondition got status unknown.
+[eva:alarm] tests/gmp/functions.c:47: Warning:
+ function __e_acsl_assert: precondition got status unknown.
+[eva:alarm] tests/gmp/functions.c:48: Warning:
+ function __e_acsl_assert: precondition got status unknown.
+[eva:alarm] tests/gmp/functions.c:49: Warning:
+ function __e_acsl_assert: precondition got status unknown.
+[eva:alarm] tests/gmp/functions.c:68: Warning:
+ non-finite double value. assert \is_finite(__gen_e_acsl__10);
+[eva:alarm] tests/gmp/functions.c:68: Warning:
+ function __e_acsl_assert: precondition got status unknown.
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/functions_contiki.res.oracle b/src/plugins/e-acsl/tests/gmp/oracle/functions_contiki.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..57f78f5cdc08934b47a367198890e64a8a3455a6
--- /dev/null
+++ b/src/plugins/e-acsl/tests/gmp/oracle/functions_contiki.res.oracle
@@ -0,0 +1,7 @@
+[e-acsl] beginning translation.
+[e-acsl] tests/gmp/functions_contiki.c:27: Warning:
+ E-ACSL construct `logic functions with labels' is not yet supported.
+ Ignoring annotation.
+[e-acsl] translation done in project "e-acsl".
+[eva:alarm] tests/gmp/functions_contiki.c:27: Warning:
+ assertion got status unknown.
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/functions_rec.res.oracle b/src/plugins/e-acsl/tests/gmp/oracle/functions_rec.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..d6226e87d23134d7df3ce0d9e01f2c14905c7c76
--- /dev/null
+++ b/src/plugins/e-acsl/tests/gmp/oracle/functions_rec.res.oracle
@@ -0,0 +1,66 @@
+[e-acsl] beginning translation.
+[e-acsl] translation done in project "e-acsl".
+[eva:alarm] tests/gmp/functions_rec.c:26: Warning: assertion got status unknown.
+[eva] tests/gmp/functions_rec.c:10: Warning:
+ recursive call during value analysis
+ of __gen_e_acsl_f2_2 (__gen_e_acsl_f2_2 <- __gen_e_acsl_f2_2 :: tests/gmp/functions_rec.c:10 <-
+ __gen_e_acsl_f2 :: tests/gmp/functions_rec.c:26 <-
+ main).
+ Assuming the call has no effect. The analysis will be unsound.
+[eva] tests/gmp/functions_rec.c:10: Warning:
+ recursive call during value analysis
+ of __gen_e_acsl_f2_2 (__gen_e_acsl_f2_2 <- __gen_e_acsl_f2_2 :: tests/gmp/functions_rec.c:10 <-
+ __gen_e_acsl_f2 :: tests/gmp/functions_rec.c:26 <-
+ main).
+ Assuming the call has no effect. The analysis will be unsound.
+[eva] tests/gmp/functions_rec.c:10: Warning:
+ recursive call during value analysis
+ of __gen_e_acsl_f2_2 (__gen_e_acsl_f2_2 <- __gen_e_acsl_f2_2 :: tests/gmp/functions_rec.c:10 <-
+ __gen_e_acsl_f2 :: tests/gmp/functions_rec.c:26 <-
+ main).
+ Assuming the call has no effect. The analysis will be unsound.
+[eva:alarm] tests/gmp/functions_rec.c:10: Warning:
+ function __e_acsl_assert: precondition got status unknown.
+[eva:alarm] tests/gmp/functions_rec.c:10: Warning:
+ division by zero. assert __gen_e_acsl_f2_8 ≢ 0;
+[eva:alarm] tests/gmp/functions_rec.c:10: Warning:
+ signed overflow.
+ assert -2147483648 ≤ __gen_e_acsl_f2_4 * __gen_e_acsl_f2_6;
+[eva:alarm] tests/gmp/functions_rec.c:10: Warning:
+ signed overflow. assert __gen_e_acsl_f2_4 * __gen_e_acsl_f2_6 ≤ 2147483647;
+[eva:alarm] tests/gmp/functions_rec.c:10: Warning:
+ signed overflow.
+ assert
+ (int)(__gen_e_acsl_f2_4 * __gen_e_acsl_f2_6) / __gen_e_acsl_f2_8 ≤
+ 2147483647;
+[eva:alarm] tests/gmp/functions_rec.c:10: Warning:
+ division by zero. assert __gen_e_acsl_f2_13 ≢ 0;
+[eva:alarm] tests/gmp/functions_rec.c:10: Warning:
+ signed overflow.
+ assert -2147483648 ≤ __gen_e_acsl_f2_9 * __gen_e_acsl_f2_11;
+[eva:alarm] tests/gmp/functions_rec.c:10: Warning:
+ signed overflow.
+ assert __gen_e_acsl_f2_9 * __gen_e_acsl_f2_11 ≤ 2147483647;
+[eva:alarm] tests/gmp/functions_rec.c:10: Warning:
+ signed overflow.
+ assert
+ (int)(__gen_e_acsl_f2_9 * __gen_e_acsl_f2_11) / __gen_e_acsl_f2_13 ≤
+ 2147483647;
+[eva:alarm] tests/gmp/functions_rec.c:26: Warning:
+ function __e_acsl_assert: precondition got status unknown.
+[eva:alarm] tests/gmp/functions_rec.c:28: Warning: assertion got status unknown.
+[eva] tests/gmp/functions_rec.c:14: Warning:
+ recursive call during value analysis
+ of __gen_e_acsl_f3_2 (__gen_e_acsl_f3_2 <- __gen_e_acsl_f3_2 :: tests/gmp/functions_rec.c:14 <-
+ __gen_e_acsl_f3 :: tests/gmp/functions_rec.c:28 <-
+ main).
+ Assuming the call has no effect. The analysis will be unsound.
+[eva:alarm] tests/gmp/functions_rec.c:30: Warning: assertion got status unknown.
+[eva] tests/gmp/functions_rec.c:17: Warning:
+ recursive call during value analysis
+ of __gen_e_acsl_f4_2 (__gen_e_acsl_f4_2 <- __gen_e_acsl_f4_2 :: tests/gmp/functions_rec.c:17 <-
+ __gen_e_acsl_f4 :: tests/gmp/functions_rec.c:30 <-
+ main).
+ Assuming the call has no effect. The analysis will be unsound.
+[eva:alarm] tests/gmp/functions_rec.c:30: Warning:
+ function __e_acsl_assert: precondition got status unknown.
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/integer_constant.res.oracle b/src/plugins/e-acsl/tests/gmp/oracle/integer_constant.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..5a492da3fd4128e9f0d2742af80b905237760728
--- /dev/null
+++ b/src/plugins/e-acsl/tests/gmp/oracle/integer_constant.res.oracle
@@ -0,0 +1,4 @@
+[e-acsl] beginning translation.
+[e-acsl] translation done in project "e-acsl".
+[eva:alarm] tests/gmp/integer_constant.i:11: Warning:
+ function __e_acsl_assert: precondition got status unknown.
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/let.res.oracle b/src/plugins/e-acsl/tests/gmp/oracle/let.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..f8c1c0d9938107d8020321184e68538a1af53c32
--- /dev/null
+++ b/src/plugins/e-acsl/tests/gmp/oracle/let.res.oracle
@@ -0,0 +1,19 @@
+[e-acsl] beginning translation.
+[e-acsl] tests/gmp/let.c:30: Warning:
+ E-ACSL construct `let-binding on array or pointer' is not yet supported.
+ Ignoring annotation.
+[e-acsl] translation done in project "e-acsl".
+[eva:alarm] tests/gmp/let.c:7: Warning: assertion got status unknown.
+[eva:alarm] tests/gmp/let.c:9: Warning: assertion got status unknown.
+[eva:alarm] tests/gmp/let.c:12: Warning: assertion got status unknown.
+[eva:alarm] tests/gmp/let.c:14: Warning: assertion got status unknown.
+[eva:alarm] tests/gmp/let.c:17: Warning: assertion got status unknown.
+[eva:alarm] tests/gmp/let.c:21: Warning: assertion got status unknown.
+[eva:alarm] tests/gmp/let.c:21: Warning:
+ function __e_acsl_assert: precondition got status unknown.
+[eva:alarm] tests/gmp/let.c:24: Warning: assertion got status unknown.
+[eva:alarm] tests/gmp/let.c:27: Warning: assertion got status unknown.
+[eva:alarm] tests/gmp/let.c:30: Warning: assertion got status unknown.
+[eva:alarm] tests/gmp/let.c:32: Warning: assertion got status unknown.
+[eva:alarm] tests/gmp/let.c:35: Warning: assertion got status unknown.
+[eva:alarm] tests/gmp/let.c:39: Warning: assertion got status unknown.
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/longlong.res.oracle b/src/plugins/e-acsl/tests/gmp/oracle/longlong.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..2360617faf6ad096890375cf3c02bdb7ed973496
--- /dev/null
+++ b/src/plugins/e-acsl/tests/gmp/oracle/longlong.res.oracle
@@ -0,0 +1,14 @@
+[e-acsl] beginning translation.
+[e-acsl] translation done in project "e-acsl".
+[eva] tests/gmp/longlong.i:9: Warning:
+ recursive call during value analysis
+ of my_pow (my_pow <- my_pow :: tests/gmp/longlong.i:16 <- main). Assuming
+ the call has no effect. The analysis will be unsound.
+[eva:alarm] tests/gmp/longlong.i:10: Warning:
+ signed overflow. assert -2147483648 ≤ tmp * tmp;
+[eva:alarm] tests/gmp/longlong.i:10: Warning:
+ signed overflow. assert tmp * tmp ≤ 2147483647;
+[eva:alarm] tests/gmp/longlong.i:17: Warning:
+ function __gmpz_import: precondition got status unknown.
+[eva:alarm] tests/gmp/longlong.i:17: Warning:
+ function __e_acsl_assert: precondition got status unknown.
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/not.res.oracle b/src/plugins/e-acsl/tests/gmp/oracle/not.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..efd026311297e55d8fefb674326118e6ece88624
--- /dev/null
+++ b/src/plugins/e-acsl/tests/gmp/oracle/not.res.oracle
@@ -0,0 +1,2 @@
+[e-acsl] beginning translation.
+[e-acsl] translation done in project "e-acsl".
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/quantif.res.oracle b/src/plugins/e-acsl/tests/gmp/oracle/quantif.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..6636cdc4391eb2f2ea94e51302a5ac438a55a6fd
--- /dev/null
+++ b/src/plugins/e-acsl/tests/gmp/oracle/quantif.res.oracle
@@ -0,0 +1,25 @@
+[e-acsl] beginning translation.
+[e-acsl] translation done in project "e-acsl".
+[eva:alarm] tests/gmp/quantif.i:9: Warning: assertion got status unknown.
+[eva:alarm] tests/gmp/quantif.i:10: Warning: assertion got status unknown.
+[eva:alarm] tests/gmp/quantif.i:11: Warning: assertion got status unknown.
+[eva:alarm] tests/gmp/quantif.i:15: Warning: assertion got status unknown.
+[eva:alarm] tests/gmp/quantif.i:15: Warning:
+ function __e_acsl_assert: precondition got status unknown.
+[eva:alarm] tests/gmp/quantif.i:20: Warning: assertion got status unknown.
+[eva:alarm] tests/gmp/quantif.i:24: Warning: assertion got status unknown.
+[eva:alarm] tests/gmp/quantif.i:24: Warning:
+ function __e_acsl_assert: precondition got status unknown.
+[eva:alarm] tests/gmp/quantif.i:30: Warning: assertion got status unknown.
+[eva:alarm] tests/gmp/quantif.i:30: Warning:
+ function __e_acsl_assert: precondition got status unknown.
+[eva:alarm] tests/gmp/quantif.i:31: Warning:
+ function __e_acsl_assert: precondition got status unknown.
+[eva:alarm] tests/gmp/quantif.i:32: Warning: assertion got status unknown.
+[eva:alarm] tests/gmp/quantif.i:32: Warning:
+ function __e_acsl_assert: precondition got status unknown.
+[eva:alarm] tests/gmp/quantif.i:33: Warning: assertion got status unknown.
+[eva:alarm] tests/gmp/quantif.i:33: Warning:
+ function __e_acsl_assert: precondition got status unknown.
+[eva:alarm] tests/gmp/quantif.i:37: Warning: assertion got status unknown.
+[eva:alarm] tests/gmp/quantif.i:40: Warning: assertion got status unknown.
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/reals.res.oracle b/src/plugins/e-acsl/tests/gmp/oracle/reals.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..b556402d9c02078689197c3880f6c352e3870b42
--- /dev/null
+++ b/src/plugins/e-acsl/tests/gmp/oracle/reals.res.oracle
@@ -0,0 +1,48 @@
+[kernel:parser:decimal-float] tests/gmp/reals.c:22: Warning:
+ Floating-point constant 0.2f is not represented exactly. Will use 0x1.99999a0000000p-3.
+ (warn-once: no further messages from category 'parser:decimal-float' will be emitted)
+[e-acsl] beginning translation.
+[e-acsl] Warning: R to float: double rounding might cause unsoundness
+[e-acsl] tests/gmp/reals.c:19: Warning:
+ E-ACSL construct `predicate with no definition nor reads clause'
+ is not yet supported.
+ Ignoring annotation.
+[e-acsl] translation done in project "e-acsl".
+[eva:alarm] tests/gmp/reals.c:15: Warning:
+ function __e_acsl_assert: precondition got status unknown.
+[eva:alarm] tests/gmp/reals.c:16: Warning: assertion got status unknown.
+[eva:alarm] tests/gmp/reals.c:16: Warning:
+ function __e_acsl_assert: precondition got status unknown.
+[eva:alarm] tests/gmp/reals.c:18: Warning: assertion got status unknown.
+[eva:alarm] tests/gmp/reals.c:18: Warning:
+ non-finite double value. assert \is_finite(__gen_e_acsl__6);
+[eva:alarm] tests/gmp/reals.c:18: Warning:
+ function __e_acsl_assert: precondition got status unknown.
+[eva:alarm] tests/gmp/reals.c:19: Warning:
+ non-finite double value. assert \is_finite(__gen_e_acsl__9);
+[eva:alarm] tests/gmp/reals.c:19: Warning:
+ non-finite double value. assert \is_finite(__gen_e_acsl__10);
+[eva:alarm] tests/gmp/reals.c:19: Warning:
+ non-finite float value. assert \is_finite((float)__gen_e_acsl__9);
+[eva:alarm] tests/gmp/reals.c:19: Warning:
+ function __e_acsl_assert: precondition got status unknown.
+[eva:alarm] tests/gmp/reals.c:20: Warning: assertion got status unknown.
+[eva:alarm] tests/gmp/reals.c:20: Warning:
+ non-finite double value. assert \is_finite(__gen_e_acsl__12);
+[eva:alarm] tests/gmp/reals.c:20: Warning:
+ function __e_acsl_assert: precondition got status unknown.
+[eva:alarm] tests/gmp/reals.c:21: Warning: assertion got status unknown.
+[eva:alarm] tests/gmp/reals.c:21: Warning:
+ function __e_acsl_assert: precondition got status unknown.
+[eva:alarm] tests/gmp/reals.c:25: Warning:
+ function __e_acsl_assert: precondition got status unknown.
+[eva:alarm] tests/gmp/reals.c:26: Warning: assertion got status unknown.
+[eva:alarm] tests/gmp/reals.c:26: Warning:
+ function __e_acsl_assert: precondition got status unknown.
+[eva:alarm] tests/gmp/reals.c:6: Warning:
+ function __e_acsl_assert: precondition got status unknown.
+[eva:alarm] tests/gmp/reals.c:6: Warning:
+ function __gen_e_acsl_avg: postcondition got status unknown.
+[eva:alarm] tests/gmp/reals.c:32: Warning: assertion got status unknown.
+[eva:alarm] tests/gmp/reals.c:32: Warning:
+ function __e_acsl_assert: precondition got status unknown.
diff --git a/src/plugins/e-acsl/tests/gmp/test_config b/src/plugins/e-acsl/tests/gmp/test_config
deleted file mode 100644
index b2a9e07a1cb38c32a99ed4d562ef04cbb1a396d3..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/gmp/test_config
+++ /dev/null
@@ -1,5 +0,0 @@
-LOG: gen_@PTEST_NAME@.c
-OPT: -machdep gcc_x86_64 -check -e-acsl -then-last -load-script tests/print.cmxs -print -ocode tests/gmp/result/gen_@PTEST_NAME@.c -kernel-verbose 0 -eva @EVA_OPTIONS@
-EXEC: ./scripts/testrun.sh @PTEST_NAME@ gmp "1" "--frama-c=@frama-c@"
-LOG: gen_@PTEST_NAME@2.c
-OPT: -machdep gcc_x86_64 -check -e-acsl -e-acsl-gmp-only -then-last -load-script tests/print.cmxs -print -ocode tests/gmp/result/gen_@PTEST_NAME@2.c -kernel-verbose 0 -eva @EVA_OPTIONS@
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/base_addr.res.oracle b/src/plugins/e-acsl/tests/runtime/oracle/base_addr.res.oracle
index c70e1ab6c4dbfdb3f2daec4d1853e5b2924903b1..efd026311297e55d8fefb674326118e6ece88624 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/base_addr.res.oracle
+++ b/src/plugins/e-acsl/tests/runtime/oracle/base_addr.res.oracle
@@ -1,29 +1,2 @@
[e-acsl] beginning translation.
[e-acsl] translation done in project "e-acsl".
-[eva:alarm] tests/runtime/base_addr.c:46: Warning: assertion got status unknown.
-[eva:alarm] tests/runtime/base_addr.c:46: Warning:
- function __e_acsl_assert: precondition got status unknown.
-[eva:alarm] tests/runtime/base_addr.c:47: Warning: assertion got status unknown.
-[eva:alarm] tests/runtime/base_addr.c:47: Warning:
- function __e_acsl_assert: precondition got status unknown.
-[eva:alarm] tests/runtime/base_addr.c:48: Warning: assertion got status unknown.
-[eva:alarm] tests/runtime/base_addr.c:48: Warning:
- function __e_acsl_assert: precondition got status unknown.
-[eva:alarm] tests/runtime/base_addr.c:50: Warning: assertion got status unknown.
-[eva:alarm] tests/runtime/base_addr.c:50: Warning:
- function __e_acsl_assert: precondition got status unknown.
-[eva:alarm] tests/runtime/base_addr.c:51: Warning: assertion got status unknown.
-[eva:alarm] tests/runtime/base_addr.c:51: Warning:
- function __e_acsl_assert: precondition got status unknown.
-[eva:alarm] tests/runtime/base_addr.c:57: Warning: assertion got status unknown.
-[eva:alarm] tests/runtime/base_addr.c:57: Warning:
- function __e_acsl_assert: precondition got status unknown.
-[eva:alarm] tests/runtime/base_addr.c:59: Warning: assertion got status unknown.
-[eva:alarm] tests/runtime/base_addr.c:59: Warning:
- function __e_acsl_assert: precondition got status unknown.
-[eva:alarm] tests/runtime/base_addr.c:61: Warning: assertion got status unknown.
-[eva:alarm] tests/runtime/base_addr.c:61: Warning:
- function __e_acsl_assert: precondition got status unknown.
-[eva:alarm] tests/runtime/base_addr.c:63: Warning: assertion got status unknown.
-[eva:alarm] tests/runtime/base_addr.c:63: Warning:
- function __e_acsl_assert: precondition got status unknown.
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/block_length.res.oracle b/src/plugins/e-acsl/tests/runtime/oracle/block_length.res.oracle
index a65c86b9580f9b1cd10982d46c6c9daaabee5bec..efd026311297e55d8fefb674326118e6ece88624 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/block_length.res.oracle
+++ b/src/plugins/e-acsl/tests/runtime/oracle/block_length.res.oracle
@@ -1,22 +1,2 @@
[e-acsl] beginning translation.
[e-acsl] translation done in project "e-acsl".
-[eva:alarm] tests/runtime/block_length.c:50: Warning:
- assertion got status unknown.
-[eva:alarm] tests/runtime/block_length.c:50: Warning:
- function __e_acsl_assert: precondition got status unknown.
-[eva:alarm] tests/runtime/block_length.c:51: Warning:
- assertion got status unknown.
-[eva:alarm] tests/runtime/block_length.c:51: Warning:
- function __e_acsl_assert: precondition got status unknown.
-[eva:alarm] tests/runtime/block_length.c:53: Warning:
- assertion got status unknown.
-[eva:alarm] tests/runtime/block_length.c:53: Warning:
- function __e_acsl_assert: precondition got status unknown.
-[eva:alarm] tests/runtime/block_length.c:59: Warning:
- assertion got status unknown.
-[eva:alarm] tests/runtime/block_length.c:59: Warning:
- function __e_acsl_assert: precondition got status unknown.
-[eva:alarm] tests/runtime/block_length.c:61: Warning:
- assertion got status unknown.
-[eva:alarm] tests/runtime/block_length.c:61: Warning:
- function __e_acsl_assert: precondition got status unknown.
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/block_valid.res.oracle b/src/plugins/e-acsl/tests/runtime/oracle/block_valid.res.oracle
index 38722b0c803d3f3bd3d96460b7bc7dac51169be6..48f95d7442c30a836bf0d015d4e12c0f1066e5da 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/block_valid.res.oracle
+++ b/src/plugins/e-acsl/tests/runtime/oracle/block_valid.res.oracle
@@ -1,9 +1,5 @@
[e-acsl] beginning translation.
[e-acsl] translation done in project "e-acsl".
-[eva:alarm] tests/runtime/block_valid.c:45: Warning:
- out of bounds write. assert \valid(pmin);
-[eva:alarm] tests/runtime/block_valid.c:46: Warning:
- out of bounds write. assert \valid(pmax);
[eva:alarm] tests/runtime/block_valid.c:49: Warning:
function __e_acsl_assert: precondition got status unknown.
[eva:alarm] tests/runtime/block_valid.c:50: Warning:
@@ -16,4 +12,3 @@
assertion got status unknown.
[eva:alarm] tests/runtime/block_valid.c:54: Warning:
function __e_acsl_assert: precondition got status unknown.
-[scope:rm_asserts] removing 2 assertion(s)
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_block_valid.c b/src/plugins/e-acsl/tests/runtime/oracle/gen_block_valid.c
index b20b24b8cb71e3097a0c8372ae1af93e4614baaa..c8beb84f9f767bf1199a38ec71dfad279ec2511c 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/gen_block_valid.c
+++ b/src/plugins/e-acsl/tests/runtime/oracle/gen_block_valid.c
@@ -98,10 +98,8 @@ int main(int argc, char **argv)
__e_acsl_delete_block((void *)(& t));
}
__e_acsl_initialize((void *)pmin,sizeof(char));
- /*@ assert Eva: mem_access: \valid(pmin); */
*pmin = (char)'P';
__e_acsl_initialize((void *)pmax,sizeof(char));
- /*@ assert Eva: mem_access: \valid(pmax); */
*pmax = (char)'L';
int diff = (int)((unsigned long)pmax - (unsigned long)pmin);
/*@ assert \valid(pmin); */
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_initialized.c b/src/plugins/e-acsl/tests/runtime/oracle/gen_initialized.c
index f228f8b071b886d560decd1e725df14d8a5e9ca1..10ada7d1065cf07e043c5526e9da48a2b3cafd2b 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/gen_initialized.c
+++ b/src/plugins/e-acsl/tests/runtime/oracle/gen_initialized.c
@@ -304,7 +304,6 @@ int main(void)
/*@ assert ¬\initialized(q); */
{
int __gen_e_acsl_initialized_31;
- /*@ assert Eva: dangling_pointer: ¬\dangling(&q); */
__gen_e_acsl_initialized_31 = __e_acsl_initialized((void *)q,sizeof(int));
__e_acsl_assert(! __gen_e_acsl_initialized_31,(char *)"Assertion",
(char *)"main",(char *)"!\\initialized(q)",86);
@@ -335,12 +334,8 @@ int main(void)
{
int i = 0;
while (i < size) {
- if (i % 2 != 0)
- /*@ assert Eva: mem_access: \valid(partsc + i); */
- *(partsc + i) = (char)'0';
- else
- /*@ assert Eva: mem_access: \valid(partsi + i); */
- *(partsi + i) = (char)0;
+ if (i % 2 != 0) *(partsc + i) = (char)'0';
+ else *(partsi + i) = (char)0;
i ++;
}
}
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_local_goto.c b/src/plugins/e-acsl/tests/runtime/oracle/gen_local_goto.c
index 7143f574e29b67fbc1ae425722ac81ecbac0944b..18ceafe4d81e54118ac386239051e8e12a7b9969 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/gen_local_goto.c
+++ b/src/plugins/e-acsl/tests/runtime/oracle/gen_local_goto.c
@@ -5,8 +5,6 @@ char *__gen_e_acsl_literal_string;
char *__gen_e_acsl_literal_string_3;
char *__gen_e_acsl_literal_string_2;
char *__gen_e_acsl_literal_string_4;
-extern int __e_acsl_sound_verdict;
-
void __e_acsl_globals_init(void)
{
static char __e_acsl_already_run = 0;
@@ -42,8 +40,7 @@ int main(int argc, char const **argv)
int t = 0;
UP: ;
if (t == 2) {
- __gen_e_acsl_printf_va_1(__gen_e_acsl_literal_string,t,
- (char *)__gen_e_acsl_literal_string_2);
+ printf(__gen_e_acsl_literal_string,t,__gen_e_acsl_literal_string_2);
goto RET;
}
AGAIN:
@@ -61,8 +58,7 @@ int main(int argc, char const **argv)
(char *)"\\valid(&a)",25);
}
if (t == 2) {
- __gen_e_acsl_printf_va_2(__gen_e_acsl_literal_string,t,
- (char *)__gen_e_acsl_literal_string_3);
+ printf(__gen_e_acsl_literal_string,t,__gen_e_acsl_literal_string_3);
__e_acsl_delete_block((void *)(& a));
goto UP;
}
@@ -78,8 +74,7 @@ int main(int argc, char const **argv)
__e_acsl_assert(__gen_e_acsl_valid_2,(char *)"Assertion",
(char *)"main",(char *)"\\valid(&b)",36);
}
- __gen_e_acsl_printf_va_3(__gen_e_acsl_literal_string,t,
- (char *)__gen_e_acsl_literal_string_4);
+ printf(__gen_e_acsl_literal_string,t,__gen_e_acsl_literal_string_4);
__e_acsl_delete_block((void *)(& a));
__e_acsl_delete_block((void *)(& b));
goto AGAIN;
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/initialized.res.oracle b/src/plugins/e-acsl/tests/runtime/oracle/initialized.res.oracle
index 04a89818e5de47aaaab1755b2d1adf7c7dc1e377..c420e591edcef860a33f6edcb47fcd8ebab9b193 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/initialized.res.oracle
+++ b/src/plugins/e-acsl/tests/runtime/oracle/initialized.res.oracle
@@ -1,45 +1,7 @@
[e-acsl] beginning translation.
[e-acsl] translation done in project "e-acsl".
-[eva:alarm] tests/runtime/initialized.c:66: Warning:
- assertion got status unknown.
-[eva:alarm] tests/runtime/initialized.c:66: Warning:
- function __e_acsl_assert: precondition got status unknown.
-[eva:alarm] tests/runtime/initialized.c:70: Warning:
- assertion got status unknown.
-[eva:alarm] tests/runtime/initialized.c:70: Warning:
- function __e_acsl_assert: precondition got status unknown.
-[eva:alarm] tests/runtime/initialized.c:75: Warning:
- assertion got status unknown.
-[eva:alarm] tests/runtime/initialized.c:75: Warning:
- function __e_acsl_assert: precondition got status unknown.
-[eva:alarm] tests/runtime/initialized.c:77: Warning:
- assertion got status unknown.
-[eva:alarm] tests/runtime/initialized.c:77: Warning:
- function __e_acsl_assert: precondition got status unknown.
[eva:alarm] tests/runtime/initialized.c:85: Warning:
assertion got status unknown.
[eva:alarm] tests/runtime/initialized.c:85: Warning:
accessing left-value that contains escaping addresses.
assert ¬\dangling(&p);
-[eva:alarm] tests/runtime/initialized.c:85: Warning:
- function __e_acsl_assert: precondition got status unknown.
-[eva:alarm] tests/runtime/initialized.c:86: Warning:
- assertion got status unknown.
-[eva:alarm] tests/runtime/initialized.c:86: Warning:
- accessing left-value that contains escaping addresses.
- assert ¬\dangling(&q);
-[eva:alarm] tests/runtime/initialized.c:86: Warning:
- function __e_acsl_assert: precondition got status unknown.
-[eva:alarm] tests/runtime/initialized.c:94: Warning:
- assertion got status unknown.
-[eva:alarm] tests/runtime/initialized.c:94: Warning:
- function __e_acsl_assert: precondition got status unknown.
-[eva:alarm] tests/runtime/initialized.c:97: Warning:
- assertion got status unknown.
-[eva:alarm] tests/runtime/initialized.c:97: Warning:
- function __e_acsl_assert: precondition got status unknown.
-[eva:alarm] tests/runtime/initialized.c:108: Warning:
- out of bounds write. assert \valid(partsi + i);
-[eva:alarm] tests/runtime/initialized.c:106: Warning:
- out of bounds write. assert \valid(partsc + i);
-[scope:rm_asserts] removing 5 assertion(s)
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/local_goto.res.oracle b/src/plugins/e-acsl/tests/runtime/oracle/local_goto.res.oracle
index a2e7e709cc1b03f77f747ddda9fc902b26666500..9811cdbf49f1324c0f4cffd3aed7d450deac04cb 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/local_goto.res.oracle
+++ b/src/plugins/e-acsl/tests/runtime/oracle/local_goto.res.oracle
@@ -1,29 +1,4 @@
[e-acsl] beginning translation.
-[e-acsl] Warning: annotating undefined function `printf_va_1':
- the generated program may miss memory instrumentation
- if there are memory-related annotations.
-[e-acsl] Warning: annotating undefined function `printf_va_2':
- the generated program may miss memory instrumentation
- if there are memory-related annotations.
-[e-acsl] Warning: annotating undefined function `printf_va_3':
- the generated program may miss memory instrumentation
- if there are memory-related annotations.
-[e-acsl] tests/runtime/local_goto.c:37: Warning:
- E-ACSL construct `logic functions with labels' is not yet supported.
- Ignoring annotation.
-[e-acsl] tests/runtime/local_goto.c:37: Warning:
- E-ACSL construct `assigns clause in behavior' is not yet supported.
- Ignoring annotation.
-[e-acsl] tests/runtime/local_goto.c:28: Warning:
- E-ACSL construct `logic functions with labels' is not yet supported.
- Ignoring annotation.
-[e-acsl] tests/runtime/local_goto.c:28: Warning:
- E-ACSL construct `assigns clause in behavior' is not yet supported.
- Ignoring annotation.
-[e-acsl] tests/runtime/local_goto.c:16: Warning:
- E-ACSL construct `logic functions with labels' is not yet supported.
- Ignoring annotation.
-[e-acsl] tests/runtime/local_goto.c:16: Warning:
- E-ACSL construct `assigns clause in behavior' is not yet supported.
- Ignoring annotation.
+[kernel:annot:missing-spec] FRAMAC_SHARE/libc/stdio.h:169: Warning:
+ Neither code nor specification for function printf, generating default assigns from the prototype
[e-acsl] translation done in project "e-acsl".
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/mainargs.res.oracle b/src/plugins/e-acsl/tests/runtime/oracle/mainargs.res.oracle
index bb9147c4b0e9addaee53ab74367d4c34a7e0a0a4..f74e35f0e120a351bf3d408ef97f23e92f884ac2 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/mainargs.res.oracle
+++ b/src/plugins/e-acsl/tests/runtime/oracle/mainargs.res.oracle
@@ -41,4 +41,3 @@
[eva:alarm] tests/runtime/mainargs.c:20: Warning: assertion got status unknown.
[eva:alarm] tests/runtime/mainargs.c:20: Warning:
function __e_acsl_assert: precondition got status unknown.
-[scope:rm_asserts] removing 1 assertion(s)
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/memalign.res.oracle b/src/plugins/e-acsl/tests/runtime/oracle/memalign.res.oracle
index 505c3a9513d560559bd6786634c1d6a699413323..b7fc1a1f56521acd0b52bf324c7c7253b3258ab3 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/memalign.res.oracle
+++ b/src/plugins/e-acsl/tests/runtime/oracle/memalign.res.oracle
@@ -1,7 +1,4 @@
[e-acsl] beginning translation.
[e-acsl] translation done in project "e-acsl".
-[eva:alarm] tests/runtime/memalign.c:12: Warning:
- function posix_memalign: precondition 'valid_memptr' got status unknown.
[eva:alarm] tests/runtime/memalign.c:14: Warning:
accessing uninitialized left-value. assert \initialized(memptr);
-[scope:rm_asserts] removing 2 assertion(s)
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/memsize.res.oracle b/src/plugins/e-acsl/tests/runtime/oracle/memsize.res.oracle
index 8862c572bb0532491075e376e4082cade59fbff2..742bcfb05433e896ed6b89247eb1d514c025bab1 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/memsize.res.oracle
+++ b/src/plugins/e-acsl/tests/runtime/oracle/memsize.res.oracle
@@ -3,4 +3,3 @@
[eva:alarm] tests/runtime/memsize.c:14: Warning: assertion got status unknown.
[eva:alarm] tests/runtime/memsize.c:16: Warning:
assertion got status invalid (stopping propagation).
-[scope:rm_asserts] removing 6 assertion(s)
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/ranges_in_builtins.res.oracle b/src/plugins/e-acsl/tests/runtime/oracle/ranges_in_builtins.res.oracle
index 465b591b22527e94c1e2353681ba04c781924dfb..2b65e90e6d9994eb574ae54dceaccbaf1e78732d 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/ranges_in_builtins.res.oracle
+++ b/src/plugins/e-acsl/tests/runtime/oracle/ranges_in_builtins.res.oracle
@@ -4,7 +4,5 @@
is not yet supported.
Ignoring annotation.
[e-acsl] translation done in project "e-acsl".
-[eva:alarm] tests/runtime/ranges_in_builtins.c:19: Warning:
- assertion got status unknown.
[eva:alarm] tests/runtime/ranges_in_builtins.c:21: Warning:
assertion got status invalid (stopping propagation).
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/vector.res.oracle b/src/plugins/e-acsl/tests/runtime/oracle/vector.res.oracle
index ea0de0ba7383a386091c52a983888d5c5007f310..1891087e5580531e7cb0f22b3349948d9625b8f9 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/vector.res.oracle
+++ b/src/plugins/e-acsl/tests/runtime/oracle/vector.res.oracle
@@ -3,4 +3,3 @@
[eva:alarm] tests/runtime/vector.c:26: Warning:
accessing uninitialized left-value. assert \initialized(v2 + 2);
[eva:alarm] tests/runtime/vector.c:28: Warning: assertion got status unknown.
-[scope:rm_asserts] removing 1 assertion(s)
diff --git a/src/plugins/e-acsl/tests/runtime/test_config b/src/plugins/e-acsl/tests/runtime/test_config
deleted file mode 100644
index 49e3e5e1028f11fde69f1e65163604f33b658af8..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/runtime/test_config
+++ /dev/null
@@ -1,3 +0,0 @@
-LOG: gen_@PTEST_NAME@.c
-OPT: -machdep gcc_x86_64 -check -e-acsl -then-last -load-script tests/print.cmxs -print -ocode tests/runtime/result/gen_@PTEST_NAME@.c -kernel-verbose 0 -eva -eva-verbose 0 -eva-warn-key libc:unsupported-spec=inactive
-EXEC: ./scripts/testrun.sh @PTEST_NAME@ runtime "" "--frama-c=@frama-c@"
diff --git a/src/plugins/e-acsl/tests/segment-only/oracle/constructor.res.oracle b/src/plugins/e-acsl/tests/segment-only/oracle/constructor.res.oracle
index fb1184a3e5634daf84200d210428dfcd8c91aa44..9811cdbf49f1324c0f4cffd3aed7d450deac04cb 100644
--- a/src/plugins/e-acsl/tests/segment-only/oracle/constructor.res.oracle
+++ b/src/plugins/e-acsl/tests/segment-only/oracle/constructor.res.oracle
@@ -1,20 +1,4 @@
[e-acsl] beginning translation.
-[e-acsl] Warning: annotating undefined function `printf_va_1':
- the generated program may miss memory instrumentation
- if there are memory-related annotations.
-[e-acsl] Warning: annotating undefined function `printf_va_2':
- the generated program may miss memory instrumentation
- if there are memory-related annotations.
-[e-acsl] tests/segment-only/constructor.c:16: Warning:
- E-ACSL construct `logic function application' is not yet supported.
- Ignoring annotation.
-[e-acsl] tests/segment-only/constructor.c:16: Warning:
- E-ACSL construct `assigns clause in behavior' is not yet supported.
- Ignoring annotation.
-[e-acsl] tests/segment-only/constructor.c:10: Warning:
- E-ACSL construct `logic function application' is not yet supported.
- Ignoring annotation.
-[e-acsl] tests/segment-only/constructor.c:10: Warning:
- E-ACSL construct `assigns clause in behavior' is not yet supported.
- Ignoring annotation.
+[kernel:annot:missing-spec] FRAMAC_SHARE/libc/stdio.h:169: Warning:
+ Neither code nor specification for function printf, generating default assigns from the prototype
[e-acsl] translation done in project "e-acsl".
diff --git a/src/plugins/e-acsl/tests/segment-only/oracle/gen_constructor.c b/src/plugins/e-acsl/tests/segment-only/oracle/gen_constructor.c
index eefdbbe0fd9c57b351169fd473ed0a95dc5ef0c9..15a99b43c04dacb8866abecb8ce0ef28e7db4bbf 100644
--- a/src/plugins/e-acsl/tests/segment-only/oracle/gen_constructor.c
+++ b/src/plugins/e-acsl/tests/segment-only/oracle/gen_constructor.c
@@ -6,7 +6,7 @@ char *__gen_e_acsl_literal_string;
void f(void) __attribute__((__constructor__));
void f(void)
{
- __gen_e_acsl_printf_va_1(__gen_e_acsl_literal_string);
+ printf(__gen_e_acsl_literal_string);
char *buf = malloc((unsigned long)10 * sizeof(char));
free((void *)buf);
return;
@@ -14,15 +14,19 @@ void f(void)
void __e_acsl_globals_init(void)
{
- __gen_e_acsl_literal_string_2 = "main\n";
- __e_acsl_store_block((void *)__gen_e_acsl_literal_string_2,
- sizeof("main\n"));
- __e_acsl_full_init((void *)__gen_e_acsl_literal_string_2);
- __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_2);
- __gen_e_acsl_literal_string = "f\n";
- __e_acsl_store_block((void *)__gen_e_acsl_literal_string,sizeof("f\n"));
- __e_acsl_full_init((void *)__gen_e_acsl_literal_string);
- __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string);
+ static char __e_acsl_already_run = 0;
+ if (! __e_acsl_already_run) {
+ __e_acsl_already_run = 1;
+ __gen_e_acsl_literal_string_2 = "main\n";
+ __e_acsl_store_block((void *)__gen_e_acsl_literal_string_2,
+ sizeof("main\n"));
+ __e_acsl_full_init((void *)__gen_e_acsl_literal_string_2);
+ __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_2);
+ __gen_e_acsl_literal_string = "f\n";
+ __e_acsl_store_block((void *)__gen_e_acsl_literal_string,sizeof("f\n"));
+ __e_acsl_full_init((void *)__gen_e_acsl_literal_string);
+ __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string);
+ }
return;
}
@@ -31,7 +35,7 @@ int main(void)
int __retres;
__e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
__e_acsl_globals_init();
- __gen_e_acsl_printf_va_2(__gen_e_acsl_literal_string_2);
+ printf(__gen_e_acsl_literal_string_2);
__retres = 0;
__e_acsl_memory_clean();
return __retres;
diff --git a/src/plugins/e-acsl/tests/segment-only/test_config b/src/plugins/e-acsl/tests/segment-only/test_config
deleted file mode 100644
index 3aa2fcbc6b1e0f167afe722d6f48c707129bab6d..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/segment-only/test_config
+++ /dev/null
@@ -1,3 +0,0 @@
-LOG: gen_@PTEST_NAME@.c
-OPT: -machdep gcc_x86_64 -check -e-acsl -then-last -load-script tests/print.cmxs -print -ocode tests/segment-only/result/gen_@PTEST_NAME@.c -kernel-verbose 0 -eva -eva-verbose 0
-EXEC: ./scripts/testrun.sh @PTEST_NAME@ segment-only "" "--frama-c=@frama-c@" "segment"
\ No newline at end of file
diff --git a/src/plugins/e-acsl/tests/temporal/oracle/gen_t_dpointer.c b/src/plugins/e-acsl/tests/temporal/oracle/gen_t_dpointer.c
index 13d59a6a146231814ede4cb1396e6323ee436107..8a600eed354a833a550e737cc928c75e20c9d93a 100644
--- a/src/plugins/e-acsl/tests/temporal/oracle/gen_t_dpointer.c
+++ b/src/plugins/e-acsl/tests/temporal/oracle/gen_t_dpointer.c
@@ -24,7 +24,6 @@ int main(void)
__e_acsl_temporal_reset_parameters();
__e_acsl_temporal_reset_return();
__e_acsl_initialize((void *)(p + i),sizeof(int *));
- /*@ assert Eva: mem_access: \valid(p + i); */
*(p + i) = (int *)malloc(sizeof(int));
/*@ assert Eva: initialization: \initialized(p + i); */
__e_acsl_temporal_store_nblock((void *)(p + i),(void *)*(p + i));
@@ -59,7 +58,6 @@ int main(void)
__e_acsl_temporal_reset_return();
__e_acsl_temporal_save_nreferent_parameter((void *)(p + 2),0U);
/*@ assert Eva: initialization: \initialized(p + 2); */
- /*@ assert Eva: mem_access: \valid_read(p + 2); */
free((void *)*(p + 2));
__e_acsl_temporal_reset_parameters();
__e_acsl_temporal_reset_return();
diff --git a/src/plugins/e-acsl/tests/temporal/oracle/gen_t_malloc-asan.c b/src/plugins/e-acsl/tests/temporal/oracle/gen_t_malloc-asan.c
index ffecf62daef023a69fb5a1da15c5d8c41d1f17c6..8095a59581baf85e20d7e1ba6fb1b92f7260cc0b 100644
--- a/src/plugins/e-acsl/tests/temporal/oracle/gen_t_malloc-asan.c
+++ b/src/plugins/e-acsl/tests/temporal/oracle/gen_t_malloc-asan.c
@@ -2,8 +2,6 @@
#include "stdio.h"
#include "stdlib.h"
char *__gen_e_acsl_literal_string;
-extern int __e_acsl_sound_verdict;
-
void __e_acsl_globals_init(void)
{
static char __e_acsl_already_run = 0;
@@ -59,18 +57,15 @@ int main(void)
__e_acsl_temporal_reset_parameters();
__e_acsl_temporal_reset_return();
__e_acsl_temporal_save_nreferent_parameter((void *)(& p),1U);
- __gen_e_acsl_printf_va_1(__gen_e_acsl_literal_string,(void *)p,counter);
+ printf(__gen_e_acsl_literal_string,p,counter);
break;
}
__e_acsl_temporal_store_nblock((void *)(& p),(void *)0);
__e_acsl_full_init((void *)(& p));
p = (int *)0;
}
- /*@ assert Eva: dangling_pointer: ¬\dangling(&p); */
if (p) {
- /*@ assert Eva: dangling_pointer: ¬\dangling(&q); */
__e_acsl_initialize((void *)q,sizeof(int));
- /*@ assert Eva: mem_access: \valid(q); */
*q = 1;
__e_acsl_initialize((void *)p,sizeof(int));
*p = 2;
diff --git a/src/plugins/e-acsl/tests/temporal/oracle/gen_t_memcpy.c b/src/plugins/e-acsl/tests/temporal/oracle/gen_t_memcpy.c
index 1bfc00a908d32def5d7fce8ea952b20aab92bb1b..18a7163bb5648065ea7fb49a9c45a9a2b3e8343b 100644
--- a/src/plugins/e-acsl/tests/temporal/oracle/gen_t_memcpy.c
+++ b/src/plugins/e-acsl/tests/temporal/oracle/gen_t_memcpy.c
@@ -156,7 +156,6 @@ int main(void)
__e_acsl_temporal_store_nblock((void *)(& q),(void *)*(& q));
__e_acsl_temporal_store_nblock((void *)p,(void *)(& a));
__e_acsl_initialize((void *)p,sizeof(int *));
- /*@ assert Eva: mem_access: \valid(p); */
*p = & a;
__e_acsl_temporal_store_nblock((void *)(p + 1),(void *)(& a));
__e_acsl_initialize((void *)(p + 1),sizeof(int *));
@@ -239,8 +238,6 @@ int main(void)
else __gen_e_acsl_and_10 = 0;
__e_acsl_assert(__gen_e_acsl_and_10,(char *)"RTE",(char *)"main",
(char *)"mem_access: \\valid_read(q)",44);
- /*@ assert Eva: initialization: \initialized(q); */
- /*@ assert Eva: mem_access: \valid_read(q); */
__gen_e_acsl_valid_9 = __e_acsl_valid((void *)*q,sizeof(int),
(void *)*q,(void *)q);
__gen_e_acsl_and_11 = __gen_e_acsl_valid_9;
@@ -264,8 +261,6 @@ int main(void)
(void *)(& q));
__e_acsl_assert(__gen_e_acsl_valid_read_4,(char *)"RTE",(char *)"main",
(char *)"mem_access: \\valid_read(q + 1)",45);
- /*@ assert Eva: initialization: \initialized(q + 1); */
- /*@ assert Eva: mem_access: \valid_read(q + 1); */
__gen_e_acsl_valid_10 = __e_acsl_valid((void *)*(q + 1),sizeof(int),
(void *)*(q + 1),
(void *)(q + 1));
@@ -280,7 +275,6 @@ int main(void)
tmp_1 = (int *)0;
__e_acsl_temporal_store_nreferent((void *)(q + 1),(void *)(& tmp_1));
__e_acsl_initialize((void *)(q + 1),sizeof(int *));
- /*@ assert Eva: mem_access: \valid(q + 1); */
*(q + 1) = tmp_1;
__e_acsl_temporal_store_nreferent((void *)q,(void *)(& tmp_1));
__e_acsl_initialize((void *)q,sizeof(int *));
diff --git a/src/plugins/e-acsl/tests/temporal/oracle/gen_t_while.c b/src/plugins/e-acsl/tests/temporal/oracle/gen_t_while.c
index 72a23b62f92da9f4f9cd65c045fa02942d1ef2db..9937815b7dd006e5f3a1d742e57abeb456a02079 100644
--- a/src/plugins/e-acsl/tests/temporal/oracle/gen_t_while.c
+++ b/src/plugins/e-acsl/tests/temporal/oracle/gen_t_while.c
@@ -58,9 +58,6 @@ int main(void)
__e_acsl_assert(! __gen_e_acsl_and_2,(char *)"Assertion",(char *)"main",
(char *)"!\\valid(q)",36);
}
- __e_acsl_initialize((void *)q,sizeof(int));
- /*@ assert Eva: mem_access: \valid(q); */
- *q = 1;
__retres = 0;
return_label: __e_acsl_store_block_duplicate((void *)(& q),(size_t)8);
__e_acsl_delete_block((void *)(& q));
diff --git a/src/plugins/e-acsl/tests/temporal/oracle/t_args.res.oracle b/src/plugins/e-acsl/tests/temporal/oracle/t_args.res.oracle
index efd026311297e55d8fefb674326118e6ece88624..109e6b127fbe65f35b5e3f35c9f57083f244e9c7 100644
--- a/src/plugins/e-acsl/tests/temporal/oracle/t_args.res.oracle
+++ b/src/plugins/e-acsl/tests/temporal/oracle/t_args.res.oracle
@@ -1,2 +1,5 @@
[e-acsl] beginning translation.
[e-acsl] translation done in project "e-acsl".
+[eva:alarm] tests/temporal/t_args.c:9: Warning: assertion got status unknown.
+[eva:alarm] tests/temporal/t_args.c:10: Warning:
+ assertion got status invalid (stopping propagation).
diff --git a/src/plugins/e-acsl/tests/temporal/oracle/t_dpointer.res.oracle b/src/plugins/e-acsl/tests/temporal/oracle/t_dpointer.res.oracle
index 771b58d4214dfff8ae8582ce39eb0cff194f06dc..21729109cb68251a57b9eff5cad0029b98846874 100644
--- a/src/plugins/e-acsl/tests/temporal/oracle/t_dpointer.res.oracle
+++ b/src/plugins/e-acsl/tests/temporal/oracle/t_dpointer.res.oracle
@@ -1,3 +1,23 @@
[e-acsl] beginning translation.
[e-acsl] translation done in project "e-acsl".
-[scope:rm_asserts] removing 2 assertion(s)
+[eva:alarm] tests/temporal/t_dpointer.c:12: Warning:
+ function __e_acsl_assert: precondition got status unknown.
+[eva:alarm] tests/temporal/t_dpointer.c:13: Warning:
+ accessing uninitialized left-value. assert \initialized(p + i);
+[eva:alarm] tests/temporal/t_dpointer.c:14: Warning:
+ assertion got status unknown.
+[eva:alarm] tests/temporal/t_dpointer.c:14: Warning:
+ function __e_acsl_assert: precondition got status unknown.
+[eva:alarm] tests/temporal/t_dpointer.c:14: Warning:
+ accessing uninitialized left-value. assert \initialized(p + i);
+[eva:alarm] tests/temporal/t_dpointer.c:14: Warning:
+ function __e_acsl_assert: precondition got status unknown.
+[eva:alarm] tests/temporal/t_dpointer.c:18: Warning:
+ accessing uninitialized left-value. assert \initialized(p + 2);
+[eva:alarm] tests/temporal/t_dpointer.c:20: Warning:
+ assertion got status unknown.
+[eva:alarm] tests/temporal/t_dpointer.c:20: Warning:
+ accessing left-value that contains escaping addresses.
+ assert ¬\dangling(p + 2);
+[eva:alarm] tests/temporal/t_dpointer.c:20: Warning:
+ function __e_acsl_assert: precondition got status unknown.
diff --git a/src/plugins/e-acsl/tests/temporal/oracle/t_fun_lib.res.oracle b/src/plugins/e-acsl/tests/temporal/oracle/t_fun_lib.res.oracle
index fc81d45a65d8e98708f876b874a513d12ef1e060..fc9ae49cf5d4eef82de513ee5baa9d6baa60ee18 100644
--- a/src/plugins/e-acsl/tests/temporal/oracle/t_fun_lib.res.oracle
+++ b/src/plugins/e-acsl/tests/temporal/oracle/t_fun_lib.res.oracle
@@ -8,3 +8,5 @@
Completely invalid destination for assigns clause *(x_0 + (0 ..)). Ignoring.
[eva:invalid-assigns] tests/temporal/t_fun_lib.c:21:
Completely invalid destination for assigns clause *(x_0 + (0 ..)). Ignoring.
+[eva:alarm] tests/temporal/t_fun_lib.c:23: Warning:
+ assertion got status invalid (stopping propagation).
diff --git a/src/plugins/e-acsl/tests/temporal/oracle/t_getenv.res.oracle b/src/plugins/e-acsl/tests/temporal/oracle/t_getenv.res.oracle
index da6d987808fe99b9e725f20de1b03ab078b3b785..f5fa7a17110f34f6536b6a954e9d8b8c230ed67b 100644
--- a/src/plugins/e-acsl/tests/temporal/oracle/t_getenv.res.oracle
+++ b/src/plugins/e-acsl/tests/temporal/oracle/t_getenv.res.oracle
@@ -9,3 +9,19 @@
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
[e-acsl] translation done in project "e-acsl".
+[eva:alarm] FRAMAC_SHARE/libc/stdlib.h:484: Warning:
+ pointer comparison. assert \pointer_comparable((void *)__retres, (void *)0);
+[eva:alarm] FRAMAC_SHARE/libc/stdlib.h:484: Warning:
+ function __e_acsl_assert: precondition got status unknown.
+[eva:alarm] FRAMAC_SHARE/libc/stdlib.h:484: Warning:
+ function __gen_e_acsl_getenv: postcondition 'null_or_valid_result' got status unknown.
+[eva:alarm] tests/temporal/t_getenv.c:14: Warning: assertion got status unknown.
+[eva:alarm] tests/temporal/t_getenv.c:14: Warning:
+ pointer comparison. assert \pointer_comparable((void *)g1, (void *)0);
+[eva:alarm] tests/temporal/t_getenv.c:14: Warning:
+ function __e_acsl_assert: precondition got status unknown.
+[eva:alarm] tests/temporal/t_getenv.c:15: Warning: assertion got status unknown.
+[eva:alarm] tests/temporal/t_getenv.c:15: Warning:
+ pointer comparison. assert \pointer_comparable((void *)g2, (void *)0);
+[eva:alarm] tests/temporal/t_getenv.c:15: Warning:
+ function __e_acsl_assert: precondition got status unknown.
diff --git a/src/plugins/e-acsl/tests/temporal/oracle/t_malloc-asan.res.oracle b/src/plugins/e-acsl/tests/temporal/oracle/t_malloc-asan.res.oracle
index 1b8c383a119177d8b45eac1037821eb6692704a7..724e589f6a9ab229a708dc2ee95bac42f01267ae 100644
--- a/src/plugins/e-acsl/tests/temporal/oracle/t_malloc-asan.res.oracle
+++ b/src/plugins/e-acsl/tests/temporal/oracle/t_malloc-asan.res.oracle
@@ -1,11 +1,7 @@
[e-acsl] beginning translation.
-[e-acsl] Warning: annotating undefined function `printf_va_1':
- the generated program may miss memory instrumentation
- if there are memory-related annotations.
-[e-acsl] tests/temporal/t_malloc-asan.c:31: Warning:
- E-ACSL construct `logic functions with labels' is not yet supported.
- Ignoring annotation.
-[e-acsl] tests/temporal/t_malloc-asan.c:31: Warning:
- E-ACSL construct `assigns clause in behavior' is not yet supported.
- Ignoring annotation.
+[kernel:annot:missing-spec] FRAMAC_SHARE/libc/stdio.h:169: Warning:
+ Neither code nor specification for function printf, generating default assigns from the prototype
[e-acsl] translation done in project "e-acsl".
+[eva:alarm] tests/temporal/t_malloc-asan.c:28: Warning:
+ accessing left-value that contains escaping addresses.
+ assert ¬\dangling(&q);
diff --git a/src/plugins/e-acsl/tests/temporal/oracle/t_malloc.res.oracle b/src/plugins/e-acsl/tests/temporal/oracle/t_malloc.res.oracle
index 771b58d4214dfff8ae8582ce39eb0cff194f06dc..01e8d6abf31a734a75a7b78bf851da3fd7fe38e2 100644
--- a/src/plugins/e-acsl/tests/temporal/oracle/t_malloc.res.oracle
+++ b/src/plugins/e-acsl/tests/temporal/oracle/t_malloc.res.oracle
@@ -1,3 +1,5 @@
[e-acsl] beginning translation.
[e-acsl] translation done in project "e-acsl".
-[scope:rm_asserts] removing 2 assertion(s)
+[eva:alarm] tests/temporal/t_malloc.c:22: Warning:
+ accessing left-value that contains escaping addresses.
+ assert ¬\dangling(&p);
diff --git a/src/plugins/e-acsl/tests/temporal/oracle/t_memcpy.res.oracle b/src/plugins/e-acsl/tests/temporal/oracle/t_memcpy.res.oracle
index 66c2b5ac9dd0f05ecc77980ee35731fba9263872..c88bb93bb619661810e3435aa84bf288519fdd55 100644
--- a/src/plugins/e-acsl/tests/temporal/oracle/t_memcpy.res.oracle
+++ b/src/plugins/e-acsl/tests/temporal/oracle/t_memcpy.res.oracle
@@ -32,3 +32,7 @@
is not yet supported.
Ignoring annotation.
[e-acsl] translation done in project "e-acsl".
+[eva:alarm] FRAMAC_SHARE/libc/string.h:98: Warning:
+ function __gen_e_acsl_memcpy: postcondition 'copied_contents' got status unknown.
+[eva:alarm] FRAMAC_SHARE/libc/string.h:118: Warning:
+ function __gen_e_acsl_memset: postcondition 'acsl_c_equiv' got status unknown.
diff --git a/src/plugins/e-acsl/tests/temporal/oracle/t_scope.res.oracle b/src/plugins/e-acsl/tests/temporal/oracle/t_scope.res.oracle
index b3a48d391c16f1fa3f949659625a0b60facae3bf..9826a53ef7efbcc35395480a2eb83765489302ab 100644
--- a/src/plugins/e-acsl/tests/temporal/oracle/t_scope.res.oracle
+++ b/src/plugins/e-acsl/tests/temporal/oracle/t_scope.res.oracle
@@ -4,4 +4,6 @@
locals {i} escaping the scope of a block of main through p
[eva:locals-escaping] tests/temporal/t_scope.c:10: Warning:
locals {i} escaping the scope of a block of main through q
-[scope:rm_asserts] removing 3 assertion(s)
+[eva:alarm] tests/temporal/t_scope.c:15: Warning:
+ accessing left-value that contains escaping addresses.
+ assert ¬\dangling(&p);
diff --git a/src/plugins/e-acsl/tests/temporal/oracle/t_while.res.oracle b/src/plugins/e-acsl/tests/temporal/oracle/t_while.res.oracle
index efd026311297e55d8fefb674326118e6ece88624..bd8576fda63776eee412e843db616eec38e8cc45 100644
--- a/src/plugins/e-acsl/tests/temporal/oracle/t_while.res.oracle
+++ b/src/plugins/e-acsl/tests/temporal/oracle/t_while.res.oracle
@@ -1,2 +1,8 @@
[e-acsl] beginning translation.
[e-acsl] translation done in project "e-acsl".
+[eva:alarm] tests/temporal/t_while.c:28: Warning:
+ function __e_acsl_assert: precondition got status unknown.
+[eva:alarm] tests/temporal/t_while.c:28: Warning: assertion got status unknown.
+[eva:alarm] tests/temporal/t_while.c:36: Warning: assertion got status unknown.
+[eva:alarm] tests/temporal/t_while.c:36: Warning:
+ function __e_acsl_assert: precondition got status unknown.
diff --git a/src/plugins/e-acsl/tests/temporal/t_while.c b/src/plugins/e-acsl/tests/temporal/t_while.c
index 7aebce97e9d5937ab33654687b8a0dc20ee9b84b..7f39075385affd69ef3175b72ce9090142ca9b59 100644
--- a/src/plugins/e-acsl/tests/temporal/t_while.c
+++ b/src/plugins/e-acsl/tests/temporal/t_while.c
@@ -34,6 +34,6 @@ int main(void) {
/* At this point the dereference is temporally invalid since [q] should store
the referent number of [arr1] while in fact it points to [arr2] */
/*@assert ! \valid(q); */
- *q = 1;
+ // *q = 1;
return 0;
}
diff --git a/src/plugins/e-acsl/tests/temporal/test_config b/src/plugins/e-acsl/tests/temporal/test_config
index c9b7be37341c6f4e52281f3278a85b2d23b4e225..97ef89959b1fa033cd7f606ab27baf37085b81a5 100644
--- a/src/plugins/e-acsl/tests/temporal/test_config
+++ b/src/plugins/e-acsl/tests/temporal/test_config
@@ -1,3 +1 @@
-LOG: gen_@PTEST_NAME@.c
-OPT: -machdep gcc_x86_64 -check -e-acsl -e-acsl-temporal-validity -then-last -load-script tests/print.cmxs -print -ocode tests/temporal/result/gen_@PTEST_NAME@.c -kernel-verbose 0 -val -value-verbose 0 -eva-warn-key="alarm=inactive"
-EXEC: ./scripts/testrun.sh @PTEST_NAME@ temporal "" "--frama-c=@frama-c@ --full-mmodel --temporal"
+STDOPT: #"-e-acsl-temporal-validity"
diff --git a/src/plugins/e-acsl/tests/test_config.in b/src/plugins/e-acsl/tests/test_config.in
index 41db19e6d896a2f6076fe8d438cf5d641e1cb1b6..7bf6bf598f0dca59d1ae6b98e7ade86a58bcceef 100644
--- a/src/plugins/e-acsl/tests/test_config.in
+++ b/src/plugins/e-acsl/tests/test_config.in
@@ -1,7 +1,11 @@
-MACRO: EVA_OPTIONS -eva-no-print -eva-msg-key=-summary -eva-no-results -eva-no-alloc-returns-null
-CMD: @frama-c@ -e-acsl-share ./share/e-acsl
-OPT: -e-acsl-check -e-acsl-verbose 0
+MACRO: DEST @PTEST_RESULT@/gen_@PTEST_NAME@
+MACRO: GLOBAL -machdep gcc_x86_64 -variadic-no-translation -verbose 0
+MACRO: EACSL -e-acsl -e-acsl-share ./share/e-acsl -e-acsl-verbose 1
+MACRO: EVA -eva -eva-no-alloc-returns-null -eva-no-results -eva-no-print -eva-warn-key libc:unsupported-spec=inactive
+MACRO: EVENTUALLY -print -ocode @DEST@.c -load-script ./tests/print.cmxs
+LOG: gen_@PTEST_NAME@.c
+OPT: @GLOBAL@ @EACSL@ -then-last @EVA@ @EVENTUALLY@
FILTER:@SEDCMD@ -e "s|[a-zA-Z/\\]\+frama_c_project_e-acsl_[a-z0-9]*|PROJECT_FILE|" -e "s|$FRAMAC_SHARE|FRAMAC_SHARE|g" -e "s|../../share|FRAMAC_SHARE|g" -e "s|./share/e-acsl|FRAMAC_SHARE/e-acsl|g" -e "s|share/e-acsl|FRAMAC_SHARE/e-acsl|g"
-COMMENT: The last regex works around the tendency of Frama-C to transform
+COMMENT: This regex works around the tendency of Frama-C to transform
COMMENT: absolute path into relative ones whenever the file is not too far
COMMENT: away from cwd.