Skip to content
Snippets Groups Projects
Commit b9b5e52e authored by Andre Maroneze's avatar Andre Maroneze
Browse files

[Eva] update Eva-related options in tests

parent d2a23373
No related branches found
No related tags found
No related merge requests found
Showing
with 30 additions and 30 deletions
/* run.config*
GCC:
STDOPT: #"-no-val-builtins-auto"
STDOPT: #"-no-val-builtins-auto -absolute-valid-range 0x100-0x200 -main main_abs"
STDOPT: #"-eva-no-builtins-auto"
STDOPT: #"-eva-no-builtins-auto -absolute-valid-range 0x100-0x200 -main main_abs"
*/
#define malloc(n) Frama_C_malloc_fresh(n)
......
/* run.config*
STDOPT: +"-no-val-alloc-returns-null"
STDOPT: +"-eva-no-alloc-returns-null"
*/
#include <stdlib.h>
......
/* run.config*
STDOPT: +"-slevel 1 -val-mlevel 0"
STDOPT: +"-slevel 999 -val-builtin malloc:Frama_C_malloc_fresh,__fc_vla_alloc:Frama_C_malloc_fresh,__fc_vla_free:Frama_C_vla_free"
STDOPT: +"-slevel 1 -eva-mlevel 0"
STDOPT: +"-slevel 999 -eva-builtin malloc:Frama_C_malloc_fresh,__fc_vla_alloc:Frama_C_malloc_fresh,__fc_vla_free:Frama_C_vla_free"
*/
#define assert_bottom(exp) if (nondet) {exp; Frama_C_show_each_unreachable();}
......
/* run.config*
OPT: -val-show-progress -print -journal-disable -val -report
OPT: -eva-show-progress -print -journal-disable -eva -report
OPT: -load-script tests/builtins/big_local_array_script.ml -then-on prj -print -report
OPT: -val-show-progress -print -journal-disable -no-initialized-padding-locals -val
OPT: -eva-show-progress -print -journal-disable -no-initialized-padding-locals -eva
*/
struct S {
......
/* run.config*
STDOPT: #"-no-val-builtins-auto -val-alloc-returns-null"
STDOPT: #"-no-val-builtins-auto -val-alloc-returns-null -val-builtin calloc:Frama_C_calloc_fresh"
STDOPT: #"-no-val-builtins-auto -val-alloc-returns-null -val-builtin calloc:Frama_C_calloc_by_stack"
STDOPT: #"-no-val-builtins-auto -no-val-alloc-returns-null -val-builtin calloc:Frama_C_calloc_fresh"
STDOPT: #"-no-val-builtins-auto -no-val-alloc-returns-null -val-builtin calloc:Frama_C_calloc_by_stack"
STDOPT: #"-eva-no-builtins-auto -eva-alloc-returns-null"
STDOPT: #"-eva-no-builtins-auto -eva-alloc-returns-null -eva-builtin calloc:Frama_C_calloc_fresh"
STDOPT: #"-eva-no-builtins-auto -eva-alloc-returns-null -eva-builtin calloc:Frama_C_calloc_by_stack"
STDOPT: #"-eva-no-builtins-auto -eva-no-alloc-returns-null -eva-builtin calloc:Frama_C_calloc_fresh"
STDOPT: #"-eva-no-builtins-auto -eva-no-alloc-returns-null -eva-builtin calloc:Frama_C_calloc_by_stack"
*/
#include <stdlib.h>
......
/* run.config*
STDOPT: #" -val-builtin malloc:Frama_C_malloc_fresh"
STDOPT: #" -eva-builtin malloc:Frama_C_malloc_fresh"
*/
#include "stdlib.h"
volatile v;
......
/* run.config*
OPT: @VALUECONFIG@ -no-val-builtins-auto -deps -journal-disable
OPT: @VALUECONFIG@ -eva-no-builtins-auto -deps -journal-disable
*/
#define malloc(n) Frama_C_malloc_fresh(n)
#include "../../share/libc/stdlib.c"
......
/* run.config*
STDOPT: +"-machdep gcc_x86_32 -val-builtin malloc:Frama_C_malloc_fresh -slevel 11"
STDOPT: +"-machdep gcc_x86_32 -eva-builtin malloc:Frama_C_malloc_fresh -slevel 11"
*/
#include <stdlib.h>
......
/* run.config*
STDOPT: #" -val-mlevel 0 -no-val-alloc-returns-null"
STDOPT: #" -eva-mlevel 0 -eva-no-alloc-returns-null"
*/
extern int i;
......
/* run.config*
STDOPT: #"-load-module variadic -no-val-builtins-auto"
STDOPT: #"-load-module variadic -plevel 100 -big-ints-hex 257 -no-val-builtins-auto"
STDOPT: #"-load-module variadic -slevel 12 -big-ints-hex 257 -no-val-builtins-auto"
STDOPT: #"-load-module variadic -eva-no-builtins-auto"
STDOPT: #"-load-module variadic -plevel 100 -big-ints-hex 257 -eva-no-builtins-auto"
STDOPT: #"-load-module variadic -slevel 12 -big-ints-hex 257 -eva-no-builtins-auto"
*/
#include "__fc_define_size_t.h"
......
/* run.config*
OPT: -val @VALUECONFIG@ -deps -calldeps -inout -slevel 5 -value-msg-key malloc
OPT: -eva @VALUECONFIG@ -deps -calldeps -inout -slevel 5 -eva-msg-key malloc
*/
//@ assigns \result \from \nothing;
void *Frama_C_malloc_fresh(unsigned long n);
......
/* run.config*
STDOPT: +"-slevel 30 -val-slevel-merge-after-loop @all -val-malloc-functions malloc -memexec-all"
STDOPT: +"-slevel 30 -eva-slevel-merge-after-loop @all -eva-malloc-functions malloc -memexec-all"
*/
//@ assigns \result \from \nothing;
......
/* run.config*
OPT: -val @VALUECONFIG@ -val-mlevel 3
OPT: -val @VALUECONFIG@ -val-malloc-functions my_calloc
OPT: -eva @VALUECONFIG@ -eva-mlevel 3
OPT: -eva @VALUECONFIG@ -eva-malloc-functions my_calloc
*/
#include <stdlib.h>
......
/* run.config*
OPT: -val @VALUECONFIG@ -slevel 10 -val-mlevel 0
OPT: -eva @VALUECONFIG@ -slevel 10 -eva-mlevel 0
*/
void *Frama_C_malloc_by_stack(unsigned long i);
......
/* run.config*
OPT: -val @VALUECONFIG@
OPT: -eva @VALUECONFIG@
*/
#include <stdlib.h>
......
/* run.config*
STDOPT: #"-no-val-builtins-auto"
STDOPT: #"-eva-no-builtins-auto"
*/
#define malloc(n) Frama_C_malloc_fresh(n)
#include "share/libc/stdlib.c"
......
/* run.config*
OPT: -val @VALUECONFIG@ -memexec-all -deps -inout -val-mlevel 0
OPT: -eva @VALUECONFIG@ -memexec-all -deps -inout -eva-mlevel 0
*/
//@ assigns \result;
......
/* run.config*
OPT: -val @VALUECONFIG@ -slevel 50 -val-mlevel 5
OPT: -eva @VALUECONFIG@ -slevel 50 -eva-mlevel 5
*/
#include<stdlib.h>
#define MAX 10
......
/* run.config*
STDOPT: +"-calldeps -slevel-function init:2000 -value-msg-key imprecision -plevel 150 -main main_all -inout -no-deps -absolute-valid-range 100000-100001 -then -load-module report -report"
STDOPT: +"-calldeps -slevel-function init:2000 -eva-msg-key imprecision -plevel 150 -main main_all -inout -no-deps -absolute-valid-range 100000-100001 -then -load-module report -report"
*/
#include "string.h"
......
/* run.config*
OPT: -val @VALUECONFIG@ -journal-disable -calldeps
OPT: -eva @VALUECONFIG@ -journal-disable -calldeps
*/
/*@ assigns \result \from min, max;
......
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