diff --git a/src/plugins/e-acsl/Makefile.in b/src/plugins/e-acsl/Makefile.in
index 3d3906f75733a327c680d133eb8b2925c2a68d6a..c65ee7fc37ac62d05fe10711f2df2c334cf27b75 100644
--- a/src/plugins/e-acsl/Makefile.in
+++ b/src/plugins/e-acsl/Makefile.in
@@ -176,6 +176,7 @@ PLUGIN_TESTS_DIRS := \
language_constructs \
arith \
memory \
+ gmp-only \
full-mmodel \
format \
temporal \
diff --git a/src/plugins/e-acsl/tests/arith/oracle/arith.0.res.oracle b/src/plugins/e-acsl/tests/arith/oracle/arith.0.res.oracle
deleted file mode 100644
index 3ef62b7790e061fd4ac0f78b5019b26de3768a85..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/arith/oracle/arith.0.res.oracle
+++ /dev/null
@@ -1,32 +0,0 @@
-[e-acsl] beginning translation.
-[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]
-[eva] using specification for function __e_acsl_memory_init
-[eva] using specification for function __e_acsl_assert
-[eva] using specification for function __gmpz_init_set_str
-[eva] using specification for function __gmpz_init_set_si
-[eva] using specification for function __gmpz_cmp
-[eva] using specification for function __gmpz_init
-[eva:alarm] tests/gmp/arith.i:18: Warning:
- function __e_acsl_assert: precondition got status unknown.
-[eva] using specification for function __gmpz_tdiv_q
-[eva] using specification for function __gmpz_get_si
-[eva] using specification for function __gmpz_clear
-[eva] using specification for function __gmpz_add
-[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.
-[eva] done for function main
diff --git a/src/plugins/e-acsl/tests/arith/oracle/arith.1.res.oracle b/src/plugins/e-acsl/tests/arith/oracle/arith.1.res.oracle
deleted file mode 100644
index 03a8b877a7d7b268d726797bf9a0bef61c5d60da..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/arith/oracle/arith.1.res.oracle
+++ /dev/null
@@ -1,69 +0,0 @@
-[e-acsl] beginning translation.
-[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]
-[eva] using specification for function __e_acsl_memory_init
-[eva] using specification for function __gmpz_init_set_si
-[eva] using specification for function __gmpz_init
-[eva] using specification for function __gmpz_neg
-[eva] using specification for function __gmpz_cmp
-[eva] using specification for function __e_acsl_assert
-[eva:alarm] tests/gmp/arith.i:10: Warning:
- function __e_acsl_assert: precondition got status unknown.
-[eva] using specification for function __gmpz_clear
-[eva:alarm] tests/gmp/arith.i:11: Warning:
- function __e_acsl_assert: precondition got status unknown.
-[eva] using specification for function __gmpz_com
-[eva:alarm] tests/gmp/arith.i:12: Warning:
- function __e_acsl_assert: precondition got status unknown.
-[eva] using specification for function __gmpz_add
-[eva:alarm] tests/gmp/arith.i:14: Warning:
- function __e_acsl_assert: precondition got status unknown.
-[eva] using specification for function __gmpz_sub
-[eva:alarm] tests/gmp/arith.i:15: Warning:
- function __e_acsl_assert: precondition got status unknown.
-[eva] using specification for function __gmpz_mul
-[eva:alarm] tests/gmp/arith.i:16: Warning:
- function __e_acsl_assert: precondition got status unknown.
-[eva:alarm] tests/gmp/arith.i:17: Warning:
- function __e_acsl_assert: precondition got status unknown.
-[eva] using specification for function __gmpz_tdiv_q
-[eva] using specification for function __gmpz_init_set_str
-[eva:alarm] tests/gmp/arith.i:18: Warning:
- function __e_acsl_assert: precondition got status unknown.
-[eva:alarm] tests/gmp/arith.i:19: Warning:
- function __e_acsl_assert: precondition got status unknown.
-[eva] using specification for function __gmpz_tdiv_r
-[eva:alarm] tests/gmp/arith.i:20: Warning:
- function __e_acsl_assert: precondition got status unknown.
-[eva:alarm] tests/gmp/arith.i:21: Warning:
- function __e_acsl_assert: precondition got status unknown.
-[eva:alarm] tests/gmp/arith.i:23: Warning:
- function __e_acsl_assert: precondition got status unknown.
-[eva:alarm] tests/gmp/arith.i:25: Warning:
- function __e_acsl_assert: precondition got status unknown.
-[eva:alarm] tests/gmp/arith.i:26: Warning:
- function __e_acsl_assert: precondition got status unknown.
-[eva:alarm] tests/gmp/arith.i:27: Warning:
- function __e_acsl_assert: precondition got status unknown.
-[eva:alarm] tests/gmp/arith.i:28: Warning:
- function __e_acsl_assert: precondition got status unknown.
-[eva:alarm] tests/gmp/arith.i:30: Warning:
- function __e_acsl_assert: precondition got status unknown.
-[eva:alarm] tests/gmp/arith.i:31: Warning:
- function __e_acsl_assert: precondition got status unknown.
-[eva] using specification for function __gmpz_init_set_ui
-[eva:alarm] tests/gmp/arith.i:34: 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:36: Warning:
- function __e_acsl_assert: precondition got status unknown.
-[eva] done for function main
diff --git a/src/plugins/e-acsl/tests/arith/oracle/array.0.res.oracle b/src/plugins/e-acsl/tests/arith/oracle/array.0.res.oracle
deleted file mode 100644
index 89ea2c8602c1745a92b34e4ad5996e3393d1e946..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/arith/oracle/array.0.res.oracle
+++ /dev/null
@@ -1,24 +0,0 @@
-[e-acsl] beginning translation.
-[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]
- T1[0..2] ∈ {0}
- T2[0..3] ∈ {0}
-[eva] using specification for function __e_acsl_memory_init
-[eva] tests/gmp/array.i:10: starting to merge loop iterations
-[eva] tests/gmp/array.i:11: starting to merge loop iterations
-[eva:alarm] tests/gmp/array.i:13: Warning: assertion got status unknown.
-[eva] using specification for function __e_acsl_assert
-[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.
-[eva] done for function main
diff --git a/src/plugins/e-acsl/tests/arith/oracle/array.1.res.oracle b/src/plugins/e-acsl/tests/arith/oracle/array.1.res.oracle
deleted file mode 100644
index 83ca5f03f31bb4769d3c854ed013cd215a368fb1..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/arith/oracle/array.1.res.oracle
+++ /dev/null
@@ -1,27 +0,0 @@
-[e-acsl] beginning translation.
-[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]
- T1[0..2] ∈ {0}
- T2[0..3] ∈ {0}
-[eva] using specification for function __e_acsl_memory_init
-[eva] tests/gmp/array.i:10: starting to merge loop iterations
-[eva] tests/gmp/array.i:11: starting to merge loop iterations
-[eva:alarm] tests/gmp/array.i:13: Warning: assertion got status unknown.
-[eva] using specification for function __gmpz_init_set_si
-[eva] using specification for function __gmpz_cmp
-[eva] using specification for function __e_acsl_assert
-[eva:alarm] tests/gmp/array.i:13: Warning:
- function __e_acsl_assert: precondition got status unknown.
-[eva] using specification for function __gmpz_clear
-[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.
-[eva] done for function main
diff --git a/src/plugins/e-acsl/tests/arith/oracle/at.0.res.oracle b/src/plugins/e-acsl/tests/arith/oracle/at.0.res.oracle
deleted file mode 100644
index 32eac07f54ef1084f71b0d0bc0a4ea23106f840a..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/arith/oracle/at.0.res.oracle
+++ /dev/null
@@ -1,43 +0,0 @@
-[e-acsl] beginning translation.
-[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]
- A ∈ {0}
- __e_acsl_sound_verdict ∈ [--..--]
-[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_delete_block
-[eva] using specification for function __e_acsl_assert
-[eva] tests/gmp/at.i:12:
- cannot evaluate ACSL term, \at() on a C label is unsupported
-[eva:alarm] tests/gmp/at.i:12: Warning: assertion got status unknown.
-[eva] tests/gmp/at.i:14:
- cannot evaluate ACSL term, \at() on a C label is unsupported
-[eva:alarm] tests/gmp/at.i:14: Warning: assertion got status unknown.
-[eva] tests/gmp/at.i:48:
- cannot evaluate ACSL term, \at() on a C label is unsupported
-[eva:alarm] tests/gmp/at.i:48: Warning: assertion got status unknown.
-[eva] tests/gmp/at.i:49:
- cannot evaluate ACSL term, \at() on a C label is unsupported
-[eva:alarm] tests/gmp/at.i:49: Warning: assertion got status unknown.
-[eva] tests/gmp/at.i:50:
- cannot evaluate ACSL term, \at() on a C label is unsupported
-[eva:alarm] tests/gmp/at.i:50: Warning: assertion got status unknown.
-[eva] using specification for function __e_acsl_initialize
-[eva] using specification for function __e_acsl_valid_read
-[eva] tests/gmp/at.i:26:
- cannot evaluate ACSL term, \at() on a C label is unsupported
-[eva:alarm] tests/gmp/at.i:26: Warning: assertion got status unknown.
-[eva] tests/gmp/at.i:28:
- cannot evaluate ACSL term, \at() on a C label is unsupported
-[eva:alarm] tests/gmp/at.i:28: Warning: assertion got status unknown.
-[eva] using specification for function __e_acsl_memory_clean
-[eva] done for function main
diff --git a/src/plugins/e-acsl/tests/arith/oracle/at.1.res.oracle b/src/plugins/e-acsl/tests/arith/oracle/at.1.res.oracle
deleted file mode 100644
index 8fd885d000d4d337ff55accb89e24169746717cf..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/arith/oracle/at.1.res.oracle
+++ /dev/null
@@ -1,77 +0,0 @@
-[e-acsl] beginning translation.
-[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]
- A ∈ {0}
- __e_acsl_sound_verdict ∈ [--..--]
-[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 __gmpz_init_set_si
-[eva] using specification for function __gmpz_init_set
-[eva] using specification for function __gmpz_clear
-[eva] using specification for function __e_acsl_delete_block
-[eva] using specification for function __gmpz_cmp
-[eva] using specification for function __e_acsl_assert
-[eva:alarm] tests/gmp/at.i:35: Warning:
- function __e_acsl_assert: precondition got status unknown.
-[eva] using specification for function __gmpz_init
-[eva] using specification for function __gmpz_add
-[eva:alarm] tests/gmp/at.i:43: Warning:
- function __gmpz_init_set: precondition ¬\initialized(z) got status unknown.
-[eva:alarm] tests/gmp/at.i:43: Warning:
- function __e_acsl_assert: precondition got status unknown.
-[eva:alarm] tests/gmp/at.i:9: Warning:
- function __gmpz_init_set: precondition ¬\initialized(z) got status unknown.
-[eva:alarm] tests/gmp/at.i:11: Warning:
- function __e_acsl_assert: precondition got status unknown.
-[eva] tests/gmp/at.i:12:
- cannot evaluate ACSL term, \at() on a C label is unsupported
-[eva:alarm] tests/gmp/at.i:12: Warning: assertion got status unknown.
-[eva:alarm] tests/gmp/at.i:12: Warning:
- function __e_acsl_assert: precondition got status unknown.
-[eva:alarm] tests/gmp/at.i:13: Warning:
- function __e_acsl_assert: precondition got status unknown.
-[eva] tests/gmp/at.i:14:
- cannot evaluate ACSL term, \at() on a C label is unsupported
-[eva:alarm] tests/gmp/at.i:14: Warning: assertion got status unknown.
-[eva:alarm] tests/gmp/at.i:14: Warning:
- function __e_acsl_assert: precondition got status unknown.
-[eva:alarm] tests/gmp/at.i:7: Warning:
- function __e_acsl_assert: precondition got status unknown.
-[eva] tests/gmp/at.i:48:
- cannot evaluate ACSL term, \at() on a C label is unsupported
-[eva:alarm] tests/gmp/at.i:48: Warning: assertion got status unknown.
-[eva:alarm] tests/gmp/at.i:48: Warning:
- function __e_acsl_assert: precondition got status unknown.
-[eva] tests/gmp/at.i:49:
- cannot evaluate ACSL term, \at() on a C label is unsupported
-[eva:alarm] tests/gmp/at.i:49: Warning: assertion got status unknown.
-[eva:alarm] tests/gmp/at.i:49: Warning:
- function __e_acsl_assert: precondition got status unknown.
-[eva] tests/gmp/at.i:50:
- cannot evaluate ACSL term, \at() on a C label is unsupported
-[eva:alarm] tests/gmp/at.i:50: Warning: assertion got status unknown.
-[eva:alarm] tests/gmp/at.i:50: Warning:
- function __e_acsl_assert: precondition got status unknown.
-[eva] using specification for function __e_acsl_initialize
-[eva] using specification for function __e_acsl_valid_read
-[eva] tests/gmp/at.i:26:
- cannot evaluate ACSL term, \at() on a C label is unsupported
-[eva:alarm] tests/gmp/at.i:26: Warning: assertion got status unknown.
-[eva:alarm] tests/gmp/at.i:26: Warning:
- function __e_acsl_assert: precondition got status unknown.
-[eva] tests/gmp/at.i:28:
- cannot evaluate ACSL term, \at() on a C label is unsupported
-[eva:alarm] tests/gmp/at.i:28: Warning: assertion got status unknown.
-[eva:alarm] tests/gmp/at.i:28: Warning:
- function __e_acsl_assert: precondition got status unknown.
-[eva] using specification for function __e_acsl_memory_clean
-[eva] done for function main
diff --git a/src/plugins/e-acsl/tests/arith/oracle/at_on-purely-logic-variables.0.res.oracle b/src/plugins/e-acsl/tests/arith/oracle/at_on-purely-logic-variables.0.res.oracle
deleted file mode 100644
index db9bf51a98a39fbbb758d39bf869e1c07c263efb..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/arith/oracle/at_on-purely-logic-variables.0.res.oracle
+++ /dev/null
@@ -1,157 +0,0 @@
-[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] 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]
- __e_acsl_sound_verdict ∈ [--..--]
-[eva] using specification for function __e_acsl_memory_init
-[eva] tests/gmp/at_on-purely-logic-variables.c:57:
- allocating variable __malloc_main_l57
-[eva] tests/gmp/at_on-purely-logic-variables.c:45:
- allocating variable __malloc_main_l45
-[eva] tests/gmp/at_on-purely-logic-variables.c:41:
- allocating variable __malloc_main_l41
-[eva] tests/gmp/at_on-purely-logic-variables.c:37:
- allocating variable __malloc_main_l37
-[eva] tests/gmp/at_on-purely-logic-variables.c:34:
- allocating variable __malloc_main_l34
-[eva] tests/gmp/at_on-purely-logic-variables.c:29:
- allocating variable __malloc_main_l29
-[eva] tests/gmp/at_on-purely-logic-variables.c:28:
- allocating variable __malloc_main_l28
-[eva] using specification for function __e_acsl_store_block
-[eva] using specification for function __e_acsl_full_init
-[eva] tests/gmp/at_on-purely-logic-variables.c:29:
- starting to merge loop iterations
-[eva] tests/gmp/at_on-purely-logic-variables.c:57:
- starting to merge loop iterations
-[eva] tests/gmp/at_on-purely-logic-variables.c:45:
- starting to merge loop iterations
-[eva] tests/gmp/at_on-purely-logic-variables.c:34:
- starting to merge loop iterations
-[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:28: Warning:
- assertion got status unknown.
-[eva] using specification for function __e_acsl_valid_read
-[eva] using specification for function __e_acsl_assert
-[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] tests/gmp/at_on-purely-logic-variables.c:29:
- starting to merge loop iterations
-[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] tests/gmp/at_on-purely-logic-variables.c:33:
- starting to merge loop iterations
-[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] tests/gmp/at_on-purely-logic-variables.c:41:
- starting to merge loop iterations
-[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] tests/gmp/at_on-purely-logic-variables.c:41:
- starting to merge loop iterations
-[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] tests/gmp/at_on-purely-logic-variables.c:44:
- starting to merge loop iterations
-[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:45: Warning:
- function __e_acsl_assert: precondition got status unknown.
-[eva] tests/gmp/at_on-purely-logic-variables.c:8:
- allocating variable __malloc___gen_e_acsl_f_l8
-[eva] tests/gmp/at_on-purely-logic-variables.c:8:
- allocating variable __malloc___gen_e_acsl_f_l8_0
-[eva] tests/gmp/at_on-purely-logic-variables.c:7:
- allocating variable __malloc___gen_e_acsl_f_l7
-[eva] tests/gmp/at_on-purely-logic-variables.c:7:
- allocating variable __malloc___gen_e_acsl_f_l7_0
-[eva] tests/gmp/at_on-purely-logic-variables.c:7:
- starting to merge loop iterations
-[eva] tests/gmp/at_on-purely-logic-variables.c:7:
- starting to merge loop iterations
-[eva] using specification for function __e_acsl_delete_block
-[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] tests/gmp/at_on-purely-logic-variables.c:6:
- starting to merge loop iterations
-[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] tests/gmp/at_on-purely-logic-variables.c:16:
- allocating variable __malloc_g_l16
-[eva] tests/gmp/at_on-purely-logic-variables.c:16:
- starting to merge loop iterations
-[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] tests/gmp/at_on-purely-logic-variables.c:16:
- starting to merge loop iterations
-[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.
-[eva] using specification for function __e_acsl_memory_clean
-[eva] done for function main
diff --git a/src/plugins/e-acsl/tests/arith/oracle/at_on-purely-logic-variables.1.res.oracle b/src/plugins/e-acsl/tests/arith/oracle/at_on-purely-logic-variables.1.res.oracle
deleted file mode 100644
index 589d49adf20dd7b5fa5b20755d6815275e3080a5..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/arith/oracle/at_on-purely-logic-variables.1.res.oracle
+++ /dev/null
@@ -1,99 +0,0 @@
-[e-acsl] beginning translation.
-[e-acsl] tests/gmp/at_on-purely-logic-variables.c:16: 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:28: 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:29: 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:34: 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:37: Warning:
- E-ACSL construct `\at on purely logic variables and over gmp type'
- is not yet supported.
- Ignoring annotation.
-[e-acsl] tests/gmp/at_on-purely-logic-variables.c:41: Warning:
- E-ACSL construct `\at on purely logic variables and over gmp type'
- is not yet supported.
- Ignoring annotation.
-[e-acsl] tests/gmp/at_on-purely-logic-variables.c:45: Warning:
- E-ACSL construct
- `\at on purely logic variables and with quantifier that uses too complex bound (E-ACSL cannot infer a finite upper bound to it)'
- is not yet supported.
- Ignoring annotation.
-[e-acsl] tests/gmp/at_on-purely-logic-variables.c:57: 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: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] tests/gmp/at_on-purely-logic-variables.c:7: 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:8: 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] 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]
- __e_acsl_sound_verdict ∈ [--..--]
-[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: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:31: Warning:
- assertion 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:43: Warning:
- assertion got status unknown.
-[eva] using specification for function __e_acsl_delete_block
-[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:54: Warning:
- assertion got status unknown.
-[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.
-[eva] using specification for function __e_acsl_memory_clean
-[eva] done for function main
diff --git a/src/plugins/e-acsl/tests/arith/oracle/cast.0.res.oracle b/src/plugins/e-acsl/tests/arith/oracle/cast.0.res.oracle
deleted file mode 100644
index e7ac9d9dec4083d410b7ec698e1f64027c0cd3a8..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/arith/oracle/cast.0.res.oracle
+++ /dev/null
@@ -1,16 +0,0 @@
-[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".
-[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]
-[eva] using specification for function __e_acsl_memory_init
-[eva] using specification for function __e_acsl_assert
-[eva] done for function main
diff --git a/src/plugins/e-acsl/tests/arith/oracle/cast.1.res.oracle b/src/plugins/e-acsl/tests/arith/oracle/cast.1.res.oracle
deleted file mode 100644
index 33fc270fbf28281dcc2a2ae460b83b6a31648ae2..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/arith/oracle/cast.1.res.oracle
+++ /dev/null
@@ -1,35 +0,0 @@
-[e-acsl] beginning translation.
-[e-acsl] tests/gmp/cast.i:23: Warning:
- E-ACSL construct `reals: cast from R to Z' 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]
-[eva] using specification for function __e_acsl_memory_init
-[eva] using specification for function __gmpz_init_set_si
-[eva] using specification for function __gmpz_get_si
-[eva] using specification for function __gmpz_cmp
-[eva] using specification for function __e_acsl_assert
-[eva:alarm] tests/gmp/cast.i:10: Warning:
- function __e_acsl_assert: precondition got status unknown.
-[eva] using specification for function __gmpz_clear
-[eva:alarm] tests/gmp/cast.i:11: Warning:
- function __e_acsl_assert: precondition got status unknown.
-[eva:alarm] tests/gmp/cast.i:13: Warning:
- function __e_acsl_assert: precondition got status unknown.
-[eva] using specification for function __gmpz_get_ui
-[eva] using specification for function __gmpz_init_set_ui
-[eva:alarm] tests/gmp/cast.i:14: Warning:
- function __e_acsl_assert: precondition got status unknown.
-[eva:alarm] tests/gmp/cast.i:17: Warning:
- function __e_acsl_assert: precondition got status unknown.
-[eva:alarm] tests/gmp/cast.i:18: Warning:
- function __e_acsl_assert: precondition got status unknown.
-[eva] done for function main
diff --git a/src/plugins/e-acsl/tests/arith/oracle/comparison.0.res.oracle b/src/plugins/e-acsl/tests/arith/oracle/comparison.0.res.oracle
deleted file mode 100644
index 7046e21167e2fa05413d343de5b74544da9e443c..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/arith/oracle/comparison.0.res.oracle
+++ /dev/null
@@ -1,14 +0,0 @@
-[e-acsl] beginning translation.
-[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]
-[eva] using specification for function __e_acsl_memory_init
-[eva] using specification for function __e_acsl_assert
-[eva] done for function main
diff --git a/src/plugins/e-acsl/tests/arith/oracle/comparison.1.res.oracle b/src/plugins/e-acsl/tests/arith/oracle/comparison.1.res.oracle
deleted file mode 100644
index e8b574d9be6ff7ef3b90d3e1652d30e9e401ccdb..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/arith/oracle/comparison.1.res.oracle
+++ /dev/null
@@ -1,51 +0,0 @@
-[e-acsl] beginning translation.
-[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]
-[eva] using specification for function __e_acsl_memory_init
-[eva] using specification for function __gmpz_init_set_si
-[eva] using specification for function __gmpz_cmp
-[eva] using specification for function __e_acsl_assert
-[eva:alarm] tests/gmp/comparison.i:7: Warning:
- function __e_acsl_assert: precondition got status unknown.
-[eva] using specification for function __gmpz_clear
-[eva:alarm] tests/gmp/comparison.i:8: Warning:
- function __e_acsl_assert: precondition got status unknown.
-[eva:alarm] tests/gmp/comparison.i:9: Warning:
- function __e_acsl_assert: precondition got status unknown.
-[eva:alarm] tests/gmp/comparison.i:10: Warning:
- function __e_acsl_assert: precondition got status unknown.
-[eva:alarm] tests/gmp/comparison.i:15: Warning:
- function __e_acsl_assert: precondition got status unknown.
-[eva:alarm] tests/gmp/comparison.i:16: Warning:
- function __e_acsl_assert: precondition got status unknown.
-[eva:alarm] tests/gmp/comparison.i:17: Warning:
- function __e_acsl_assert: precondition got status unknown.
-[eva:alarm] tests/gmp/comparison.i:18: Warning:
- function __e_acsl_assert: precondition got status unknown.
-[eva:alarm] tests/gmp/comparison.i:19: Warning:
- function __e_acsl_assert: precondition got status unknown.
-[eva:alarm] tests/gmp/comparison.i:20: Warning:
- function __e_acsl_assert: precondition got status unknown.
-[eva] using specification for function __gmpz_init
-[eva] using specification for function __gmpz_neg
-[eva:alarm] tests/gmp/comparison.i:22: Warning:
- function __e_acsl_assert: precondition got status unknown.
-[eva:alarm] tests/gmp/comparison.i:23: Warning:
- function __e_acsl_assert: precondition got status unknown.
-[eva:alarm] tests/gmp/comparison.i:24: Warning:
- function __e_acsl_assert: precondition got status unknown.
-[eva:alarm] tests/gmp/comparison.i:25: Warning:
- function __e_acsl_assert: precondition got status unknown.
-[eva:alarm] tests/gmp/comparison.i:26: Warning:
- function __e_acsl_assert: precondition got status unknown.
-[eva:alarm] tests/gmp/comparison.i:27: Warning:
- function __e_acsl_assert: precondition got status unknown.
-[eva] done for function main
diff --git a/src/plugins/e-acsl/tests/arith/oracle/functions.0.res.oracle b/src/plugins/e-acsl/tests/arith/oracle/functions.0.res.oracle
deleted file mode 100644
index f20e6ae071aa0ada8c28355286c969718bbc003f..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/arith/oracle/functions.0.res.oracle
+++ /dev/null
@@ -1,41 +0,0 @@
-[e-acsl] beginning translation.
-[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]
- glob ∈ {5}
- __e_acsl_sound_verdict ∈ [--..--]
-[eva] using specification for function __e_acsl_memory_init
-[eva] using specification for function __e_acsl_assert
-[eva] using specification for function __gmpz_init_set_str
-[eva] using specification for function __gmpz_init_set_si
-[eva] using specification for function __gmpz_init
-[eva] using specification for function __gmpz_add
-[eva] using specification for function __gmpz_cmp
-[eva] using specification for function __gmpz_clear
-[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] using specification for function __gmpz_init_set
-[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] using specification for function __gmpq_init
-[eva] using specification for function __gmpq_set_str
-[eva] using specification for function __gmpq_set_d
-[eva] using specification for function __gmpq_div
-[eva] using specification for function __gmpq_get_d
-[eva] using specification for function __gmpq_clear
-[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.
-[eva] done for function main
diff --git a/src/plugins/e-acsl/tests/arith/oracle/functions.1.res.oracle b/src/plugins/e-acsl/tests/arith/oracle/functions.1.res.oracle
deleted file mode 100644
index f284f855063f4db71d25017acdbf33b569c77493..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/arith/oracle/functions.1.res.oracle
+++ /dev/null
@@ -1,60 +0,0 @@
-[e-acsl] beginning translation.
-[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]
- glob ∈ {5}
- __e_acsl_sound_verdict ∈ [--..--]
-[eva] using specification for function __e_acsl_memory_init
-[eva] using specification for function __gmpz_init_set_si
-[eva] using specification for function __gmpz_init
-[eva] using specification for function __gmpz_add
-[eva] using specification for function __gmpz_cmp
-[eva] using specification for function __gmpz_clear
-[eva] using specification for function __e_acsl_assert
-[eva:alarm] tests/gmp/functions.c:42: Warning:
- function __e_acsl_assert: precondition got status unknown.
-[eva:alarm] tests/gmp/functions.c:43: Warning:
- function __e_acsl_assert: precondition got status unknown.
-[eva] using specification for function __gmpz_init_set_str
-[eva:alarm] tests/gmp/functions.c:44: Warning:
- function __e_acsl_assert: precondition got status unknown.
-[eva] using specification for function __gmpz_init_set
-[eva:alarm] tests/gmp/functions.c:46: Warning:
- function __e_acsl_assert: precondition got status unknown.
-[eva:alarm] tests/gmp/functions.c:47: Warning:
- accessing uninitialized left-value.
- assert \initialized((__e_acsl_mpz_struct *)__gen_e_acsl_f1_4);
-[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:53: Warning:
- function __e_acsl_assert: precondition got status unknown.
-[eva:alarm] tests/gmp/functions.c:56: Warning:
- function __e_acsl_assert: precondition got status unknown.
-[eva:alarm] tests/gmp/functions.c:58: Warning:
- function __e_acsl_assert: precondition got status unknown.
-[eva:alarm] tests/gmp/functions.c:63: Warning:
- function __e_acsl_assert: precondition got status unknown.
-[eva:alarm] tests/gmp/functions.c:25: Warning:
- function __e_acsl_assert: precondition got status unknown.
-[eva] using specification for function __gmpq_init
-[eva] using specification for function __gmpq_set_str
-[eva] using specification for function __gmpq_set_d
-[eva] using specification for function __gmpq_div
-[eva] using specification for function __gmpq_get_d
-[eva] using specification for function __gmpq_clear
-[eva:alarm] tests/gmp/functions.c:68: Warning:
- non-finite double value. assert \is_finite(__gen_e_acsl__15);
-[eva:alarm] tests/gmp/functions.c:68: Warning:
- function __e_acsl_assert: precondition got status unknown.
-[eva] done for function main
diff --git a/src/plugins/e-acsl/tests/arith/oracle/functions_rec.0.res.oracle b/src/plugins/e-acsl/tests/arith/oracle/functions_rec.0.res.oracle
deleted file mode 100644
index cbf74d13ac79e1568bba0f82bc91e82493871cf4..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/arith/oracle/functions_rec.0.res.oracle
+++ /dev/null
@@ -1,87 +0,0 @@
-[e-acsl] beginning translation.
-[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]
-[eva] using specification for function __e_acsl_memory_init
-[eva] tests/gmp/functions_rec.c:26:
- cannot evaluate ACSL term, unsupported ACSL construct: logic function f2
-[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] using specification for function __gen_e_acsl_f2_2
-[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] using specification for function __e_acsl_assert
-[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] tests/gmp/functions_rec.c:28:
- cannot evaluate ACSL term, unsupported ACSL construct: logic function f3
-[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] using specification for function __gen_e_acsl_f3_2
-[eva] tests/gmp/functions_rec.c:30:
- cannot evaluate ACSL term, unsupported ACSL construct: logic function f4
-[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] using specification for function __gen_e_acsl_f4_2
-[eva:alarm] tests/gmp/functions_rec.c:30: Warning:
- function __e_acsl_assert: precondition got status unknown.
-[eva] done for function main
diff --git a/src/plugins/e-acsl/tests/arith/oracle/functions_rec.1.res.oracle b/src/plugins/e-acsl/tests/arith/oracle/functions_rec.1.res.oracle
deleted file mode 100644
index ad15ac476ccad3eb4c1c7c322456de28b5dc3c3f..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/arith/oracle/functions_rec.1.res.oracle
+++ /dev/null
@@ -1,116 +0,0 @@
-[e-acsl] beginning translation.
-[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]
-[eva] using specification for function __e_acsl_memory_init
-[eva] tests/gmp/functions_rec.c:26:
- cannot evaluate ACSL term, unsupported ACSL construct: logic function f2
-[eva:alarm] tests/gmp/functions_rec.c:26: Warning: assertion got status unknown.
-[eva] using specification for function __gmpz_init_set_si
-[eva] using specification for function __gmpz_cmp
-[eva] using specification for function __gmpz_init_set
-[eva] using specification for function __gmpz_clear
-[eva] using specification for function __gmpz_init
-[eva] using specification for function __gmpz_sub
-[eva:alarm] tests/gmp/functions_rec.c:10: Warning:
- accessing uninitialized left-value.
- assert \initialized((__e_acsl_mpz_struct *)__gen_e_acsl_sub);
-[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:
- accessing uninitialized left-value.
- assert \initialized((__e_acsl_mpz_struct *)__gen_e_acsl_sub_2);
-[eva] using specification for function __gen_e_acsl_f2_2
-[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:
- accessing uninitialized left-value.
- assert \initialized((__e_acsl_mpz_struct *)__gen_e_acsl_sub_3);
-[eva] using specification for function __gmpz_mul
-[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:
- accessing uninitialized left-value.
- assert \initialized((__e_acsl_mpz_struct *)__gen_e_acsl_sub_4);
-[eva] :0:
- cannot evaluate ACSL term, unsupported ACSL construct: logic function f2
-[eva:alarm] tests/gmp/functions_rec.c:10: Warning:
- assertion 'E_ACSL' got status unknown.
-[eva] using specification for function __e_acsl_assert
-[eva:alarm] tests/gmp/functions_rec.c:10: Warning:
- function __e_acsl_assert: precondition got status unknown.
-[eva] using specification for function __gmpz_tdiv_q
-[eva:alarm] tests/gmp/functions_rec.c:10: Warning:
- accessing uninitialized left-value.
- assert \initialized((__e_acsl_mpz_struct *)__gen_e_acsl_sub_5);
-[eva:alarm] tests/gmp/functions_rec.c:10: Warning:
- accessing uninitialized left-value.
- assert \initialized((__e_acsl_mpz_struct *)__gen_e_acsl_sub_6);
-[eva:alarm] tests/gmp/functions_rec.c:26: Warning:
- function __e_acsl_assert: precondition got status unknown.
-[eva] tests/gmp/functions_rec.c:28:
- cannot evaluate ACSL term, unsupported ACSL construct: logic function f3
-[eva:alarm] tests/gmp/functions_rec.c:28: Warning: assertion got status unknown.
-[eva:alarm] tests/gmp/functions_rec.c:14: Warning:
- accessing uninitialized left-value.
- assert \initialized((__e_acsl_mpz_struct *)__gen_e_acsl_sub_7);
-[eva] using specification for function __gmpz_get_si
-[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:14: Warning:
- accessing uninitialized left-value.
- assert \initialized((__e_acsl_mpz_struct *)__gen_e_acsl_sub_8);
-[eva] using specification for function __gen_e_acsl_f3_2
-[eva] using specification for function __gmpz_add
-[eva:alarm] tests/gmp/functions_rec.c:14: Warning:
- accessing uninitialized left-value.
- assert \initialized((__e_acsl_mpz_struct *)__gen_e_acsl_add);
-[eva:alarm] tests/gmp/functions_rec.c:14: Warning:
- accessing uninitialized left-value.
- assert \initialized((__e_acsl_mpz_struct *)__gen_e_acsl_add_2);
-[eva] using specification for function __gmpz_neg
-[eva:alarm] tests/gmp/functions_rec.c:28: Warning:
- function __e_acsl_assert: precondition got status unknown.
-[eva] tests/gmp/functions_rec.c:30:
- cannot evaluate ACSL term, unsupported ACSL construct: logic function f4
-[eva:alarm] tests/gmp/functions_rec.c:30: Warning: assertion got status unknown.
-[eva:alarm] tests/gmp/functions_rec.c:17: Warning:
- accessing uninitialized left-value.
- assert \initialized((__e_acsl_mpz_struct *)__gen_e_acsl_add_3);
-[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:17: Warning:
- accessing uninitialized left-value.
- assert \initialized((__e_acsl_mpz_struct *)__gen_e_acsl_add_4);
-[eva] using specification for function __gen_e_acsl_f4_2
-[eva] using specification for function __gmpz_init_set_ui
-[eva:alarm] tests/gmp/functions_rec.c:30: Warning:
- function __e_acsl_assert: precondition got status unknown.
-[eva] done for function main
diff --git a/src/plugins/e-acsl/tests/arith/oracle/gen_array2.c b/src/plugins/e-acsl/tests/arith/oracle/gen_array2.c
deleted file mode 100644
index 6f61fb210e9cf50361b4e61d509f2f193f589969..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/arith/oracle/gen_array2.c
+++ /dev/null
@@ -1,56 +0,0 @@
-/* Generated by Frama-C */
-#include "stdio.h"
-#include "stdlib.h"
-int T1[3];
-int T2[4];
-int main(void)
-{
- int __retres;
- __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
- {
- int i = 0;
- while (i < 3) {
- T1[i] = i;
- i ++;
- }
- }
- {
- int i_0 = 0;
- while (i_0 < 4) {
- T2[i_0] = 2 * i_0;
- i_0 ++;
- }
- }
- /*@ assert T1[0] ≡ T2[0]; */
- {
- __e_acsl_mpz_t __gen_e_acsl_;
- __e_acsl_mpz_t __gen_e_acsl__2;
- int __gen_e_acsl_eq;
- __gmpz_init_set_si(__gen_e_acsl_,(long)T1[0]);
- __gmpz_init_set_si(__gen_e_acsl__2,(long)T2[0]);
- __gen_e_acsl_eq = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__2));
- __e_acsl_assert(__gen_e_acsl_eq == 0,(char *)"Assertion",(char *)"main",
- (char *)"T1[0] == T2[0]",13);
- __gmpz_clear(__gen_e_acsl_);
- __gmpz_clear(__gen_e_acsl__2);
- }
- /*@ assert T1[1] ≢ T2[1]; */
- {
- __e_acsl_mpz_t __gen_e_acsl__3;
- __e_acsl_mpz_t __gen_e_acsl__4;
- int __gen_e_acsl_ne;
- __gmpz_init_set_si(__gen_e_acsl__3,(long)T1[1]);
- __gmpz_init_set_si(__gen_e_acsl__4,(long)T2[1]);
- __gen_e_acsl_ne = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl__3),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__4));
- __e_acsl_assert(__gen_e_acsl_ne != 0,(char *)"Assertion",(char *)"main",
- (char *)"T1[1] != T2[1]",14);
- __gmpz_clear(__gen_e_acsl__3);
- __gmpz_clear(__gen_e_acsl__4);
- }
- __retres = 0;
- return __retres;
-}
-
-
diff --git a/src/plugins/e-acsl/tests/arith/oracle/gen_at2.c b/src/plugins/e-acsl/tests/arith/oracle/gen_at2.c
deleted file mode 100644
index fa778073aa6c871f80084c715f59769fabf1af8e..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/arith/oracle/gen_at2.c
+++ /dev/null
@@ -1,366 +0,0 @@
-/* Generated by Frama-C */
-#include "stdio.h"
-#include "stdlib.h"
-extern int __e_acsl_sound_verdict;
-
-int A = 0;
-/*@ ensures \at(A,Post) ≡ 3; */
-void __gen_e_acsl_f(void);
-
-void f(void)
-{
- __e_acsl_mpz_t __gen_e_acsl_at_3;
- __e_acsl_mpz_t __gen_e_acsl_at_2;
- __e_acsl_mpz_t __gen_e_acsl_at;
- {
- __e_acsl_mpz_t __gen_e_acsl_A_4;
- __gmpz_init_set_si(__gen_e_acsl_A_4,(long)A);
- __gmpz_init_set(__gen_e_acsl_at,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_A_4));
- __gmpz_clear(__gen_e_acsl_A_4);
- }
- {
- __e_acsl_mpz_t __gen_e_acsl_A;
- __gmpz_init_set_si(__gen_e_acsl_A,(long)A);
- __gmpz_init_set(__gen_e_acsl_at,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_A));
- __gmpz_clear(__gen_e_acsl_A);
- }
- A = 1;
- F:
- {
- __gmpz_init_set(__gen_e_acsl_at_3,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_at));
- {
- __e_acsl_mpz_t __gen_e_acsl_A_2;
- __gmpz_init_set_si(__gen_e_acsl_A_2,(long)A);
- __gmpz_init_set(__gen_e_acsl_at_2,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_A_2));
- __gmpz_clear(__gen_e_acsl_A_2);
- }
- A = 2;
- }
- /*@ assert \at(A,Pre) ≡ 0; */
- {
- __e_acsl_mpz_t __gen_e_acsl_;
- int __gen_e_acsl_eq;
- __gmpz_init_set_si(__gen_e_acsl_,0L);
- __gen_e_acsl_eq = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_at),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_));
- __e_acsl_assert(__gen_e_acsl_eq == 0,(char *)"Assertion",(char *)"f",
- (char *)"\\at(A,Pre) == 0",11);
- __gmpz_clear(__gen_e_acsl_);
- }
- /*@ assert \at(A,F) ≡ 1; */
- {
- __e_acsl_mpz_t __gen_e_acsl__2;
- int __gen_e_acsl_eq_2;
- __gmpz_init_set_si(__gen_e_acsl__2,1L);
- __gen_e_acsl_eq_2 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_at_2),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__2));
- __e_acsl_assert(__gen_e_acsl_eq_2 == 0,(char *)"Assertion",(char *)"f",
- (char *)"\\at(A,F) == 1",12);
- __gmpz_clear(__gen_e_acsl__2);
- }
- /*@ assert \at(A,Here) ≡ 2; */
- {
- __e_acsl_mpz_t __gen_e_acsl_A_3;
- __e_acsl_mpz_t __gen_e_acsl__3;
- int __gen_e_acsl_eq_3;
- __gmpz_init_set_si(__gen_e_acsl_A_3,(long)A);
- __gmpz_init_set_si(__gen_e_acsl__3,2L);
- __gen_e_acsl_eq_3 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_A_3),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__3));
- __e_acsl_assert(__gen_e_acsl_eq_3 == 0,(char *)"Assertion",(char *)"f",
- (char *)"\\at(A,Here) == 2",13);
- __gmpz_clear(__gen_e_acsl_A_3);
- __gmpz_clear(__gen_e_acsl__3);
- }
- /*@ assert \at(\at(A,Pre),F) ≡ 0; */
- {
- __e_acsl_mpz_t __gen_e_acsl__4;
- int __gen_e_acsl_eq_4;
- __gmpz_init_set_si(__gen_e_acsl__4,0L);
- __gen_e_acsl_eq_4 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_at_3),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__4));
- __e_acsl_assert(__gen_e_acsl_eq_4 == 0,(char *)"Assertion",(char *)"f",
- (char *)"\\at(\\at(A,Pre),F) == 0",14);
- __gmpz_clear(__gen_e_acsl__4);
- }
- A = 3;
- __gmpz_clear(__gen_e_acsl_at);
- __gmpz_clear(__gen_e_acsl_at_2);
- __gmpz_clear(__gen_e_acsl_at_3);
- return;
-}
-
-void g(int *p, int *q)
-{
- int __gen_e_acsl_at_3;
- __e_acsl_mpz_t __gen_e_acsl_at_2;
- int __gen_e_acsl_at;
- __e_acsl_store_block((void *)(& q),(size_t)8);
- __e_acsl_store_block((void *)(& p),(size_t)8);
- __e_acsl_initialize((void *)p,sizeof(int));
- *p = 0;
- __e_acsl_initialize((void *)(p + 1),sizeof(int));
- *(p + 1) = 1;
- __e_acsl_initialize((void *)q,sizeof(int));
- *q = 0;
- L1:
- {
- {
- int __gen_e_acsl_valid_read_3;
- __gen_e_acsl_valid_read_3 = __e_acsl_valid_read((void *)q,sizeof(int),
- (void *)q,
- (void *)(& q));
- __e_acsl_assert(__gen_e_acsl_valid_read_3,(char *)"RTE",(char *)"g",
- (char *)"mem_access: \\valid_read(q)",28);
- __gen_e_acsl_at_3 = *q;
- }
- {
- int __gen_e_acsl_valid_read;
- __gen_e_acsl_valid_read = __e_acsl_valid_read((void *)q,sizeof(int),
- (void *)q,(void *)(& q));
- __e_acsl_assert(__gen_e_acsl_valid_read,(char *)"RTE",(char *)"g",
- (char *)"mem_access: \\valid_read(q)",26);
- __gen_e_acsl_at = *q;
- }
- __e_acsl_initialize((void *)p,sizeof(int));
- *p = 2;
- }
- __e_acsl_initialize((void *)(p + 1),sizeof(int));
- *(p + 1) = 3;
- __e_acsl_initialize((void *)q,sizeof(int));
- *q = 1;
- L2:
- {
- {
- int __gen_e_acsl_valid_read_2;
- __e_acsl_mpz_t __gen_e_acsl_;
- __gen_e_acsl_valid_read_2 = __e_acsl_valid_read((void *)(p + __gen_e_acsl_at),
- sizeof(int),(void *)p,
- (void *)(& p));
- __e_acsl_assert(__gen_e_acsl_valid_read_2,(char *)"RTE",(char *)"g",
- (char *)"mem_access: \\valid_read(p + __gen_e_acsl_at)",
- 26);
- __gmpz_init_set_si(__gen_e_acsl_,(long)*(p + __gen_e_acsl_at));
- __gmpz_init_set(__gen_e_acsl_at_2,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_));
- __gmpz_clear(__gen_e_acsl_);
- }
- A = 4;
- }
- /*@ assert \at(*(p + \at(*q,L1)),L2) ≡ 2; */
- {
- __e_acsl_mpz_t __gen_e_acsl__2;
- int __gen_e_acsl_eq;
- __gmpz_init_set_si(__gen_e_acsl__2,2L);
- __gen_e_acsl_eq = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_at_2),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__2));
- __e_acsl_assert(__gen_e_acsl_eq == 0,(char *)"Assertion",(char *)"g",
- (char *)"\\at(*(p + \\at(*q,L1)),L2) == 2",26);
- __gmpz_clear(__gen_e_acsl__2);
- }
- L3:
- /*@ assert \at(*(p + \at(*q,L1)),Here) ≡ 2; */
- {
- __e_acsl_mpz_t __gen_e_acsl__3;
- __e_acsl_mpz_t __gen_e_acsl__4;
- int __gen_e_acsl_eq_2;
- __gmpz_init_set_si(__gen_e_acsl__3,(long)*(p + __gen_e_acsl_at_3));
- __gmpz_init_set_si(__gen_e_acsl__4,2L);
- __gen_e_acsl_eq_2 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl__3),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__4));
- __e_acsl_assert(__gen_e_acsl_eq_2 == 0,(char *)"Assertion",(char *)"g",
- (char *)"\\at(*(p + \\at(*q,L1)),Here) == 2",28);
- __gmpz_clear(__gen_e_acsl__3);
- __gmpz_clear(__gen_e_acsl__4);
- }
- __e_acsl_delete_block((void *)(& q));
- __e_acsl_delete_block((void *)(& p));
- __gmpz_clear(__gen_e_acsl_at_2);
- return;
-}
-
-/*@ ensures \result ≡ \old(x); */
-int __gen_e_acsl_h(int x);
-
-int h(int x)
-{
- __e_acsl_store_block((void *)(& x),(size_t)4);
- __e_acsl_delete_block((void *)(& x));
- return x;
-}
-
-int main(void)
-{
- __e_acsl_mpz_t __gen_e_acsl_at_2;
- __e_acsl_mpz_t __gen_e_acsl_at;
- int __retres;
- int x;
- int t[2];
- __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
- __e_acsl_store_block((void *)(t),(size_t)8);
- __e_acsl_store_block((void *)(& x),(size_t)4);
- __e_acsl_full_init((void *)(& x));
- x = __gen_e_acsl_h(0);
- L:
- /*@ assert x ≡ 0; */
- {
- {
- __e_acsl_mpz_t __gen_e_acsl_x_4;
- __gmpz_init_set_si(__gen_e_acsl_x_4,(long)x);
- __gmpz_init_set(__gen_e_acsl_at,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_x_4));
- __gmpz_clear(__gen_e_acsl_x_4);
- }
- {
- __e_acsl_mpz_t __gen_e_acsl_x_3;
- __e_acsl_mpz_t __gen_e_acsl__3;
- __e_acsl_mpz_t __gen_e_acsl_add;
- __gmpz_init_set_si(__gen_e_acsl_x_3,(long)x);
- __gmpz_init_set_si(__gen_e_acsl__3,1L);
- __gmpz_init(__gen_e_acsl_add);
- __gmpz_add(__gen_e_acsl_add,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_x_3),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__3));
- __gmpz_init_set(__gen_e_acsl_at_2,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_add));
- __gmpz_clear(__gen_e_acsl_x_3);
- __gmpz_clear(__gen_e_acsl__3);
- __gmpz_clear(__gen_e_acsl_add);
- }
- {
- __e_acsl_mpz_t __gen_e_acsl_x_2;
- __gmpz_init_set_si(__gen_e_acsl_x_2,(long)x);
- __gmpz_init_set(__gen_e_acsl_at,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_x_2));
- __gmpz_clear(__gen_e_acsl_x_2);
- }
- {
- __e_acsl_mpz_t __gen_e_acsl_x;
- __e_acsl_mpz_t __gen_e_acsl_;
- int __gen_e_acsl_eq;
- __gmpz_init_set_si(__gen_e_acsl_x,(long)x);
- __gmpz_init_set_si(__gen_e_acsl_,0L);
- __gen_e_acsl_eq = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_x),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_));
- __e_acsl_assert(__gen_e_acsl_eq == 0,(char *)"Assertion",
- (char *)"main",(char *)"x == 0",43);
- __gmpz_clear(__gen_e_acsl_x);
- __gmpz_clear(__gen_e_acsl_);
- }
- }
- __e_acsl_full_init((void *)(& x));
- x = 1;
- __e_acsl_full_init((void *)(& x));
- x = 2;
- __gen_e_acsl_f();
- /*@ assert \at(x,L) ≡ 0; */
- {
- __e_acsl_mpz_t __gen_e_acsl__2;
- int __gen_e_acsl_eq_2;
- __gmpz_init_set_si(__gen_e_acsl__2,0L);
- __gen_e_acsl_eq_2 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_at),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__2));
- __e_acsl_assert(__gen_e_acsl_eq_2 == 0,(char *)"Assertion",
- (char *)"main",(char *)"\\at(x,L) == 0",48);
- __gmpz_clear(__gen_e_acsl__2);
- }
- /*@ assert \at(x + 1,L) ≡ 1; */
- {
- __e_acsl_mpz_t __gen_e_acsl__4;
- int __gen_e_acsl_eq_3;
- __gmpz_init_set_si(__gen_e_acsl__4,1L);
- __gen_e_acsl_eq_3 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_at_2),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__4));
- __e_acsl_assert(__gen_e_acsl_eq_3 == 0,(char *)"Assertion",
- (char *)"main",(char *)"\\at(x + 1,L) == 1",49);
- __gmpz_clear(__gen_e_acsl__4);
- }
- /*@ assert \at(x,L) + 1 ≡ 1; */
- {
- __e_acsl_mpz_t __gen_e_acsl__5;
- __e_acsl_mpz_t __gen_e_acsl_add_2;
- int __gen_e_acsl_eq_4;
- __gmpz_init_set_si(__gen_e_acsl__5,1L);
- __gmpz_init(__gen_e_acsl_add_2);
- __gmpz_add(__gen_e_acsl_add_2,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_at),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__5));
- __gen_e_acsl_eq_4 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_add_2),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__5));
- __e_acsl_assert(__gen_e_acsl_eq_4 == 0,(char *)"Assertion",
- (char *)"main",(char *)"\\at(x,L) + 1 == 1",50);
- __gmpz_clear(__gen_e_acsl__5);
- __gmpz_clear(__gen_e_acsl_add_2);
- }
- g(t,& x);
- __retres = 0;
- __gmpz_clear(__gen_e_acsl_at);
- __gmpz_clear(__gen_e_acsl_at_2);
- __e_acsl_delete_block((void *)(t));
- __e_acsl_delete_block((void *)(& x));
- __e_acsl_memory_clean();
- return __retres;
-}
-
-/*@ ensures \result ≡ \old(x); */
-int __gen_e_acsl_h(int x)
-{
- __e_acsl_mpz_t __gen_e_acsl_at;
- int __retres;
- __e_acsl_store_block((void *)(& __retres),(size_t)4);
- {
- __e_acsl_mpz_t __gen_e_acsl_x;
- __gmpz_init_set_si(__gen_e_acsl_x,(long)x);
- __gmpz_init_set(__gen_e_acsl_at,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_x));
- __gmpz_clear(__gen_e_acsl_x);
- }
- __e_acsl_store_block((void *)(& x),(size_t)4);
- __retres = h(x);
- {
- __e_acsl_mpz_t __gen_e_acsl_result;
- int __gen_e_acsl_eq;
- __gmpz_init_set_si(__gen_e_acsl_result,(long)__retres);
- __gen_e_acsl_eq = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_result),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_at));
- __e_acsl_assert(__gen_e_acsl_eq == 0,(char *)"Postcondition",(char *)"h",
- (char *)"\\result == \\old(x)",35);
- __e_acsl_delete_block((void *)(& x));
- __gmpz_clear(__gen_e_acsl_result);
- __gmpz_clear(__gen_e_acsl_at);
- __e_acsl_delete_block((void *)(& __retres));
- return __retres;
- }
-}
-
-/*@ ensures \at(A,Post) ≡ 3; */
-void __gen_e_acsl_f(void)
-{
- __e_acsl_mpz_t __gen_e_acsl_at;
- f();
- {
- __e_acsl_mpz_t __gen_e_acsl_;
- int __gen_e_acsl_eq;
- {
- __e_acsl_mpz_t __gen_e_acsl_A;
- __gmpz_init_set_si(__gen_e_acsl_A,(long)A);
- __gmpz_init_set(__gen_e_acsl_at,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_A));
- __gmpz_clear(__gen_e_acsl_A);
- }
- __gmpz_init_set_si(__gen_e_acsl_,3L);
- __gen_e_acsl_eq = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_at),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_));
- __e_acsl_assert(__gen_e_acsl_eq == 0,(char *)"Postcondition",(char *)"f",
- (char *)"\\at(A,Post) == 3",7);
- __gmpz_clear(__gen_e_acsl_);
- __gmpz_clear(__gen_e_acsl_at);
- return;
- }
-}
-
-
diff --git a/src/plugins/e-acsl/tests/arith/oracle/gen_at_on-purely-logic-variables2.c b/src/plugins/e-acsl/tests/arith/oracle/gen_at_on-purely-logic-variables2.c
deleted file mode 100644
index 6b577c505abf058eaf630cf172cfc76ef795fac6..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/arith/oracle/gen_at_on-purely-logic-variables2.c
+++ /dev/null
@@ -1,105 +0,0 @@
-/* Generated by Frama-C */
-#include "stdio.h"
-#include "stdlib.h"
-extern int __e_acsl_sound_verdict;
-
-/*@ ensures
- ∀ ℤ n;
- 1 < n ≤ 3 ⇒ \old(*(t + n) ≡ 12) ∧ \old(*(t + (n - 1)) > 5);
- ensures \let m = 4; \old(*(t + m) ≡ -4) ∧ \old(*(t + (m - 4))) ≡ 9;
- */
-void __gen_e_acsl_f(int *t);
-
-void f(int *t)
-{
- __e_acsl_store_block((void *)(& t),(size_t)8);
- __e_acsl_delete_block((void *)(& t));
- return;
-}
-
-void g(void)
-{
- int m;
- m = 8;
- Q: ;
- m = 10;
- /*@ assert ∃ ℤ w; 3 ≤ w < 6 ∧ \at(m + w ≡ 12,Q); */ ;
- return;
-}
-
-int main(void)
-{
- int __retres;
- int n;
- __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
- __e_acsl_store_block((void *)(& n),(size_t)4);
- __e_acsl_full_init((void *)(& n));
- n = 7;
- L: ;
- __e_acsl_full_init((void *)(& n));
- n = 9;
- K: ;
- __e_acsl_full_init((void *)(& n));
- n = 666;
- /*@ assert \let i = 3; \at(n + i ≡ 10,L); */ ;
- /*@ assert ∃ ℤ j; 2 ≤ j < 5 ∧ \at(n + j ≡ 11,L); */ ;
- /*@
- assert \let k = -7;
- ∃ ℤ u;
- 9 ≤ u < 21 ∧
- (∀ ℤ v; -5 < v ≤ 6 ⇒ \at((u > 0? n + k: u + v) > 0,K));
- */
- ;
- /*@ assert \let i = 3; \at(n + i,L) ≡ 10; */ ;
- unsigned int m = (unsigned int)3;
- G: ;
- m = (unsigned int)(-3);
- /*@ assert ∃ ℤ k; -9 < k < 0 ∧ \at(m + k,G) ≡ 0; */ ;
- /*@
- assert
- ∃ ℤ u;
- 9 ≤ u < 21 ∧
- (∀ ℤ v; -5 < v ≤ (u < 15? u + 6: 3) ⇒ \at((n + u) + v > 0,K));
- */
- ;
- int t[5] = {9, 12, 12, 12, -4};
- __e_acsl_store_block((void *)(t),(size_t)20);
- __e_acsl_full_init((void *)(& t));
- __gen_e_acsl_f(t);
- g();
- /*@
- assert
- ∃ ℤ u;
- 10 ≤ u < 20 ∧
- (∃ ℤ v;
- -10 < v ≤ -5 + (\let u = -2; u) ∧
- (∃ ℤ w;
- 100 < w ≤ 200 ∧
- \at((((n - u) + (\let u = 42; u)) + v) + w > 0,K)));
- */
- ;
- /*@ assert ∃ ℤ j; 2 ≤ j < 10000000000000000 ∧ \at(n + j ≡ 11,L);
- */
- ;
- /*@ assert \let i = n; \at(n + i ≡ 10,L); */ ;
- __retres = 0;
- __e_acsl_delete_block((void *)(t));
- __e_acsl_delete_block((void *)(& n));
- __e_acsl_memory_clean();
- return __retres;
-}
-
-/*@ ensures
- ∀ ℤ n;
- 1 < n ≤ 3 ⇒ \old(*(t + n) ≡ 12) ∧ \old(*(t + (n - 1)) > 5);
- ensures \let m = 4; \old(*(t + m) ≡ -4) ∧ \old(*(t + (m - 4))) ≡ 9;
- */
-void __gen_e_acsl_f(int *t)
-{
- __e_acsl_store_block((void *)(& t),(size_t)8);
- f(t);
- __e_acsl_delete_block((void *)(& t));
- return;
-}
-
-
diff --git a/src/plugins/e-acsl/tests/arith/oracle/gen_cast2.c b/src/plugins/e-acsl/tests/arith/oracle/gen_cast2.c
deleted file mode 100644
index 30144953b681e8e7405c1d2237aebbd599fa4892..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/arith/oracle/gen_cast2.c
+++ /dev/null
@@ -1,143 +0,0 @@
-/* Generated by Frama-C */
-#include "stdio.h"
-#include "stdlib.h"
-int main(void)
-{
- int __retres;
- __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
- long x = (long)0;
- int y = 0;
- /*@ assert (int)x ≡ y; */
- {
- __e_acsl_mpz_t __gen_e_acsl_x;
- long __gen_e_acsl_cast;
- __e_acsl_mpz_t __gen_e_acsl_;
- __e_acsl_mpz_t __gen_e_acsl_y;
- int __gen_e_acsl_eq;
- __gmpz_init_set_si(__gen_e_acsl_x,x);
- __gen_e_acsl_cast = __gmpz_get_si((__e_acsl_mpz_struct const *)(__gen_e_acsl_x));
- __gmpz_init_set_si(__gen_e_acsl_,__gen_e_acsl_cast);
- __gmpz_init_set_si(__gen_e_acsl_y,(long)y);
- __gen_e_acsl_eq = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_y));
- __e_acsl_assert(__gen_e_acsl_eq == 0,(char *)"Assertion",(char *)"main",
- (char *)"(int)x == y",10);
- __gmpz_clear(__gen_e_acsl_x);
- __gmpz_clear(__gen_e_acsl_);
- __gmpz_clear(__gen_e_acsl_y);
- }
- /*@ assert x ≡ (long)y; */
- {
- __e_acsl_mpz_t __gen_e_acsl_x_2;
- __e_acsl_mpz_t __gen_e_acsl_y_2;
- long __gen_e_acsl_cast_2;
- __e_acsl_mpz_t __gen_e_acsl__2;
- int __gen_e_acsl_eq_2;
- __gmpz_init_set_si(__gen_e_acsl_x_2,x);
- __gmpz_init_set_si(__gen_e_acsl_y_2,(long)y);
- __gen_e_acsl_cast_2 = __gmpz_get_si((__e_acsl_mpz_struct const *)(__gen_e_acsl_y_2));
- __gmpz_init_set_si(__gen_e_acsl__2,__gen_e_acsl_cast_2);
- __gen_e_acsl_eq_2 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_x_2),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__2));
- __e_acsl_assert(__gen_e_acsl_eq_2 == 0,(char *)"Assertion",
- (char *)"main",(char *)"x == (long)y",11);
- __gmpz_clear(__gen_e_acsl_x_2);
- __gmpz_clear(__gen_e_acsl_y_2);
- __gmpz_clear(__gen_e_acsl__2);
- }
- /*@ assert y ≡ (int)0; */
- {
- __e_acsl_mpz_t __gen_e_acsl_y_3;
- __e_acsl_mpz_t __gen_e_acsl__3;
- long __gen_e_acsl_cast_3;
- __e_acsl_mpz_t __gen_e_acsl__4;
- int __gen_e_acsl_eq_3;
- __gmpz_init_set_si(__gen_e_acsl_y_3,(long)y);
- __gmpz_init_set_si(__gen_e_acsl__3,0L);
- __gen_e_acsl_cast_3 = __gmpz_get_si((__e_acsl_mpz_struct const *)(__gen_e_acsl__3));
- __gmpz_init_set_si(__gen_e_acsl__4,__gen_e_acsl_cast_3);
- __gen_e_acsl_eq_3 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_y_3),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__4));
- __e_acsl_assert(__gen_e_acsl_eq_3 == 0,(char *)"Assertion",
- (char *)"main",(char *)"y == (int)0",13);
- __gmpz_clear(__gen_e_acsl_y_3);
- __gmpz_clear(__gen_e_acsl__3);
- __gmpz_clear(__gen_e_acsl__4);
- }
- /*@ assert (unsigned int)y ≡ (unsigned int)0; */
- {
- __e_acsl_mpz_t __gen_e_acsl_y_4;
- unsigned long __gen_e_acsl_cast_4;
- __e_acsl_mpz_t __gen_e_acsl__5;
- __e_acsl_mpz_t __gen_e_acsl__6;
- unsigned long __gen_e_acsl_cast_5;
- __e_acsl_mpz_t __gen_e_acsl__7;
- int __gen_e_acsl_eq_4;
- __gmpz_init_set_si(__gen_e_acsl_y_4,(long)y);
- __gen_e_acsl_cast_4 = __gmpz_get_ui((__e_acsl_mpz_struct const *)(__gen_e_acsl_y_4));
- __gmpz_init_set_ui(__gen_e_acsl__5,__gen_e_acsl_cast_4);
- __gmpz_init_set_si(__gen_e_acsl__6,0L);
- __gen_e_acsl_cast_5 = __gmpz_get_ui((__e_acsl_mpz_struct const *)(__gen_e_acsl__6));
- __gmpz_init_set_ui(__gen_e_acsl__7,__gen_e_acsl_cast_5);
- __gen_e_acsl_eq_4 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl__5),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__7));
- __e_acsl_assert(__gen_e_acsl_eq_4 == 0,(char *)"Assertion",
- (char *)"main",
- (char *)"(unsigned int)y == (unsigned int)0",14);
- __gmpz_clear(__gen_e_acsl_y_4);
- __gmpz_clear(__gen_e_acsl__5);
- __gmpz_clear(__gen_e_acsl__6);
- __gmpz_clear(__gen_e_acsl__7);
- }
- /*@ assert y ≢ (int)0xfffffffffffffff; */
- {
- __e_acsl_mpz_t __gen_e_acsl_y_5;
- __e_acsl_mpz_t __gen_e_acsl__8;
- long __gen_e_acsl_cast_6;
- __e_acsl_mpz_t __gen_e_acsl__9;
- int __gen_e_acsl_ne;
- __gmpz_init_set_si(__gen_e_acsl_y_5,(long)y);
- __gmpz_init_set_ui(__gen_e_acsl__8,1152921504606846975UL);
- __gen_e_acsl_cast_6 = __gmpz_get_si((__e_acsl_mpz_struct const *)(__gen_e_acsl__8));
- __gmpz_init_set_si(__gen_e_acsl__9,__gen_e_acsl_cast_6);
- __gen_e_acsl_ne = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_y_5),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__9));
- __e_acsl_assert(__gen_e_acsl_ne != 0,(char *)"Assertion",(char *)"main",
- (char *)"y != (int)0xfffffffffffffff",17);
- __gmpz_clear(__gen_e_acsl_y_5);
- __gmpz_clear(__gen_e_acsl__8);
- __gmpz_clear(__gen_e_acsl__9);
- }
- /*@ assert (unsigned int)y ≢ (unsigned int)0xfffffffffffffff; */
- {
- __e_acsl_mpz_t __gen_e_acsl_y_6;
- unsigned long __gen_e_acsl_cast_7;
- __e_acsl_mpz_t __gen_e_acsl__10;
- __e_acsl_mpz_t __gen_e_acsl__11;
- unsigned long __gen_e_acsl_cast_8;
- __e_acsl_mpz_t __gen_e_acsl__12;
- int __gen_e_acsl_ne_2;
- __gmpz_init_set_si(__gen_e_acsl_y_6,(long)y);
- __gen_e_acsl_cast_7 = __gmpz_get_ui((__e_acsl_mpz_struct const *)(__gen_e_acsl_y_6));
- __gmpz_init_set_ui(__gen_e_acsl__10,__gen_e_acsl_cast_7);
- __gmpz_init_set_ui(__gen_e_acsl__11,1152921504606846975UL);
- __gen_e_acsl_cast_8 = __gmpz_get_ui((__e_acsl_mpz_struct const *)(__gen_e_acsl__11));
- __gmpz_init_set_ui(__gen_e_acsl__12,__gen_e_acsl_cast_8);
- __gen_e_acsl_ne_2 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl__10),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__12));
- __e_acsl_assert(__gen_e_acsl_ne_2 != 0,(char *)"Assertion",
- (char *)"main",
- (char *)"(unsigned int)y != (unsigned int)0xfffffffffffffff",
- 18);
- __gmpz_clear(__gen_e_acsl_y_6);
- __gmpz_clear(__gen_e_acsl__10);
- __gmpz_clear(__gen_e_acsl__11);
- __gmpz_clear(__gen_e_acsl__12);
- }
- int t[2] = {0, 1};
- /*@ assert (float)x ≡ t[(int)0.1]; */ ;
- __retres = 0;
- return __retres;
-}
-
-
diff --git a/src/plugins/e-acsl/tests/arith/oracle/gen_comparison2.c b/src/plugins/e-acsl/tests/arith/oracle/gen_comparison2.c
deleted file mode 100644
index 4cfbcae218e6680962cd2343400a0593e947bb36..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/arith/oracle/gen_comparison2.c
+++ /dev/null
@@ -1,266 +0,0 @@
-/* Generated by Frama-C */
-#include "stdio.h"
-#include "stdlib.h"
-int main(void)
-{
- int __retres;
- __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
- int x = 0;
- int y = 1;
- /*@ assert x < y; */
- {
- __e_acsl_mpz_t __gen_e_acsl_x;
- __e_acsl_mpz_t __gen_e_acsl_y;
- int __gen_e_acsl_lt;
- __gmpz_init_set_si(__gen_e_acsl_x,(long)x);
- __gmpz_init_set_si(__gen_e_acsl_y,(long)y);
- __gen_e_acsl_lt = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_x),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_y));
- __e_acsl_assert(__gen_e_acsl_lt < 0,(char *)"Assertion",(char *)"main",
- (char *)"x < y",7);
- __gmpz_clear(__gen_e_acsl_x);
- __gmpz_clear(__gen_e_acsl_y);
- }
- /*@ assert y > x; */
- {
- __e_acsl_mpz_t __gen_e_acsl_y_2;
- __e_acsl_mpz_t __gen_e_acsl_x_2;
- int __gen_e_acsl_gt;
- __gmpz_init_set_si(__gen_e_acsl_y_2,(long)y);
- __gmpz_init_set_si(__gen_e_acsl_x_2,(long)x);
- __gen_e_acsl_gt = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_y_2),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_x_2));
- __e_acsl_assert(__gen_e_acsl_gt > 0,(char *)"Assertion",(char *)"main",
- (char *)"y > x",8);
- __gmpz_clear(__gen_e_acsl_y_2);
- __gmpz_clear(__gen_e_acsl_x_2);
- }
- /*@ assert x ≤ 0; */
- {
- __e_acsl_mpz_t __gen_e_acsl_x_3;
- __e_acsl_mpz_t __gen_e_acsl_;
- int __gen_e_acsl_le;
- __gmpz_init_set_si(__gen_e_acsl_x_3,(long)x);
- __gmpz_init_set_si(__gen_e_acsl_,0L);
- __gen_e_acsl_le = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_x_3),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_));
- __e_acsl_assert(__gen_e_acsl_le <= 0,(char *)"Assertion",(char *)"main",
- (char *)"x <= 0",9);
- __gmpz_clear(__gen_e_acsl_x_3);
- __gmpz_clear(__gen_e_acsl_);
- }
- /*@ assert y ≥ 1; */
- {
- __e_acsl_mpz_t __gen_e_acsl_y_3;
- __e_acsl_mpz_t __gen_e_acsl__2;
- int __gen_e_acsl_ge;
- __gmpz_init_set_si(__gen_e_acsl_y_3,(long)y);
- __gmpz_init_set_si(__gen_e_acsl__2,1L);
- __gen_e_acsl_ge = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_y_3),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__2));
- __e_acsl_assert(__gen_e_acsl_ge >= 0,(char *)"Assertion",(char *)"main",
- (char *)"y >= 1",10);
- __gmpz_clear(__gen_e_acsl_y_3);
- __gmpz_clear(__gen_e_acsl__2);
- }
- char *s = (char *)"toto";
- /*@ assert s ≡ s; */
- __e_acsl_assert(s == s,(char *)"Assertion",(char *)"main",(char *)"s == s",
- 12);
- /*@ assert 5 < 18; */
- {
- __e_acsl_mpz_t __gen_e_acsl__3;
- __e_acsl_mpz_t __gen_e_acsl__4;
- int __gen_e_acsl_lt_2;
- __gmpz_init_set_si(__gen_e_acsl__3,5L);
- __gmpz_init_set_si(__gen_e_acsl__4,18L);
- __gen_e_acsl_lt_2 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl__3),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__4));
- __e_acsl_assert(__gen_e_acsl_lt_2 < 0,(char *)"Assertion",(char *)"main",
- (char *)"5 < 18",15);
- __gmpz_clear(__gen_e_acsl__3);
- __gmpz_clear(__gen_e_acsl__4);
- }
- /*@ assert 32 > 3; */
- {
- __e_acsl_mpz_t __gen_e_acsl__5;
- __e_acsl_mpz_t __gen_e_acsl__6;
- int __gen_e_acsl_gt_2;
- __gmpz_init_set_si(__gen_e_acsl__5,32L);
- __gmpz_init_set_si(__gen_e_acsl__6,3L);
- __gen_e_acsl_gt_2 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl__5),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__6));
- __e_acsl_assert(__gen_e_acsl_gt_2 > 0,(char *)"Assertion",(char *)"main",
- (char *)"32 > 3",16);
- __gmpz_clear(__gen_e_acsl__5);
- __gmpz_clear(__gen_e_acsl__6);
- }
- /*@ assert 12 ≤ 13; */
- {
- __e_acsl_mpz_t __gen_e_acsl__7;
- __e_acsl_mpz_t __gen_e_acsl__8;
- int __gen_e_acsl_le_2;
- __gmpz_init_set_si(__gen_e_acsl__7,12L);
- __gmpz_init_set_si(__gen_e_acsl__8,13L);
- __gen_e_acsl_le_2 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl__7),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__8));
- __e_acsl_assert(__gen_e_acsl_le_2 <= 0,(char *)"Assertion",
- (char *)"main",(char *)"12 <= 13",17);
- __gmpz_clear(__gen_e_acsl__7);
- __gmpz_clear(__gen_e_acsl__8);
- }
- /*@ assert 123 ≥ 12; */
- {
- __e_acsl_mpz_t __gen_e_acsl__9;
- __e_acsl_mpz_t __gen_e_acsl__10;
- int __gen_e_acsl_ge_2;
- __gmpz_init_set_si(__gen_e_acsl__9,123L);
- __gmpz_init_set_si(__gen_e_acsl__10,12L);
- __gen_e_acsl_ge_2 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl__9),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__10));
- __e_acsl_assert(__gen_e_acsl_ge_2 >= 0,(char *)"Assertion",
- (char *)"main",(char *)"123 >= 12",18);
- __gmpz_clear(__gen_e_acsl__9);
- __gmpz_clear(__gen_e_acsl__10);
- }
- /*@ assert 0xff ≡ 0xff; */
- {
- __e_acsl_mpz_t __gen_e_acsl__11;
- int __gen_e_acsl_eq;
- __gmpz_init_set_si(__gen_e_acsl__11,255L);
- __gen_e_acsl_eq = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl__11),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__11));
- __e_acsl_assert(__gen_e_acsl_eq == 0,(char *)"Assertion",(char *)"main",
- (char *)"0xff == 0xff",19);
- __gmpz_clear(__gen_e_acsl__11);
- }
- /*@ assert 1 ≢ 2; */
- {
- __e_acsl_mpz_t __gen_e_acsl__12;
- __e_acsl_mpz_t __gen_e_acsl__13;
- int __gen_e_acsl_ne;
- __gmpz_init_set_si(__gen_e_acsl__12,1L);
- __gmpz_init_set_si(__gen_e_acsl__13,2L);
- __gen_e_acsl_ne = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl__12),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__13));
- __e_acsl_assert(__gen_e_acsl_ne != 0,(char *)"Assertion",(char *)"main",
- (char *)"1 != 2",20);
- __gmpz_clear(__gen_e_acsl__12);
- __gmpz_clear(__gen_e_acsl__13);
- }
- /*@ assert -5 < 18; */
- {
- __e_acsl_mpz_t __gen_e_acsl__14;
- __e_acsl_mpz_t __gen_e_acsl_neg;
- __e_acsl_mpz_t __gen_e_acsl__15;
- int __gen_e_acsl_lt_3;
- __gmpz_init_set_si(__gen_e_acsl__14,5L);
- __gmpz_init(__gen_e_acsl_neg);
- __gmpz_neg(__gen_e_acsl_neg,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__14));
- __gmpz_init_set_si(__gen_e_acsl__15,18L);
- __gen_e_acsl_lt_3 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_neg),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__15));
- __e_acsl_assert(__gen_e_acsl_lt_3 < 0,(char *)"Assertion",(char *)"main",
- (char *)"-5 < 18",22);
- __gmpz_clear(__gen_e_acsl__14);
- __gmpz_clear(__gen_e_acsl_neg);
- __gmpz_clear(__gen_e_acsl__15);
- }
- /*@ assert 32 > -3; */
- {
- __e_acsl_mpz_t __gen_e_acsl__16;
- __e_acsl_mpz_t __gen_e_acsl__17;
- __e_acsl_mpz_t __gen_e_acsl_neg_2;
- int __gen_e_acsl_gt_3;
- __gmpz_init_set_si(__gen_e_acsl__16,32L);
- __gmpz_init_set_si(__gen_e_acsl__17,3L);
- __gmpz_init(__gen_e_acsl_neg_2);
- __gmpz_neg(__gen_e_acsl_neg_2,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__17));
- __gen_e_acsl_gt_3 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl__16),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_neg_2));
- __e_acsl_assert(__gen_e_acsl_gt_3 > 0,(char *)"Assertion",(char *)"main",
- (char *)"32 > -3",23);
- __gmpz_clear(__gen_e_acsl__16);
- __gmpz_clear(__gen_e_acsl__17);
- __gmpz_clear(__gen_e_acsl_neg_2);
- }
- /*@ assert -12 ≤ 13; */
- {
- __e_acsl_mpz_t __gen_e_acsl__18;
- __e_acsl_mpz_t __gen_e_acsl_neg_3;
- __e_acsl_mpz_t __gen_e_acsl__19;
- int __gen_e_acsl_le_3;
- __gmpz_init_set_si(__gen_e_acsl__18,12L);
- __gmpz_init(__gen_e_acsl_neg_3);
- __gmpz_neg(__gen_e_acsl_neg_3,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__18));
- __gmpz_init_set_si(__gen_e_acsl__19,13L);
- __gen_e_acsl_le_3 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_neg_3),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__19));
- __e_acsl_assert(__gen_e_acsl_le_3 <= 0,(char *)"Assertion",
- (char *)"main",(char *)"-12 <= 13",24);
- __gmpz_clear(__gen_e_acsl__18);
- __gmpz_clear(__gen_e_acsl_neg_3);
- __gmpz_clear(__gen_e_acsl__19);
- }
- /*@ assert 123 ≥ -12; */
- {
- __e_acsl_mpz_t __gen_e_acsl__20;
- __e_acsl_mpz_t __gen_e_acsl__21;
- __e_acsl_mpz_t __gen_e_acsl_neg_4;
- int __gen_e_acsl_ge_3;
- __gmpz_init_set_si(__gen_e_acsl__20,123L);
- __gmpz_init_set_si(__gen_e_acsl__21,12L);
- __gmpz_init(__gen_e_acsl_neg_4);
- __gmpz_neg(__gen_e_acsl_neg_4,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__21));
- __gen_e_acsl_ge_3 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl__20),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_neg_4));
- __e_acsl_assert(__gen_e_acsl_ge_3 >= 0,(char *)"Assertion",
- (char *)"main",(char *)"123 >= -12",25);
- __gmpz_clear(__gen_e_acsl__20);
- __gmpz_clear(__gen_e_acsl__21);
- __gmpz_clear(__gen_e_acsl_neg_4);
- }
- /*@ assert -0xff ≡ -0xff; */
- {
- __e_acsl_mpz_t __gen_e_acsl__22;
- __e_acsl_mpz_t __gen_e_acsl_neg_5;
- int __gen_e_acsl_eq_2;
- __gmpz_init_set_si(__gen_e_acsl__22,255L);
- __gmpz_init(__gen_e_acsl_neg_5);
- __gmpz_neg(__gen_e_acsl_neg_5,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__22));
- __gen_e_acsl_eq_2 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_neg_5),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_neg_5));
- __e_acsl_assert(__gen_e_acsl_eq_2 == 0,(char *)"Assertion",
- (char *)"main",(char *)"-0xff == -0xff",26);
- __gmpz_clear(__gen_e_acsl__22);
- __gmpz_clear(__gen_e_acsl_neg_5);
- }
- /*@ assert 1 ≢ -2; */
- {
- __e_acsl_mpz_t __gen_e_acsl__23;
- __e_acsl_mpz_t __gen_e_acsl__24;
- __e_acsl_mpz_t __gen_e_acsl_neg_6;
- int __gen_e_acsl_ne_2;
- __gmpz_init_set_si(__gen_e_acsl__23,1L);
- __gmpz_init_set_si(__gen_e_acsl__24,2L);
- __gmpz_init(__gen_e_acsl_neg_6);
- __gmpz_neg(__gen_e_acsl_neg_6,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__24));
- __gen_e_acsl_ne_2 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl__23),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_neg_6));
- __e_acsl_assert(__gen_e_acsl_ne_2 != 0,(char *)"Assertion",
- (char *)"main",(char *)"1 != -2",27);
- __gmpz_clear(__gen_e_acsl__23);
- __gmpz_clear(__gen_e_acsl__24);
- __gmpz_clear(__gen_e_acsl_neg_6);
- }
- __retres = 0;
- return __retres;
-}
-
-
diff --git a/src/plugins/e-acsl/tests/arith/oracle/gen_functions_rec2.c b/src/plugins/e-acsl/tests/arith/oracle/gen_functions_rec2.c
deleted file mode 100644
index 9af269bd2db4bf590352f544990b3b31d0b32030..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/arith/oracle/gen_functions_rec2.c
+++ /dev/null
@@ -1,593 +0,0 @@
-/* Generated by Frama-C */
-#include "stdio.h"
-#include "stdlib.h"
-/*@ logic ℤ f1(ℤ n) = n ≤ 0? 0: f1(n - 1) + n;
- */
-/*@ logic ℤ f2(ℤ n) = n < 0? 1: (f2(n - 1) * f2(n - 2)) / f2(n - 3);
-
-*/
-void __gen_e_acsl_f2(__e_acsl_mpz_t *__retres_arg, int n);
-
-void __gen_e_acsl_f2_2(__e_acsl_mpz_t *__retres_arg, __e_acsl_mpz_struct * n);
-
-/*@ logic ℤ g(ℤ n) = 0;
-
-*/
-void __gen_e_acsl_g(__e_acsl_mpz_t *__retres_arg, int n);
-
-void __gen_e_acsl_g_5(__e_acsl_mpz_t *__retres_arg, __e_acsl_mpz_struct * n);
-
-/*@ logic ℤ f3(ℤ n) = n > 0? g(n) * f3(n - 1) - 5: g(n + 1);
-
-*/
-void __gen_e_acsl_f3(__e_acsl_mpz_t *__retres_arg, int n);
-
-void __gen_e_acsl_f3_2(__e_acsl_mpz_t *__retres_arg, __e_acsl_mpz_struct * n);
-
-/*@
-logic ℤ f4(ℤ n) =
- n < 100? f4(n + 1): (n < 0x7fffffffffffffffL? 0x7fffffffffffffffL: 6);
-
-*/
-void __gen_e_acsl_f4(__e_acsl_mpz_t *__retres_arg, int n);
-
-void __gen_e_acsl_f4_2(__e_acsl_mpz_t *__retres_arg, __e_acsl_mpz_struct * n);
-
-int main(void)
-{
- int __retres;
- __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
- /*@ assert f2(7) ≡ 1; */
- {
- __e_acsl_mpz_t __gen_e_acsl_f2_14;
- __e_acsl_mpz_t __gen_e_acsl__13;
- int __gen_e_acsl_eq;
- __gen_e_acsl_f2(& __gen_e_acsl_f2_14,7);
- __gmpz_init_set_si(__gen_e_acsl__13,1L);
- __gen_e_acsl_eq = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_f2_14),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__13));
- __e_acsl_assert(__gen_e_acsl_eq == 0,(char *)"Assertion",(char *)"main",
- (char *)"f2(7) == 1",26);
- __gmpz_clear(__gen_e_acsl_f2_14);
- __gmpz_clear(__gen_e_acsl__13);
- }
- /*@ assert f3(6) ≡ -5; */
- {
- __e_acsl_mpz_t __gen_e_acsl_f3_6;
- __e_acsl_mpz_t __gen_e_acsl__23;
- __e_acsl_mpz_t __gen_e_acsl_neg;
- int __gen_e_acsl_eq_2;
- __gen_e_acsl_f3(& __gen_e_acsl_f3_6,6);
- __gmpz_init_set_si(__gen_e_acsl__23,5L);
- __gmpz_init(__gen_e_acsl_neg);
- __gmpz_neg(__gen_e_acsl_neg,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__23));
- __gen_e_acsl_eq_2 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_f3_6),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_neg));
- __e_acsl_assert(__gen_e_acsl_eq_2 == 0,(char *)"Assertion",
- (char *)"main",(char *)"f3(6) == -5",28);
- __gmpz_clear(__gen_e_acsl_f3_6);
- __gmpz_clear(__gen_e_acsl__23);
- __gmpz_clear(__gen_e_acsl_neg);
- }
- /*@ assert f4(9) > 0; */
- {
- __e_acsl_mpz_t __gen_e_acsl_f4_6;
- __e_acsl_mpz_t __gen_e_acsl__34;
- int __gen_e_acsl_gt_3;
- __gen_e_acsl_f4(& __gen_e_acsl_f4_6,9);
- __gmpz_init_set_si(__gen_e_acsl__34,0L);
- __gen_e_acsl_gt_3 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_f4_6),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__34));
- __e_acsl_assert(__gen_e_acsl_gt_3 > 0,(char *)"Assertion",(char *)"main",
- (char *)"f4(9) > 0",30);
- __gmpz_clear(__gen_e_acsl_f4_6);
- __gmpz_clear(__gen_e_acsl__34);
- }
- __retres = 0;
- return __retres;
-}
-
-void __gen_e_acsl_f2(__e_acsl_mpz_t *__retres_arg, int n)
-{
- __e_acsl_mpz_t __gen_e_acsl_n;
- __e_acsl_mpz_t __gen_e_acsl_;
- int __gen_e_acsl_lt;
- __e_acsl_mpz_t __gen_e_acsl_if_2;
- __gmpz_init_set_si(__gen_e_acsl_n,(long)n);
- __gmpz_init_set_si(__gen_e_acsl_,0L);
- __gen_e_acsl_lt = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_n),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_));
- if (__gen_e_acsl_lt < 0) {
- __e_acsl_mpz_t __gen_e_acsl__2;
- __gmpz_init_set_si(__gen_e_acsl__2,1L);
- __gmpz_init_set(__gen_e_acsl_if_2,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__2));
- __gmpz_clear(__gen_e_acsl__2);
- }
- else {
- __e_acsl_mpz_t __gen_e_acsl_n_2;
- __e_acsl_mpz_t __gen_e_acsl__3;
- __e_acsl_mpz_t __gen_e_acsl_sub;
- __e_acsl_mpz_t __gen_e_acsl_f2_9;
- __e_acsl_mpz_t __gen_e_acsl__10;
- __e_acsl_mpz_t __gen_e_acsl_sub_5;
- __e_acsl_mpz_t __gen_e_acsl_f2_11;
- __e_acsl_mpz_t __gen_e_acsl_mul_2;
- __e_acsl_mpz_t __gen_e_acsl__11;
- __e_acsl_mpz_t __gen_e_acsl_sub_6;
- __e_acsl_mpz_t __gen_e_acsl_f2_13;
- __e_acsl_mpz_t __gen_e_acsl__12;
- int __gen_e_acsl_div_guard_2;
- __e_acsl_mpz_t __gen_e_acsl_div_2;
- __gmpz_init_set_si(__gen_e_acsl_n_2,(long)n);
- __gmpz_init_set_si(__gen_e_acsl__3,1L);
- __gmpz_init(__gen_e_acsl_sub);
- __gmpz_sub(__gen_e_acsl_sub,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_n_2),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__3));
- /*@ assert
- Eva: initialization:
- \initialized((__e_acsl_mpz_struct *)__gen_e_acsl_sub);
- */
- __gen_e_acsl_f2_2(& __gen_e_acsl_f2_9,
- (__e_acsl_mpz_struct *)__gen_e_acsl_sub);
- __gmpz_init_set_si(__gen_e_acsl__10,2L);
- __gmpz_init(__gen_e_acsl_sub_5);
- __gmpz_sub(__gen_e_acsl_sub_5,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_n_2),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__10));
- /*@ assert
- Eva: initialization:
- \initialized((__e_acsl_mpz_struct *)__gen_e_acsl_sub_5);
- */
- __gen_e_acsl_f2_2(& __gen_e_acsl_f2_11,
- (__e_acsl_mpz_struct *)__gen_e_acsl_sub_5);
- __gmpz_init(__gen_e_acsl_mul_2);
- __gmpz_mul(__gen_e_acsl_mul_2,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_f2_9),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_f2_11));
- __gmpz_init_set_si(__gen_e_acsl__11,3L);
- __gmpz_init(__gen_e_acsl_sub_6);
- __gmpz_sub(__gen_e_acsl_sub_6,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_n_2),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__11));
- /*@ assert
- Eva: initialization:
- \initialized((__e_acsl_mpz_struct *)__gen_e_acsl_sub_6);
- */
- __gen_e_acsl_f2_2(& __gen_e_acsl_f2_13,
- (__e_acsl_mpz_struct *)__gen_e_acsl_sub_6);
- __gmpz_init_set_si(__gen_e_acsl__12,0L);
- __gen_e_acsl_div_guard_2 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_f2_13),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__12));
- __gmpz_init(__gen_e_acsl_div_2);
- /*@ assert E_ACSL: f2(n - 3) ≢ 0; */
- __e_acsl_assert(! (__gen_e_acsl_div_guard_2 == 0),(char *)"Assertion",
- (char *)"f2",(char *)"f2(n - 3) == 0",10);
- __gmpz_tdiv_q(__gen_e_acsl_div_2,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_mul_2),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_f2_13));
- __gmpz_init_set(__gen_e_acsl_if_2,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_div_2));
- __gmpz_clear(__gen_e_acsl_n_2);
- __gmpz_clear(__gen_e_acsl__3);
- __gmpz_clear(__gen_e_acsl_sub);
- __gmpz_clear(__gen_e_acsl_f2_9);
- __gmpz_clear(__gen_e_acsl__10);
- __gmpz_clear(__gen_e_acsl_sub_5);
- __gmpz_clear(__gen_e_acsl_f2_11);
- __gmpz_clear(__gen_e_acsl_mul_2);
- __gmpz_clear(__gen_e_acsl__11);
- __gmpz_clear(__gen_e_acsl_sub_6);
- __gmpz_clear(__gen_e_acsl_f2_13);
- __gmpz_clear(__gen_e_acsl__12);
- __gmpz_clear(__gen_e_acsl_div_2);
- }
- __gmpz_init_set(*__retres_arg,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_if_2));
- __gmpz_clear(__gen_e_acsl_n);
- __gmpz_clear(__gen_e_acsl_);
- __gmpz_clear(__gen_e_acsl_if_2);
- return;
-}
-
-void __gen_e_acsl_f2_2(__e_acsl_mpz_t *__retres_arg, __e_acsl_mpz_struct * n)
-{
- __e_acsl_mpz_t __gen_e_acsl__4;
- int __gen_e_acsl_lt_2;
- __e_acsl_mpz_t __gen_e_acsl_if;
- __gmpz_init_set_si(__gen_e_acsl__4,0L);
- __gen_e_acsl_lt_2 = __gmpz_cmp((__e_acsl_mpz_struct const *)(n),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__4));
- if (__gen_e_acsl_lt_2 < 0) {
- __e_acsl_mpz_t __gen_e_acsl__5;
- __gmpz_init_set_si(__gen_e_acsl__5,1L);
- __gmpz_init_set(__gen_e_acsl_if,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__5));
- __gmpz_clear(__gen_e_acsl__5);
- }
- else {
- __e_acsl_mpz_t __gen_e_acsl__6;
- __e_acsl_mpz_t __gen_e_acsl_sub_2;
- __e_acsl_mpz_t __gen_e_acsl_f2_4;
- __e_acsl_mpz_t __gen_e_acsl__7;
- __e_acsl_mpz_t __gen_e_acsl_sub_3;
- __e_acsl_mpz_t __gen_e_acsl_f2_6;
- __e_acsl_mpz_t __gen_e_acsl_mul;
- __e_acsl_mpz_t __gen_e_acsl__8;
- __e_acsl_mpz_t __gen_e_acsl_sub_4;
- __e_acsl_mpz_t __gen_e_acsl_f2_8;
- __e_acsl_mpz_t __gen_e_acsl__9;
- int __gen_e_acsl_div_guard;
- __e_acsl_mpz_t __gen_e_acsl_div;
- __gmpz_init_set_si(__gen_e_acsl__6,1L);
- __gmpz_init(__gen_e_acsl_sub_2);
- __gmpz_sub(__gen_e_acsl_sub_2,(__e_acsl_mpz_struct const *)(n),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__6));
- /*@ assert
- Eva: initialization:
- \initialized((__e_acsl_mpz_struct *)__gen_e_acsl_sub_2);
- */
- __gen_e_acsl_f2_2(& __gen_e_acsl_f2_4,
- (__e_acsl_mpz_struct *)__gen_e_acsl_sub_2);
- __gmpz_init_set_si(__gen_e_acsl__7,2L);
- __gmpz_init(__gen_e_acsl_sub_3);
- __gmpz_sub(__gen_e_acsl_sub_3,(__e_acsl_mpz_struct const *)(n),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__7));
- /*@ assert
- Eva: initialization:
- \initialized((__e_acsl_mpz_struct *)__gen_e_acsl_sub_3);
- */
- __gen_e_acsl_f2_2(& __gen_e_acsl_f2_6,
- (__e_acsl_mpz_struct *)__gen_e_acsl_sub_3);
- __gmpz_init(__gen_e_acsl_mul);
- __gmpz_mul(__gen_e_acsl_mul,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_f2_4),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_f2_6));
- __gmpz_init_set_si(__gen_e_acsl__8,3L);
- __gmpz_init(__gen_e_acsl_sub_4);
- __gmpz_sub(__gen_e_acsl_sub_4,(__e_acsl_mpz_struct const *)(n),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__8));
- /*@ assert
- Eva: initialization:
- \initialized((__e_acsl_mpz_struct *)__gen_e_acsl_sub_4);
- */
- __gen_e_acsl_f2_2(& __gen_e_acsl_f2_8,
- (__e_acsl_mpz_struct *)__gen_e_acsl_sub_4);
- __gmpz_init_set_si(__gen_e_acsl__9,0L);
- __gen_e_acsl_div_guard = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_f2_8),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__9));
- __gmpz_init(__gen_e_acsl_div);
- /*@ assert E_ACSL: f2(n - 3) ≢ 0; */
- __e_acsl_assert(! (__gen_e_acsl_div_guard == 0),(char *)"Assertion",
- (char *)"f2_2",(char *)"f2(n - 3) == 0",10);
- __gmpz_tdiv_q(__gen_e_acsl_div,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_mul),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_f2_8));
- __gmpz_init_set(__gen_e_acsl_if,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_div));
- __gmpz_clear(__gen_e_acsl__6);
- __gmpz_clear(__gen_e_acsl_sub_2);
- __gmpz_clear(__gen_e_acsl_f2_4);
- __gmpz_clear(__gen_e_acsl__7);
- __gmpz_clear(__gen_e_acsl_sub_3);
- __gmpz_clear(__gen_e_acsl_f2_6);
- __gmpz_clear(__gen_e_acsl_mul);
- __gmpz_clear(__gen_e_acsl__8);
- __gmpz_clear(__gen_e_acsl_sub_4);
- __gmpz_clear(__gen_e_acsl_f2_8);
- __gmpz_clear(__gen_e_acsl__9);
- __gmpz_clear(__gen_e_acsl_div);
- }
- __gmpz_init_set(*__retres_arg,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_if));
- __gmpz_clear(__gen_e_acsl__4);
- __gmpz_clear(__gen_e_acsl_if);
- return;
-}
-
-void __gen_e_acsl_g(__e_acsl_mpz_t *__retres_arg, int n)
-{
- __gmpz_init_set_si(*__retres_arg,0L);
- return;
-}
-
-void __gen_e_acsl_g_5(__e_acsl_mpz_t *__retres_arg, __e_acsl_mpz_struct * n)
-{
- __gmpz_init_set_si(*__retres_arg,0L);
- return;
-}
-
-void __gen_e_acsl_f3(__e_acsl_mpz_t *__retres_arg, int n)
-{
- __e_acsl_mpz_t __gen_e_acsl_n_3;
- __e_acsl_mpz_t __gen_e_acsl__14;
- int __gen_e_acsl_gt;
- __e_acsl_mpz_t __gen_e_acsl_if_4;
- __gmpz_init_set_si(__gen_e_acsl_n_3,(long)n);
- __gmpz_init_set_si(__gen_e_acsl__14,0L);
- __gen_e_acsl_gt = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_n_3),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__14));
- if (__gen_e_acsl_gt > 0) {
- __e_acsl_mpz_t __gen_e_acsl_g_2;
- __e_acsl_mpz_t __gen_e_acsl_n_4;
- __e_acsl_mpz_t __gen_e_acsl__15;
- __e_acsl_mpz_t __gen_e_acsl_sub_7;
- __e_acsl_mpz_t __gen_e_acsl_f3_5;
- __e_acsl_mpz_t __gen_e_acsl_mul_4;
- __e_acsl_mpz_t __gen_e_acsl__21;
- __e_acsl_mpz_t __gen_e_acsl_sub_10;
- __gen_e_acsl_g(& __gen_e_acsl_g_2,n);
- __gmpz_init_set_si(__gen_e_acsl_n_4,(long)n);
- __gmpz_init_set_si(__gen_e_acsl__15,1L);
- __gmpz_init(__gen_e_acsl_sub_7);
- __gmpz_sub(__gen_e_acsl_sub_7,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_n_4),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__15));
- /*@ assert
- Eva: initialization:
- \initialized((__e_acsl_mpz_struct *)__gen_e_acsl_sub_7);
- */
- __gen_e_acsl_f3_2(& __gen_e_acsl_f3_5,
- (__e_acsl_mpz_struct *)__gen_e_acsl_sub_7);
- __gmpz_init(__gen_e_acsl_mul_4);
- __gmpz_mul(__gen_e_acsl_mul_4,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_g_2),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_f3_5));
- __gmpz_init_set_si(__gen_e_acsl__21,5L);
- __gmpz_init(__gen_e_acsl_sub_10);
- __gmpz_sub(__gen_e_acsl_sub_10,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_mul_4),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__21));
- __gmpz_init_set(__gen_e_acsl_if_4,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_sub_10));
- __gmpz_clear(__gen_e_acsl_g_2);
- __gmpz_clear(__gen_e_acsl_n_4);
- __gmpz_clear(__gen_e_acsl__15);
- __gmpz_clear(__gen_e_acsl_sub_7);
- __gmpz_clear(__gen_e_acsl_f3_5);
- __gmpz_clear(__gen_e_acsl_mul_4);
- __gmpz_clear(__gen_e_acsl__21);
- __gmpz_clear(__gen_e_acsl_sub_10);
- }
- else {
- __e_acsl_mpz_t __gen_e_acsl_n_5;
- __e_acsl_mpz_t __gen_e_acsl__22;
- __e_acsl_mpz_t __gen_e_acsl_add_2;
- __e_acsl_mpz_t __gen_e_acsl_g_8;
- __gmpz_init_set_si(__gen_e_acsl_n_5,(long)n);
- __gmpz_init_set_si(__gen_e_acsl__22,1L);
- __gmpz_init(__gen_e_acsl_add_2);
- __gmpz_add(__gen_e_acsl_add_2,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_n_5),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__22));
- /*@ assert
- Eva: initialization:
- \initialized((__e_acsl_mpz_struct *)__gen_e_acsl_add_2);
- */
- __gen_e_acsl_g_5(& __gen_e_acsl_g_8,
- (__e_acsl_mpz_struct *)__gen_e_acsl_add_2);
- __gmpz_init_set(__gen_e_acsl_if_4,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_g_8));
- __gmpz_clear(__gen_e_acsl_n_5);
- __gmpz_clear(__gen_e_acsl__22);
- __gmpz_clear(__gen_e_acsl_add_2);
- __gmpz_clear(__gen_e_acsl_g_8);
- }
- __gmpz_init_set(*__retres_arg,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_if_4));
- __gmpz_clear(__gen_e_acsl_n_3);
- __gmpz_clear(__gen_e_acsl__14);
- __gmpz_clear(__gen_e_acsl_if_4);
- return;
-}
-
-void __gen_e_acsl_f3_2(__e_acsl_mpz_t *__retres_arg, __e_acsl_mpz_struct * n)
-{
- __e_acsl_mpz_t __gen_e_acsl__16;
- int __gen_e_acsl_gt_2;
- __e_acsl_mpz_t __gen_e_acsl_if_3;
- __gmpz_init_set_si(__gen_e_acsl__16,0L);
- __gen_e_acsl_gt_2 = __gmpz_cmp((__e_acsl_mpz_struct const *)(n),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__16));
- if (__gen_e_acsl_gt_2 > 0) {
- long __gen_e_acsl__17;
- __e_acsl_mpz_t __gen_e_acsl_g_4;
- __e_acsl_mpz_t __gen_e_acsl__18;
- __e_acsl_mpz_t __gen_e_acsl_sub_8;
- __e_acsl_mpz_t __gen_e_acsl_f3_4;
- __e_acsl_mpz_t __gen_e_acsl_mul_3;
- __e_acsl_mpz_t __gen_e_acsl__19;
- __e_acsl_mpz_t __gen_e_acsl_sub_9;
- __gen_e_acsl__17 = __gmpz_get_si((__e_acsl_mpz_struct const *)(n));
- __gen_e_acsl_g(& __gen_e_acsl_g_4,(int)__gen_e_acsl__17);
- __gmpz_init_set_si(__gen_e_acsl__18,1L);
- __gmpz_init(__gen_e_acsl_sub_8);
- __gmpz_sub(__gen_e_acsl_sub_8,(__e_acsl_mpz_struct const *)(n),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__18));
- /*@ assert
- Eva: initialization:
- \initialized((__e_acsl_mpz_struct *)__gen_e_acsl_sub_8);
- */
- __gen_e_acsl_f3_2(& __gen_e_acsl_f3_4,
- (__e_acsl_mpz_struct *)__gen_e_acsl_sub_8);
- __gmpz_init(__gen_e_acsl_mul_3);
- __gmpz_mul(__gen_e_acsl_mul_3,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_g_4),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_f3_4));
- __gmpz_init_set_si(__gen_e_acsl__19,5L);
- __gmpz_init(__gen_e_acsl_sub_9);
- __gmpz_sub(__gen_e_acsl_sub_9,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_mul_3),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__19));
- __gmpz_init_set(__gen_e_acsl_if_3,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_sub_9));
- __gmpz_clear(__gen_e_acsl_g_4);
- __gmpz_clear(__gen_e_acsl__18);
- __gmpz_clear(__gen_e_acsl_sub_8);
- __gmpz_clear(__gen_e_acsl_f3_4);
- __gmpz_clear(__gen_e_acsl_mul_3);
- __gmpz_clear(__gen_e_acsl__19);
- __gmpz_clear(__gen_e_acsl_sub_9);
- }
- else {
- __e_acsl_mpz_t __gen_e_acsl__20;
- __e_acsl_mpz_t __gen_e_acsl_add;
- __e_acsl_mpz_t __gen_e_acsl_g_6;
- __gmpz_init_set_si(__gen_e_acsl__20,1L);
- __gmpz_init(__gen_e_acsl_add);
- __gmpz_add(__gen_e_acsl_add,(__e_acsl_mpz_struct const *)(n),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__20));
- /*@ assert
- Eva: initialization:
- \initialized((__e_acsl_mpz_struct *)__gen_e_acsl_add);
- */
- __gen_e_acsl_g_5(& __gen_e_acsl_g_6,
- (__e_acsl_mpz_struct *)__gen_e_acsl_add);
- __gmpz_init_set(__gen_e_acsl_if_3,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_g_6));
- __gmpz_clear(__gen_e_acsl__20);
- __gmpz_clear(__gen_e_acsl_add);
- __gmpz_clear(__gen_e_acsl_g_6);
- }
- __gmpz_init_set(*__retres_arg,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_if_3));
- __gmpz_clear(__gen_e_acsl__16);
- __gmpz_clear(__gen_e_acsl_if_3);
- return;
-}
-
-void __gen_e_acsl_f4(__e_acsl_mpz_t *__retres_arg, int n)
-{
- __e_acsl_mpz_t __gen_e_acsl_n_6;
- __e_acsl_mpz_t __gen_e_acsl__24;
- int __gen_e_acsl_lt_3;
- __e_acsl_mpz_t __gen_e_acsl_if_8;
- __gmpz_init_set_si(__gen_e_acsl_n_6,(long)n);
- __gmpz_init_set_si(__gen_e_acsl__24,100L);
- __gen_e_acsl_lt_3 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_n_6),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__24));
- if (__gen_e_acsl_lt_3 < 0) {
- __e_acsl_mpz_t __gen_e_acsl_n_7;
- __e_acsl_mpz_t __gen_e_acsl__25;
- __e_acsl_mpz_t __gen_e_acsl_add_3;
- __e_acsl_mpz_t __gen_e_acsl_f4_5;
- __gmpz_init_set_si(__gen_e_acsl_n_7,(long)n);
- __gmpz_init_set_si(__gen_e_acsl__25,1L);
- __gmpz_init(__gen_e_acsl_add_3);
- __gmpz_add(__gen_e_acsl_add_3,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_n_7),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__25));
- /*@ assert
- Eva: initialization:
- \initialized((__e_acsl_mpz_struct *)__gen_e_acsl_add_3);
- */
- __gen_e_acsl_f4_2(& __gen_e_acsl_f4_5,
- (__e_acsl_mpz_struct *)__gen_e_acsl_add_3);
- __gmpz_init_set(__gen_e_acsl_if_8,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_f4_5));
- __gmpz_clear(__gen_e_acsl_n_7);
- __gmpz_clear(__gen_e_acsl__25);
- __gmpz_clear(__gen_e_acsl_add_3);
- __gmpz_clear(__gen_e_acsl_f4_5);
- }
- else {
- __e_acsl_mpz_t __gen_e_acsl_n_8;
- __e_acsl_mpz_t __gen_e_acsl__31;
- int __gen_e_acsl_lt_6;
- __e_acsl_mpz_t __gen_e_acsl_if_7;
- __gmpz_init_set_si(__gen_e_acsl_n_8,(long)n);
- __gmpz_init_set_ui(__gen_e_acsl__31,9223372036854775807UL);
- __gen_e_acsl_lt_6 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_n_8),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__31));
- if (__gen_e_acsl_lt_6 < 0) {
- __e_acsl_mpz_t __gen_e_acsl__32;
- __gmpz_init_set_ui(__gen_e_acsl__32,9223372036854775807UL);
- __gmpz_init_set(__gen_e_acsl_if_7,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__32));
- __gmpz_clear(__gen_e_acsl__32);
- }
- else {
- __e_acsl_mpz_t __gen_e_acsl__33;
- __gmpz_init_set_si(__gen_e_acsl__33,6L);
- __gmpz_init_set(__gen_e_acsl_if_7,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__33));
- __gmpz_clear(__gen_e_acsl__33);
- }
- __gmpz_init_set(__gen_e_acsl_if_8,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_if_7));
- __gmpz_clear(__gen_e_acsl_n_8);
- __gmpz_clear(__gen_e_acsl__31);
- __gmpz_clear(__gen_e_acsl_if_7);
- }
- __gmpz_init_set(*__retres_arg,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_if_8));
- __gmpz_clear(__gen_e_acsl_n_6);
- __gmpz_clear(__gen_e_acsl__24);
- __gmpz_clear(__gen_e_acsl_if_8);
- return;
-}
-
-void __gen_e_acsl_f4_2(__e_acsl_mpz_t *__retres_arg, __e_acsl_mpz_struct * n)
-{
- __e_acsl_mpz_t __gen_e_acsl__26;
- int __gen_e_acsl_lt_4;
- __e_acsl_mpz_t __gen_e_acsl_if_6;
- __gmpz_init_set_si(__gen_e_acsl__26,100L);
- __gen_e_acsl_lt_4 = __gmpz_cmp((__e_acsl_mpz_struct const *)(n),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__26));
- if (__gen_e_acsl_lt_4 < 0) {
- __e_acsl_mpz_t __gen_e_acsl__27;
- __e_acsl_mpz_t __gen_e_acsl_add_4;
- __e_acsl_mpz_t __gen_e_acsl_f4_4;
- __gmpz_init_set_si(__gen_e_acsl__27,1L);
- __gmpz_init(__gen_e_acsl_add_4);
- __gmpz_add(__gen_e_acsl_add_4,(__e_acsl_mpz_struct const *)(n),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__27));
- /*@ assert
- Eva: initialization:
- \initialized((__e_acsl_mpz_struct *)__gen_e_acsl_add_4);
- */
- __gen_e_acsl_f4_2(& __gen_e_acsl_f4_4,
- (__e_acsl_mpz_struct *)__gen_e_acsl_add_4);
- __gmpz_init_set(__gen_e_acsl_if_6,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_f4_4));
- __gmpz_clear(__gen_e_acsl__27);
- __gmpz_clear(__gen_e_acsl_add_4);
- __gmpz_clear(__gen_e_acsl_f4_4);
- }
- else {
- __e_acsl_mpz_t __gen_e_acsl__28;
- int __gen_e_acsl_lt_5;
- __e_acsl_mpz_t __gen_e_acsl_if_5;
- __gmpz_init_set_ui(__gen_e_acsl__28,9223372036854775807UL);
- __gen_e_acsl_lt_5 = __gmpz_cmp((__e_acsl_mpz_struct const *)(n),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__28));
- if (__gen_e_acsl_lt_5 < 0) {
- __e_acsl_mpz_t __gen_e_acsl__29;
- __gmpz_init_set_ui(__gen_e_acsl__29,9223372036854775807UL);
- __gmpz_init_set(__gen_e_acsl_if_5,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__29));
- __gmpz_clear(__gen_e_acsl__29);
- }
- else {
- __e_acsl_mpz_t __gen_e_acsl__30;
- __gmpz_init_set_si(__gen_e_acsl__30,6L);
- __gmpz_init_set(__gen_e_acsl_if_5,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__30));
- __gmpz_clear(__gen_e_acsl__30);
- }
- __gmpz_init_set(__gen_e_acsl_if_6,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_if_5));
- __gmpz_clear(__gen_e_acsl__28);
- __gmpz_clear(__gen_e_acsl_if_5);
- }
- __gmpz_init_set(*__retres_arg,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_if_6));
- __gmpz_clear(__gen_e_acsl__26);
- __gmpz_clear(__gen_e_acsl_if_6);
- return;
-}
-
-
diff --git a/src/plugins/e-acsl/tests/arith/oracle/gen_integer_constant2.c b/src/plugins/e-acsl/tests/arith/oracle/gen_integer_constant2.c
deleted file mode 100644
index bd5aabaa923ae680ccaf997600f18659c1599e98..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/arith/oracle/gen_integer_constant2.c
+++ /dev/null
@@ -1,69 +0,0 @@
-/* Generated by Frama-C */
-#include "stdio.h"
-#include "stdlib.h"
-int main(void)
-{
- int __retres;
- int x;
- __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
- /*@ assert 0 ≡ 0; */
- {
- __e_acsl_mpz_t __gen_e_acsl_;
- int __gen_e_acsl_eq;
- __gmpz_init_set_si(__gen_e_acsl_,0L);
- __gen_e_acsl_eq = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_));
- __e_acsl_assert(__gen_e_acsl_eq == 0,(char *)"Assertion",(char *)"main",
- (char *)"0 == 0",6);
- __gmpz_clear(__gen_e_acsl_);
- }
- x = 0;
- x ++;
- /*@ assert 0 ≢ 1; */
- {
- __e_acsl_mpz_t __gen_e_acsl__2;
- __e_acsl_mpz_t __gen_e_acsl__3;
- int __gen_e_acsl_ne;
- __gmpz_init_set_si(__gen_e_acsl__2,0L);
- __gmpz_init_set_si(__gen_e_acsl__3,1L);
- __gen_e_acsl_ne = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl__2),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__3));
- __e_acsl_assert(__gen_e_acsl_ne != 0,(char *)"Assertion",(char *)"main",
- (char *)"0 != 1",8);
- __gmpz_clear(__gen_e_acsl__2);
- __gmpz_clear(__gen_e_acsl__3);
- }
- /*@ assert 1152921504606846975 ≡ 0xfffffffffffffff; */
- {
- __e_acsl_mpz_t __gen_e_acsl__4;
- int __gen_e_acsl_eq_2;
- __gmpz_init_set_ui(__gen_e_acsl__4,1152921504606846975UL);
- __gen_e_acsl_eq_2 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl__4),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__4));
- __e_acsl_assert(__gen_e_acsl_eq_2 == 0,(char *)"Assertion",
- (char *)"main",
- (char *)"1152921504606846975 == 0xfffffffffffffff",9);
- __gmpz_clear(__gen_e_acsl__4);
- }
- /*@ assert
- 0xffffffffffffffffffffffffffffffff ≡
- 0xffffffffffffffffffffffffffffffff;
- */
- {
- __e_acsl_mpz_t __gen_e_acsl__5;
- int __gen_e_acsl_eq_3;
- __gmpz_init_set_str(__gen_e_acsl__5,
- "340282366920938463463374607431768211455",10);
- __gen_e_acsl_eq_3 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl__5),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__5));
- __e_acsl_assert(__gen_e_acsl_eq_3 == 0,(char *)"Assertion",
- (char *)"main",
- (char *)"0xffffffffffffffffffffffffffffffff == 0xffffffffffffffffffffffffffffffff",
- 11);
- __gmpz_clear(__gen_e_acsl__5);
- }
- __retres = 0;
- return __retres;
-}
-
-
diff --git a/src/plugins/e-acsl/tests/arith/oracle/gen_let2.c b/src/plugins/e-acsl/tests/arith/oracle/gen_let2.c
deleted file mode 100644
index 111063ef2ab67bf20e648ebee2ccb5dcfcac3202..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/arith/oracle/gen_let2.c
+++ /dev/null
@@ -1,293 +0,0 @@
-/* Generated by Frama-C */
-#include "stdio.h"
-#include "stdlib.h"
-struct __anonstruct_r_1 {
- int x ;
- int y ;
-};
-union __anonunion_s_2 {
- int x ;
- char *y ;
-};
-int main(void)
-{
- int __retres;
- union __anonunion_s_2 s;
- __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
- int n = -2;
- /*@ assert \let u = n * n; u ≥ 0; */
- {
- __e_acsl_mpz_t __gen_e_acsl_u;
- __e_acsl_mpz_t __gen_e_acsl_n;
- __e_acsl_mpz_t __gen_e_acsl_mul;
- __e_acsl_mpz_t __gen_e_acsl_;
- int __gen_e_acsl_ge;
- __gmpz_init_set_si(__gen_e_acsl_n,(long)n);
- __gmpz_init(__gen_e_acsl_mul);
- __gmpz_mul(__gen_e_acsl_mul,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_n),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_n));
- __gmpz_init_set(__gen_e_acsl_u,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_mul));
- __gmpz_init_set_si(__gen_e_acsl_,0L);
- __gen_e_acsl_ge = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_u),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_));
- __e_acsl_assert(__gen_e_acsl_ge >= 0,(char *)"Assertion",(char *)"main",
- (char *)"\\let u = n * n; u >= 0",7);
- __gmpz_clear(__gen_e_acsl_u);
- __gmpz_clear(__gen_e_acsl_n);
- __gmpz_clear(__gen_e_acsl_mul);
- __gmpz_clear(__gen_e_acsl_);
- }
- /*@ assert \let u = n * n; \let v = u + 1; u > 0; */
- {
- __e_acsl_mpz_t __gen_e_acsl_u_2;
- __e_acsl_mpz_t __gen_e_acsl_n_2;
- __e_acsl_mpz_t __gen_e_acsl_mul_2;
- __e_acsl_mpz_t __gen_e_acsl_v;
- __e_acsl_mpz_t __gen_e_acsl__2;
- __e_acsl_mpz_t __gen_e_acsl_add;
- __e_acsl_mpz_t __gen_e_acsl__3;
- int __gen_e_acsl_gt;
- __gmpz_init_set_si(__gen_e_acsl_n_2,(long)n);
- __gmpz_init(__gen_e_acsl_mul_2);
- __gmpz_mul(__gen_e_acsl_mul_2,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_n_2),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_n_2));
- __gmpz_init_set(__gen_e_acsl_u_2,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_mul_2));
- __gmpz_init_set_si(__gen_e_acsl__2,1L);
- __gmpz_init(__gen_e_acsl_add);
- __gmpz_add(__gen_e_acsl_add,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_u_2),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__2));
- __gmpz_init_set(__gen_e_acsl_v,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_add));
- __gmpz_init_set_si(__gen_e_acsl__3,0L);
- __gen_e_acsl_gt = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_u_2),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__3));
- __e_acsl_assert(__gen_e_acsl_gt > 0,(char *)"Assertion",(char *)"main",
- (char *)"\\let u = n * n;\n\\let v = u + 1; u > 0",9);
- __gmpz_clear(__gen_e_acsl_u_2);
- __gmpz_clear(__gen_e_acsl_n_2);
- __gmpz_clear(__gen_e_acsl_mul_2);
- __gmpz_clear(__gen_e_acsl_v);
- __gmpz_clear(__gen_e_acsl__2);
- __gmpz_clear(__gen_e_acsl_add);
- __gmpz_clear(__gen_e_acsl__3);
- }
- /*@ assert (\let u = 1; u) + 1 ≡ 2; */
- {
- int __gen_e_acsl_u_3;
- __e_acsl_mpz_t __gen_e_acsl_u_4;
- __e_acsl_mpz_t __gen_e_acsl__4;
- __e_acsl_mpz_t __gen_e_acsl_add_2;
- __e_acsl_mpz_t __gen_e_acsl__5;
- int __gen_e_acsl_eq;
- __gen_e_acsl_u_3 = 1;
- __gmpz_init_set_si(__gen_e_acsl_u_4,(long)__gen_e_acsl_u_3);
- __gmpz_init_set_si(__gen_e_acsl__4,1L);
- __gmpz_init(__gen_e_acsl_add_2);
- __gmpz_add(__gen_e_acsl_add_2,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_u_4),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__4));
- __gmpz_init_set_si(__gen_e_acsl__5,2L);
- __gen_e_acsl_eq = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_add_2),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__5));
- __e_acsl_assert(__gen_e_acsl_eq == 0,(char *)"Assertion",(char *)"main",
- (char *)"(\\let u = 1; u) + 1 == 2",12);
- __gmpz_clear(__gen_e_acsl_u_4);
- __gmpz_clear(__gen_e_acsl__4);
- __gmpz_clear(__gen_e_acsl_add_2);
- __gmpz_clear(__gen_e_acsl__5);
- }
- /*@ assert \let u = 1; (\let v = u + 1; v) ≡ 2; */
- {
- int __gen_e_acsl_u_5;
- __e_acsl_mpz_t __gen_e_acsl_v_2;
- __e_acsl_mpz_t __gen_e_acsl_u_6;
- __e_acsl_mpz_t __gen_e_acsl__6;
- __e_acsl_mpz_t __gen_e_acsl_add_3;
- __e_acsl_mpz_t __gen_e_acsl__7;
- int __gen_e_acsl_eq_2;
- __gen_e_acsl_u_5 = 1;
- __gmpz_init_set_si(__gen_e_acsl_u_6,(long)__gen_e_acsl_u_5);
- __gmpz_init_set_si(__gen_e_acsl__6,1L);
- __gmpz_init(__gen_e_acsl_add_3);
- __gmpz_add(__gen_e_acsl_add_3,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_u_6),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__6));
- __gmpz_init_set(__gen_e_acsl_v_2,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_add_3));
- __gmpz_init_set_si(__gen_e_acsl__7,2L);
- __gen_e_acsl_eq_2 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_v_2),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__7));
- __e_acsl_assert(__gen_e_acsl_eq_2 == 0,(char *)"Assertion",
- (char *)"main",
- (char *)"\\let u = 1; (\\let v = u + 1; v) == 2",14);
- __gmpz_clear(__gen_e_acsl_v_2);
- __gmpz_clear(__gen_e_acsl_u_6);
- __gmpz_clear(__gen_e_acsl__6);
- __gmpz_clear(__gen_e_acsl_add_3);
- __gmpz_clear(__gen_e_acsl__7);
- }
- /*@ assert \let u = 1; (\let u = u + 1; u) ≡ 2; */
- {
- int __gen_e_acsl_u_7;
- __e_acsl_mpz_t __gen_e_acsl_u_8;
- __e_acsl_mpz_t __gen_e_acsl_u_9;
- __e_acsl_mpz_t __gen_e_acsl__8;
- __e_acsl_mpz_t __gen_e_acsl_add_4;
- __e_acsl_mpz_t __gen_e_acsl__9;
- int __gen_e_acsl_eq_3;
- __gen_e_acsl_u_7 = 1;
- __gmpz_init_set_si(__gen_e_acsl_u_9,(long)__gen_e_acsl_u_7);
- __gmpz_init_set_si(__gen_e_acsl__8,1L);
- __gmpz_init(__gen_e_acsl_add_4);
- __gmpz_add(__gen_e_acsl_add_4,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_u_9),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__8));
- __gmpz_init_set(__gen_e_acsl_u_8,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_add_4));
- __gmpz_init_set_si(__gen_e_acsl__9,2L);
- __gen_e_acsl_eq_3 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_u_8),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__9));
- __e_acsl_assert(__gen_e_acsl_eq_3 == 0,(char *)"Assertion",
- (char *)"main",
- (char *)"\\let u = 1; (\\let u = u + 1; u) == 2",17);
- __gmpz_clear(__gen_e_acsl_u_8);
- __gmpz_clear(__gen_e_acsl_u_9);
- __gmpz_clear(__gen_e_acsl__8);
- __gmpz_clear(__gen_e_acsl_add_4);
- __gmpz_clear(__gen_e_acsl__9);
- }
- long m = 0x7fffffffffffffffL;
- /*@ assert (\let u = m; u * u) > m; */
- {
- long __gen_e_acsl_u_10;
- __e_acsl_mpz_t __gen_e_acsl_u_11;
- __e_acsl_mpz_t __gen_e_acsl_mul_3;
- __e_acsl_mpz_t __gen_e_acsl_m;
- int __gen_e_acsl_gt_2;
- __gen_e_acsl_u_10 = m;
- __gmpz_init_set_si(__gen_e_acsl_u_11,__gen_e_acsl_u_10);
- __gmpz_init(__gen_e_acsl_mul_3);
- __gmpz_mul(__gen_e_acsl_mul_3,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_u_11),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_u_11));
- __gmpz_init_set_si(__gen_e_acsl_m,m);
- __gen_e_acsl_gt_2 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_mul_3),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_m));
- __e_acsl_assert(__gen_e_acsl_gt_2 > 0,(char *)"Assertion",(char *)"main",
- (char *)"(\\let u = m; u * u) > m",21);
- __gmpz_clear(__gen_e_acsl_u_11);
- __gmpz_clear(__gen_e_acsl_mul_3);
- __gmpz_clear(__gen_e_acsl_m);
- }
- char c = (char)'a';
- /*@ assert \let u = 'b'; c < u; */
- {
- int __gen_e_acsl_u_12;
- __e_acsl_mpz_t __gen_e_acsl_c;
- __e_acsl_mpz_t __gen_e_acsl_u_13;
- int __gen_e_acsl_lt;
- __gen_e_acsl_u_12 = 'b';
- __gmpz_init_set_si(__gen_e_acsl_c,(long)c);
- __gmpz_init_set_si(__gen_e_acsl_u_13,(long)__gen_e_acsl_u_12);
- __gen_e_acsl_lt = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_c),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_u_13));
- __e_acsl_assert(__gen_e_acsl_lt < 0,(char *)"Assertion",(char *)"main",
- (char *)"\\let u = \'b\'; c < u",24);
- __gmpz_clear(__gen_e_acsl_c);
- __gmpz_clear(__gen_e_acsl_u_13);
- }
- float f = 1.0f;
- __e_acsl_store_block((void *)(& f),(size_t)4);
- __e_acsl_full_init((void *)(& f));
- /*@ assert \let u = f; u ≡ f; */
- {
- float __gen_e_acsl_u_14;
- __gen_e_acsl_u_14 = f;
- __e_acsl_assert(__gen_e_acsl_u_14 == f,(char *)"Assertion",
- (char *)"main",(char *)"\\let u = f; u == f",27);
- }
- int t[4] = {1, 2, 3, 4};
- /*@ assert \let u = &t[1]; 1 ≡ 1; */
- {
- int * /*[4]*/ __gen_e_acsl_u_15;
- __e_acsl_mpz_t __gen_e_acsl__10;
- int __gen_e_acsl_eq_4;
- __gen_e_acsl_u_15 = & t[1];
- __gmpz_init_set_si(__gen_e_acsl__10,1L);
- __gen_e_acsl_eq_4 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl__10),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__10));
- __e_acsl_assert(__gen_e_acsl_eq_4 == 0,(char *)"Assertion",
- (char *)"main",(char *)"\\let u = &t[1]; 1 == 1",30);
- __gmpz_clear(__gen_e_acsl__10);
- }
- /*@ assert (\let u = &t[1]; 1) ≡ 1; */
- {
- int * /*[4]*/ __gen_e_acsl_u_16;
- __e_acsl_mpz_t __gen_e_acsl__11;
- int __gen_e_acsl_eq_5;
- __gen_e_acsl_u_16 = & t[1];
- __gmpz_init_set_si(__gen_e_acsl__11,1L);
- __gen_e_acsl_eq_5 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl__11),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__11));
- __e_acsl_assert(__gen_e_acsl_eq_5 == 0,(char *)"Assertion",
- (char *)"main",(char *)"(\\let u = &t[1]; 1) == 1",32);
- __gmpz_clear(__gen_e_acsl__11);
- }
- struct __anonstruct_r_1 r = {.x = 1, .y = 2};
- __e_acsl_store_block((void *)(& r),(size_t)8);
- __e_acsl_full_init((void *)(& r));
- /*@ assert \let u = r; u.x + u.y ≡ 3; */
- {
- struct __anonstruct_r_1 __gen_e_acsl_u_17;
- __e_acsl_mpz_t __gen_e_acsl__12;
- __e_acsl_mpz_t __gen_e_acsl__13;
- __e_acsl_mpz_t __gen_e_acsl_add_5;
- __e_acsl_mpz_t __gen_e_acsl__14;
- int __gen_e_acsl_eq_6;
- __gen_e_acsl_u_17 = r;
- __gmpz_init_set_si(__gen_e_acsl__12,(long)__gen_e_acsl_u_17.x);
- __gmpz_init_set_si(__gen_e_acsl__13,(long)__gen_e_acsl_u_17.y);
- __gmpz_init(__gen_e_acsl_add_5);
- __gmpz_add(__gen_e_acsl_add_5,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__12),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__13));
- __gmpz_init_set_si(__gen_e_acsl__14,3L);
- __gen_e_acsl_eq_6 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_add_5),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__14));
- __e_acsl_assert(__gen_e_acsl_eq_6 == 0,(char *)"Assertion",
- (char *)"main",(char *)"\\let u = r; u.x + u.y == 3",35);
- __gmpz_clear(__gen_e_acsl__12);
- __gmpz_clear(__gen_e_acsl__13);
- __gmpz_clear(__gen_e_acsl_add_5);
- __gmpz_clear(__gen_e_acsl__14);
- }
- s.x = 5;
- /*@ assert (\let u = s; u.x) > 0; */
- {
- union __anonunion_s_2 __gen_e_acsl_u_18;
- __e_acsl_mpz_t __gen_e_acsl__15;
- __e_acsl_mpz_t __gen_e_acsl__16;
- int __gen_e_acsl_gt_3;
- __gen_e_acsl_u_18 = s;
- __gmpz_init_set_si(__gen_e_acsl__15,(long)__gen_e_acsl_u_18.x);
- __gmpz_init_set_si(__gen_e_acsl__16,0L);
- __gen_e_acsl_gt_3 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl__15),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__16));
- __e_acsl_assert(__gen_e_acsl_gt_3 > 0,(char *)"Assertion",(char *)"main",
- (char *)"(\\let u = s; u.x) > 0",39);
- __gmpz_clear(__gen_e_acsl__15);
- __gmpz_clear(__gen_e_acsl__16);
- }
- __retres = 0;
- __e_acsl_delete_block((void *)(& r));
- __e_acsl_delete_block((void *)(& f));
- __e_acsl_memory_clean();
- return __retres;
-}
-
-
diff --git a/src/plugins/e-acsl/tests/arith/oracle/gen_longlong2.c b/src/plugins/e-acsl/tests/arith/oracle/gen_longlong2.c
deleted file mode 100644
index 203245a06493a161763875b504af3b52ade5466b..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/arith/oracle/gen_longlong2.c
+++ /dev/null
@@ -1,80 +0,0 @@
-/* Generated by Frama-C */
-#include "stdio.h"
-#include "stdlib.h"
-unsigned long long my_pow(unsigned int x, unsigned int n)
-{
- unsigned long long __retres;
- int tmp;
- unsigned long long tmp_0;
- if (n <= (unsigned int)1) {
- __retres = (unsigned long long)1;
- goto return_label;
- }
- tmp_0 = my_pow(x,n / (unsigned int)2);
- tmp = (int)tmp_0;
- /*@ assert Eva: signed_overflow: -2147483648 ≤ tmp * tmp; */
- /*@ assert Eva: signed_overflow: tmp * tmp ≤ 2147483647; */
- tmp *= tmp;
- if (n % (unsigned int)2 == (unsigned int)0) {
- __retres = (unsigned long long)tmp;
- goto return_label;
- }
- __retres = (unsigned long long)(x * (unsigned int)tmp);
- return_label: return __retres;
-}
-
-int main(void)
-{
- int __retres;
- __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
- unsigned long long x = my_pow((unsigned int)2,(unsigned int)63);
- /*@ assert (2 * x + 1) % 2 ≡ 1; */
- {
- __e_acsl_mpz_t __gen_e_acsl_;
- __e_acsl_mpz_t __gen_e_acsl_x;
- __e_acsl_mpz_t __gen_e_acsl_mul;
- __e_acsl_mpz_t __gen_e_acsl__2;
- __e_acsl_mpz_t __gen_e_acsl_add;
- __e_acsl_mpz_t __gen_e_acsl__3;
- int __gen_e_acsl_mod_guard;
- __e_acsl_mpz_t __gen_e_acsl_mod;
- int __gen_e_acsl_eq;
- __gmpz_init_set_si(__gen_e_acsl_,2L);
- __gmpz_init(__gen_e_acsl_x);
- __gmpz_import(__gen_e_acsl_x,(size_t)1,1,(size_t)8,0,(size_t)0,
- (void const *)(& x));
- __gmpz_init(__gen_e_acsl_mul);
- __gmpz_mul(__gen_e_acsl_mul,(__e_acsl_mpz_struct const *)(__gen_e_acsl_),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_x));
- __gmpz_init_set_si(__gen_e_acsl__2,1L);
- __gmpz_init(__gen_e_acsl_add);
- __gmpz_add(__gen_e_acsl_add,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_mul),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__2));
- __gmpz_init_set_si(__gen_e_acsl__3,0L);
- __gen_e_acsl_mod_guard = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__3));
- __gmpz_init(__gen_e_acsl_mod);
- /*@ assert E_ACSL: 2 ≢ 0; */
- __e_acsl_assert(! (__gen_e_acsl_mod_guard == 0),(char *)"Assertion",
- (char *)"main",(char *)"2 == 0",17);
- __gmpz_tdiv_r(__gen_e_acsl_mod,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_add),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_));
- __gen_e_acsl_eq = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_mod),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__2));
- __e_acsl_assert(__gen_e_acsl_eq == 0,(char *)"Assertion",(char *)"main",
- (char *)"(2 * x + 1) % 2 == 1",17);
- __gmpz_clear(__gen_e_acsl_);
- __gmpz_clear(__gen_e_acsl_x);
- __gmpz_clear(__gen_e_acsl_mul);
- __gmpz_clear(__gen_e_acsl__2);
- __gmpz_clear(__gen_e_acsl_add);
- __gmpz_clear(__gen_e_acsl__3);
- __gmpz_clear(__gen_e_acsl_mod);
- }
- __retres = 0;
- return __retres;
-}
-
-
diff --git a/src/plugins/e-acsl/tests/arith/oracle/gen_not2.c b/src/plugins/e-acsl/tests/arith/oracle/gen_not2.c
deleted file mode 100644
index 93d25da6a7e7515b76a88c683328b2dd0815c2da..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/arith/oracle/gen_not2.c
+++ /dev/null
@@ -1,43 +0,0 @@
-/* Generated by Frama-C */
-#include "stdio.h"
-#include "stdlib.h"
-int main(void)
-{
- int __retres;
- __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
- int x = 0;
- /*@ assert x ≡ 0; */
- {
- __e_acsl_mpz_t __gen_e_acsl_x;
- __e_acsl_mpz_t __gen_e_acsl_;
- int __gen_e_acsl_eq;
- __gmpz_init_set_si(__gen_e_acsl_x,(long)x);
- __gmpz_init_set_si(__gen_e_acsl_,0L);
- __gen_e_acsl_eq = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_x),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_));
- __e_acsl_assert(__gen_e_acsl_eq == 0,(char *)"Assertion",(char *)"main",
- (char *)"x == 0",6);
- __gmpz_clear(__gen_e_acsl_x);
- __gmpz_clear(__gen_e_acsl_);
- }
- if (x) {
- /*@ assert x ≢ 0; */
- {
- __e_acsl_mpz_t __gen_e_acsl_x_2;
- __e_acsl_mpz_t __gen_e_acsl__2;
- int __gen_e_acsl_ne;
- __gmpz_init_set_si(__gen_e_acsl_x_2,(long)x);
- __gmpz_init_set_si(__gen_e_acsl__2,0L);
- __gen_e_acsl_ne = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_x_2),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__2));
- __e_acsl_assert(__gen_e_acsl_ne != 0,(char *)"Assertion",
- (char *)"main",(char *)"x != 0",7);
- __gmpz_clear(__gen_e_acsl_x_2);
- __gmpz_clear(__gen_e_acsl__2);
- }
- }
- __retres = 0;
- return __retres;
-}
-
-
diff --git a/src/plugins/e-acsl/tests/arith/oracle/gen_quantif2.c b/src/plugins/e-acsl/tests/arith/oracle/gen_quantif2.c
deleted file mode 100644
index 4559cf6c2d592cf1abcf1516a3358f8c38c61af6..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/arith/oracle/gen_quantif2.c
+++ /dev/null
@@ -1,796 +0,0 @@
-/* Generated by Frama-C */
-#include "stdio.h"
-#include "stdlib.h"
-int main(void)
-{
- int __retres;
- __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
- /*@ assert ∀ ℤ x; 0 ≤ x ≤ 1 ⇒ x ≡ 0 ∨ x ≡ 1; */
- {
- int __gen_e_acsl_forall;
- __e_acsl_mpz_t __gen_e_acsl_x;
- __gen_e_acsl_forall = 1;
- __gmpz_init(__gen_e_acsl_x);
- {
- __e_acsl_mpz_t __gen_e_acsl__3;
- __gmpz_init_set_si(__gen_e_acsl__3,0L);
- __gmpz_set(__gen_e_acsl_x,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__3));
- __gmpz_clear(__gen_e_acsl__3);
- }
- while (1) {
- {
- __e_acsl_mpz_t __gen_e_acsl__4;
- int __gen_e_acsl_le;
- __gmpz_init_set_si(__gen_e_acsl__4,1L);
- __gen_e_acsl_le = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_x),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__4));
- if (__gen_e_acsl_le <= 0) ; else break;
- __gmpz_clear(__gen_e_acsl__4);
- }
- {
- __e_acsl_mpz_t __gen_e_acsl_;
- int __gen_e_acsl_eq;
- int __gen_e_acsl_or;
- __gmpz_init_set_si(__gen_e_acsl_,0L);
- __gen_e_acsl_eq = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_x),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_));
- if (__gen_e_acsl_eq == 0) __gen_e_acsl_or = 1;
- else {
- __e_acsl_mpz_t __gen_e_acsl__2;
- int __gen_e_acsl_eq_2;
- __gmpz_init_set_si(__gen_e_acsl__2,1L);
- __gen_e_acsl_eq_2 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_x),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__2));
- __gen_e_acsl_or = __gen_e_acsl_eq_2 == 0;
- __gmpz_clear(__gen_e_acsl__2);
- }
- __gmpz_clear(__gen_e_acsl_);
- if (__gen_e_acsl_or) ;
- else {
- __gen_e_acsl_forall = 0;
- goto e_acsl_end_loop1;
- }
- }
- {
- __e_acsl_mpz_t __gen_e_acsl__5;
- __e_acsl_mpz_t __gen_e_acsl_add;
- __gmpz_init_set_str(__gen_e_acsl__5,"1",10);
- __gmpz_init(__gen_e_acsl_add);
- __gmpz_add(__gen_e_acsl_add,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_x),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__5));
- __gmpz_set(__gen_e_acsl_x,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_add));
- __gmpz_clear(__gen_e_acsl__5);
- __gmpz_clear(__gen_e_acsl_add);
- }
- }
- e_acsl_end_loop1: ;
- __e_acsl_assert(__gen_e_acsl_forall,(char *)"Assertion",(char *)"main",
- (char *)"\\forall integer x; 0 <= x <= 1 ==> x == 0 || x == 1",
- 9);
- __gmpz_clear(__gen_e_acsl_x);
- }
- /*@ assert ∀ ℤ x; 0 < x ≤ 1 ⇒ x ≡ 1; */
- {
- int __gen_e_acsl_forall_2;
- __e_acsl_mpz_t __gen_e_acsl_x_2;
- __gen_e_acsl_forall_2 = 1;
- __gmpz_init(__gen_e_acsl_x_2);
- {
- __e_acsl_mpz_t __gen_e_acsl__7;
- __e_acsl_mpz_t __gen_e_acsl__8;
- __e_acsl_mpz_t __gen_e_acsl_add_2;
- __gmpz_init_set_si(__gen_e_acsl__7,0L);
- __gmpz_init_set_si(__gen_e_acsl__8,1L);
- __gmpz_init(__gen_e_acsl_add_2);
- __gmpz_add(__gen_e_acsl_add_2,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__7),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__8));
- __gmpz_set(__gen_e_acsl_x_2,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_add_2));
- __gmpz_clear(__gen_e_acsl__7);
- __gmpz_clear(__gen_e_acsl__8);
- __gmpz_clear(__gen_e_acsl_add_2);
- }
- while (1) {
- {
- __e_acsl_mpz_t __gen_e_acsl__9;
- int __gen_e_acsl_le_2;
- __gmpz_init_set_si(__gen_e_acsl__9,1L);
- __gen_e_acsl_le_2 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_x_2),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__9));
- if (__gen_e_acsl_le_2 <= 0) ; else break;
- __gmpz_clear(__gen_e_acsl__9);
- }
- {
- __e_acsl_mpz_t __gen_e_acsl__6;
- int __gen_e_acsl_eq_3;
- __gmpz_init_set_si(__gen_e_acsl__6,1L);
- __gen_e_acsl_eq_3 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_x_2),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__6));
- __gmpz_clear(__gen_e_acsl__6);
- if (__gen_e_acsl_eq_3 == 0) ;
- else {
- __gen_e_acsl_forall_2 = 0;
- goto e_acsl_end_loop2;
- }
- }
- {
- __e_acsl_mpz_t __gen_e_acsl__10;
- __e_acsl_mpz_t __gen_e_acsl_add_3;
- __gmpz_init_set_str(__gen_e_acsl__10,"1",10);
- __gmpz_init(__gen_e_acsl_add_3);
- __gmpz_add(__gen_e_acsl_add_3,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_x_2),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__10));
- __gmpz_set(__gen_e_acsl_x_2,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_add_3));
- __gmpz_clear(__gen_e_acsl__10);
- __gmpz_clear(__gen_e_acsl_add_3);
- }
- }
- e_acsl_end_loop2: ;
- __e_acsl_assert(__gen_e_acsl_forall_2,(char *)"Assertion",(char *)"main",
- (char *)"\\forall integer x; 0 < x <= 1 ==> x == 1",10);
- __gmpz_clear(__gen_e_acsl_x_2);
- }
- /*@ assert ∀ ℤ x; 0 ≤ x < 1 ⇒ x ≡ 0; */
- {
- int __gen_e_acsl_forall_3;
- __e_acsl_mpz_t __gen_e_acsl_x_3;
- __gen_e_acsl_forall_3 = 1;
- __gmpz_init(__gen_e_acsl_x_3);
- {
- __e_acsl_mpz_t __gen_e_acsl__12;
- __gmpz_init_set_si(__gen_e_acsl__12,0L);
- __gmpz_set(__gen_e_acsl_x_3,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__12));
- __gmpz_clear(__gen_e_acsl__12);
- }
- while (1) {
- {
- __e_acsl_mpz_t __gen_e_acsl__13;
- int __gen_e_acsl_lt;
- __gmpz_init_set_si(__gen_e_acsl__13,1L);
- __gen_e_acsl_lt = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_x_3),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__13));
- if (__gen_e_acsl_lt < 0) ; else break;
- __gmpz_clear(__gen_e_acsl__13);
- }
- {
- __e_acsl_mpz_t __gen_e_acsl__11;
- int __gen_e_acsl_eq_4;
- __gmpz_init_set_si(__gen_e_acsl__11,0L);
- __gen_e_acsl_eq_4 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_x_3),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__11));
- __gmpz_clear(__gen_e_acsl__11);
- if (__gen_e_acsl_eq_4 == 0) ;
- else {
- __gen_e_acsl_forall_3 = 0;
- goto e_acsl_end_loop3;
- }
- }
- {
- __e_acsl_mpz_t __gen_e_acsl__14;
- __e_acsl_mpz_t __gen_e_acsl_add_4;
- __gmpz_init_set_str(__gen_e_acsl__14,"1",10);
- __gmpz_init(__gen_e_acsl_add_4);
- __gmpz_add(__gen_e_acsl_add_4,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_x_3),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__14));
- __gmpz_set(__gen_e_acsl_x_3,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_add_4));
- __gmpz_clear(__gen_e_acsl__14);
- __gmpz_clear(__gen_e_acsl_add_4);
- }
- }
- e_acsl_end_loop3: ;
- __e_acsl_assert(__gen_e_acsl_forall_3,(char *)"Assertion",(char *)"main",
- (char *)"\\forall integer x; 0 <= x < 1 ==> x == 0",11);
- __gmpz_clear(__gen_e_acsl_x_3);
- }
- /*@ assert
- ∀ ℤ x, ℤ y, ℤ z;
- 0 ≤ x < 2 ∧ 0 ≤ y < 5 ∧ 0 ≤ z ≤ y ⇒ x + z ≤ y + 1;
- */
- {
- int __gen_e_acsl_forall_4;
- __e_acsl_mpz_t __gen_e_acsl_x_4;
- __e_acsl_mpz_t __gen_e_acsl_y;
- __e_acsl_mpz_t __gen_e_acsl_z;
- __gen_e_acsl_forall_4 = 1;
- __gmpz_init(__gen_e_acsl_x_4);
- __gmpz_init(__gen_e_acsl_y);
- __gmpz_init(__gen_e_acsl_z);
- {
- __e_acsl_mpz_t __gen_e_acsl__21;
- __gmpz_init_set_si(__gen_e_acsl__21,0L);
- __gmpz_set(__gen_e_acsl_x_4,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__21));
- __gmpz_clear(__gen_e_acsl__21);
- }
- while (1) {
- {
- __e_acsl_mpz_t __gen_e_acsl__22;
- int __gen_e_acsl_lt_3;
- __gmpz_init_set_si(__gen_e_acsl__22,2L);
- __gen_e_acsl_lt_3 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_x_4),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__22));
- if (__gen_e_acsl_lt_3 < 0) ; else break;
- __gmpz_clear(__gen_e_acsl__22);
- }
- {
- __e_acsl_mpz_t __gen_e_acsl__18;
- __gmpz_init_set_si(__gen_e_acsl__18,0L);
- __gmpz_set(__gen_e_acsl_y,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__18));
- __gmpz_clear(__gen_e_acsl__18);
- }
- while (1) {
- {
- __e_acsl_mpz_t __gen_e_acsl__19;
- int __gen_e_acsl_lt_2;
- __gmpz_init_set_si(__gen_e_acsl__19,5L);
- __gen_e_acsl_lt_2 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_y),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__19));
- if (__gen_e_acsl_lt_2 < 0) ; else break;
- __gmpz_clear(__gen_e_acsl__19);
- }
- {
- __e_acsl_mpz_t __gen_e_acsl__16;
- __gmpz_init_set_si(__gen_e_acsl__16,0L);
- __gmpz_set(__gen_e_acsl_z,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__16));
- __gmpz_clear(__gen_e_acsl__16);
- }
- while (1) {
- {
- int __gen_e_acsl_le_4;
- __gen_e_acsl_le_4 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_z),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_y));
- if (__gen_e_acsl_le_4 <= 0) ; else break;
- }
- {
- __e_acsl_mpz_t __gen_e_acsl_add_5;
- __e_acsl_mpz_t __gen_e_acsl__15;
- __e_acsl_mpz_t __gen_e_acsl_add_6;
- int __gen_e_acsl_le_3;
- __gmpz_init(__gen_e_acsl_add_5);
- __gmpz_add(__gen_e_acsl_add_5,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_x_4),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_z));
- __gmpz_init_set_si(__gen_e_acsl__15,1L);
- __gmpz_init(__gen_e_acsl_add_6);
- __gmpz_add(__gen_e_acsl_add_6,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_y),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__15));
- __gen_e_acsl_le_3 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_add_5),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_add_6));
- __gmpz_clear(__gen_e_acsl_add_5);
- __gmpz_clear(__gen_e_acsl__15);
- __gmpz_clear(__gen_e_acsl_add_6);
- if (__gen_e_acsl_le_3 <= 0) ;
- else {
- __gen_e_acsl_forall_4 = 0;
- goto e_acsl_end_loop4;
- }
- }
- {
- __e_acsl_mpz_t __gen_e_acsl__17;
- __e_acsl_mpz_t __gen_e_acsl_add_7;
- __gmpz_init_set_str(__gen_e_acsl__17,"1",10);
- __gmpz_init(__gen_e_acsl_add_7);
- __gmpz_add(__gen_e_acsl_add_7,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_z),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__17));
- __gmpz_set(__gen_e_acsl_z,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_add_7));
- __gmpz_clear(__gen_e_acsl__17);
- __gmpz_clear(__gen_e_acsl_add_7);
- }
- }
- {
- __e_acsl_mpz_t __gen_e_acsl__20;
- __e_acsl_mpz_t __gen_e_acsl_add_8;
- __gmpz_init_set_str(__gen_e_acsl__20,"1",10);
- __gmpz_init(__gen_e_acsl_add_8);
- __gmpz_add(__gen_e_acsl_add_8,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_y),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__20));
- __gmpz_set(__gen_e_acsl_y,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_add_8));
- __gmpz_clear(__gen_e_acsl__20);
- __gmpz_clear(__gen_e_acsl_add_8);
- }
- }
- {
- __e_acsl_mpz_t __gen_e_acsl__23;
- __e_acsl_mpz_t __gen_e_acsl_add_9;
- __gmpz_init_set_str(__gen_e_acsl__23,"1",10);
- __gmpz_init(__gen_e_acsl_add_9);
- __gmpz_add(__gen_e_acsl_add_9,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_x_4),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__23));
- __gmpz_set(__gen_e_acsl_x_4,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_add_9));
- __gmpz_clear(__gen_e_acsl__23);
- __gmpz_clear(__gen_e_acsl_add_9);
- }
- }
- e_acsl_end_loop4: ;
- __e_acsl_assert(__gen_e_acsl_forall_4,(char *)"Assertion",(char *)"main",
- (char *)"\\forall integer x, integer y, integer z;\n 0 <= x < 2 && 0 <= y < 5 && 0 <= z <= y ==> x + z <= y + 1",
- 15);
- __gmpz_clear(__gen_e_acsl_x_4);
- __gmpz_clear(__gen_e_acsl_y);
- __gmpz_clear(__gen_e_acsl_z);
- }
- /*@ assert ∃ int x; 0 ≤ x < 10 ∧ x ≡ 5; */
- {
- int __gen_e_acsl_exists;
- __e_acsl_mpz_t __gen_e_acsl_x_5;
- __gen_e_acsl_exists = 0;
- __gmpz_init(__gen_e_acsl_x_5);
- {
- __e_acsl_mpz_t __gen_e_acsl__25;
- __gmpz_init_set_si(__gen_e_acsl__25,0L);
- __gmpz_set(__gen_e_acsl_x_5,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__25));
- __gmpz_clear(__gen_e_acsl__25);
- }
- while (1) {
- {
- __e_acsl_mpz_t __gen_e_acsl__26;
- int __gen_e_acsl_lt_4;
- __gmpz_init_set_si(__gen_e_acsl__26,10L);
- __gen_e_acsl_lt_4 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_x_5),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__26));
- if (__gen_e_acsl_lt_4 < 0) ; else break;
- __gmpz_clear(__gen_e_acsl__26);
- }
- {
- __e_acsl_mpz_t __gen_e_acsl__24;
- int __gen_e_acsl_eq_5;
- __gmpz_init_set_si(__gen_e_acsl__24,5L);
- __gen_e_acsl_eq_5 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_x_5),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__24));
- __gmpz_clear(__gen_e_acsl__24);
- if (! (__gen_e_acsl_eq_5 == 0)) ;
- else {
- __gen_e_acsl_exists = 1;
- goto e_acsl_end_loop5;
- }
- }
- {
- __e_acsl_mpz_t __gen_e_acsl__27;
- __e_acsl_mpz_t __gen_e_acsl_add_10;
- __gmpz_init_set_str(__gen_e_acsl__27,"1",10);
- __gmpz_init(__gen_e_acsl_add_10);
- __gmpz_add(__gen_e_acsl_add_10,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_x_5),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__27));
- __gmpz_set(__gen_e_acsl_x_5,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_add_10));
- __gmpz_clear(__gen_e_acsl__27);
- __gmpz_clear(__gen_e_acsl_add_10);
- }
- }
- e_acsl_end_loop5: ;
- __e_acsl_assert(__gen_e_acsl_exists,(char *)"Assertion",(char *)"main",
- (char *)"\\exists int x; 0 <= x < 10 && x == 5",20);
- __gmpz_clear(__gen_e_acsl_x_5);
- }
- /*@ assert
- ∀ int x;
- 0 ≤ x < 10 ⇒
- x % 2 ≡ 0 ⇒ (∃ ℤ y; 0 ≤ y ≤ x / 2 ∧ x ≡ 2 * y);
- */
- {
- int __gen_e_acsl_forall_5;
- __e_acsl_mpz_t __gen_e_acsl_x_6;
- __gen_e_acsl_forall_5 = 1;
- __gmpz_init(__gen_e_acsl_x_6);
- {
- __e_acsl_mpz_t __gen_e_acsl__35;
- __gmpz_init_set_si(__gen_e_acsl__35,0L);
- __gmpz_set(__gen_e_acsl_x_6,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__35));
- __gmpz_clear(__gen_e_acsl__35);
- }
- while (1) {
- {
- __e_acsl_mpz_t __gen_e_acsl__36;
- int __gen_e_acsl_lt_5;
- __gmpz_init_set_si(__gen_e_acsl__36,10L);
- __gen_e_acsl_lt_5 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_x_6),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__36));
- if (__gen_e_acsl_lt_5 < 0) ; else break;
- __gmpz_clear(__gen_e_acsl__36);
- }
- {
- __e_acsl_mpz_t __gen_e_acsl__28;
- __e_acsl_mpz_t __gen_e_acsl__29;
- int __gen_e_acsl_mod_guard;
- __e_acsl_mpz_t __gen_e_acsl_mod;
- int __gen_e_acsl_eq_6;
- int __gen_e_acsl_implies;
- __gmpz_init_set_si(__gen_e_acsl__28,2L);
- __gmpz_init_set_si(__gen_e_acsl__29,0L);
- __gen_e_acsl_mod_guard = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl__28),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__29));
- __gmpz_init(__gen_e_acsl_mod);
- /*@ assert E_ACSL: 2 ≢ 0; */
- __e_acsl_assert(! (__gen_e_acsl_mod_guard == 0),(char *)"Assertion",
- (char *)"main",(char *)"2 == 0",25);
- __gmpz_tdiv_r(__gen_e_acsl_mod,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_x_6),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__28));
- __gen_e_acsl_eq_6 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_mod),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__29));
- if (! (__gen_e_acsl_eq_6 == 0)) __gen_e_acsl_implies = 1;
- else {
- int __gen_e_acsl_exists_2;
- __e_acsl_mpz_t __gen_e_acsl_y_2;
- __gen_e_acsl_exists_2 = 0;
- __gmpz_init(__gen_e_acsl_y_2);
- {
- __e_acsl_mpz_t __gen_e_acsl__31;
- __gmpz_init_set_si(__gen_e_acsl__31,0L);
- __gmpz_set(__gen_e_acsl_y_2,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__31));
- __gmpz_clear(__gen_e_acsl__31);
- }
- while (1) {
- {
- __e_acsl_mpz_t __gen_e_acsl__32;
- __e_acsl_mpz_t __gen_e_acsl__33;
- int __gen_e_acsl_div_guard;
- __e_acsl_mpz_t __gen_e_acsl_div;
- int __gen_e_acsl_le_5;
- __gmpz_init_set_si(__gen_e_acsl__32,2L);
- __gmpz_init_set_si(__gen_e_acsl__33,0L);
- __gen_e_acsl_div_guard = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl__32),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__33));
- __gmpz_init(__gen_e_acsl_div);
- /*@ assert E_ACSL: 2 ≢ 0; */
- __e_acsl_assert(! (__gen_e_acsl_div_guard == 0),
- (char *)"Assertion",(char *)"main",
- (char *)"2 == 0",25);
- __gmpz_tdiv_q(__gen_e_acsl_div,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_x_6),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__32));
- __gen_e_acsl_le_5 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_y_2),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_div));
- if (__gen_e_acsl_le_5 <= 0) ; else break;
- __gmpz_clear(__gen_e_acsl__32);
- __gmpz_clear(__gen_e_acsl__33);
- __gmpz_clear(__gen_e_acsl_div);
- }
- {
- __e_acsl_mpz_t __gen_e_acsl__30;
- __e_acsl_mpz_t __gen_e_acsl_mul;
- int __gen_e_acsl_eq_7;
- __gmpz_init_set_si(__gen_e_acsl__30,2L);
- __gmpz_init(__gen_e_acsl_mul);
- __gmpz_mul(__gen_e_acsl_mul,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__30),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_y_2));
- __gen_e_acsl_eq_7 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_x_6),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_mul));
- __gmpz_clear(__gen_e_acsl__30);
- __gmpz_clear(__gen_e_acsl_mul);
- if (! (__gen_e_acsl_eq_7 == 0)) ;
- else {
- __gen_e_acsl_exists_2 = 1;
- goto e_acsl_end_loop6;
- }
- }
- {
- __e_acsl_mpz_t __gen_e_acsl__34;
- __e_acsl_mpz_t __gen_e_acsl_add_11;
- __gmpz_init_set_str(__gen_e_acsl__34,"1",10);
- __gmpz_init(__gen_e_acsl_add_11);
- __gmpz_add(__gen_e_acsl_add_11,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_y_2),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__34));
- __gmpz_set(__gen_e_acsl_y_2,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_add_11));
- __gmpz_clear(__gen_e_acsl__34);
- __gmpz_clear(__gen_e_acsl_add_11);
- }
- }
- e_acsl_end_loop6: ;
- __gen_e_acsl_implies = __gen_e_acsl_exists_2;
- __gmpz_clear(__gen_e_acsl_y_2);
- }
- __gmpz_clear(__gen_e_acsl__28);
- __gmpz_clear(__gen_e_acsl__29);
- __gmpz_clear(__gen_e_acsl_mod);
- if (__gen_e_acsl_implies) ;
- else {
- __gen_e_acsl_forall_5 = 0;
- goto e_acsl_end_loop7;
- }
- }
- {
- __e_acsl_mpz_t __gen_e_acsl__37;
- __e_acsl_mpz_t __gen_e_acsl_add_12;
- __gmpz_init_set_str(__gen_e_acsl__37,"1",10);
- __gmpz_init(__gen_e_acsl_add_12);
- __gmpz_add(__gen_e_acsl_add_12,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_x_6),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__37));
- __gmpz_set(__gen_e_acsl_x_6,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_add_12));
- __gmpz_clear(__gen_e_acsl__37);
- __gmpz_clear(__gen_e_acsl_add_12);
- }
- }
- e_acsl_end_loop7: ;
- __e_acsl_assert(__gen_e_acsl_forall_5,(char *)"Assertion",(char *)"main",
- (char *)"\\forall int x;\n 0 <= x < 10 ==>\n x % 2 == 0 ==> (\\exists integer y; 0 <= y <= x / 2 && x == 2 * y)",
- 24);
- __gmpz_clear(__gen_e_acsl_x_6);
- }
- {
- int buf[10];
- __e_acsl_store_block((void *)(buf),(size_t)40);
- unsigned long len = (unsigned long)9;
- /*@ assert ∀ ℤ i; 0 ≤ i < 10 ⇒ \valid(&buf[i]); */
- {
- int __gen_e_acsl_forall_6;
- __e_acsl_mpz_t __gen_e_acsl_i;
- __gen_e_acsl_forall_6 = 1;
- __gmpz_init(__gen_e_acsl_i);
- {
- __e_acsl_mpz_t __gen_e_acsl__38;
- __gmpz_init_set_si(__gen_e_acsl__38,0L);
- __gmpz_set(__gen_e_acsl_i,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__38));
- __gmpz_clear(__gen_e_acsl__38);
- }
- while (1) {
- {
- __e_acsl_mpz_t __gen_e_acsl__39;
- int __gen_e_acsl_lt_6;
- __gmpz_init_set_si(__gen_e_acsl__39,10L);
- __gen_e_acsl_lt_6 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_i),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__39));
- if (__gen_e_acsl_lt_6 < 0) ; else break;
- __gmpz_clear(__gen_e_acsl__39);
- }
- {
- long __gen_e_acsl_i_2;
- int __gen_e_acsl_valid;
- __gen_e_acsl_i_2 = __gmpz_get_si((__e_acsl_mpz_struct const *)(__gen_e_acsl_i));
- __gen_e_acsl_valid = __e_acsl_valid((void *)(& buf[__gen_e_acsl_i_2]),
- sizeof(int),
- (void *)(& buf[__gen_e_acsl_i_2]),
- (void *)0);
- if (__gen_e_acsl_valid) ;
- else {
- __gen_e_acsl_forall_6 = 0;
- goto e_acsl_end_loop8;
- }
- }
- {
- __e_acsl_mpz_t __gen_e_acsl__40;
- __e_acsl_mpz_t __gen_e_acsl_add_13;
- __gmpz_init_set_str(__gen_e_acsl__40,"1",10);
- __gmpz_init(__gen_e_acsl_add_13);
- __gmpz_add(__gen_e_acsl_add_13,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_i),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__40));
- __gmpz_set(__gen_e_acsl_i,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_add_13));
- __gmpz_clear(__gen_e_acsl__40);
- __gmpz_clear(__gen_e_acsl_add_13);
- }
- }
- e_acsl_end_loop8: ;
- __e_acsl_assert(__gen_e_acsl_forall_6,(char *)"Assertion",
- (char *)"main",
- (char *)"\\forall integer i; 0 <= i < 10 ==> \\valid(&buf[i])",
- 30);
- __gmpz_clear(__gen_e_acsl_i);
- }
- /*@ assert ∀ char i; 0 ≤ i < 10 ⇒ \valid(&buf[i]); */
- {
- int __gen_e_acsl_forall_7;
- __e_acsl_mpz_t __gen_e_acsl_i_3;
- __gen_e_acsl_forall_7 = 1;
- __gmpz_init(__gen_e_acsl_i_3);
- {
- __e_acsl_mpz_t __gen_e_acsl__41;
- __gmpz_init_set_si(__gen_e_acsl__41,0L);
- __gmpz_set(__gen_e_acsl_i_3,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__41));
- __gmpz_clear(__gen_e_acsl__41);
- }
- while (1) {
- {
- __e_acsl_mpz_t __gen_e_acsl__42;
- int __gen_e_acsl_lt_7;
- __gmpz_init_set_si(__gen_e_acsl__42,10L);
- __gen_e_acsl_lt_7 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_i_3),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__42));
- if (__gen_e_acsl_lt_7 < 0) ; else break;
- __gmpz_clear(__gen_e_acsl__42);
- }
- {
- long __gen_e_acsl_i_4;
- int __gen_e_acsl_valid_2;
- __gen_e_acsl_i_4 = __gmpz_get_si((__e_acsl_mpz_struct const *)(__gen_e_acsl_i_3));
- __gen_e_acsl_valid_2 = __e_acsl_valid((void *)(& buf[__gen_e_acsl_i_4]),
- sizeof(int),
- (void *)(& buf[__gen_e_acsl_i_4]),
- (void *)0);
- if (__gen_e_acsl_valid_2) ;
- else {
- __gen_e_acsl_forall_7 = 0;
- goto e_acsl_end_loop9;
- }
- }
- {
- __e_acsl_mpz_t __gen_e_acsl__43;
- __e_acsl_mpz_t __gen_e_acsl_add_14;
- __gmpz_init_set_str(__gen_e_acsl__43,"1",10);
- __gmpz_init(__gen_e_acsl_add_14);
- __gmpz_add(__gen_e_acsl_add_14,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_i_3),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__43));
- __gmpz_set(__gen_e_acsl_i_3,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_add_14));
- __gmpz_clear(__gen_e_acsl__43);
- __gmpz_clear(__gen_e_acsl_add_14);
- }
- }
- e_acsl_end_loop9: ;
- __e_acsl_assert(__gen_e_acsl_forall_7,(char *)"Assertion",
- (char *)"main",
- (char *)"\\forall char i; 0 <= i < 10 ==> \\valid(&buf[i])",
- 31);
- __gmpz_clear(__gen_e_acsl_i_3);
- }
- /*@ assert ∀ ℤ i; 0 ≤ i < len ⇒ \valid(&buf[i]); */
- {
- int __gen_e_acsl_forall_8;
- __e_acsl_mpz_t __gen_e_acsl_i_5;
- __gen_e_acsl_forall_8 = 1;
- __gmpz_init(__gen_e_acsl_i_5);
- {
- __e_acsl_mpz_t __gen_e_acsl__44;
- __gmpz_init_set_si(__gen_e_acsl__44,0L);
- __gmpz_set(__gen_e_acsl_i_5,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__44));
- __gmpz_clear(__gen_e_acsl__44);
- }
- while (1) {
- {
- __e_acsl_mpz_t __gen_e_acsl_len;
- int __gen_e_acsl_lt_8;
- __gmpz_init_set_ui(__gen_e_acsl_len,len);
- __gen_e_acsl_lt_8 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_i_5),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_len));
- if (__gen_e_acsl_lt_8 < 0) ; else break;
- __gmpz_clear(__gen_e_acsl_len);
- }
- {
- long __gen_e_acsl_i_6;
- int __gen_e_acsl_valid_3;
- __gen_e_acsl_i_6 = __gmpz_get_si((__e_acsl_mpz_struct const *)(__gen_e_acsl_i_5));
- __gen_e_acsl_valid_3 = __e_acsl_valid((void *)(& buf[__gen_e_acsl_i_6]),
- sizeof(int),
- (void *)(& buf[__gen_e_acsl_i_6]),
- (void *)0);
- if (__gen_e_acsl_valid_3) ;
- else {
- __gen_e_acsl_forall_8 = 0;
- goto e_acsl_end_loop10;
- }
- }
- {
- __e_acsl_mpz_t __gen_e_acsl__45;
- __e_acsl_mpz_t __gen_e_acsl_add_15;
- __gmpz_init_set_str(__gen_e_acsl__45,"1",10);
- __gmpz_init(__gen_e_acsl_add_15);
- __gmpz_add(__gen_e_acsl_add_15,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_i_5),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__45));
- __gmpz_set(__gen_e_acsl_i_5,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_add_15));
- __gmpz_clear(__gen_e_acsl__45);
- __gmpz_clear(__gen_e_acsl_add_15);
- }
- }
- e_acsl_end_loop10: ;
- __e_acsl_assert(__gen_e_acsl_forall_8,(char *)"Assertion",
- (char *)"main",
- (char *)"\\forall integer i; 0 <= i < len ==> \\valid(&buf[i])",
- 32);
- __gmpz_clear(__gen_e_acsl_i_5);
- }
- /*@ assert ∀ ℤ i; 0 ≤ i ≤ len ⇒ \valid(&buf[i]); */
- {
- int __gen_e_acsl_forall_9;
- __e_acsl_mpz_t __gen_e_acsl_i_7;
- __gen_e_acsl_forall_9 = 1;
- __gmpz_init(__gen_e_acsl_i_7);
- {
- __e_acsl_mpz_t __gen_e_acsl__46;
- __gmpz_init_set_si(__gen_e_acsl__46,0L);
- __gmpz_set(__gen_e_acsl_i_7,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__46));
- __gmpz_clear(__gen_e_acsl__46);
- }
- while (1) {
- {
- __e_acsl_mpz_t __gen_e_acsl_len_2;
- int __gen_e_acsl_le_6;
- __gmpz_init_set_ui(__gen_e_acsl_len_2,len);
- __gen_e_acsl_le_6 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_i_7),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_len_2));
- if (__gen_e_acsl_le_6 <= 0) ; else break;
- __gmpz_clear(__gen_e_acsl_len_2);
- }
- {
- long __gen_e_acsl_i_8;
- int __gen_e_acsl_valid_4;
- __gen_e_acsl_i_8 = __gmpz_get_si((__e_acsl_mpz_struct const *)(__gen_e_acsl_i_7));
- __gen_e_acsl_valid_4 = __e_acsl_valid((void *)(& buf[__gen_e_acsl_i_8]),
- sizeof(int),
- (void *)(& buf[__gen_e_acsl_i_8]),
- (void *)0);
- if (__gen_e_acsl_valid_4) ;
- else {
- __gen_e_acsl_forall_9 = 0;
- goto e_acsl_end_loop11;
- }
- }
- {
- __e_acsl_mpz_t __gen_e_acsl__47;
- __e_acsl_mpz_t __gen_e_acsl_add_16;
- __gmpz_init_set_str(__gen_e_acsl__47,"1",10);
- __gmpz_init(__gen_e_acsl_add_16);
- __gmpz_add(__gen_e_acsl_add_16,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_i_7),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__47));
- __gmpz_set(__gen_e_acsl_i_7,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_add_16));
- __gmpz_clear(__gen_e_acsl__47);
- __gmpz_clear(__gen_e_acsl_add_16);
- }
- }
- e_acsl_end_loop11: ;
- __e_acsl_assert(__gen_e_acsl_forall_9,(char *)"Assertion",
- (char *)"main",
- (char *)"\\forall integer i; 0 <= i <= len ==> \\valid(&buf[i])",
- 33);
- __gmpz_clear(__gen_e_acsl_i_7);
- __e_acsl_delete_block((void *)(buf));
- }
- }
- /*@ assert ∀ ℤ x; 0 < x < 1 ⇒ \false; */
- __e_acsl_assert(1,(char *)"Assertion",(char *)"main",
- (char *)"\\forall integer x; 0 < x < 1 ==> \\false",37);
- /*@ assert ¬(∃ char c; 10 ≤ c < 10 ∧ c ≡ 10); */
- __e_acsl_assert(! 0,(char *)"Assertion",(char *)"main",
- (char *)"!(\\exists char c; 10 <= c < 10 && c == 10)",38);
- /*@ assert \let u = 5;
- ∀ ℤ x, ℤ y; 0 ≤ x < 2 ∧ 4 < y < u ⇒ \false;
- */
- {
- int __gen_e_acsl_u;
- __gen_e_acsl_u = 5;
- __e_acsl_assert(1,(char *)"Assertion",(char *)"main",
- (char *)"\\let u = 5;\n\\forall integer x, integer y; 0 <= x < 2 && 4 < y < u ==> \\false",
- 40);
- }
- __retres = 0;
- __e_acsl_memory_clean();
- return __retres;
-}
-
-
diff --git a/src/plugins/e-acsl/tests/arith/oracle/gen_reals2.c b/src/plugins/e-acsl/tests/arith/oracle/gen_reals2.c
deleted file mode 100644
index 7e0d70df561fe3b6f221af2593afe71fb1004baf..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/arith/oracle/gen_reals2.c
+++ /dev/null
@@ -1,356 +0,0 @@
-/* Generated by Frama-C */
-#include "stdio.h"
-#include "stdlib.h"
-extern int __e_acsl_sound_verdict;
-
-/*@ ensures \let delta = 1;
- \let avg_real = (\old(a) + \old(b)) / 2;
- avg_real - delta < \result < avg_real + delta;
- */
-double __gen_e_acsl_avg(double a, double b);
-
-double avg(double a, double b)
-{
- double __retres;
- __retres = (a + b) / (double)2;
- return __retres;
-}
-
-int main(void)
-{
- int __retres;
- __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
- /*@ assert 3 ≢ 1.5; */
- __e_acsl_assert(3. != 1.5,(char *)"Assertion",(char *)"main",
- (char *)"3 != 1.5",14);
- /*@ assert 3 ≡ 1.5 + 1.5; */
- {
- __e_acsl_mpq_t __gen_e_acsl_;
- __e_acsl_mpq_t __gen_e_acsl__2;
- __e_acsl_mpq_t __gen_e_acsl__3;
- __e_acsl_mpq_t __gen_e_acsl_add;
- int __gen_e_acsl_eq;
- __gmpq_init(__gen_e_acsl_);
- __gmpq_set_str(__gen_e_acsl_,"3",10);
- __gmpq_init(__gen_e_acsl__2);
- __gmpq_set_d(__gen_e_acsl__2,1.5);
- __gmpq_init(__gen_e_acsl__3);
- __gmpq_set_d(__gen_e_acsl__3,1.5);
- __gmpq_init(__gen_e_acsl_add);
- __gmpq_add(__gen_e_acsl_add,
- (__e_acsl_mpq_struct const *)(__gen_e_acsl__2),
- (__e_acsl_mpq_struct const *)(__gen_e_acsl__3));
- __gen_e_acsl_eq = __gmpq_cmp((__e_acsl_mpq_struct const *)(__gen_e_acsl_),
- (__e_acsl_mpq_struct const *)(__gen_e_acsl_add));
- __e_acsl_assert(__gen_e_acsl_eq == 0,(char *)"Assertion",(char *)"main",
- (char *)"3 == 1.5 + 1.5",15);
- __gmpq_clear(__gen_e_acsl_);
- __gmpq_clear(__gen_e_acsl__2);
- __gmpq_clear(__gen_e_acsl__3);
- __gmpq_clear(__gen_e_acsl_add);
- }
- /*@ assert 0.1 ≡ 0.1; */
- {
- __e_acsl_mpq_t __gen_e_acsl__4;
- int __gen_e_acsl_eq_2;
- __gmpq_init(__gen_e_acsl__4);
- __gmpq_set_str(__gen_e_acsl__4,"01/10",10);
- __gen_e_acsl_eq_2 = __gmpq_cmp((__e_acsl_mpq_struct const *)(__gen_e_acsl__4),
- (__e_acsl_mpq_struct const *)(__gen_e_acsl__4));
- __e_acsl_assert(__gen_e_acsl_eq_2 == 0,(char *)"Assertion",
- (char *)"main",(char *)"0.1 == 0.1",16);
- __gmpq_clear(__gen_e_acsl__4);
- }
- /*@ assert (double)1.0 ≡ 1.0; */
- __e_acsl_assert(1. == 1.,(char *)"Assertion",(char *)"main",
- (char *)"(double)1.0 == 1.0",17);
- /*@ assert (double)0.1 ≢ 0.1; */
- {
- __e_acsl_mpq_t __gen_e_acsl__5;
- double __gen_e_acsl__6;
- __e_acsl_mpq_t __gen_e_acsl__7;
- int __gen_e_acsl_ne;
- __gmpq_init(__gen_e_acsl__5);
- __gmpq_set_str(__gen_e_acsl__5,"01/10",10);
- __gen_e_acsl__6 = __gmpq_get_d((__e_acsl_mpq_struct const *)(__gen_e_acsl__5));
- __gmpq_init(__gen_e_acsl__7);
- /*@ assert Eva: is_nan_or_infinite: \is_finite(__gen_e_acsl__6); */
- __gmpq_set_d(__gen_e_acsl__7,__gen_e_acsl__6);
- __gen_e_acsl_ne = __gmpq_cmp((__e_acsl_mpq_struct const *)(__gen_e_acsl__7),
- (__e_acsl_mpq_struct const *)(__gen_e_acsl__5));
- __e_acsl_assert(__gen_e_acsl_ne != 0,(char *)"Assertion",(char *)"main",
- (char *)"(double)0.1 != 0.1",18);
- __gmpq_clear(__gen_e_acsl__5);
- __gmpq_clear(__gen_e_acsl__7);
- }
- /*@ assert (float)0.1 ≢ (double)0.1; */
- {
- __e_acsl_mpq_t __gen_e_acsl__8;
- double __gen_e_acsl__9;
- double __gen_e_acsl__10;
- __gmpq_init(__gen_e_acsl__8);
- __gmpq_set_str(__gen_e_acsl__8,"01/10",10);
- __gen_e_acsl__9 = __gmpq_get_d((__e_acsl_mpq_struct const *)(__gen_e_acsl__8));
- __gen_e_acsl__10 = __gmpq_get_d((__e_acsl_mpq_struct const *)(__gen_e_acsl__8));
- /*@ assert Eva: is_nan_or_infinite: \is_finite(__gen_e_acsl__9); */
- /*@ assert Eva: is_nan_or_infinite: \is_finite(__gen_e_acsl__10); */
- /*@ assert Eva: is_nan_or_infinite: \is_finite((float)__gen_e_acsl__9);
- */
- __e_acsl_assert((double)((float)__gen_e_acsl__9) != __gen_e_acsl__10,
- (char *)"Assertion",(char *)"main",
- (char *)"(float)0.1 != (double)0.1",19);
- __gmpq_clear(__gen_e_acsl__8);
- }
- /*@ assert (double)1.1 ≢ 1 + 0.1; */
- {
- __e_acsl_mpq_t __gen_e_acsl__11;
- double __gen_e_acsl__12;
- __e_acsl_mpq_t __gen_e_acsl__13;
- __e_acsl_mpq_t __gen_e_acsl__14;
- __e_acsl_mpq_t __gen_e_acsl_add_2;
- __e_acsl_mpq_t __gen_e_acsl__15;
- int __gen_e_acsl_ne_2;
- __gmpq_init(__gen_e_acsl__11);
- __gmpq_set_str(__gen_e_acsl__11,"11/10",10);
- __gen_e_acsl__12 = __gmpq_get_d((__e_acsl_mpq_struct const *)(__gen_e_acsl__11));
- __gmpq_init(__gen_e_acsl__13);
- __gmpq_set_str(__gen_e_acsl__13,"1",10);
- __gmpq_init(__gen_e_acsl__14);
- __gmpq_set_str(__gen_e_acsl__14,"01/10",10);
- __gmpq_init(__gen_e_acsl_add_2);
- __gmpq_add(__gen_e_acsl_add_2,
- (__e_acsl_mpq_struct const *)(__gen_e_acsl__13),
- (__e_acsl_mpq_struct const *)(__gen_e_acsl__14));
- __gmpq_init(__gen_e_acsl__15);
- /*@ assert Eva: is_nan_or_infinite: \is_finite(__gen_e_acsl__12); */
- __gmpq_set_d(__gen_e_acsl__15,__gen_e_acsl__12);
- __gen_e_acsl_ne_2 = __gmpq_cmp((__e_acsl_mpq_struct const *)(__gen_e_acsl__15),
- (__e_acsl_mpq_struct const *)(__gen_e_acsl_add_2));
- __e_acsl_assert(__gen_e_acsl_ne_2 != 0,(char *)"Assertion",
- (char *)"main",(char *)"(double)1.1 != 1 + 0.1",20);
- __gmpq_clear(__gen_e_acsl__11);
- __gmpq_clear(__gen_e_acsl__13);
- __gmpq_clear(__gen_e_acsl__14);
- __gmpq_clear(__gen_e_acsl_add_2);
- __gmpq_clear(__gen_e_acsl__15);
- }
- /*@ assert 1 + 0.1 ≡ 2 - 0.9; */
- {
- __e_acsl_mpq_t __gen_e_acsl__16;
- __e_acsl_mpq_t __gen_e_acsl__17;
- __e_acsl_mpq_t __gen_e_acsl_add_3;
- __e_acsl_mpq_t __gen_e_acsl__18;
- __e_acsl_mpq_t __gen_e_acsl__19;
- __e_acsl_mpq_t __gen_e_acsl_sub;
- int __gen_e_acsl_eq_3;
- __gmpq_init(__gen_e_acsl__16);
- __gmpq_set_str(__gen_e_acsl__16,"1",10);
- __gmpq_init(__gen_e_acsl__17);
- __gmpq_set_str(__gen_e_acsl__17,"01/10",10);
- __gmpq_init(__gen_e_acsl_add_3);
- __gmpq_add(__gen_e_acsl_add_3,
- (__e_acsl_mpq_struct const *)(__gen_e_acsl__16),
- (__e_acsl_mpq_struct const *)(__gen_e_acsl__17));
- __gmpq_init(__gen_e_acsl__18);
- __gmpq_set_str(__gen_e_acsl__18,"2",10);
- __gmpq_init(__gen_e_acsl__19);
- __gmpq_set_str(__gen_e_acsl__19,"09/10",10);
- __gmpq_init(__gen_e_acsl_sub);
- __gmpq_sub(__gen_e_acsl_sub,
- (__e_acsl_mpq_struct const *)(__gen_e_acsl__18),
- (__e_acsl_mpq_struct const *)(__gen_e_acsl__19));
- __gen_e_acsl_eq_3 = __gmpq_cmp((__e_acsl_mpq_struct const *)(__gen_e_acsl_add_3),
- (__e_acsl_mpq_struct const *)(__gen_e_acsl_sub));
- __e_acsl_assert(__gen_e_acsl_eq_3 == 0,(char *)"Assertion",
- (char *)"main",(char *)"1 + 0.1 == 2 - 0.9",21);
- __gmpq_clear(__gen_e_acsl__16);
- __gmpq_clear(__gen_e_acsl__17);
- __gmpq_clear(__gen_e_acsl_add_3);
- __gmpq_clear(__gen_e_acsl__18);
- __gmpq_clear(__gen_e_acsl__19);
- __gmpq_clear(__gen_e_acsl_sub);
- }
- float x = 0.2f;
- float y = 0.3f;
- float sum = x + y;
- /*@ assert sum ≢ x * y; */
- {
- __e_acsl_mpq_t __gen_e_acsl_y;
- __e_acsl_mpq_t __gen_e_acsl__20;
- __e_acsl_mpq_t __gen_e_acsl_mul;
- __e_acsl_mpq_t __gen_e_acsl__21;
- int __gen_e_acsl_ne_3;
- __gmpq_init(__gen_e_acsl_y);
- __gmpq_set_d(__gen_e_acsl_y,(double)y);
- __gmpq_init(__gen_e_acsl__20);
- __gmpq_set_d(__gen_e_acsl__20,(double)x);
- __gmpq_init(__gen_e_acsl_mul);
- __gmpq_mul(__gen_e_acsl_mul,
- (__e_acsl_mpq_struct const *)(__gen_e_acsl__20),
- (__e_acsl_mpq_struct const *)(__gen_e_acsl_y));
- __gmpq_init(__gen_e_acsl__21);
- __gmpq_set_d(__gen_e_acsl__21,(double)sum);
- __gen_e_acsl_ne_3 = __gmpq_cmp((__e_acsl_mpq_struct const *)(__gen_e_acsl__21),
- (__e_acsl_mpq_struct const *)(__gen_e_acsl_mul));
- __e_acsl_assert(__gen_e_acsl_ne_3 != 0,(char *)"Assertion",
- (char *)"main",(char *)"sum != x * y",25);
- __gmpq_clear(__gen_e_acsl_y);
- __gmpq_clear(__gen_e_acsl__20);
- __gmpq_clear(__gen_e_acsl_mul);
- __gmpq_clear(__gen_e_acsl__21);
- }
- /*@ assert \let n = 1; 4 ≡ n + 3.0; */
- {
- int __gen_e_acsl_n;
- __e_acsl_mpq_t __gen_e_acsl__22;
- __e_acsl_mpq_t __gen_e_acsl__23;
- __e_acsl_mpq_t __gen_e_acsl__24;
- __e_acsl_mpq_t __gen_e_acsl_add_4;
- int __gen_e_acsl_eq_4;
- __gen_e_acsl_n = 1;
- __gmpq_init(__gen_e_acsl__22);
- __gmpq_set_str(__gen_e_acsl__22,"4",10);
- __gmpq_init(__gen_e_acsl__23);
- __gmpq_set_d(__gen_e_acsl__23,3.);
- __gmpq_init(__gen_e_acsl__24);
- __gmpq_set_si(__gen_e_acsl__24,(long)__gen_e_acsl_n);
- __gmpq_init(__gen_e_acsl_add_4);
- __gmpq_add(__gen_e_acsl_add_4,
- (__e_acsl_mpq_struct const *)(__gen_e_acsl__24),
- (__e_acsl_mpq_struct const *)(__gen_e_acsl__23));
- __gen_e_acsl_eq_4 = __gmpq_cmp((__e_acsl_mpq_struct const *)(__gen_e_acsl__22),
- (__e_acsl_mpq_struct const *)(__gen_e_acsl_add_4));
- __e_acsl_assert(__gen_e_acsl_eq_4 == 0,(char *)"Assertion",
- (char *)"main",(char *)"\\let n = 1; 4 == n + 3.0",26);
- __gmpq_clear(__gen_e_acsl__22);
- __gmpq_clear(__gen_e_acsl__23);
- __gmpq_clear(__gen_e_acsl__24);
- __gmpq_clear(__gen_e_acsl_add_4);
- }
- double d = 0.1;
- __gen_e_acsl_avg(4.3,11.7);
- /*@ assert 1.1d ≢ 1 + 0.1; */
- {
- __e_acsl_mpq_t __gen_e_acsl__25;
- __e_acsl_mpq_t __gen_e_acsl__26;
- __e_acsl_mpq_t __gen_e_acsl_add_5;
- __e_acsl_mpq_t __gen_e_acsl__27;
- int __gen_e_acsl_ne_4;
- __gmpq_init(__gen_e_acsl__25);
- __gmpq_set_str(__gen_e_acsl__25,"1",10);
- __gmpq_init(__gen_e_acsl__26);
- __gmpq_set_str(__gen_e_acsl__26,"01/10",10);
- __gmpq_init(__gen_e_acsl_add_5);
- __gmpq_add(__gen_e_acsl_add_5,
- (__e_acsl_mpq_struct const *)(__gen_e_acsl__25),
- (__e_acsl_mpq_struct const *)(__gen_e_acsl__26));
- __gmpq_init(__gen_e_acsl__27);
- __gmpq_set_d(__gen_e_acsl__27,1.1);
- __gen_e_acsl_ne_4 = __gmpq_cmp((__e_acsl_mpq_struct const *)(__gen_e_acsl__27),
- (__e_acsl_mpq_struct const *)(__gen_e_acsl_add_5));
- __e_acsl_assert(__gen_e_acsl_ne_4 != 0,(char *)"Assertion",
- (char *)"main",(char *)"1.1d != 1 + 0.1",32);
- __gmpq_clear(__gen_e_acsl__25);
- __gmpq_clear(__gen_e_acsl__26);
- __gmpq_clear(__gen_e_acsl_add_5);
- __gmpq_clear(__gen_e_acsl__27);
- }
- __retres = 0;
- return __retres;
-}
-
-/*@ ensures \let delta = 1;
- \let avg_real = (\old(a) + \old(b)) / 2;
- avg_real - delta < \result < avg_real + delta;
- */
-double __gen_e_acsl_avg(double a, double b)
-{
- double __gen_e_acsl_at_2;
- __e_acsl_mpq_t __gen_e_acsl_at;
- double __retres;
- __gen_e_acsl_at_2 = b;
- {
- __e_acsl_mpq_t __gen_e_acsl_a;
- __gmpq_init(__gen_e_acsl_a);
- __gmpq_set_d(__gen_e_acsl_a,a);
- __gmpq_init(__gen_e_acsl_at);
- __gmpq_set(__gen_e_acsl_at,(__e_acsl_mpq_struct const *)(__gen_e_acsl_a));
- __gmpq_clear(__gen_e_acsl_a);
- }
- __retres = avg(a,b);
- {
- int __gen_e_acsl_delta;
- __e_acsl_mpq_t __gen_e_acsl_avg_real;
- __e_acsl_mpq_t __gen_e_acsl_;
- __e_acsl_mpq_t __gen_e_acsl_add;
- __e_acsl_mpq_t __gen_e_acsl__2;
- __e_acsl_mpq_t __gen_e_acsl_div;
- __e_acsl_mpq_t __gen_e_acsl_delta_2;
- __e_acsl_mpq_t __gen_e_acsl_sub;
- __e_acsl_mpq_t __gen_e_acsl__3;
- int __gen_e_acsl_lt;
- int __gen_e_acsl_and;
- __gen_e_acsl_delta = 1;
- __gmpq_init(__gen_e_acsl_);
- __gmpq_set_d(__gen_e_acsl_,__gen_e_acsl_at_2);
- __gmpq_init(__gen_e_acsl_add);
- __gmpq_add(__gen_e_acsl_add,
- (__e_acsl_mpq_struct const *)(__gen_e_acsl_at),
- (__e_acsl_mpq_struct const *)(__gen_e_acsl_));
- __gmpq_init(__gen_e_acsl__2);
- __gmpq_set_str(__gen_e_acsl__2,"2",10);
- __gmpq_init(__gen_e_acsl_div);
- __gmpq_div(__gen_e_acsl_div,
- (__e_acsl_mpq_struct const *)(__gen_e_acsl_add),
- (__e_acsl_mpq_struct const *)(__gen_e_acsl__2));
- __gmpq_init(__gen_e_acsl_avg_real);
- __gmpq_set(__gen_e_acsl_avg_real,
- (__e_acsl_mpq_struct const *)(__gen_e_acsl_div));
- __gmpq_init(__gen_e_acsl_delta_2);
- __gmpq_set_si(__gen_e_acsl_delta_2,(long)__gen_e_acsl_delta);
- __gmpq_init(__gen_e_acsl_sub);
- __gmpq_sub(__gen_e_acsl_sub,
- (__e_acsl_mpq_struct const *)(__gen_e_acsl_avg_real),
- (__e_acsl_mpq_struct const *)(__gen_e_acsl_delta_2));
- __gmpq_init(__gen_e_acsl__3);
- __gmpq_set_d(__gen_e_acsl__3,__retres);
- __gen_e_acsl_lt = __gmpq_cmp((__e_acsl_mpq_struct const *)(__gen_e_acsl_sub),
- (__e_acsl_mpq_struct const *)(__gen_e_acsl__3));
- if (__gen_e_acsl_lt < 0) {
- __e_acsl_mpq_t __gen_e_acsl_delta_3;
- __e_acsl_mpq_t __gen_e_acsl_add_2;
- __e_acsl_mpq_t __gen_e_acsl__4;
- int __gen_e_acsl_lt_2;
- __gmpq_init(__gen_e_acsl_delta_3);
- __gmpq_set_si(__gen_e_acsl_delta_3,(long)__gen_e_acsl_delta);
- __gmpq_init(__gen_e_acsl_add_2);
- __gmpq_add(__gen_e_acsl_add_2,
- (__e_acsl_mpq_struct const *)(__gen_e_acsl_avg_real),
- (__e_acsl_mpq_struct const *)(__gen_e_acsl_delta_3));
- __gmpq_init(__gen_e_acsl__4);
- __gmpq_set_d(__gen_e_acsl__4,__retres);
- __gen_e_acsl_lt_2 = __gmpq_cmp((__e_acsl_mpq_struct const *)(__gen_e_acsl__4),
- (__e_acsl_mpq_struct const *)(__gen_e_acsl_add_2));
- __gen_e_acsl_and = __gen_e_acsl_lt_2 < 0;
- __gmpq_clear(__gen_e_acsl_delta_3);
- __gmpq_clear(__gen_e_acsl_add_2);
- __gmpq_clear(__gen_e_acsl__4);
- }
- else __gen_e_acsl_and = 0;
- __e_acsl_assert(__gen_e_acsl_and,(char *)"Postcondition",(char *)"avg",
- (char *)"\\let delta = 1;\n\\let avg_real = (\\old(a) + \\old(b)) / 2;\n avg_real - delta < \\result < avg_real + delta",
- 6);
- __gmpq_clear(__gen_e_acsl_avg_real);
- __gmpq_clear(__gen_e_acsl_);
- __gmpq_clear(__gen_e_acsl_add);
- __gmpq_clear(__gen_e_acsl__2);
- __gmpq_clear(__gen_e_acsl_div);
- __gmpq_clear(__gen_e_acsl_delta_2);
- __gmpq_clear(__gen_e_acsl_sub);
- __gmpq_clear(__gen_e_acsl__3);
- __gmpq_clear(__gen_e_acsl_at);
- return __retres;
- }
-}
-
-
diff --git a/src/plugins/e-acsl/tests/arith/oracle/integer_constant.0.res.oracle b/src/plugins/e-acsl/tests/arith/oracle/integer_constant.0.res.oracle
deleted file mode 100644
index d26faebb6d6db5774c38989a0857d3f9114bf3fc..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/arith/oracle/integer_constant.0.res.oracle
+++ /dev/null
@@ -1,19 +0,0 @@
-[e-acsl] beginning translation.
-[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]
-[eva] using specification for function __e_acsl_memory_init
-[eva] using specification for function __e_acsl_assert
-[eva] using specification for function __gmpz_init_set_str
-[eva] using specification for function __gmpz_cmp
-[eva:alarm] tests/gmp/integer_constant.i:11: Warning:
- function __e_acsl_assert: precondition got status unknown.
-[eva] using specification for function __gmpz_clear
-[eva] done for function main
diff --git a/src/plugins/e-acsl/tests/arith/oracle/integer_constant.1.res.oracle b/src/plugins/e-acsl/tests/arith/oracle/integer_constant.1.res.oracle
deleted file mode 100644
index 97496ed852dcf2e603df0069b031a53c97d465df..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/arith/oracle/integer_constant.1.res.oracle
+++ /dev/null
@@ -1,27 +0,0 @@
-[e-acsl] beginning translation.
-[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]
-[eva] using specification for function __e_acsl_memory_init
-[eva] using specification for function __gmpz_init_set_si
-[eva] using specification for function __gmpz_cmp
-[eva] using specification for function __e_acsl_assert
-[eva:alarm] tests/gmp/integer_constant.i:6: Warning:
- function __e_acsl_assert: precondition got status unknown.
-[eva] using specification for function __gmpz_clear
-[eva:alarm] tests/gmp/integer_constant.i:8: Warning:
- function __e_acsl_assert: precondition got status unknown.
-[eva] using specification for function __gmpz_init_set_ui
-[eva:alarm] tests/gmp/integer_constant.i:9: Warning:
- function __e_acsl_assert: precondition got status unknown.
-[eva] using specification for function __gmpz_init_set_str
-[eva:alarm] tests/gmp/integer_constant.i:11: Warning:
- function __e_acsl_assert: precondition got status unknown.
-[eva] done for function main
diff --git a/src/plugins/e-acsl/tests/arith/oracle/let.0.res.oracle b/src/plugins/e-acsl/tests/arith/oracle/let.0.res.oracle
deleted file mode 100644
index eb489ce6c2576da5bebb4949ba0e066c54997a77..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/arith/oracle/let.0.res.oracle
+++ /dev/null
@@ -1,48 +0,0 @@
-[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] 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]
-[eva] using specification for function __e_acsl_memory_init
-[eva:alarm] tests/gmp/let.c:7: Warning: assertion got status unknown.
-[eva] using specification for function __e_acsl_assert
-[eva:alarm] tests/gmp/let.c:9: Warning: assertion got status unknown.
-[eva] tests/gmp/let.c:12:
- cannot evaluate ACSL term, unsupported ACSL construct: \let bindings
-[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] tests/gmp/let.c:21:
- cannot evaluate ACSL term, unsupported ACSL construct: \let bindings
-[eva:alarm] tests/gmp/let.c:21: Warning: assertion got status unknown.
-[eva] using specification for function __gmpz_init_set_si
-[eva] using specification for function __gmpz_init
-[eva] using specification for function __gmpz_mul
-[eva] using specification for function __gmpz_cmp
-[eva:alarm] tests/gmp/let.c:21: Warning:
- function __e_acsl_assert: precondition got status unknown.
-[eva] using specification for function __gmpz_clear
-[eva:alarm] tests/gmp/let.c:24: Warning: assertion got status unknown.
-[eva] using specification for function __e_acsl_store_block
-[eva] using specification for function __e_acsl_full_init
-[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] tests/gmp/let.c:32:
- cannot evaluate ACSL term, unsupported ACSL construct: \let bindings
-[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] tests/gmp/let.c:39:
- cannot evaluate ACSL term, unsupported ACSL construct: \let bindings
-[eva:alarm] tests/gmp/let.c:39: Warning: assertion got status unknown.
-[eva] using specification for function __e_acsl_delete_block
-[eva] using specification for function __e_acsl_memory_clean
-[eva] done for function main
diff --git a/src/plugins/e-acsl/tests/arith/oracle/let.1.res.oracle b/src/plugins/e-acsl/tests/arith/oracle/let.1.res.oracle
deleted file mode 100644
index 4ef2a9f67a28af8af5599e60d8657f9d7bc338a3..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/arith/oracle/let.1.res.oracle
+++ /dev/null
@@ -1,70 +0,0 @@
-[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] 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]
-[eva] using specification for function __e_acsl_memory_init
-[eva:alarm] tests/gmp/let.c:7: Warning: assertion got status unknown.
-[eva] using specification for function __gmpz_init_set_si
-[eva] using specification for function __gmpz_init
-[eva] using specification for function __gmpz_mul
-[eva] using specification for function __gmpz_init_set
-[eva] using specification for function __gmpz_cmp
-[eva] using specification for function __e_acsl_assert
-[eva:alarm] tests/gmp/let.c:7: Warning:
- function __e_acsl_assert: precondition got status unknown.
-[eva] using specification for function __gmpz_clear
-[eva:alarm] tests/gmp/let.c:9: Warning: assertion got status unknown.
-[eva] using specification for function __gmpz_add
-[eva:alarm] tests/gmp/let.c:9: Warning:
- function __e_acsl_assert: precondition got status unknown.
-[eva] tests/gmp/let.c:12:
- cannot evaluate ACSL term, unsupported ACSL construct: \let bindings
-[eva:alarm] tests/gmp/let.c:12: Warning: assertion got status unknown.
-[eva:alarm] tests/gmp/let.c:12: Warning:
- function __e_acsl_assert: precondition got status unknown.
-[eva:alarm] tests/gmp/let.c:14: Warning: assertion got status unknown.
-[eva:alarm] tests/gmp/let.c:14: Warning:
- function __e_acsl_assert: precondition got status unknown.
-[eva:alarm] tests/gmp/let.c:17: Warning: assertion got status unknown.
-[eva:alarm] tests/gmp/let.c:17: Warning:
- function __e_acsl_assert: precondition got status unknown.
-[eva] tests/gmp/let.c:21:
- cannot evaluate ACSL term, unsupported ACSL construct: \let bindings
-[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:24: Warning:
- function __e_acsl_assert: precondition got status unknown.
-[eva] using specification for function __e_acsl_store_block
-[eva] using specification for function __e_acsl_full_init
-[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:30: Warning:
- function __e_acsl_assert: precondition got status unknown.
-[eva] tests/gmp/let.c:32:
- cannot evaluate ACSL term, unsupported ACSL construct: \let bindings
-[eva:alarm] tests/gmp/let.c:32: Warning: assertion got status unknown.
-[eva:alarm] tests/gmp/let.c:32: Warning:
- function __e_acsl_assert: precondition got status unknown.
-[eva:alarm] tests/gmp/let.c:35: Warning: assertion got status unknown.
-[eva:alarm] tests/gmp/let.c:35: Warning:
- function __e_acsl_assert: precondition got status unknown.
-[eva] tests/gmp/let.c:39:
- cannot evaluate ACSL term, unsupported ACSL construct: \let bindings
-[eva:alarm] tests/gmp/let.c:39: Warning: assertion got status unknown.
-[eva:alarm] tests/gmp/let.c:39: Warning:
- function __e_acsl_assert: precondition got status unknown.
-[eva] using specification for function __e_acsl_delete_block
-[eva] using specification for function __e_acsl_memory_clean
-[eva] done for function main
diff --git a/src/plugins/e-acsl/tests/arith/oracle/longlong.0.res.oracle b/src/plugins/e-acsl/tests/arith/oracle/longlong.0.res.oracle
deleted file mode 100644
index 5b07e0a1fffa404bdfca5158b6fe3344d7a65cf8..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/arith/oracle/longlong.0.res.oracle
+++ /dev/null
@@ -1,39 +0,0 @@
-[e-acsl] beginning translation.
-[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]
-[eva] using specification for function __e_acsl_memory_init
-[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] using specification for function my_pow
-[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] using specification for function __gmpz_init_set_si
-[eva] using specification for function __gmpz_init
-[eva] using specification for function __gmpz_import
-[eva:alarm] tests/gmp/longlong.i:17: Warning:
- function __gmpz_import: precondition got status unknown.
-[eva] using specification for function __gmpz_mul
-[eva] using specification for function __gmpz_add
-[eva] using specification for function __gmpz_cmp
-[eva] using specification for function __e_acsl_assert
-[eva:alarm] tests/gmp/longlong.i:17: Warning:
- function __e_acsl_assert: precondition got status unknown.
-[eva] using specification for function __gmpz_tdiv_r
-[eva] using specification for function __gmpz_get_si
-[eva] tests/gmp/longlong.i:17:
- Assigning imprecise value to __gen_e_acsl__4.
- The imprecision originates from Library function
-[eva] using specification for function __gmpz_clear
-[eva] done for function main
diff --git a/src/plugins/e-acsl/tests/arith/oracle/longlong.1.res.oracle b/src/plugins/e-acsl/tests/arith/oracle/longlong.1.res.oracle
deleted file mode 100644
index fada6aef03dec76e67853cb0de19edc20b19ea42..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/arith/oracle/longlong.1.res.oracle
+++ /dev/null
@@ -1,38 +0,0 @@
-[e-acsl] beginning translation.
-[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]
-[eva] using specification for function __e_acsl_memory_init
-[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] using specification for function my_pow
-[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] using specification for function __gmpz_init_set_si
-[eva] using specification for function __gmpz_init
-[eva] using specification for function __gmpz_import
-[eva:alarm] tests/gmp/longlong.i:17: Warning:
- function __gmpz_import: precondition got status unknown.
-[eva] using specification for function __gmpz_mul
-[eva] using specification for function __gmpz_add
-[eva] using specification for function __gmpz_cmp
-[eva] using specification for function __e_acsl_assert
-[eva:alarm] tests/gmp/longlong.i:17: Warning:
- function __e_acsl_assert: precondition got status unknown.
-[eva] using specification for function __gmpz_tdiv_r
-[eva] tests/gmp/longlong.i:17:
- Assigning imprecise value to __gen_e_acsl_eq.
- The imprecision originates from Library function
-[eva] using specification for function __gmpz_clear
-[eva] done for function main
diff --git a/src/plugins/e-acsl/tests/arith/oracle/not.0.res.oracle b/src/plugins/e-acsl/tests/arith/oracle/not.0.res.oracle
deleted file mode 100644
index 7046e21167e2fa05413d343de5b74544da9e443c..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/arith/oracle/not.0.res.oracle
+++ /dev/null
@@ -1,14 +0,0 @@
-[e-acsl] beginning translation.
-[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]
-[eva] using specification for function __e_acsl_memory_init
-[eva] using specification for function __e_acsl_assert
-[eva] done for function main
diff --git a/src/plugins/e-acsl/tests/arith/oracle/not.1.res.oracle b/src/plugins/e-acsl/tests/arith/oracle/not.1.res.oracle
deleted file mode 100644
index a19969e8d99da935ae8b4a81507b74dc56768965..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/arith/oracle/not.1.res.oracle
+++ /dev/null
@@ -1,19 +0,0 @@
-[e-acsl] beginning translation.
-[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]
-[eva] using specification for function __e_acsl_memory_init
-[eva] using specification for function __gmpz_init_set_si
-[eva] using specification for function __gmpz_cmp
-[eva] using specification for function __e_acsl_assert
-[eva:alarm] tests/gmp/not.i:6: Warning:
- function __e_acsl_assert: precondition got status unknown.
-[eva] using specification for function __gmpz_clear
-[eva] done for function main
diff --git a/src/plugins/e-acsl/tests/arith/oracle/quantif.0.res.oracle b/src/plugins/e-acsl/tests/arith/oracle/quantif.0.res.oracle
deleted file mode 100644
index cb1d4c89b8132622aac175ec0694dae23e9bee18..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/arith/oracle/quantif.0.res.oracle
+++ /dev/null
@@ -1,59 +0,0 @@
-[e-acsl] beginning translation.
-[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]
-[eva] using specification for function __e_acsl_memory_init
-[eva:alarm] tests/gmp/quantif.i:9: Warning: assertion got status unknown.
-[eva] tests/gmp/quantif.i:9: starting to merge loop iterations
-[eva] using specification for function __e_acsl_assert
-[eva:alarm] tests/gmp/quantif.i:10: Warning: assertion got status unknown.
-[eva] tests/gmp/quantif.i:10: starting to merge loop iterations
-[eva:alarm] tests/gmp/quantif.i:11: Warning: assertion got status unknown.
-[eva] tests/gmp/quantif.i:11: starting to merge loop iterations
-[eva:alarm] tests/gmp/quantif.i:15: Warning: assertion got status unknown.
-[eva] tests/gmp/quantif.i:15: starting to merge loop iterations
-[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] tests/gmp/quantif.i:20: starting to merge loop iterations
-[eva:alarm] tests/gmp/quantif.i:24: Warning: assertion got status unknown.
-[eva] tests/gmp/quantif.i:24: starting to merge loop iterations
-[eva] tests/gmp/quantif.i:25: starting to merge loop iterations
-[eva:alarm] tests/gmp/quantif.i:24: Warning:
- function __e_acsl_assert: precondition got status unknown.
-[eva] using specification for function __e_acsl_store_block
-[eva:alarm] tests/gmp/quantif.i:30: Warning: assertion got status unknown.
-[eva] using specification for function __e_acsl_valid
-[eva] tests/gmp/quantif.i:30: starting to merge loop iterations
-[eva:alarm] tests/gmp/quantif.i:30: Warning:
- function __e_acsl_assert: precondition got status unknown.
-[eva] tests/gmp/quantif.i:31: starting to merge loop iterations
-[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] tests/gmp/quantif.i:32: starting to merge loop iterations
-[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] using specification for function __gmpz_init
-[eva] using specification for function __gmpz_init_set_si
-[eva] using specification for function __gmpz_set
-[eva] using specification for function __gmpz_clear
-[eva] using specification for function __gmpz_init_set_ui
-[eva] using specification for function __gmpz_cmp
-[eva] using specification for function __gmpz_get_si
-[eva] using specification for function __gmpz_add
-[eva:alarm] tests/gmp/quantif.i:33: Warning:
- function __e_acsl_assert: precondition got status unknown.
-[eva] using specification for function __e_acsl_delete_block
-[eva:alarm] tests/gmp/quantif.i:37: Warning: assertion got status unknown.
-[eva:alarm] tests/gmp/quantif.i:40: Warning: assertion got status unknown.
-[eva] using specification for function __e_acsl_memory_clean
-[eva] done for function main
diff --git a/src/plugins/e-acsl/tests/arith/oracle/quantif.1.res.oracle b/src/plugins/e-acsl/tests/arith/oracle/quantif.1.res.oracle
deleted file mode 100644
index 7a6b1edc0f88581437072a2dbe2e53ca7130feb3..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/arith/oracle/quantif.1.res.oracle
+++ /dev/null
@@ -1,65 +0,0 @@
-[e-acsl] beginning translation.
-[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]
-[eva] using specification for function __e_acsl_memory_init
-[eva:alarm] tests/gmp/quantif.i:9: Warning: assertion got status unknown.
-[eva] using specification for function __gmpz_init
-[eva] using specification for function __gmpz_init_set_si
-[eva] using specification for function __gmpz_set
-[eva] using specification for function __gmpz_clear
-[eva] using specification for function __gmpz_cmp
-[eva] using specification for function __gmpz_init_set_str
-[eva] using specification for function __gmpz_add
-[eva] using specification for function __e_acsl_assert
-[eva:alarm] tests/gmp/quantif.i:9: Warning:
- function __e_acsl_assert: precondition got status unknown.
-[eva:alarm] tests/gmp/quantif.i:10: Warning: assertion got status unknown.
-[eva:alarm] tests/gmp/quantif.i:10: Warning:
- function __e_acsl_assert: precondition got status unknown.
-[eva:alarm] tests/gmp/quantif.i:11: Warning: assertion got status unknown.
-[eva:alarm] tests/gmp/quantif.i:11: Warning:
- function __e_acsl_assert: precondition 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:20: Warning:
- function __e_acsl_assert: precondition got status unknown.
-[eva:alarm] tests/gmp/quantif.i:24: Warning: assertion got status unknown.
-[eva:alarm] tests/gmp/quantif.i:25: Warning:
- function __e_acsl_assert: precondition got status unknown.
-[eva] using specification for function __gmpz_tdiv_r
-[eva:alarm] tests/gmp/quantif.i:25: Warning:
- function __e_acsl_assert: precondition got status unknown.
-[eva] using specification for function __gmpz_tdiv_q
-[eva] using specification for function __gmpz_mul
-[eva:alarm] tests/gmp/quantif.i:24: Warning:
- function __e_acsl_assert: precondition got status unknown.
-[eva] using specification for function __e_acsl_store_block
-[eva:alarm] tests/gmp/quantif.i:30: Warning: assertion got status unknown.
-[eva] using specification for function __gmpz_get_si
-[eva] using specification for function __e_acsl_valid
-[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] using specification for function __gmpz_init_set_ui
-[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] using specification for function __e_acsl_delete_block
-[eva:alarm] tests/gmp/quantif.i:37: Warning: assertion got status unknown.
-[eva:alarm] tests/gmp/quantif.i:40: Warning: assertion got status unknown.
-[eva] using specification for function __e_acsl_memory_clean
-[eva] done for function main
diff --git a/src/plugins/e-acsl/tests/gmp-only/arith.i b/src/plugins/e-acsl/tests/gmp-only/arith.i
new file mode 100644
index 0000000000000000000000000000000000000000..df97877fb148968c52cd69013790c311dcf6160b
--- /dev/null
+++ b/src/plugins/e-acsl/tests/gmp-only/arith.i
@@ -0,0 +1,39 @@
+/* run.config
+ COMMENT: arithmetic operations
+*/
+
+int main(void) {
+ int x = -3;
+ int y = 2;
+ long z = 2L;
+
+ /*@ assert -3 == x; */ ;
+ /*@ assert x == -3; */ ;
+ /*@ assert 0 != ~0; */ ;
+
+ /*@ assert x+1 == -2; */ ;
+ /*@ assert x-1 == -4; */ ;
+ /*@ assert x*3 == -9; */ ;
+ /*@ assert x/3 == -1; */ ;
+ /*@ assert 0xffffffffffffffffffffff/0xffffffffffffffffffffff == 1; */ ;
+ /*@ assert x % 2 == -1; */ ;
+ /*@ assert -3 % -2 == -1; */ ;
+ /*@ assert 3 % -2 == 1; */ ;
+
+ /*@ assert x * 2 + (3 + y) - 4 + (x - y) == -10; */ ;
+
+ /*@ assert (0 == 1) == !(0 == 0); */ ;
+ /*@ assert (0 <= -1) == (0 > 0); */ ;
+ /*@ assert (0 >= -1) == (0 <= 0); */ ;
+ /*@ assert (0 != 1) == !(0 != 0); */ ;
+
+ /*@ assert 0 == !1; */ ;
+ /*@ assert 4 / y == 2; */ // non trivial division added when fixing bts #751
+
+ // example from the JFLA'15 paper (but for a 64-bit architecture)
+ /*@ assert 1 + ((z+1) / (y-123456789123456789)) == 1; */
+
+ /*@ assert 1 - x == -x + 1; */ // test GIT issue #37
+
+ return 0;
+}
diff --git a/src/plugins/e-acsl/tests/gmp-only/functions.c b/src/plugins/e-acsl/tests/gmp-only/functions.c
new file mode 100644
index 0000000000000000000000000000000000000000..9d0bc001ab61c0b89201f3c3ecffae481965c120
--- /dev/null
+++ b/src/plugins/e-acsl/tests/gmp-only/functions.c
@@ -0,0 +1,73 @@
+/* run.config
+ COMMENT: logic functions without labels
+*/
+
+/*@ predicate p1(int x, int y) = x + y > 0; */
+/*@ predicate p2(integer x, integer y) = x + y > 0; */
+
+/*@ logic integer f1(integer x, integer y) = x + y; */
+
+// E-ACSL integer typing:
+// types less than int are considered as int
+/*@ logic char h_char(char c) = c; */
+/*@ logic short h_short(short s) = s; */
+
+/*@ logic int g_hidden(int x) = x; */
+/*@ logic int g(int x) = g_hidden(x); */
+
+struct mystruct { int k, l; };
+typedef struct mystruct mystruct;
+/*@ logic mystruct t1(mystruct m) = m; */
+/*@ logic integer t2(mystruct m) = m.k + m.l; */
+
+// To test function call in other clauses than assert:
+/*@ predicate k_pred(integer x) = x > 0; */
+/*@ requires k_pred(x); */
+void k(int x) {}
+
+// To test non-interference with global inits:
+int glob = 5;
+
+// To test that functions that are never called are not generated:
+/*@ predicate never_called(int x) = x == x; */
+
+/*@ logic double f2(double x) = (double)(1/x); */ /* handle in MR !226 */
+
+// To test not_yet:
+/*@ predicate p_notyet{L}(integer x) = x > 0; */
+/*@ logic integer f_notyet{L}(integer x) = x; */
+
+int main (void) {
+ int x = 1, y = 2;
+ /*@ assert p1(x, y); */ ;
+ /*@ assert p2(3, 4); */ ;
+ /*@ assert p2(5, 99999999999999999999999999999); */ ;
+
+ /*@ assert f1(x, y) == 3; */ ;
+ /*@ assert p2(x, f1(3, 4)); */ ;
+ /*@ assert f1(9, 99999999999999999999999999999) > 0; */ ;
+ /*@ assert f1(99999999999999999999999999999,
+ 99999999999999999999999999999) ==
+ 199999999999999999999999999998; */ ;
+
+ /*@ assert g(x) == x; */ ;
+
+ char c = 'c';
+ /*@ assert h_char(c) == c; */ ;
+ short s = 1;
+ /*@ assert h_short(s) == s; */ ;
+
+ mystruct m;
+ m.k = 8;
+ m.l = 9;
+ /*@ assert t2(t1(m)) == 17; */ ;
+
+ k(9);
+
+ double d = 2.0;
+ /*@ assert f2(d) > 0; */ ;
+
+ // not yet supported
+ /* /\*@ assert p_notyet(27); *\/ ; */
+ /* /\*@ assert f_notyet(27) == 27; *\/ ; */
+}
diff --git a/src/plugins/e-acsl/tests/gmp-only/oracle/arith.res.oracle b/src/plugins/e-acsl/tests/gmp-only/oracle/arith.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..58ff928b06ae06fc7cc29f0189bd96640c51f53b
--- /dev/null
+++ b/src/plugins/e-acsl/tests/gmp-only/oracle/arith.res.oracle
@@ -0,0 +1,44 @@
+[e-acsl] beginning translation.
+[e-acsl] translation done in project "e-acsl".
+[eva:alarm] tests/gmp-only/arith.i:10: Warning:
+ function __e_acsl_assert: precondition got status unknown.
+[eva:alarm] tests/gmp-only/arith.i:11: Warning:
+ function __e_acsl_assert: precondition got status unknown.
+[eva:alarm] tests/gmp-only/arith.i:12: Warning:
+ function __e_acsl_assert: precondition got status unknown.
+[eva:alarm] tests/gmp-only/arith.i:14: Warning:
+ function __e_acsl_assert: precondition got status unknown.
+[eva:alarm] tests/gmp-only/arith.i:15: Warning:
+ function __e_acsl_assert: precondition got status unknown.
+[eva:alarm] tests/gmp-only/arith.i:16: Warning:
+ function __e_acsl_assert: precondition got status unknown.
+[eva:alarm] tests/gmp-only/arith.i:17: Warning:
+ function __e_acsl_assert: precondition got status unknown.
+[eva:alarm] tests/gmp-only/arith.i:18: Warning:
+ function __e_acsl_assert: precondition got status unknown.
+[eva:alarm] tests/gmp-only/arith.i:19: Warning:
+ function __e_acsl_assert: precondition got status unknown.
+[eva:alarm] tests/gmp-only/arith.i:20: Warning:
+ function __e_acsl_assert: precondition got status unknown.
+[eva:alarm] tests/gmp-only/arith.i:21: Warning:
+ function __e_acsl_assert: precondition got status unknown.
+[eva:alarm] tests/gmp-only/arith.i:23: Warning:
+ function __e_acsl_assert: precondition got status unknown.
+[eva:alarm] tests/gmp-only/arith.i:25: Warning:
+ function __e_acsl_assert: precondition got status unknown.
+[eva:alarm] tests/gmp-only/arith.i:26: Warning:
+ function __e_acsl_assert: precondition got status unknown.
+[eva:alarm] tests/gmp-only/arith.i:27: Warning:
+ function __e_acsl_assert: precondition got status unknown.
+[eva:alarm] tests/gmp-only/arith.i:28: Warning:
+ function __e_acsl_assert: precondition got status unknown.
+[eva:alarm] tests/gmp-only/arith.i:30: Warning:
+ function __e_acsl_assert: precondition got status unknown.
+[eva:alarm] tests/gmp-only/arith.i:31: Warning:
+ function __e_acsl_assert: precondition got status unknown.
+[eva:alarm] tests/gmp-only/arith.i:34: Warning:
+ function __e_acsl_assert: precondition got status unknown.
+[eva:alarm] tests/gmp-only/arith.i:34: Warning:
+ function __e_acsl_assert: precondition got status unknown.
+[eva:alarm] tests/gmp-only/arith.i:36: Warning:
+ function __e_acsl_assert: precondition got status unknown.
diff --git a/src/plugins/e-acsl/tests/gmp-only/oracle/functions.res.oracle b/src/plugins/e-acsl/tests/gmp-only/oracle/functions.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..3a0b1952d64396dde8a2ee52c59bb7dcc12fa20a
--- /dev/null
+++ b/src/plugins/e-acsl/tests/gmp-only/oracle/functions.res.oracle
@@ -0,0 +1,33 @@
+[e-acsl] beginning translation.
+[e-acsl] translation done in project "e-acsl".
+[eva:alarm] tests/gmp-only/functions.c:42: Warning:
+ function __e_acsl_assert: precondition got status unknown.
+[eva:alarm] tests/gmp-only/functions.c:43: Warning:
+ function __e_acsl_assert: precondition got status unknown.
+[eva:alarm] tests/gmp-only/functions.c:44: Warning:
+ function __e_acsl_assert: precondition got status unknown.
+[eva:alarm] tests/gmp-only/functions.c:46: Warning:
+ function __e_acsl_assert: precondition got status unknown.
+[eva:alarm] tests/gmp-only/functions.c:47: Warning:
+ accessing uninitialized left-value.
+ assert \initialized((__e_acsl_mpz_struct *)__gen_e_acsl_f1_4);
+[eva:alarm] tests/gmp-only/functions.c:47: Warning:
+ function __e_acsl_assert: precondition got status unknown.
+[eva:alarm] tests/gmp-only/functions.c:48: Warning:
+ function __e_acsl_assert: precondition got status unknown.
+[eva:alarm] tests/gmp-only/functions.c:49: Warning:
+ function __e_acsl_assert: precondition got status unknown.
+[eva:alarm] tests/gmp-only/functions.c:53: Warning:
+ function __e_acsl_assert: precondition got status unknown.
+[eva:alarm] tests/gmp-only/functions.c:56: Warning:
+ function __e_acsl_assert: precondition got status unknown.
+[eva:alarm] tests/gmp-only/functions.c:58: Warning:
+ function __e_acsl_assert: precondition got status unknown.
+[eva:alarm] tests/gmp-only/functions.c:63: Warning:
+ function __e_acsl_assert: precondition got status unknown.
+[eva:alarm] tests/gmp-only/functions.c:25: Warning:
+ function __e_acsl_assert: precondition got status unknown.
+[eva:alarm] tests/gmp-only/functions.c:68: Warning:
+ non-finite double value. assert \is_finite(__gen_e_acsl__15);
+[eva:alarm] tests/gmp-only/functions.c:68: Warning:
+ function __e_acsl_assert: precondition got status unknown.
diff --git a/src/plugins/e-acsl/tests/arith/oracle/gen_arith2.c b/src/plugins/e-acsl/tests/gmp-only/oracle/gen_arith.c
similarity index 100%
rename from src/plugins/e-acsl/tests/arith/oracle/gen_arith2.c
rename to src/plugins/e-acsl/tests/gmp-only/oracle/gen_arith.c
diff --git a/src/plugins/e-acsl/tests/arith/oracle/gen_functions2.c b/src/plugins/e-acsl/tests/gmp-only/oracle/gen_functions.c
similarity index 100%
rename from src/plugins/e-acsl/tests/arith/oracle/gen_functions2.c
rename to src/plugins/e-acsl/tests/gmp-only/oracle/gen_functions.c
diff --git a/src/plugins/e-acsl/tests/gmp-only/test_config b/src/plugins/e-acsl/tests/gmp-only/test_config
new file mode 100644
index 0000000000000000000000000000000000000000..e69447aecb415446e1813d1d1154ecdbb77a0a57
--- /dev/null
+++ b/src/plugins/e-acsl/tests/gmp-only/test_config
@@ -0,0 +1 @@
+STDOPT: #"-e-acsl-gmp-only"