Skip to content
Snippets Groups Projects
Commit c9f05c24 authored by Thibault Martin's avatar Thibault Martin Committed by Allan Blanchard
Browse files

Use the new syntax for ACSL extension in tests

parent fa26b8ad
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Showing
with 48 additions and 48 deletions
share/libc/netdb.c
+ 2
− 2
View file @ c9f05c24
......@@ -58,11 +58,11 @@ int getaddrinfo(
struct sockaddr* sa = malloc(sizeof(*sa));
if (!sa) return EAI_MEMORY;
sa -> sa_family = Frama_C_interval(0,AF_MAX);
//@ slevel 15;
//@ \eva::slevel 15;
for (int i = 0; i < 14; i++) {
sa -> sa_data[i] = Frama_C_interval(CHAR_MIN,CHAR_MAX);
}
//@ slevel default;
//@ \eva::slevel default;
ai -> ai_flags = 0;
ai -> ai_family = sa -> sa_family;
ai -> ai_socktype = Frama_C_interval(0,SOCK_SEQPACKET);
......
src/plugins/aorai/tests/ya/serial.c
+ 1
− 1
View file @ c9f05c24
......@@ -71,7 +71,7 @@ void main(void)
n = 0;
continue;
}
//@ split data & 0x40;
//@ \eva::split data & 0x40;
}
else { // data receieved
if (n == 0) { // but status was expected}
......
src/plugins/wp/tests/wp_plugin/nullable_ext.c
+ 7
− 7
View file @ c9f05c24
......@@ -17,7 +17,7 @@ int x;
int *g;
/*@ assigns *g, *p, x ;
wp_nullable_args p ;
\wp::wp_nullable_args p ;
*/
void nullable_coherence(int *p) {
if (p == (void *)0) {
......@@ -31,7 +31,7 @@ void nullable_coherence(int *p) {
}
/*@ assigns *p, *q, *r, *s, *t ;
wp_nullable_args p, q, r ;
\wp::wp_nullable_args p, q, r ;
*/
void nullable_in_context(int *p, int *q, int *r, int *s, int *t) {
*p = 42;
......@@ -41,35 +41,35 @@ void nullable_in_context(int *p, int *q, int *r, int *s, int *t) {
}
/*@ assigns *ptr ;
wp_nullable_args ptr ;
\wp::wp_nullable_args ptr ;
*/
void with_declaration(int *ptr);
void with_declaration(int *ptr) {}
#ifdef FAIL_1
/*@ assigns *ptr ;
wp_nullable_args unexisting_ptr ;
\wp::wp_nullable_args unexisting_ptr ;
*/
void fails_no_variable(int *ptr) {}
#endif
#ifdef FAIL_2
/*@ assigns *ptr ;
wp_nullable_args *ptr ;
\wp::wp_nullable_args *ptr ;
*/
void not_a_variable(int *ptr) {}
#endif
#ifdef FAIL_3
/*@ assigns *ptr ;
wp_nullable_args g ;
\wp::wp_nullable_args g ;
*/
void not_a_formal(int *ptr) {}
#endif
#ifdef FAIL_4
/*@ assigns x ;
wp_nullable_args f ;
\wp::wp_nullable_args f ;
*/
void not_a_pointer(int f) {}
#endif
src/plugins/wp/tests/wp_region/annot.i
+ 4
− 4
View file @ c9f05c24
......@@ -31,7 +31,7 @@ typedef struct Block {
SN sum ;
} FB ;
//@ region *fb ;
//@ \wp::region *fb ;
void fb_ADD(FB *fb)
{
fb->out1->v = fb->out1->v + fb->out2->v ;
......@@ -39,9 +39,9 @@ void fb_ADD(FB *fb)
}
/*@
region IN: (fb->inp1 .. fb->inp3), \pattern{PMEM} ;
region OUT: (fb->out1 .. fb->out3), \pattern{PVECTOR} ;
region IDX: (fb->idx1 .. fb->idx3), \pattern{PVECTOR} ;
\wp::region IN: (fb->inp1 .. fb->inp3), \pattern{PMEM} ;
\wp::region OUT: (fb->out1 .. fb->out3), \pattern{PVECTOR} ;
\wp::region IDX: (fb->idx1 .. fb->idx3), \pattern{PVECTOR} ;
*/
void fb_SORT(FB *fb)
{
......
src/plugins/wp/tests/wp_region/annot/a.i
+ 4
− 4
View file @ c9f05c24
......@@ -24,7 +24,7 @@ struct Block {
};
typedef struct Block FB;
/*@ terminates \true;
region *fb; */
\wp::region *fb; */
void fb_ADD(FB *fb)
{
(fb->out1)->v += (fb->out2)->v;
......@@ -33,9 +33,9 @@ void fb_ADD(FB *fb)
}
/*@ terminates \true;
region IN: \pattern{PMEM}, (fb->inp1..fb->inp3);
region OUT: \pattern{PVECTOR}, (fb->out1..fb->out3);
region IDX: \pattern{PVECTOR}, (fb->idx1..fb->idx3);
\wp::region IN: \pattern{PMEM}, (fb->inp1..fb->inp3);
\wp::region OUT: \pattern{PVECTOR}, (fb->out1..fb->out3);
\wp::region IDX: \pattern{PVECTOR}, (fb->idx1..fb->idx3);
*/
void fb_SORT(FB *fb)
{
......
src/plugins/wp/tests/wp_region/annot/b.i
+ 4
− 4
View file @ c9f05c24
......@@ -24,7 +24,7 @@ struct Block {
};
typedef struct Block FB;
/*@ terminates \true;
region *fb; */
\wp::region *fb; */
void fb_ADD(FB *fb)
{
(fb->out1)->v += (fb->out2)->v;
......@@ -33,9 +33,9 @@ void fb_ADD(FB *fb)
}
/*@ terminates \true;
region IN: \pattern{PMEM}, (fb->inp1..fb->inp3);
region OUT: \pattern{PVECTOR}, (fb->out1..fb->out3);
region IDX: \pattern{PVECTOR}, (fb->idx1..fb->idx3);
\wp::region IN: \pattern{PMEM}, (fb->inp1..fb->inp3);
\wp::region OUT: \pattern{PVECTOR}, (fb->out1..fb->out3);
\wp::region IDX: \pattern{PVECTOR}, (fb->idx1..fb->idx3);
*/
void fb_SORT(FB *fb)
{
......
src/plugins/wp/tests/wp_region/array1.i
+ 1
− 1
View file @ c9f05c24
//@ region *p, *q ;
//@ \wp::region *p, *q ;
int job( int n, int * p , int * q )
{
int s = 0 ;
......
src/plugins/wp/tests/wp_region/array2.i
+ 1
− 1
View file @ c9f05c24
//@ region *p; region *q ;
//@ \wp::region *p; \wp::region *q ;
int job( int n, int * p , int * q )
{
int s = 0 ;
......
src/plugins/wp/tests/wp_region/fb_ADD.i
+ 1
− 1
View file @ c9f05c24
......@@ -16,7 +16,7 @@ typedef struct Block {
} FB ;
/*@
region A: fb ;
\wp::region A: fb ;
*/
void job(FB *fb)
{
......
src/plugins/wp/tests/wp_region/fb_SORT.i
+ 4
− 4
View file @ c9f05c24
......@@ -16,10 +16,10 @@ typedef struct Block {
} FB ;
/*@
region Shared: *(fb->inp1 .. fb->inp3);
region IN: (fb->inp1 .. fb->inp3);
region OUT: (fb->out1 .. fb->out3);
region IDX: (fb->idx1 .. fb->idx3);
\wp::region Shared: *(fb->inp1 .. fb->inp3);
\wp::region IN: (fb->inp1 .. fb->inp3);
\wp::region OUT: (fb->out1 .. fb->out3);
\wp::region IDX: (fb->idx1 .. fb->idx3);
*/
void job(FB *fb)
{
......
src/plugins/wp/tests/wp_region/structarray1.i
+ 1
− 1
View file @ c9f05c24
......@@ -6,7 +6,7 @@ typedef struct Matrix {
int coef[4][4];
} * matrix ;
//@ region *X , *R ;
//@ \wp::region *X , *R ;
void job( matrix M , vector X , vector R )
{
for (int i = 0; i < 4; i++) {
......
src/plugins/wp/tests/wp_tip/oracle/pp-trailing.c.out.c
+ 2
− 2
View file @ c9f05c24
/* Generated by Frama-C */
/*@ strategy Prover: \prover("alt-ergo",0.1); */
/*@ \wp::strategy Prover: \prover("alt-ergo",0.1); */
/*@
strategy Lazy:
\wp::strategy Lazy:
Prover,
\tactic("Wp.overflow",
\pattern(\target:\any(P(_, (..)), Q((..)))),
......
src/plugins/wp/tests/wp_tip/oracle/pp-trailing.c.reparse.c
+ 2
− 2
View file @ c9f05c24
/* Generated by Frama-C */
/*@ strategy Prover: \prover("alt-ergo",0.1); */
/*@ \wp::strategy Prover: \prover("alt-ergo",0.1); */
/*@
strategy Lazy:
\wp::strategy Lazy:
Prover,
\tactic("Wp.overflow",
\pattern(\target:\any(P(_, (..)), Q((..)))),
......
src/plugins/wp/tests/wp_tip/pp-trailing.c
+ 2
− 2
View file @ c9f05c24
......@@ -8,8 +8,8 @@
*/
/*@
strategy Prover: \prover("alt-ergo",0.1);
strategy Lazy:
\wp::strategy Prover: \prover("alt-ergo",0.1);
\wp::strategy Lazy:
Prover,
\tactic("Wp.overflow"
,\pattern(\any(P(_, (..)),Q((..))))
......
src/plugins/wp/tests/wp_tip/proof.i
+ 4
− 4
View file @ c9f05c24
......@@ -9,8 +9,8 @@
// Provers
/*@
strategy P1: \prover("alt-ergo");
strategy P2: \prover(0.5);
strategy P3: \prover("alt-ergo",3.0);
strategy P4: P1, P2, P3, \default;
\wp::strategy P1: \prover("alt-ergo");
\wp::strategy P2: \prover(0.5);
\wp::strategy P3: \prover("alt-ergo",3.0);
\wp::strategy P4: P1, P2, P3, \default;
*/
src/plugins/wp/tests/wp_tip/strategy.c
+ 4
− 4
View file @ c9f05c24
......@@ -16,21 +16,21 @@
*/
/*@
strategy Prover: \prover("alt-ergo",0.1);
\wp::strategy Prover: \prover("alt-ergo",0.1);
strategy Lazy:
\wp::strategy Lazy:
Prover,
\tactic("Wp.overflow"
,\pattern(\any(to_uint32(_),to_sint32(_)))
);
strategy Eager:
\wp::strategy Eager:
\tactic("Wp.overflow"
,\pattern(\any(to_uint32(_),to_sint32(_)))
),
Prover;
strategy EagerRange:
\wp::strategy EagerRange:
\tactic("Wp.overflow"
,\pattern(\any(to_uint32(_),to_sint32(_)))
,\child("In-Range",EagerRange)
......
tests/fc_script/find-fun.t/list-functions.c
+ 1
− 1
View file @ c9f05c24
......@@ -11,7 +11,7 @@ static int static_fun() {
}
void k() {
/*@ loop unroll 10; */ // Eva is not loaded, so we must ignore the annotation
/*@ loop \eva::unroll 10; */ // Eva is not loaded, so we must ignore the annotation
for (int i = 0; i < 10; i++) {
extf();
}
......
tests/libc/pwd_c.c
+ 1
− 1
View file @ c9f05c24
......@@ -22,7 +22,7 @@ int main() {
//@ assert valid_read_string(pwd_out.pw_dir);
//@ assert valid_read_string(pwd_out.pw_shell);
}
//@ slevel merge;
//@ \eva::slevel merge;
struct passwd pwd_out2;
res = getpwnam_r("root", &pwd_out2, buf, buflen, &result);
if (result) {
......
tests/libc/stdlib_c.c
+ 1
− 1
View file @ c9f05c24
......@@ -2,7 +2,7 @@
STDOPT: #"-eva-no-builtins-auto -eva-slevel 10 -eva-builtin calloc:Frama_C_calloc -eva-alloc-builtin by_stack -eva-msg-key malloc"
STDOPT: #"-eva-no-builtins-auto -eva-slevel 10 -eva-builtin calloc:Frama_C_calloc -eva-alloc-builtin by_stack -eva-no-alloc-returns-null -eva-msg-key malloc"
STDOPT: #"-eva-no-builtins-auto"
*/ // slevel is used to unroll loops
*/ // \eva::slevel is used to \eva::unroll loops
#define malloc(n) Frama_C_malloc(n)
#include "stdlib.c"
......
tests/libc/string_c.c
+ 1
− 1
View file @ c9f05c24
/* run.config
STDOPT: #"-eva-no-builtins-auto -eva-slevel 1000 -eva-no-skip-stdlib-specs"
*/ // slevel is used to unroll loops
*/ // \eva::slevel is used to \eva::unroll loops
#include "string.c"
volatile int v;
......
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