Skip to content
Snippets Groups Projects
Commit 2a0e80ad authored by Julien Signoles's avatar Julien Signoles
Browse files

[tests] improve test organization

parent c1e98626
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Showing
with 39 additions and 295 deletions
src/plugins/e-acsl/Makefile.in
+ 2
− 0
View file @ 2a0e80ad
...@@ -171,7 +171,9 @@ ifeq (@MAY_RUN_TESTS@,yes) ...@@ -171,7 +171,9 @@ ifeq (@MAY_RUN_TESTS@,yes)
-include in_frama_ci -include in_frama_ci
PLUGIN_TESTS_DIRS := \ PLUGIN_TESTS_DIRS := \
examples \
bts \ bts \
language_constructs \
arith \ arith \
memory \ memory \
full-mmodel \ full-mmodel \
......
src/plugins/e-acsl/tests/arith/README.md deleted 100644 → 0
+ 0
− 1
View file @ c1e98626
Like runtime, but also test the -e-acsl-gmp-only mode.
src/plugins/e-acsl/tests/arith/oracle/functions_contiki.0.res.oracle deleted 100644 → 0
+ 0
− 25
View file @ c1e98626
[e-acsl] beginning translation.
[e-acsl] tests/gmp/functions_contiki.c:27: Warning:
E-ACSL construct `logic functions with labels' is not yet supported.
Ignoring annotation.
[e-acsl] translation done in project "e-acsl".
[eva] 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_store_block
[eva] using specification for function __e_acsl_initialize
[eva] using specification for function __e_acsl_full_init
[eva] tests/gmp/functions_contiki.c:27:
cannot evaluate ACSL term, unsupported ACSL construct: logic function length
[eva:alarm] tests/gmp/functions_contiki.c:27: 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
src/plugins/e-acsl/tests/arith/oracle/functions_contiki.1.res.oracle deleted 100644 → 0
+ 0
− 25
View file @ c1e98626
[e-acsl] beginning translation.
[e-acsl] tests/gmp/functions_contiki.c:27: Warning:
E-ACSL construct `logic functions with labels' is not yet supported.
Ignoring annotation.
[e-acsl] translation done in project "e-acsl".
[eva] 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_store_block
[eva] using specification for function __e_acsl_initialize
[eva] using specification for function __e_acsl_full_init
[eva] tests/gmp/functions_contiki.c:27:
cannot evaluate ACSL term, unsupported ACSL construct: logic function length
[eva:alarm] tests/gmp/functions_contiki.c:27: 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
src/plugins/e-acsl/tests/arith/oracle/gen_functions_contiki2.c deleted 100644 → 0
+ 0
− 45
View file @ c1e98626
/* Generated by Frama-C */
#include "stdio.h"
#include "stdlib.h"
struct list {
struct list *next ;
int value ;
};
/*@
logic ℤ length_aux{L}(struct list *l, ℤ n) =
\at(n < 0? -1:
(l ≡ (struct list *)((void *)0)? n:
(n < 2147483647? length_aux(l->next, n + 1): -1)),
L);
*/
/*@ logic ℤ length{L}(struct list *l) = \at(length_aux(l, 0),L);
*/
int main(void)
{
int __retres;
struct list node1;
struct list node2;
struct list node3;
__e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
__e_acsl_store_block((void *)(& node3),(size_t)16);
__e_acsl_store_block((void *)(& node2),(size_t)16);
__e_acsl_store_block((void *)(& node1),(size_t)16);
__e_acsl_initialize((void *)(& node1.next),sizeof(struct list *));
node1.next = & node2;
__e_acsl_initialize((void *)(& node2.next),sizeof(struct list *));
node2.next = & node3;
struct list *l = & node1;
__e_acsl_store_block((void *)(& l),(size_t)8);
__e_acsl_full_init((void *)(& l));
/*@ assert length(l) ≡ 3; */ ;
__retres = 0;
__e_acsl_delete_block((void *)(& l));
__e_acsl_delete_block((void *)(& node3));
__e_acsl_delete_block((void *)(& node2));
__e_acsl_delete_block((void *)(& node1));
__e_acsl_memory_clean();
return __retres;
}
src/plugins/e-acsl/tests/arith/oracle/reals.res.oracle → src/plugins/e-acsl/tests/arith/oracle/rationals.res.oracle
+ 24
− 24
View file @ 2a0e80ad
[kernel:parser:decimal-float] tests/arith/reals.c:22: Warning: [kernel:parser:decimal-float] tests/arith/rationals.c:22: Warning:
Floating-point constant 0.2f is not represented exactly. Will use 0x1.99999a0000000p-3. Floating-point constant 0.2f is not represented exactly. Will use 0x1.99999a0000000p-3.
(warn-once: no further messages from category 'parser:decimal-float' will be emitted) (warn-once: no further messages from category 'parser:decimal-float' will be emitted)
[e-acsl] beginning translation. [e-acsl] beginning translation.
[e-acsl] Warning: R to float: double rounding might cause unsoundness [e-acsl] Warning: R to float: double rounding might cause unsoundness
[e-acsl] tests/arith/reals.c:19: Warning: [e-acsl] tests/arith/rationals.c:19: Warning:
E-ACSL construct `predicate with no definition nor reads clause' E-ACSL construct `predicate with no definition nor reads clause'
is not yet supported. is not yet supported.
Ignoring annotation. Ignoring annotation.
[e-acsl] translation done in project "e-acsl". [e-acsl] translation done in project "e-acsl".
[eva:alarm] tests/arith/reals.c:15: Warning: [eva:alarm] tests/arith/rationals.c:15: Warning:
function __e_acsl_assert: precondition got status unknown. function __e_acsl_assert: precondition got status unknown.
[eva:alarm] tests/arith/reals.c:16: Warning: assertion got status unknown. [eva:alarm] tests/arith/rationals.c:16: Warning: assertion got status unknown.
[eva:alarm] tests/arith/reals.c:16: Warning: [eva:alarm] tests/arith/rationals.c:16: Warning:
function __e_acsl_assert: precondition got status unknown. function __e_acsl_assert: precondition got status unknown.
[eva:alarm] tests/arith/reals.c:18: Warning: assertion got status unknown. [eva:alarm] tests/arith/rationals.c:18: Warning: assertion got status unknown.
[eva:alarm] tests/arith/reals.c:18: Warning: [eva:alarm] tests/arith/rationals.c:18: Warning:
non-finite double value. assert \is_finite(__gen_e_acsl__6); non-finite double value. assert \is_finite(__gen_e_acsl__6);
[eva:alarm] tests/arith/reals.c:18: Warning: [eva:alarm] tests/arith/rationals.c:18: Warning:
function __e_acsl_assert: precondition got status unknown. function __e_acsl_assert: precondition got status unknown.
[eva:alarm] tests/arith/reals.c:19: Warning: [eva:alarm] tests/arith/rationals.c:19: Warning:
non-finite double value. assert \is_finite(__gen_e_acsl__9); non-finite double value. assert \is_finite(__gen_e_acsl__9);
[eva:alarm] tests/arith/reals.c:19: Warning: [eva:alarm] tests/arith/rationals.c:19: Warning:
non-finite double value. assert \is_finite(__gen_e_acsl__10); non-finite double value. assert \is_finite(__gen_e_acsl__10);
[eva:alarm] tests/arith/reals.c:19: Warning: [eva:alarm] tests/arith/rationals.c:19: Warning:
non-finite float value. assert \is_finite((float)__gen_e_acsl__9); non-finite float value. assert \is_finite((float)__gen_e_acsl__9);
[eva:alarm] tests/arith/reals.c:19: Warning: [eva:alarm] tests/arith/rationals.c:19: Warning:
function __e_acsl_assert: precondition got status unknown. function __e_acsl_assert: precondition got status unknown.
[eva:alarm] tests/arith/reals.c:20: Warning: assertion got status unknown. [eva:alarm] tests/arith/rationals.c:20: Warning: assertion got status unknown.
[eva:alarm] tests/arith/reals.c:20: Warning: [eva:alarm] tests/arith/rationals.c:20: Warning:
non-finite double value. assert \is_finite(__gen_e_acsl__12); non-finite double value. assert \is_finite(__gen_e_acsl__12);
[eva:alarm] tests/arith/reals.c:20: Warning: [eva:alarm] tests/arith/rationals.c:20: Warning:
function __e_acsl_assert: precondition got status unknown. function __e_acsl_assert: precondition got status unknown.
[eva:alarm] tests/arith/reals.c:21: Warning: assertion got status unknown. [eva:alarm] tests/arith/rationals.c:21: Warning: assertion got status unknown.
[eva:alarm] tests/arith/reals.c:21: Warning: [eva:alarm] tests/arith/rationals.c:21: Warning:
function __e_acsl_assert: precondition got status unknown. function __e_acsl_assert: precondition got status unknown.
[eva:alarm] tests/arith/reals.c:25: Warning: [eva:alarm] tests/arith/rationals.c:25: Warning:
function __e_acsl_assert: precondition got status unknown. function __e_acsl_assert: precondition got status unknown.
[eva:alarm] tests/arith/reals.c:26: Warning: assertion got status unknown. [eva:alarm] tests/arith/rationals.c:26: Warning: assertion got status unknown.
[eva:alarm] tests/arith/reals.c:26: Warning: [eva:alarm] tests/arith/rationals.c:26: Warning:
function __e_acsl_assert: precondition got status unknown. function __e_acsl_assert: precondition got status unknown.
[eva:alarm] tests/arith/reals.c:6: Warning: [eva:alarm] tests/arith/rationals.c:6: Warning:
function __e_acsl_assert: precondition got status unknown. function __e_acsl_assert: precondition got status unknown.
[eva:alarm] tests/arith/reals.c:6: Warning: [eva:alarm] tests/arith/rationals.c:6: Warning:
function __gen_e_acsl_avg: postcondition got status unknown. function __gen_e_acsl_avg: postcondition got status unknown.
[eva:alarm] tests/arith/reals.c:32: Warning: assertion got status unknown. [eva:alarm] tests/arith/rationals.c:32: Warning: assertion got status unknown.
[eva:alarm] tests/arith/reals.c:32: Warning: [eva:alarm] tests/arith/rationals.c:32: Warning:
function __e_acsl_assert: precondition got status unknown. function __e_acsl_assert: precondition got status unknown.
src/plugins/e-acsl/tests/arith/oracle/reals.0.res.oracle deleted 100644 → 0
+ 0
− 73
View file @ c1e98626
[kernel:parser:decimal-float] tests/gmp/reals.c:22: Warning:
Floating-point constant 0.2f is not represented exactly. Will use 0x1.99999a0000000p-3.
(warn-once: no further messages from category 'parser:decimal-float' will be emitted)
[e-acsl] beginning translation.
[e-acsl] Warning: R to float: double rounding might cause unsoundness
[e-acsl] tests/gmp/reals.c:19: Warning:
E-ACSL construct `predicate with no definition nor reads clause'
is not yet supported.
Ignoring annotation.
[e-acsl] translation done in project "e-acsl".
[eva] 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_assert
[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_add
[eva] using specification for function __gmpq_cmp
[eva:alarm] tests/gmp/reals.c:15: Warning:
function __e_acsl_assert: precondition got status unknown.
[eva] using specification for function __gmpq_clear
[eva:alarm] tests/gmp/reals.c:16: Warning: assertion got status unknown.
[eva:alarm] tests/gmp/reals.c:16: Warning:
function __e_acsl_assert: precondition got status unknown.
[eva:alarm] tests/gmp/reals.c:18: Warning: assertion got status unknown.
[eva] using specification for function __gmpq_get_d
[eva:alarm] tests/gmp/reals.c:18: Warning:
non-finite double value. assert \is_finite(__gen_e_acsl__6);
[eva:alarm] tests/gmp/reals.c:18: Warning:
function __e_acsl_assert: precondition got status unknown.
[eva:alarm] tests/gmp/reals.c:19: Warning:
non-finite double value. assert \is_finite(__gen_e_acsl__9);
[eva:alarm] tests/gmp/reals.c:19: Warning:
non-finite double value. assert \is_finite(__gen_e_acsl__10);
[eva:alarm] tests/gmp/reals.c:19: Warning:
non-finite float value. assert \is_finite((float)__gen_e_acsl__9);
[eva:alarm] tests/gmp/reals.c:19: Warning:
function __e_acsl_assert: precondition got status unknown.
[eva:alarm] tests/gmp/reals.c:20: Warning: assertion got status unknown.
[eva:alarm] tests/gmp/reals.c:20: Warning:
non-finite double value. assert \is_finite(__gen_e_acsl__12);
[eva:alarm] tests/gmp/reals.c:20: Warning:
function __e_acsl_assert: precondition got status unknown.
[eva:alarm] tests/gmp/reals.c:21: Warning: assertion got status unknown.
[eva] using specification for function __gmpq_sub
[eva:alarm] tests/gmp/reals.c:21: Warning:
function __e_acsl_assert: precondition got status unknown.
[eva] using specification for function __gmpq_mul
[eva:alarm] tests/gmp/reals.c:25: Warning:
function __e_acsl_assert: precondition got status unknown.
[eva:alarm] tests/gmp/reals.c:26: Warning: assertion got status unknown.
[eva] using specification for function __gmpq_set_si
[eva:alarm] tests/gmp/reals.c:26: Warning:
function __e_acsl_assert: precondition got status unknown.
[eva] using specification for function __gmpq_set
[eva] using specification for function __gmpq_div
[eva:alarm] tests/gmp/reals.c:6: Warning:
function __e_acsl_assert: precondition got status unknown.
[eva:alarm] tests/gmp/reals.c:6: Warning:
function __gen_e_acsl_avg: postcondition got status unknown.
[eva:alarm] tests/gmp/reals.c:32: Warning: assertion got status unknown.
[eva:alarm] tests/gmp/reals.c:32: Warning:
function __e_acsl_assert: precondition got status unknown.
[eva] done for function main
src/plugins/e-acsl/tests/arith/oracle/reals.1.res.oracle deleted 100644 → 0
+ 0
− 73
View file @ c1e98626
[kernel:parser:decimal-float] tests/gmp/reals.c:22: Warning:
Floating-point constant 0.2f is not represented exactly. Will use 0x1.99999a0000000p-3.
(warn-once: no further messages from category 'parser:decimal-float' will be emitted)
[e-acsl] beginning translation.
[e-acsl] Warning: R to float: double rounding might cause unsoundness
[e-acsl] tests/gmp/reals.c:19: Warning:
E-ACSL construct `predicate with no definition nor reads clause'
is not yet supported.
Ignoring annotation.
[e-acsl] translation done in project "e-acsl".
[eva] 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_assert
[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_add
[eva] using specification for function __gmpq_cmp
[eva:alarm] tests/gmp/reals.c:15: Warning:
function __e_acsl_assert: precondition got status unknown.
[eva] using specification for function __gmpq_clear
[eva:alarm] tests/gmp/reals.c:16: Warning: assertion got status unknown.
[eva:alarm] tests/gmp/reals.c:16: Warning:
function __e_acsl_assert: precondition got status unknown.
[eva:alarm] tests/gmp/reals.c:18: Warning: assertion got status unknown.
[eva] using specification for function __gmpq_get_d
[eva:alarm] tests/gmp/reals.c:18: Warning:
non-finite double value. assert \is_finite(__gen_e_acsl__6);
[eva:alarm] tests/gmp/reals.c:18: Warning:
function __e_acsl_assert: precondition got status unknown.
[eva:alarm] tests/gmp/reals.c:19: Warning:
non-finite double value. assert \is_finite(__gen_e_acsl__9);
[eva:alarm] tests/gmp/reals.c:19: Warning:
non-finite double value. assert \is_finite(__gen_e_acsl__10);
[eva:alarm] tests/gmp/reals.c:19: Warning:
non-finite float value. assert \is_finite((float)__gen_e_acsl__9);
[eva:alarm] tests/gmp/reals.c:19: Warning:
function __e_acsl_assert: precondition got status unknown.
[eva:alarm] tests/gmp/reals.c:20: Warning: assertion got status unknown.
[eva:alarm] tests/gmp/reals.c:20: Warning:
non-finite double value. assert \is_finite(__gen_e_acsl__12);
[eva:alarm] tests/gmp/reals.c:20: Warning:
function __e_acsl_assert: precondition got status unknown.
[eva:alarm] tests/gmp/reals.c:21: Warning: assertion got status unknown.
[eva] using specification for function __gmpq_sub
[eva:alarm] tests/gmp/reals.c:21: Warning:
function __e_acsl_assert: precondition got status unknown.
[eva] using specification for function __gmpq_mul
[eva:alarm] tests/gmp/reals.c:25: Warning:
function __e_acsl_assert: precondition got status unknown.
[eva:alarm] tests/gmp/reals.c:26: Warning: assertion got status unknown.
[eva] using specification for function __gmpq_set_si
[eva:alarm] tests/gmp/reals.c:26: Warning:
function __e_acsl_assert: precondition got status unknown.
[eva] using specification for function __gmpq_set
[eva] using specification for function __gmpq_div
[eva:alarm] tests/gmp/reals.c:6: Warning:
function __e_acsl_assert: precondition got status unknown.
[eva:alarm] tests/gmp/reals.c:6: Warning:
function __gen_e_acsl_avg: postcondition got status unknown.
[eva:alarm] tests/gmp/reals.c:32: Warning: assertion got status unknown.
[eva:alarm] tests/gmp/reals.c:32: Warning:
function __e_acsl_assert: precondition got status unknown.
[eva] done for function main
src/plugins/e-acsl/tests/arith/reals1.c.notest deleted 100644 → 0
+ 0
− 16
View file @ c1e98626
/* run.config
COMMENT: real numbers
*/
/*@ ensures
\let delta = 1;
\let third_real = a/3;
third_real - delta < \result < third_real + delta; */
double third(double a) {
return a/3;
}
int main(void) {
int n = 1;
third(11.7);
}
\ No newline at end of file
src/plugins/e-acsl/tests/arith/oracle/functions_contiki.res.oracle → src/plugins/e-acsl/tests/examples/oracle/functions_contiki.res.oracle
+ 2
− 2
View file @ 2a0e80ad
[e-acsl] beginning translation. [e-acsl] beginning translation.
[e-acsl] tests/arith/functions_contiki.c:27: Warning: [e-acsl] tests/examples/functions_contiki.c:27: Warning:
E-ACSL construct `logic functions with labels' is not yet supported. E-ACSL construct `logic functions with labels' is not yet supported.
Ignoring annotation. Ignoring annotation.
[e-acsl] translation done in project "e-acsl". [e-acsl] translation done in project "e-acsl".
[eva:alarm] tests/arith/functions_contiki.c:27: Warning: [eva:alarm] tests/examples/functions_contiki.c:27: Warning:
assertion got status unknown. assertion got status unknown.
src/plugins/e-acsl/tests/memory/oracle/linear_search.res.oracle → src/plugins/e-acsl/tests/examples/oracle/linear_search.res.oracle
+ 11
− 11
View file @ 2a0e80ad
[e-acsl] beginning translation. [e-acsl] beginning translation.
[e-acsl] translation done in project "e-acsl". [e-acsl] translation done in project "e-acsl".
[eva:alarm] tests/memory/linear_search.i:30: Warning: [eva:alarm] tests/examples/linear_search.i:30: Warning:
function __gen_e_acsl_search: precondition got status unknown. function __gen_e_acsl_search: precondition got status unknown.
[eva:alarm] tests/memory/linear_search.i:7: Warning: [eva:alarm] tests/examples/linear_search.i:7: Warning:
function __e_acsl_assert: precondition got status unknown. function __e_acsl_assert: precondition got status unknown.
[eva:alarm] tests/memory/linear_search.i:18: Warning: [eva:alarm] tests/examples/linear_search.i:18: Warning:
loop invariant got status unknown. loop invariant got status unknown.
[eva:alarm] tests/memory/linear_search.i:18: Warning: [eva:alarm] tests/examples/linear_search.i:18: Warning:
function __e_acsl_assert: precondition got status unknown. function __e_acsl_assert: precondition got status unknown.
[eva:alarm] tests/memory/linear_search.i:10: Warning: [eva:alarm] tests/examples/linear_search.i:10: Warning:
function __e_acsl_assert: precondition got status unknown. function __e_acsl_assert: precondition got status unknown.
[eva:alarm] tests/memory/linear_search.i:13: Warning: [eva:alarm] tests/examples/linear_search.i:13: Warning:
function __e_acsl_assert: precondition got status unknown. function __e_acsl_assert: precondition got status unknown.
[eva:alarm] tests/memory/linear_search.i:10: Warning: [eva:alarm] tests/examples/linear_search.i:10: Warning:
function __gen_e_acsl_search, behavior exists: postcondition got status unknown. (Behavior may be inactive, no reduction performed.) function __gen_e_acsl_search, behavior exists: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
[eva:alarm] tests/memory/linear_search.i:13: Warning: [eva:alarm] tests/examples/linear_search.i:13: Warning:
function __gen_e_acsl_search, behavior not_exists: postcondition got status unknown. (Behavior may be inactive, no reduction performed.) function __gen_e_acsl_search, behavior not_exists: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
[eva:alarm] tests/memory/linear_search.i:31: Warning: [eva:alarm] tests/examples/linear_search.i:31: Warning:
assertion got status unknown. assertion got status unknown.
[eva:alarm] tests/memory/linear_search.i:33: Warning: [eva:alarm] tests/examples/linear_search.i:33: Warning:
function __gen_e_acsl_search: precondition got status unknown. function __gen_e_acsl_search: precondition got status unknown.
[eva:alarm] tests/memory/linear_search.i:34: Warning: [eva:alarm] tests/examples/linear_search.i:34: Warning:
assertion got status unknown. assertion got status unknown.
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment