Skip to content
GitLab
Menu
Projects
Groups
Snippets
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
pub
frama-c
Commits
73c33a2e
Commit
73c33a2e
authored
Sep 28, 2017
by
Kostyantyn Vorobyov
Committed by
Julien Signoles
Feb 20, 2018
Browse files
Test oracle updates
parent
ca38c040
Changes
116
Hide whitespace changes
Inline
Side-by-side
src/plugins/e-acsl/.gitignore
View file @
73c33a2e
...
...
@@ -56,6 +56,8 @@
/tests/test_config
/tests/runtime/*.cm*
/tests/runtime/result/*
/tests/format/result/*
/tests/builtin/result/*
/tests/temporal/result/*
/tests/special/result/*
/tests/no-main/result/*
...
...
src/plugins/e-acsl/Makefile.in
View file @
73c33a2e
...
...
@@ -130,7 +130,16 @@ $(EACSL_PLUGIN_DIR)/local_config.ml: $(EACSL_PLUGIN_DIR)/Makefile.in $(VERSION_F
ifeq
(@MAY_RUN_TESTS@,yes)
PLUGIN_TESTS_DIRS
:=
reject runtime bts gmp no-main full-mmodel temporal special
PLUGIN_TESTS_DIRS
:=
\
builtin
\
format
\
reject
\
runtime
\
bts
\
gmp
\
no-main
\
full-mmodel
\
temporal
PLUGIN_TESTS_LIB
:=
$(EACSL_PLUGIN_DIR)
/tests/print.ml
E_ACSL_TESTS
:
$(EACSL_PLUGIN_DIR)/tests/test_config
...
...
src/plugins/e-acsl/tests/bts/oracle/gen_bts1304.c
View file @
73c33a2e
/* Generated by Frama-C */
#include "stdio.h"
#include "stdlib.h"
struct
msgA
{
int
type
;
...
...
src/plugins/e-acsl/tests/bts/oracle/gen_bts1307.c
View file @
73c33a2e
/* Generated by Frama-C */
#include "stdio.h"
#include "stdlib.h"
/*@ requires \valid(Mtmax_in);
requires \valid(Mwmax);
...
...
src/plugins/e-acsl/tests/bts/oracle/gen_bts1324.c
View file @
73c33a2e
/* Generated by Frama-C */
#include "stdio.h"
#include "stdlib.h"
/*@ behavior yes:
assumes ∀ int i; 0 < i < n ⇒ *(t + (i - 1)) ≤ *(t + i);
...
...
src/plugins/e-acsl/tests/bts/oracle/gen_bts1326.c
View file @
73c33a2e
/* Generated by Frama-C */
#include "stdio.h"
#include "stdlib.h"
typedef
int
ArrayInt
[
5
];
/*@ ensures
...
...
src/plugins/e-acsl/tests/bts/oracle/gen_bts1395.c
View file @
73c33a2e
/* Generated by Frama-C */
#include "stdio.h"
#include "stdlib.h"
/*@ requires n > 0; */
int
__gen_e_acsl_fact
(
int
n
);
...
...
src/plugins/e-acsl/tests/bts/oracle/gen_bts1478.c
View file @
73c33a2e
/* Generated by Frama-C */
#include "stdio.h"
#include "stdlib.h"
int
global_i
;
...
...
src/plugins/e-acsl/tests/bts/oracle/gen_bts1700.c
View file @
73c33a2e
/* Generated by Frama-C */
#include "stdio.h"
#include "stdlib.h"
struct
toto
{
...
...
src/plugins/e-acsl/tests/bts/oracle/gen_bts1717.c
View file @
73c33a2e
/* Generated by Frama-C */
#include "stdio.h"
#include "stdlib.h"
int
main
(
void
)
{
...
...
src/plugins/e-acsl/tests/bts/oracle/gen_bts1718.c
View file @
73c33a2e
/* Generated by Frama-C */
#include "stdio.h"
#include "stdlib.h"
int
main
(
void
)
{
...
...
src/plugins/e-acsl/tests/bts/oracle/gen_bts1740.c
View file @
73c33a2e
/* Generated by Frama-C */
#include "stdio.h"
#include "stdlib.h"
int
main
(
void
)
{
...
...
src/plugins/e-acsl/tests/bts/oracle/gen_bts1837.c
View file @
73c33a2e
/* Generated by Frama-C */
#include "stdio.h"
#include "stdlib.h"
char
*
__gen_e_acsl_literal_string_3
;
char
*
__gen_e_acsl_literal_string
;
...
...
src/plugins/e-acsl/tests/bts/oracle/gen_bts2191.c
View file @
73c33a2e
/* Generated by Frama-C */
#include "stdio.h"
#include "stdlib.h"
char
*
__gen_e_acsl_literal_string
;
char
*
__gen_e_acsl_literal_string_2
;
...
...
src/plugins/e-acsl/tests/bts/oracle/gen_bts2192.c
View file @
73c33a2e
/* Generated by Frama-C */
#include "stdio.h"
#include "stdlib.h"
char
*
__gen_e_acsl_literal_string
;
int
a
;
...
...
src/plugins/e-acsl/tests/bts/oracle/gen_bts2231.c
View file @
73c33a2e
/* Generated by Frama-C */
#include "stdio.h"
#include "stdlib.h"
long
A
=
(
long
)
0
;
int
main
(
void
)
...
...
src/plugins/e-acsl/tests/bts/oracle/gen_bts2252.c
View file @
73c33a2e
/* Generated by Frama-C */
#include "stdio.h"
#include "stdlib.h"
char
*
__gen_e_acsl_literal_string
;
/*@ assigns \result, *(x_0 + (0 ..)), *(x_1 + (0 ..));
...
...
src/plugins/e-acsl/tests/builtin/oracle/gen_strcat.c
View file @
73c33a2e
...
...
@@ -188,6 +188,8 @@ void __e_acsl_globals_init(void)
__e_acsl_full_init
((
void
*
)(
&
__gen_e_acsl_strcat
));
__e_acsl_store_block
((
void
*
)(
&
__gen_e_acsl_exit
),(
size_t
)
1
);
__e_acsl_full_init
((
void
*
)(
&
__gen_e_acsl_exit
));
__e_acsl_store_block
((
void
*
)(
&
__fc_strtok_ptr
),(
size_t
)
8
);
__e_acsl_full_init
((
void
*
)(
&
__fc_strtok_ptr
));
__e_acsl_store_block
((
void
*
)(
&
signal_eval
),(
size_t
)
1
);
__e_acsl_full_init
((
void
*
)(
&
signal_eval
));
__e_acsl_store_block
((
void
*
)(
&
testno
),(
size_t
)
4
);
...
...
@@ -196,7 +198,7 @@ void __e_acsl_globals_init(void)
__e_acsl_full_init
((
void
*
)(
&
__fc_time
));
__e_acsl_store_block
((
void
*
)(
&
__fc_p_fopen
),(
size_t
)
8
);
__e_acsl_full_init
((
void
*
)(
&
__fc_p_fopen
));
__e_acsl_store_block
((
void
*
)(
__fc_fopen
),(
size_t
)
4096
);
__e_acsl_store_block
((
void
*
)(
__fc_fopen
),(
size_t
)
128
);
__e_acsl_full_init
((
void
*
)(
&
__fc_fopen
));
__e_acsl_store_block
((
void
*
)(
&
__fc_rand_max
),(
size_t
)
8
);
__e_acsl_full_init
((
void
*
)(
&
__fc_rand_max
));
...
...
@@ -260,7 +262,7 @@ int main(int argc, char const **argv)
int
process_status
;
__e_acsl_store_block
((
void
*
)(
&
process_status
),(
size_t
)
4
);
waitpid
(
pid
,
&
process_status
,
0
);
/*@ assert Value: initiali
s
ation: \initialized(&process_status); */
/*@ assert Value: initiali
z
ation: \initialized(&process_status); */
signal_eval
(
process_status
,
0
,
__gen_e_acsl_literal_string_8
);
__e_acsl_delete_block
((
void
*
)(
&
process_status
));
}
...
...
@@ -283,7 +285,7 @@ int main(int argc, char const **argv)
int
process_status_0
;
__e_acsl_store_block
((
void
*
)(
&
process_status_0
),(
size_t
)
4
);
waitpid
(
pid_0
,
&
process_status_0
,
0
);
/*@ assert Value: initiali
s
ation: \initialized(&process_status_0); */
/*@ assert Value: initiali
z
ation: \initialized(&process_status_0); */
signal_eval
(
process_status_0
,
0
,
__gen_e_acsl_literal_string_9
);
__e_acsl_delete_block
((
void
*
)(
&
process_status_0
));
}
...
...
@@ -306,7 +308,7 @@ int main(int argc, char const **argv)
int
process_status_1
;
__e_acsl_store_block
((
void
*
)(
&
process_status_1
),(
size_t
)
4
);
waitpid
(
pid_1
,
&
process_status_1
,
0
);
/*@ assert Value: initiali
s
ation: \initialized(&process_status_1); */
/*@ assert Value: initiali
z
ation: \initialized(&process_status_1); */
signal_eval
(
process_status_1
,
1
,
__gen_e_acsl_literal_string_10
);
__e_acsl_delete_block
((
void
*
)(
&
process_status_1
));
}
...
...
@@ -330,7 +332,7 @@ int main(int argc, char const **argv)
int
process_status_2
;
__e_acsl_store_block
((
void
*
)(
&
process_status_2
),(
size_t
)
4
);
waitpid
(
pid_2
,
&
process_status_2
,
0
);
/*@ assert Value: initiali
s
ation: \initialized(&process_status_2); */
/*@ assert Value: initiali
z
ation: \initialized(&process_status_2); */
signal_eval
(
process_status_2
,
1
,
__gen_e_acsl_literal_string_11
);
__e_acsl_delete_block
((
void
*
)(
&
process_status_2
));
}
...
...
@@ -354,7 +356,7 @@ int main(int argc, char const **argv)
int
process_status_3
;
__e_acsl_store_block
((
void
*
)(
&
process_status_3
),(
size_t
)
4
);
waitpid
(
pid_3
,
&
process_status_3
,
0
);
/*@ assert Value: initiali
s
ation: \initialized(&process_status_3); */
/*@ assert Value: initiali
z
ation: \initialized(&process_status_3); */
signal_eval
(
process_status_3
,
1
,
__gen_e_acsl_literal_string_12
);
__e_acsl_delete_block
((
void
*
)(
&
process_status_3
));
}
...
...
@@ -377,7 +379,7 @@ int main(int argc, char const **argv)
int
process_status_4
;
__e_acsl_store_block
((
void
*
)(
&
process_status_4
),(
size_t
)
4
);
waitpid
(
pid_4
,
&
process_status_4
,
0
);
/*@ assert Value: initiali
s
ation: \initialized(&process_status_4); */
/*@ assert Value: initiali
z
ation: \initialized(&process_status_4); */
signal_eval
(
process_status_4
,
1
,
__gen_e_acsl_literal_string_13
);
__e_acsl_delete_block
((
void
*
)(
&
process_status_4
));
}
...
...
@@ -400,7 +402,7 @@ int main(int argc, char const **argv)
int
process_status_5
;
__e_acsl_store_block
((
void
*
)(
&
process_status_5
),(
size_t
)
4
);
waitpid
(
pid_5
,
&
process_status_5
,
0
);
/*@ assert Value: initiali
s
ation: \initialized(&process_status_5); */
/*@ assert Value: initiali
z
ation: \initialized(&process_status_5); */
signal_eval
(
process_status_5
,
1
,
__gen_e_acsl_literal_string_14
);
__e_acsl_delete_block
((
void
*
)(
&
process_status_5
));
}
...
...
@@ -423,7 +425,7 @@ int main(int argc, char const **argv)
int
process_status_6
;
__e_acsl_store_block
((
void
*
)(
&
process_status_6
),(
size_t
)
4
);
waitpid
(
pid_6
,
&
process_status_6
,
0
);
/*@ assert Value: initiali
s
ation: \initialized(&process_status_6); */
/*@ assert Value: initiali
z
ation: \initialized(&process_status_6); */
signal_eval
(
process_status_6
,
1
,
__gen_e_acsl_literal_string_15
);
__e_acsl_delete_block
((
void
*
)(
&
process_status_6
));
}
...
...
@@ -446,7 +448,7 @@ int main(int argc, char const **argv)
int
process_status_7
;
__e_acsl_store_block
((
void
*
)(
&
process_status_7
),(
size_t
)
4
);
waitpid
(
pid_7
,
&
process_status_7
,
0
);
/*@ assert Value: initiali
s
ation: \initialized(&process_status_7); */
/*@ assert Value: initiali
z
ation: \initialized(&process_status_7); */
signal_eval
(
process_status_7
,
1
,
__gen_e_acsl_literal_string_16
);
__e_acsl_delete_block
((
void
*
)(
&
process_status_7
));
}
...
...
@@ -469,7 +471,7 @@ int main(int argc, char const **argv)
int
process_status_8
;
__e_acsl_store_block
((
void
*
)(
&
process_status_8
),(
size_t
)
4
);
waitpid
(
pid_8
,
&
process_status_8
,
0
);
/*@ assert Value: initiali
s
ation: \initialized(&process_status_8); */
/*@ assert Value: initiali
z
ation: \initialized(&process_status_8); */
signal_eval
(
process_status_8
,
1
,
__gen_e_acsl_literal_string_17
);
__e_acsl_delete_block
((
void
*
)(
&
process_status_8
));
}
...
...
@@ -492,7 +494,7 @@ int main(int argc, char const **argv)
int
process_status_9
;
__e_acsl_store_block
((
void
*
)(
&
process_status_9
),(
size_t
)
4
);
waitpid
(
pid_9
,
&
process_status_9
,
0
);
/*@ assert Value: initiali
s
ation: \initialized(&process_status_9); */
/*@ assert Value: initiali
z
ation: \initialized(&process_status_9); */
signal_eval
(
process_status_9
,
1
,
__gen_e_acsl_literal_string_18
);
__e_acsl_delete_block
((
void
*
)(
&
process_status_9
));
}
...
...
@@ -517,7 +519,7 @@ int main(int argc, char const **argv)
int
process_status_10
;
__e_acsl_store_block
((
void
*
)(
&
process_status_10
),(
size_t
)
4
);
waitpid
(
pid_10
,
&
process_status_10
,
0
);
/*@ assert Value: initiali
s
ation: \initialized(&process_status_10); */
/*@ assert Value: initiali
z
ation: \initialized(&process_status_10); */
signal_eval
(
process_status_10
,
0
,
__gen_e_acsl_literal_string_19
);
__e_acsl_delete_block
((
void
*
)(
&
process_status_10
));
}
...
...
@@ -540,7 +542,7 @@ int main(int argc, char const **argv)
int
process_status_11
;
__e_acsl_store_block
((
void
*
)(
&
process_status_11
),(
size_t
)
4
);
waitpid
(
pid_11
,
&
process_status_11
,
0
);
/*@ assert Value: initiali
s
ation: \initialized(&process_status_11); */
/*@ assert Value: initiali
z
ation: \initialized(&process_status_11); */
signal_eval
(
process_status_11
,
0
,
__gen_e_acsl_literal_string_20
);
__e_acsl_delete_block
((
void
*
)(
&
process_status_11
));
}
...
...
@@ -563,7 +565,7 @@ int main(int argc, char const **argv)
int
process_status_12
;
__e_acsl_store_block
((
void
*
)(
&
process_status_12
),(
size_t
)
4
);
waitpid
(
pid_12
,
&
process_status_12
,
0
);
/*@ assert Value: initiali
s
ation: \initialized(&process_status_12); */
/*@ assert Value: initiali
z
ation: \initialized(&process_status_12); */
signal_eval
(
process_status_12
,
1
,
__gen_e_acsl_literal_string_21
);
__e_acsl_delete_block
((
void
*
)(
&
process_status_12
));
}
...
...
@@ -588,7 +590,7 @@ int main(int argc, char const **argv)
int
process_status_13
;
__e_acsl_store_block
((
void
*
)(
&
process_status_13
),(
size_t
)
4
);
waitpid
(
pid_13
,
&
process_status_13
,
0
);
/*@ assert Value: initiali
s
ation: \initialized(&process_status_13); */
/*@ assert Value: initiali
z
ation: \initialized(&process_status_13); */
signal_eval
(
process_status_13
,
1
,
__gen_e_acsl_literal_string_22
);
__e_acsl_delete_block
((
void
*
)(
&
process_status_13
));
}
...
...
@@ -612,7 +614,7 @@ int main(int argc, char const **argv)
int
process_status_14
;
__e_acsl_store_block
((
void
*
)(
&
process_status_14
),(
size_t
)
4
);
waitpid
(
pid_14
,
&
process_status_14
,
0
);
/*@ assert Value: initiali
s
ation: \initialized(&process_status_14); */
/*@ assert Value: initiali
z
ation: \initialized(&process_status_14); */
signal_eval
(
process_status_14
,
1
,
__gen_e_acsl_literal_string_23
);
__e_acsl_delete_block
((
void
*
)(
&
process_status_14
));
}
...
...
@@ -636,7 +638,7 @@ int main(int argc, char const **argv)
int
process_status_15
;
__e_acsl_store_block
((
void
*
)(
&
process_status_15
),(
size_t
)
4
);
waitpid
(
pid_15
,
&
process_status_15
,
0
);
/*@ assert Value: initiali
s
ation: \initialized(&process_status_15); */
/*@ assert Value: initiali
z
ation: \initialized(&process_status_15); */
signal_eval
(
process_status_15
,
1
,
__gen_e_acsl_literal_string_24
);
__e_acsl_delete_block
((
void
*
)(
&
process_status_15
));
}
...
...
@@ -659,7 +661,7 @@ int main(int argc, char const **argv)
int
process_status_16
;
__e_acsl_store_block
((
void
*
)(
&
process_status_16
),(
size_t
)
4
);
waitpid
(
pid_16
,
&
process_status_16
,
0
);
/*@ assert Value: initiali
s
ation: \initialized(&process_status_16); */
/*@ assert Value: initiali
z
ation: \initialized(&process_status_16); */
signal_eval
(
process_status_16
,
1
,
__gen_e_acsl_literal_string_25
);
__e_acsl_delete_block
((
void
*
)(
&
process_status_16
));
}
...
...
@@ -683,7 +685,7 @@ int main(int argc, char const **argv)
int
process_status_17
;
__e_acsl_store_block
((
void
*
)(
&
process_status_17
),(
size_t
)
4
);
waitpid
(
pid_17
,
&
process_status_17
,
0
);
/*@ assert Value: initiali
s
ation: \initialized(&process_status_17); */
/*@ assert Value: initiali
z
ation: \initialized(&process_status_17); */
signal_eval
(
process_status_17
,
1
,
__gen_e_acsl_literal_string_26
);
__e_acsl_delete_block
((
void
*
)(
&
process_status_17
));
}
...
...
@@ -706,7 +708,7 @@ int main(int argc, char const **argv)
int
process_status_18
;
__e_acsl_store_block
((
void
*
)(
&
process_status_18
),(
size_t
)
4
);
waitpid
(
pid_18
,
&
process_status_18
,
0
);
/*@ assert Value: initiali
s
ation: \initialized(&process_status_18); */
/*@ assert Value: initiali
z
ation: \initialized(&process_status_18); */
signal_eval
(
process_status_18
,
1
,
__gen_e_acsl_literal_string_27
);
__e_acsl_delete_block
((
void
*
)(
&
process_status_18
));
}
...
...
@@ -729,7 +731,7 @@ int main(int argc, char const **argv)
int
process_status_19
;
__e_acsl_store_block
((
void
*
)(
&
process_status_19
),(
size_t
)
4
);
waitpid
(
pid_19
,
&
process_status_19
,
0
);
/*@ assert Value: initiali
s
ation: \initialized(&process_status_19); */
/*@ assert Value: initiali
z
ation: \initialized(&process_status_19); */
signal_eval
(
process_status_19
,
1
,
__gen_e_acsl_literal_string_28
);
__e_acsl_delete_block
((
void
*
)(
&
process_status_19
));
}
...
...
@@ -752,7 +754,7 @@ int main(int argc, char const **argv)
int
process_status_20
;
__e_acsl_store_block
((
void
*
)(
&
process_status_20
),(
size_t
)
4
);
waitpid
(
pid_20
,
&
process_status_20
,
0
);
/*@ assert Value: initiali
s
ation: \initialized(&process_status_20); */
/*@ assert Value: initiali
z
ation: \initialized(&process_status_20); */
signal_eval
(
process_status_20
,
1
,
__gen_e_acsl_literal_string_29
);
__e_acsl_delete_block
((
void
*
)(
&
process_status_20
));
}
...
...
@@ -763,6 +765,7 @@ int main(int argc, char const **argv)
__retres
=
0
;
__e_acsl_delete_block
((
void
*
)(
&
argv
));
__e_acsl_delete_block
((
void
*
)(
&
argc
));
__e_acsl_delete_block
((
void
*
)(
&
__fc_strtok_ptr
));
__e_acsl_delete_block
((
void
*
)(
&
signal_eval
));
__e_acsl_delete_block
((
void
*
)(
&
testno
));
__e_acsl_delete_block
((
void
*
)(
&
__fc_time
));
...
...
src/plugins/e-acsl/tests/builtin/oracle/gen_strcmp.c
View file @
73c33a2e
...
...
@@ -230,18 +230,20 @@ void __e_acsl_globals_init(void)
__e_acsl_full_init
((
void
*
)(
&
__gen_e_acsl_abort
));
__e_acsl_store_block
((
void
*
)(
&
fail_ncomp
),(
size_t
)
1
);
__e_acsl_full_init
((
void
*
)(
&
fail_ncomp
));
__e_acsl_store_block
((
void
*
)(
&
__fc_strtok_ptr
),(
size_t
)
8
);
__e_acsl_full_init
((
void
*
)(
&
__fc_strtok_ptr
));
__e_acsl_store_block
((
void
*
)(
&
signal_eval
),(
size_t
)
1
);
__e_acsl_full_init
((
void
*
)(
&
signal_eval
));
__e_acsl_store_block
((
void
*
)(
&
testno
),(
size_t
)
4
);
__e_acsl_full_init
((
void
*
)(
&
testno
));
__e_acsl_store_block
((
void
*
)(
&
__fc_time
),(
size_t
)
4
);
__e_acsl_full_init
((
void
*
)(
&
__fc_time
));
__e_acsl_store_block
((
void
*
)(
&
stderr
),(
size_t
)
8
);
__e_acsl_full_init
((
void
*
)(
&
stderr
));
__e_acsl_store_block
((
void
*
)(
&
__fc_p_fopen
),(
size_t
)
8
);
__e_acsl_full_init
((
void
*
)(
&
__fc_p_fopen
));
__e_acsl_store_block
((
void
*
)(
__fc_fopen
),(
size_t
)
4096
);
__e_acsl_store_block
((
void
*
)(
__fc_fopen
),(
size_t
)
128
);
__e_acsl_full_init
((
void
*
)(
&
__fc_fopen
));
__e_acsl_store_block
((
void
*
)(
&
stderr
),(
size_t
)
8
);
__e_acsl_full_init
((
void
*
)(
&
stderr
));
__e_acsl_store_block
((
void
*
)(
&
__fc_rand_max
),(
size_t
)
8
);
__e_acsl_full_init
((
void
*
)(
&
__fc_rand_max
));
return
;
...
...
@@ -299,7 +301,6 @@ int main(int argc, char const **argv)
int
process_status
;
__e_acsl_store_block
((
void
*
)(
&
process_status
),(
size_t
)
4
);
waitpid
(
pid
,
&
process_status
,
0
);
/*@ assert Value: initialisation: \initialized(&process_status); */
signal_eval
(
process_status
,
0
,
__gen_e_acsl_literal_string_8
);
__e_acsl_delete_block
((
void
*
)(
&
process_status
));
}
...
...
@@ -332,7 +333,6 @@ int main(int argc, char const **argv)
int
process_status_0
;
__e_acsl_store_block
((
void
*
)(
&
process_status_0
),(
size_t
)
4
);
waitpid
(
pid_0
,
&
process_status_0
,
0
);
/*@ assert Value: initialisation: \initialized(&process_status_0); */
signal_eval
(
process_status_0
,
0
,
__gen_e_acsl_literal_string_9
);
__e_acsl_delete_block
((
void
*
)(
&
process_status_0
));
}
...
...
@@ -365,7 +365,6 @@ int main(int argc, char const **argv)
int
process_status_1
;
__e_acsl_store_block
((
void
*
)(
&
process_status_1
),(
size_t
)
4
);
waitpid
(
pid_1
,
&
process_status_1
,
0
);
/*@ assert Value: initialisation: \initialized(&process_status_1); */
signal_eval
(
process_status_1
,
0
,
__gen_e_acsl_literal_string_10
);
__e_acsl_delete_block
((
void
*
)(
&
process_status_1
));
}
...
...
@@ -400,7 +399,6 @@ int main(int argc, char const **argv)
int
process_status_2
;
__e_acsl_store_block
((
void
*
)(
&
process_status_2
),(
size_t
)
4
);
waitpid
(
pid_2
,
&
process_status_2
,
0
);
/*@ assert Value: initialisation: \initialized(&process_status_2); */
signal_eval
(
process_status_2
,
1
,
__gen_e_acsl_literal_string_11
);
__e_acsl_delete_block
((
void
*
)(
&
process_status_2
));
}
...
...
@@ -435,7 +433,6 @@ int main(int argc, char const **argv)
int
process_status_3
;
__e_acsl_store_block
((
void
*
)(
&
process_status_3
),(
size_t
)
4
);
waitpid
(
pid_3
,
&
process_status_3
,
0
);
/*@ assert Value: initialisation: \initialized(&process_status_3); */
signal_eval
(
process_status_3
,
1
,
__gen_e_acsl_literal_string_12
);
__e_acsl_delete_block
((
void
*
)(
&
process_status_3
));
}
...
...
@@ -470,7 +467,6 @@ int main(int argc, char const **argv)
int
process_status_4
;
__e_acsl_store_block
((
void
*
)(
&
process_status_4
),(
size_t
)
4
);
waitpid
(
pid_4
,
&
process_status_4
,
0
);
/*@ assert Value: initialisation: \initialized(&process_status_4); */
signal_eval
(
process_status_4
,
1
,
__gen_e_acsl_literal_string_13
);
__e_acsl_delete_block
((
void
*
)(
&
process_status_4
));
}
...
...
@@ -505,7 +501,6 @@ int main(int argc, char const **argv)
int
process_status_5
;
__e_acsl_store_block
((
void
*
)(
&
process_status_5
),(
size_t
)
4
);
waitpid
(
pid_5
,
&
process_status_5
,
0
);
/*@ assert Value: initialisation: \initialized(&process_status_5); */
signal_eval
(
process_status_5
,
1
,
__gen_e_acsl_literal_string_14
);
__e_acsl_delete_block
((
void
*
)(
&
process_status_5
));
}
...
...
@@ -538,7 +533,6 @@ int main(int argc, char const **argv)
int
process_status_6
;
__e_acsl_store_block
((
void
*
)(
&
process_status_6
),(
size_t
)
4
);
waitpid
(
pid_6
,
&
process_status_6
,
0
);
/*@ assert Value: initialisation: \initialized(&process_status_6); */
signal_eval
(
process_status_6
,
1
,
__gen_e_acsl_literal_string_15
);
__e_acsl_delete_block
((
void
*
)(
&
process_status_6
));
}
...
...
@@ -571,7 +565,6 @@ int main(int argc, char const **argv)
int
process_status_7
;
__e_acsl_store_block
((
void
*
)(
&
process_status_7
),(
size_t
)
4
);
waitpid
(
pid_7
,
&
process_status_7
,
0
);
/*@ assert Value: initialisation: \initialized(&process_status_7); */
signal_eval
(
process_status_7
,
1
,
__gen_e_acsl_literal_string_16
);
__e_acsl_delete_block
((
void
*
)(
&
process_status_7
));
}
...
...
@@ -1071,12 +1064,13 @@ int main(int argc, char const **argv)
__e_acsl_delete_block
((
void
*
)(
&
argv
));
__e_acsl_delete_block
((
void
*
)(
&
argc
));
__e_acsl_delete_block
((
void
*
)(
&
fail_ncomp
));
__e_acsl_delete_block
((
void
*
)(
&
__fc_strtok_ptr
));
__e_acsl_delete_block
((
void
*
)(
&
signal_eval
));
__e_acsl_delete_block
((
void
*
)(
&
testno
));
__e_acsl_delete_block
((
void
*
)(
&
__fc_time
));
__e_acsl_delete_block
((
void
*
)(
&
stderr
));
__e_acsl_delete_block
((
void
*
)(
&
__fc_p_fopen
));
__e_acsl_delete_block
((
void
*
)(
__fc_fopen
));
__e_acsl_delete_block
((
void
*
)(
&
stderr
));
__e_acsl_delete_block
((
void
*
)(
&
__fc_rand_max
));
__e_acsl_delete_block
((
void
*
)(
&
res
));
__e_acsl_delete_block
((
void
*
)(
&
dr
));
...
...
src/plugins/e-acsl/tests/builtin/oracle/gen_strcpy.c
View file @
73c33a2e
...
...
@@ -160,6 +160,8 @@ void __e_acsl_globals_init(void)
__e_acsl_full_init
((
void
*
)(
&
__gen_e_acsl_strcpy
));
__e_acsl_store_block
((
void
*
)(
&
__gen_e_acsl_exit
),(
size_t
)
1
);
__e_acsl_full_init
((
void
*
)(
&
__gen_e_acsl_exit
));
__e_acsl_store_block
((
void
*
)(
&
__fc_strtok_ptr
),(
size_t
)
8
);
__e_acsl_full_init
((
void
*
)(
&
__fc_strtok_ptr
));
__e_acsl_store_block
((
void
*
)(
&
signal_eval
),(
size_t
)
1
);
__e_acsl_full_init
((
void
*
)(
&
signal_eval
));
__e_acsl_store_block
((
void
*
)(
&
testno
),(
size_t
)
4
);
...
...
@@ -168,7 +170,7 @@ void __e_acsl_globals_init(void)
__e_acsl_full_init
((
void
*
)(
&
__fc_time
));
__e_acsl_store_block
((
void
*
)(
&
__fc_p_fopen
),(
size_t
)
8
);
__e_acsl_full_init
((
void
*
)(
&
__fc_p_fopen
));
__e_acsl_store_block
((
void
*
)(
__fc_fopen
),(
size_t
)
4096
);
__e_acsl_store_block
((
void
*
)(
__fc_fopen
),(
size_t
)
128
);
__e_acsl_full_init
((
void
*
)(
&
__fc_fopen
));
__e_acsl_store_block
((
void
*
)(
&
__fc_rand_max
),(
size_t
)
8
);
__e_acsl_full_init
((
void
*
)(
&
__fc_rand_max
));
...
...
@@ -223,7 +225,6 @@ int main(int argc, char const **argv)
int
process_status
;
__e_acsl_store_block
((
void
*
)(
&
process_status
),(
size_t
)
4
);
waitpid
(
pid
,
&
process_status
,
0
);
/*@ assert Value: initialisation: \initialized(&process_status); */
signal_eval
(
process_status
,
0
,
__gen_e_acsl_literal_string_7
);
__e_acsl_delete_block
((
void
*
)(
&
process_status
));
}
...
...
@@ -246,7 +247,6 @@ int main(int argc, char const **argv)
int
process_status_0
;
__e_acsl_store_block
((
void
*
)(
&
process_status_0
),(
size_t
)
4
);
waitpid
(
pid_0
,
&
process_status_0
,
0
);
/*@ assert Value: initialisation: \initialized(&process_status_0); */
signal_eval
(
process_status_0
,
0
,
__gen_e_acsl_literal_string_9
);
__e_acsl_delete_block
((
void
*
)(
&
process_status_0
));
}
...
...
@@ -269,7 +269,6 @@ int main(int argc, char const **argv)
int
process_status_1
;
__e_acsl_store_block
((
void
*
)(
&
process_status_1
),(
size_t
)
4
);
waitpid
(
pid_1
,
&
process_status_1
,
0
);
/*@ assert Value: initialisation: \initialized(&process_status_1); */
signal_eval
(
process_status_1
,
1
,
__gen_e_acsl_literal_string_10
);
__e_acsl_delete_block
((
void
*
)(
&
process_status_1
));
}
...
...
@@ -285,7 +284,6 @@ int main(int argc, char const **argv)
__e_acsl_store_block
((
void
*
)(
&
pid_2
),(
size_t
)
4
);
__e_acsl_full_init
((
void
*
)(
&
pid_2
));
if
(
!
pid_2
)
{
/*@ assert Value: dangling_pointer: ¬\dangling(&unalloc_str); */
__gen_e_acsl_strcpy
(
unalloc_str
,(
char
const
*
)
src
);
__gen_e_acsl_exit
(
0
);
}
...
...
@@ -293,7 +291,6 @@ int main(int argc, char const **argv)
int
process_status_2
;
__e_acsl_store_block
((
void
*
)(
&
process_status_2
),(
size_t
)
4
);
waitpid
(
pid_2
,
&
process_status_2
,
0
);
/*@ assert Value: initialisation: \initialized(&process_status_2); */
signal_eval
(
process_status_2
,
1
,
__gen_e_acsl_literal_string_11
);
__e_acsl_delete_block
((
void
*
)(
&
process_status_2
));
}
...
...
@@ -316,7 +313,6 @@ int main(int argc, char const **argv)
int
process_status_3
;
__e_acsl_store_block
((
void
*
)(
&
process_status_3
),(
size_t
)
4
);
waitpid
(
pid_3
,
&
process_status_3
,
0
);
/*@ assert Value: initialisation: \initialized(&process_status_3); */
signal_eval
(
process_status_3
,
1
,
__gen_e_acsl_literal_string_12
);
__e_acsl_delete_block
((
void
*
)(
&
process_status_3
));
}
...
...
@@ -339,7 +335,6 @@ int main(int argc, char const **argv)
int
process_status_4
;
__e_acsl_store_block
((
void
*
)(
&
process_status_4
),(
size_t
)
4
);
waitpid
(
pid_4
,
&
process_status_4
,
0
);
/*@ assert Value: initialisation: \initialized(&process_status_4); */
signal_eval
(
process_status_4
,
0
,
__gen_e_acsl_literal_string_13
);
__e_acsl_delete_block
((
void
*
)(
&
process_status_4
));
}
...
...
@@ -362,7 +357,6 @@ int main(int argc, char const **argv)
int
process_status_5
;
__e_acsl_store_block
((
void
*
)(
&
process_status_5
),(
size_t
)
4
);
waitpid
(
pid_5
,
&
process_status_5
,
0
);
/*@ assert Value: initialisation: \initialized(&process_status_5); */
signal_eval
(
process_status_5
,
1
,
__gen_e_acsl_literal_string_14
);
__e_acsl_delete_block
((
void
*
)(
&
process_status_5
));
}
...
...
@@ -385,7 +379,6 @@ int main(int argc, char const **argv)
int
process_status_6
;
__e_acsl_store_block
((
void
*
)(
&
process_status_6
),(
size_t
)
4
);
waitpid
(
pid_6
,
&
process_status_6
,
0
);
/*@ assert Value: initialisation: \initialized(&process_status_6); */
signal_eval
(
process_status_6
,
0
,
__gen_e_acsl_literal_string_15
);
__e_acsl_delete_block
((
void
*
)(
&
process_status_6
));
}
...
...
@@ -408,7 +401,6 @@ int main(int argc, char const **argv)
int
process_status_7
;
__e_acsl_store_block
((
void
*
)(
&
process_status_7
),(
size_t
)
4
);
waitpid
(
pid_7
,
&
process_status_7
,
0
);
/*@ assert Value: initialisation: \initialized(&process_status_7); */
signal_eval
(
process_status_7
,
1
,
__gen_e_acsl_literal_string_16
);
__e_acsl_delete_block
((
void
*
)(
&
process_status_7
));
}
...
...
@@ -431,7 +423,6 @@ int main(int argc, char const **argv)
int
process_status_8
;
__e_acsl_store_block
((
void
*
)(
&
process_status_8
),(
size_t
)
4
);
waitpid
(
pid_8
,
&
process_status_8
,
0
);
/*@ assert Value: initialisation: \initialized(&process_status_8); */
signal_eval
(
process_status_8
,
0
,
__gen_e_acsl_literal_string_17
);
__e_acsl_delete_block
((
void
*
)(
&
process_status_8
));
}
...
...
@@ -454,7 +445,6 @@ int main(int argc, char const **argv)
int
process_status_9
;
__e_acsl_store_block
((
void
*
)(
&
process_status_9
),(
size_t
)
4
);
waitpid
(
pid_9
,
&
process_status_9
,
0
);
/*@ assert Value: initialisation: \initialized(&process_status_9); */
signal_eval
(
process_status_9
,
1
,
__gen_e_acsl_literal_string_18
);
__e_acsl_delete_block
((
void
*
)(
&
process_status_9
));
}
...
...
@@ -470,7 +460,6 @@ int main(int argc, char const **argv)
__e_acsl_store_block
((
void
*
)(
&
pid_10
),(
size_t
)
4
);
__e_acsl_full_init
((
void
*
)(
&
pid_10
));
if
(
!
pid_10
)
{
/*@ assert Value: dangling_pointer: ¬\dangling(&unalloc_str); */
__gen_e_acsl_strncpy
(
unalloc_str
,(
char
const
*
)
src
,(
unsigned
long
)
5
);
__gen_e_acsl_exit
(
0
);
}
...
...
@@ -478,7 +467,6 @@ int main(int argc, char const **argv)
int
process_status_10
;
__e_acsl_store_block
((
void
*
)(
&
process_status_10
),(
size_t
)
4
);
waitpid
(
pid_10
,
&
process_status_10
,
0
);
/*@ assert Value: initialisation: \initialized(&process_status_10); */
signal_eval
(
process_status_10
,
1
,
__gen_e_acsl_literal_string_19
);
__e_acsl_delete_block
((
void
*
)(
&
process_status_10
));
}
...
...
@@ -501,7 +489,6 @@ int main(int argc, char const **argv)
int
process_status_11
;
__e_acsl_store_block
((
void
*
)(
&
process_status_11
),(
size_t
)
4
);
waitpid
(
pid_11
,
&
process_status_11
,
0
);
/*@ assert Value: initialisation: \initialized(&process_status_11); */
signal_eval
(
process_status_11
,
1
,
__gen_e_acsl_literal_string_20
);
__e_acsl_delete_block
((
void
*
)(
&
process_status_11
));
}
...
...
@@ -524,7 +511,6 @@ int main(int argc, char const **argv)
int
process_status_12
;
__e_acsl_store_block
((
void
*
)(
&
process_status_12
),(
size_t
)
4
);
waitpid
(
pid_12
,
&
process_status_12
,
0
);
/*@ assert Value: initialisation: \initialized(&process_status_12); */
signal_eval
(
process_status_12
,
0
,
__gen_e_acsl_literal_string_21
);
__e_acsl_delete_block
((
void
*
)(
&
process_status_12
));
}
...
...
@@ -547,7 +533,6 @@ int main(int argc, char const **argv)
int
process_status_13
;
__e_acsl_store_block
((
void
*
)(
&
process_status_13
),(
size_t
)
4
);
waitpid
(
pid_13
,
&
process_status_13
,
0
);
/*@ assert Value: initialisation: \initialized(&process_status_13); */
signal_eval
(
process_status_13
,
1
,
__gen_e_acsl_literal_string_22
);
__e_acsl_delete_block
((
void
*
)(
&
process_status_13
));
}
...
...
@@ -570,7 +555,6 @@ int main(int argc, char const **argv)
int
process_status_14
;
__e_acsl_store_block
((
void
*
)(
&
process_status_14
),(
size_t
)
4
);