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

[tests] remove useless GMP tests

parent d97c6f2f
No related branches found
No related tags found
No related merge requests found
Showing
with 21 additions and 20 deletions
...@@ -75,6 +75,8 @@ ...@@ -75,6 +75,8 @@
/tests/e-acsl-reject/result/*_DEP /tests/e-acsl-reject/result/*_DEP
/tests/e-acsl-reject/result/*.log /tests/e-acsl-reject/result/*.log
/tests/bts/result/* /tests/bts/result/*
/tests/gmp/result/*.log
/tests/gmp/result/gen*.c
/tests/check/obj/* /tests/check/obj/*
.frama-c .frama-c
tests/ptests_config tests/ptests_config
......
/* run.config /* run.config
COMMENT: addrOf COMMENT: addrOf
COMMENT: no diff COMMENT: no diff
EXECNOW: LOG gen_addrOf2.c BIN gen_addrOf2.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/addrOf.i -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_addrOf2.c > /dev/null && ./gcc_runtime.sh addrOf2 COMMENT: no diff
*/ */
void f(){ void f(){
......
/* run.config /* run.config
COMMENT: alias COMMENT: alias
COMMENT: no diff COMMENT: no diff
EXECNOW: LOG gen_alias2.c BIN gen_alias2.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/alias.i -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_alias2.c > /dev/null && ./gcc_runtime.sh alias2 COMMENT: no diff
*/ */
void f(int* dest, int val) void f(int* dest, int val)
......
...@@ -2,7 +2,7 @@ ...@@ -2,7 +2,7 @@
COMMENT: function call COMMENT: function call
STDOPT: +"-val-builtin __malloc:Frama_C_alloc_size -val-builtin __free:Frama_C_free" STDOPT: +"-val-builtin __malloc:Frama_C_alloc_size -val-builtin __free:Frama_C_free"
COMMENT: no diff COMMENT: no diff
EXECNOW: LOG gen_call2.c BIN gen_call2.out @frama-c@ -cpp-extra-args="-I`@frama-c@ -print-share-path`/libc" -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/call.c -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_call2.c > /dev/null && ./gcc_runtime.sh call2 COMMENT: no diff
*/ */
#include <stdlib.h> #include <stdlib.h>
......
/* run.config /* run.config
COMMENT: Compound initializers COMMENT: Compound initializers
COMMENT: no diff COMMENT: no diff
EXECNOW: LOG gen_compound_initializers2.c BIN gen_compound_initializers2.out @frama-c@ -machdep x86_64 -cpp-extra-args="-I`@frama-c@ -print-share-path`/libc" -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/compound_initializers.c -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_compound_initializers2.c > /dev/null && ./gcc_runtime.sh compound_initializers2 COMMENT: no diff
*/ */
......
/* run.config /* run.config
COMMENT: empty file COMMENT: empty file
OPT: -e-acsl-check -e-acsl -then-on e-acsl -print OPT: -e-acsl-check -e-acsl -then-on e-acsl -print
OPT: -e-acsl-gmp-only -e-acsl -then-on e-acsl -print
*/ */
/* run.config /* run.config
COMMENT: assert \false COMMENT: assert \false
COMMENT: no diff COMMENT: no diff
EXECNOW: LOG gen_false2.c BIN gen_false2.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/false.i -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_false2.c > /dev/null && ./gcc_runtime.sh false2 COMMENT: no diff
*/ */
int main(void) { int main(void) {
int x = 0; int x = 0;
......
...@@ -2,7 +2,7 @@ ...@@ -2,7 +2,7 @@
COMMENT: \freeable COMMENT: \freeable
STDOPT: +"-val-builtin __malloc:Frama_C_alloc_size -val-builtin __free:Frama_C_free" STDOPT: +"-val-builtin __malloc:Frama_C_alloc_size -val-builtin __free:Frama_C_free"
COMMENT: no diff COMMENT: no diff
EXECNOW: LOG gen_freeable2.c BIN gen_freeable2.out @frama-c@ -machdep gcc_x86_64 -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/freeable.c -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_freeable2.c > /dev/null && ./gcc_runtime.sh freeable2 COMMENT: no diff
*/ */
#include "stdlib.h" #include "stdlib.h"
......
/* run.config /* run.config
COMMENT: function contract COMMENT: function contract
COMMENT: no diff COMMENT: no diff
EXECNOW: LOG gen_function_contract2.c BIN gen_function_contract2.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/function_contract.i -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_function_contract2.c > /dev/null && ./gcc_runtime.sh function_contract2 COMMENT: no diff
*/ */
int X = 0, Y = 2; int X = 0, Y = 2;
......
...@@ -2,7 +2,7 @@ ...@@ -2,7 +2,7 @@
COMMENT: ghost code COMMENT: ghost code
STDOPT: #"-cpp-extra-args=\"-I`@frama-c@ -print-share-path`/libc\"" +"-val-builtin __malloc:Frama_C_alloc_size -val-builtin __free:Frama_C_free" STDOPT: #"-cpp-extra-args=\"-I`@frama-c@ -print-share-path`/libc\"" +"-val-builtin __malloc:Frama_C_alloc_size -val-builtin __free:Frama_C_free"
COMMENT: no diff COMMENT: no diff
EXECNOW: LOG gen_ghost2.c BIN gen_ghost2.out @frama-c@ -cpp-extra-args="-I`@frama-c@ -print-share-path`/libc" -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/ghost.i -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_ghost2.c > /dev/null && ./gcc_runtime.sh ghost2 COMMENT: no diff
*/ */
/*@ ghost int G = 0; */ /*@ ghost int G = 0; */
......
/* run.config /* run.config
COMMENT: initialization of globals (bts #1818) COMMENT: initialization of globals (bts #1818)
COMMENT: no diff COMMENT: no diff
EXECNOW: LOG gen_init2.c BIN gen_init2.out @frama-c@ -machdep x86_64 -cpp-extra-args="-I`@frama-c@ -print-share-path`/libc" -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/init.c -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_init2.c > /dev/null && ./gcc_runtime.sh init2 COMMENT: no diff
*/ */
int a = 0, b; int a = 0, b;
......
/* run.config /* run.config
COMMENT: invariant COMMENT: invariant
STDOPT: +"-slevel 11" STDOPT: +"-slevel 11"
EXECNOW: LOG gen_invariant2.c BIN gen_invariant2.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/invariant.i -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_invariant2.c > /dev/null && ./gcc_runtime.sh invariant2 COMMENT: no diff
*/ */
int main(void) { int main(void) {
int x = 0; int x = 0;
......
/* run.config /* run.config
COMMENT: labeled stmt and gotos COMMENT: labeled stmt and gotos
COMMENT: no diff COMMENT: no diff
EXECNOW: LOG gen_labeled_stmt2.c BIN gen_labeled_stmt2.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/labeled_stmt.i -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_labeled_stmt2.c > /dev/null && ./gcc_runtime.sh labeled_stmt2 COMMENT: no diff
*/ */
int X = 0; int X = 0;
......
/* run.config /* run.config
COMMENT: terms and predicates using lazy operators COMMENT: terms and predicates using lazy operators
COMMENT: no diff COMMENT: no diff
EXECNOW: LOG gen_lazy2.c BIN gen_lazy2.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/lazy.i -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_lazy2.c > /dev/null && ./gcc_runtime.sh lazy2 COMMENT: no diff
*/ */
int main(void) { int main(void) {
......
/* run.config /* run.config
COMMENT: linear search (example from the SAC'13 article) COMMENT: linear search (example from the SAC'13 article)
COMMENT: no diff COMMENT: no diff
EXECNOW: LOG gen_linear_search2.c BIN gen_linear_search2.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/linear_search.i -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_linear_search2.c > /dev/null && ./gcc_runtime.sh linear_search2 COMMENT: no diff
*/ */
int A[10]; int A[10];
......
/* run.config /* run.config
COMMENT: literal string COMMENT: literal string
COMMENT: no diff COMMENT: no diff
EXECNOW: LOG gen_literal_string2.c BIN gen_literal_string2.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/literal_string.i -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_literal_string2.c > /dev/null && ./gcc_runtime.sh literal_string2 COMMENT: no diff
*/ */
int main(void); int main(void);
......
/* run.config /* run.config
COMMENT: allocation and de-allocation of local variables COMMENT: allocation and de-allocation of local variables
STDOPT: #"-cpp-extra-args=\"-I`@frama-c@ -print-share-path`/libc\"" +"-val-builtin __malloc:Frama_C_alloc_size -val-builtin __free:Frama_C_free" STDOPT: +"-val-builtin __malloc:Frama_C_alloc_size -val-builtin __free:Frama_C_free"
COMMENT: no diff
COMMENT: no diff COMMENT: no diff
EXECNOW: LOG gen_localvar2.c BIN gen_localvar2.out @frama-c@ -cpp-extra-args="-I`@frama-c@ -print-share-path`/libc" -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/localvar.c -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_localvar2.c > /dev/null && ./gcc_runtime.sh localvar2
*/ */
#include <stdlib.h> #include <stdlib.h>
......
...@@ -2,7 +2,7 @@ ...@@ -2,7 +2,7 @@
COMMENT: loop invariants COMMENT: loop invariants
STDOPT: +"-slevel 160" STDOPT: +"-slevel 160"
COMMENT: no diff COMMENT: no diff
EXECNOW: LOG gen_loop2.c BIN gen_loop2.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/loop.i -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_loop2.c > /dev/null && ./gcc_runtime.sh loop2 COMMENT: no diff
*/ */
void simple_loop() { void simple_loop() {
......
/* run.config /* run.config
COMMENT: the contents of argv should be valid COMMENT: the contents of argv should be valid
COMMENT: no diff COMMENT: no diff
EXECNOW: LOG gen_mainargs2.c BIN gen_mainargs2.out @frama-c@ -machdep x86_64 -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/mainargs.c -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_mainargs2.c > /dev/null && ./gcc_test.sh e-acsl-runtime mainargs2 "" bar baz COMMENT: no diff
*/ */
#include <string.h> #include <string.h>
......
/* run.config /* run.config
COMMENT: Checking heap memory size COMMENT: Checking heap memory size
COMMENT: no diff COMMENT: no diff
EXECNOW: LOG gen_memsize2.c BIN gen_memsize2.out @frama-c@ -machdep=gcc_x86_$(getconf LONG_BIT) -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/memsize.c -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_memsize2.c > /dev/null && ./gcc_runtime.sh memsize2 COMMENT: no diff
*/ */
#include <stdlib.h> #include <stdlib.h>
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment