diff --git a/test/c/collections-c/pqueue_tests.t b/test/c/collections-c/pqueue_tests.t index f60e9d61a..3e1ffb119 100644 --- a/test/c/collections-c/pqueue_tests.t +++ b/test/c/collections-c/pqueue_tests.t @@ -9,8 +9,8 @@ Pqueue tests: (symbol_3 i32) (symbol_4 i32) (symbol_5 i32)) - Reached problem! - [13] + Reached problem!Segmentation fault + [139] $ owi c -O0 -I files/normal/include files/normal/src/pqueue.c files/normal/src/common.c files/normal/src/utils.c files/normal/testsuite/pqueue/pqueue_test_pop.c --no-value Trap: memory heap buffer overflow Model: diff --git a/test/c/eacsl/not-yet-supported/gmp/explicit.t b/test/c/eacsl/not-yet-supported/gmp/explicit.t index c1396d1d0..6aabc31df 100644 --- a/test/c/eacsl/not-yet-supported/gmp/explicit.t +++ b/test/c/eacsl/not-yet-supported/gmp/explicit.t @@ -1,14 +1 @@ - $ owi c --e-acsl explicit.c --no-value 2>&1 | grep -v "wasm-ld" | grep -v "gmp.h" - __builtin_expect is a compiler builtin, only allowed for GCC-based machdeps; see option -machdep or run 'frama-c -machdep help' for the list of available machdeps - [kernel:typing:implicit-function-declaration] explicit.c:11: Warning: - __builtin_constant_p is a compiler builtin, only allowed for GCC-based machdeps; see option -machdep or run 'frama-c -machdep help' for the list of available machdeps - E-ACSL construct `assigns clause in behavior' is not yet supported. - Ignoring annotation. - E-ACSL construct `assigns clause in behavior' is not yet supported. - Ignoring annotation. - E-ACSL construct `assigns clause in behavior' is not yet supported. - Ignoring annotation. - E-ACSL construct `assigns clause in behavior' is not yet supported. - Ignoring annotation. - clang: error: linker command failed with exit code 1 (use -v to see invocation) - Clang failed: run with --debug to get the full error message + $ owi c --e-acsl explicit.c --no-value 2>&1 | grep -v "wasm-ld" | grep -v "gmp.h" > err.txt || false