Skip to content
GitLab
Explore
Sign in
Primary navigation
Search or go to…
Project
F
frama-c
Manage
Activity
Members
Labels
Plan
Issues
Issue boards
Milestones
Wiki
Code
Merge requests
Repository
Branches
Commits
Tags
Repository graph
Compare revisions
Deploy
Releases
Container Registry
Model registry
Monitor
Incidents
Analyze
Value stream analytics
Contributor analytics
Repository analytics
Model experiments
Help
Help
Support
GitLab documentation
Compare GitLab plans
Community forum
Contribute to GitLab
Provide feedback
Keyboard shortcuts
?
Snippets
Groups
Projects
Show more breadcrumbs
pub
frama-c
Commits
87564b2b
Commit
87564b2b
authored
4 years ago
by
Basile Desloges
Browse files
Options
Downloads
Patches
Plain Diff
[eacsl] Update tests
parent
58434afe
No related branches found
Branches containing commit
No related tags found
Tags containing commit
No related merge requests found
Changes
2
Hide whitespace changes
Inline
Side-by-side
Showing
2 changed files
src/plugins/e-acsl/tests/arith/oracle_ci/gen_functions.c
+42
-42
42 additions, 42 deletions
src/plugins/e-acsl/tests/arith/oracle_ci/gen_functions.c
src/plugins/e-acsl/tests/gmp-only/oracle_ci/gen_functions.c
+46
-46
46 additions, 46 deletions
src/plugins/e-acsl/tests/gmp-only/oracle_ci/gen_functions.c
with
88 additions
and
88 deletions
src/plugins/e-acsl/tests/arith/oracle_ci/gen_functions.c
+
42
−
42
View file @
87564b2b
...
@@ -17,10 +17,10 @@ int __gen_e_acsl_p1(int x, int y);
...
@@ -17,10 +17,10 @@ int __gen_e_acsl_p1(int x, int y);
*/
*/
int
__gen_e_acsl_p2
(
int
x
,
int
y
);
int
__gen_e_acsl_p2
(
int
x
,
int
y
);
int
__gen_e_acsl_p2_3
(
int
x
,
__e_acsl_mpz_struct
*
y
);
int
__gen_e_acsl_p2_5
(
int
x
,
long
y
);
int
__gen_e_acsl_p2_5
(
int
x
,
long
y
);
int
__gen_e_acsl_p2_3
(
int
x
,
__e_acsl_mpz_struct
*
y
);
/*@ logic ℤ f1(ℤ x, ℤ y) = x + y;
/*@ logic ℤ f1(ℤ x, ℤ y) = x + y;
*/
*/
...
@@ -232,56 +232,18 @@ void __gen_e_acsl_k(int x)
...
@@ -232,56 +232,18 @@ void __gen_e_acsl_k(int x)
return
;
return
;
}
}
int
__gen_e_acsl_g
(
int
x
)
{
int
__gen_e_acsl_g_hidden_2
;
__gen_e_acsl_g_hidden_2
=
__gen_e_acsl_g_hidden
(
x
);
return
__gen_e_acsl_g_hidden_2
;
}
mystruct
__gen_e_acsl_t1
(
mystruct
m
)
{
return
m
;
}
int
__gen_e_acsl_p1
(
int
x
,
int
y
)
int
__gen_e_acsl_p1
(
int
x
,
int
y
)
{
{
int
__retres
=
x
+
(
long
)
y
>
0L
;
int
__retres
=
x
+
(
long
)
y
>
0L
;
return
__retres
;
return
__retres
;
}
}
long
__gen_e_acsl_t2
(
mystruct
m
)
{
long
__retres
=
m
.
k
+
(
long
)
m
.
l
;
return
__retres
;
}
int
__gen_e_acsl_p2
(
int
x
,
int
y
)
int
__gen_e_acsl_p2
(
int
x
,
int
y
)
{
{
int
__retres
=
x
+
(
long
)
y
>
0L
;
int
__retres
=
x
+
(
long
)
y
>
0L
;
return
__retres
;
return
__retres
;
}
}
int
__gen_e_acsl_p2_3
(
int
x
,
__e_acsl_mpz_struct
*
y
)
{
__e_acsl_mpz_t
__gen_e_acsl_x
;
__e_acsl_mpz_t
__gen_e_acsl_add
;
__e_acsl_mpz_t
__gen_e_acsl__2
;
int
__gen_e_acsl_gt
;
__gmpz_init_set_si
(
__gen_e_acsl_x
,(
long
)
x
);
__gmpz_init
(
__gen_e_acsl_add
);
__gmpz_add
(
__gen_e_acsl_add
,(
__e_acsl_mpz_struct
const
*
)(
__gen_e_acsl_x
),
(
__e_acsl_mpz_struct
const
*
)(
y
));
__gmpz_init_set_si
(
__gen_e_acsl__2
,
0L
);
__gen_e_acsl_gt
=
__gmpz_cmp
((
__e_acsl_mpz_struct
const
*
)(
__gen_e_acsl_add
),
(
__e_acsl_mpz_struct
const
*
)(
__gen_e_acsl__2
));
int
__retres
=
__gen_e_acsl_gt
>
0
;
__gmpz_clear
(
__gen_e_acsl_x
);
__gmpz_clear
(
__gen_e_acsl_add
);
__gmpz_clear
(
__gen_e_acsl__2
);
return
__retres
;
}
int
__gen_e_acsl_p2_5
(
int
x
,
long
y
)
int
__gen_e_acsl_p2_5
(
int
x
,
long
y
)
{
{
__e_acsl_mpz_t
__gen_e_acsl_x_2
;
__e_acsl_mpz_t
__gen_e_acsl_x_2
;
...
@@ -306,9 +268,23 @@ int __gen_e_acsl_p2_5(int x, long y)
...
@@ -306,9 +268,23 @@ int __gen_e_acsl_p2_5(int x, long y)
return
__retres
;
return
__retres
;
}
}
int
__gen_e_acsl_
k_pred
(
int
x
)
int
__gen_e_acsl_
p2_3
(
int
x
,
__e_acsl_mpz_struct
*
y
)
{
{
int
__retres
=
x
>
0
;
__e_acsl_mpz_t
__gen_e_acsl_x
;
__e_acsl_mpz_t
__gen_e_acsl_add
;
__e_acsl_mpz_t
__gen_e_acsl__2
;
int
__gen_e_acsl_gt
;
__gmpz_init_set_si
(
__gen_e_acsl_x
,(
long
)
x
);
__gmpz_init
(
__gen_e_acsl_add
);
__gmpz_add
(
__gen_e_acsl_add
,(
__e_acsl_mpz_struct
const
*
)(
__gen_e_acsl_x
),
(
__e_acsl_mpz_struct
const
*
)(
y
));
__gmpz_init_set_si
(
__gen_e_acsl__2
,
0L
);
__gen_e_acsl_gt
=
__gmpz_cmp
((
__e_acsl_mpz_struct
const
*
)(
__gen_e_acsl_add
),
(
__e_acsl_mpz_struct
const
*
)(
__gen_e_acsl__2
));
int
__retres
=
__gen_e_acsl_gt
>
0
;
__gmpz_clear
(
__gen_e_acsl_x
);
__gmpz_clear
(
__gen_e_acsl_add
);
__gmpz_clear
(
__gen_e_acsl__2
);
return
__retres
;
return
__retres
;
}
}
...
@@ -363,6 +339,30 @@ int __gen_e_acsl_g_hidden(int x)
...
@@ -363,6 +339,30 @@ int __gen_e_acsl_g_hidden(int x)
return
x
;
return
x
;
}
}
int
__gen_e_acsl_g
(
int
x
)
{
int
__gen_e_acsl_g_hidden_2
;
__gen_e_acsl_g_hidden_2
=
__gen_e_acsl_g_hidden
(
x
);
return
__gen_e_acsl_g_hidden_2
;
}
mystruct
__gen_e_acsl_t1
(
mystruct
m
)
{
return
m
;
}
long
__gen_e_acsl_t2
(
mystruct
m
)
{
long
__retres
=
m
.
k
+
(
long
)
m
.
l
;
return
__retres
;
}
int
__gen_e_acsl_k_pred
(
int
x
)
{
int
__retres
=
x
>
0
;
return
__retres
;
}
double
__gen_e_acsl_f2
(
double
x
)
double
__gen_e_acsl_f2
(
double
x
)
{
{
__e_acsl_mpq_t
__gen_e_acsl__8
;
__e_acsl_mpq_t
__gen_e_acsl__8
;
...
...
This diff is collapsed.
Click to expand it.
src/plugins/e-acsl/tests/gmp-only/oracle_ci/gen_functions.c
+
46
−
46
View file @
87564b2b
...
@@ -288,18 +288,6 @@ void __gen_e_acsl_k(int x)
...
@@ -288,18 +288,6 @@ void __gen_e_acsl_k(int x)
return
;
return
;
}
}
int
__gen_e_acsl_g
(
int
x
)
{
int
__gen_e_acsl_g_hidden_2
;
__gen_e_acsl_g_hidden_2
=
__gen_e_acsl_g_hidden
(
x
);
return
__gen_e_acsl_g_hidden_2
;
}
mystruct
__gen_e_acsl_t1
(
mystruct
m
)
{
return
m
;
}
int
__gen_e_acsl_p1
(
int
x
,
int
y
)
int
__gen_e_acsl_p1
(
int
x
,
int
y
)
{
{
__e_acsl_mpz_t
__gen_e_acsl_x
;
__e_acsl_mpz_t
__gen_e_acsl_x
;
...
@@ -323,25 +311,6 @@ int __gen_e_acsl_p1(int x, int y)
...
@@ -323,25 +311,6 @@ int __gen_e_acsl_p1(int x, int y)
return
__retres
;
return
__retres
;
}
}
void
__gen_e_acsl_t2
(
__e_acsl_mpz_t
*
__retres_arg
,
mystruct
m
)
{
__e_acsl_mpz_t
__gen_e_acsl__10
;
__e_acsl_mpz_t
__gen_e_acsl__11
;
__e_acsl_mpz_t
__gen_e_acsl_add_7
;
__gmpz_init_set_si
(
__gen_e_acsl__10
,(
long
)
m
.
k
);
__gmpz_init_set_si
(
__gen_e_acsl__11
,(
long
)
m
.
l
);
__gmpz_init
(
__gen_e_acsl_add_7
);
__gmpz_add
(
__gen_e_acsl_add_7
,
(
__e_acsl_mpz_struct
const
*
)(
__gen_e_acsl__10
),
(
__e_acsl_mpz_struct
const
*
)(
__gen_e_acsl__11
));
__gmpz_init_set
(
*
__retres_arg
,
(
__e_acsl_mpz_struct
const
*
)(
__gen_e_acsl_add_7
));
__gmpz_clear
(
__gen_e_acsl__10
);
__gmpz_clear
(
__gen_e_acsl__11
);
__gmpz_clear
(
__gen_e_acsl_add_7
);
return
;
}
int
__gen_e_acsl_p2
(
int
x
,
int
y
)
int
__gen_e_acsl_p2
(
int
x
,
int
y
)
{
{
__e_acsl_mpz_t
__gen_e_acsl_x_2
;
__e_acsl_mpz_t
__gen_e_acsl_x_2
;
...
@@ -387,21 +356,6 @@ int __gen_e_acsl_p2_3(int x, __e_acsl_mpz_struct * y)
...
@@ -387,21 +356,6 @@ int __gen_e_acsl_p2_3(int x, __e_acsl_mpz_struct * y)
return
__retres
;
return
__retres
;
}
}
int
__gen_e_acsl_k_pred
(
int
x
)
{
__e_acsl_mpz_t
__gen_e_acsl_x
;
__e_acsl_mpz_t
__gen_e_acsl_
;
int
__gen_e_acsl_gt
;
__gmpz_init_set_si
(
__gen_e_acsl_x
,(
long
)
x
);
__gmpz_init_set_si
(
__gen_e_acsl_
,
0L
);
__gen_e_acsl_gt
=
__gmpz_cmp
((
__e_acsl_mpz_struct
const
*
)(
__gen_e_acsl_x
),
(
__e_acsl_mpz_struct
const
*
)(
__gen_e_acsl_
));
int
__retres
=
__gen_e_acsl_gt
>
0
;
__gmpz_clear
(
__gen_e_acsl_x
);
__gmpz_clear
(
__gen_e_acsl_
);
return
__retres
;
}
void
__gen_e_acsl_f1
(
__e_acsl_mpz_t
*
__retres_arg
,
int
x
,
int
y
)
void
__gen_e_acsl_f1
(
__e_acsl_mpz_t
*
__retres_arg
,
int
x
,
int
y
)
{
{
__e_acsl_mpz_t
__gen_e_acsl_x_4
;
__e_acsl_mpz_t
__gen_e_acsl_x_4
;
...
@@ -466,6 +420,52 @@ int __gen_e_acsl_g_hidden(int x)
...
@@ -466,6 +420,52 @@ int __gen_e_acsl_g_hidden(int x)
return
x
;
return
x
;
}
}
int
__gen_e_acsl_g
(
int
x
)
{
int
__gen_e_acsl_g_hidden_2
;
__gen_e_acsl_g_hidden_2
=
__gen_e_acsl_g_hidden
(
x
);
return
__gen_e_acsl_g_hidden_2
;
}
mystruct
__gen_e_acsl_t1
(
mystruct
m
)
{
return
m
;
}
void
__gen_e_acsl_t2
(
__e_acsl_mpz_t
*
__retres_arg
,
mystruct
m
)
{
__e_acsl_mpz_t
__gen_e_acsl__10
;
__e_acsl_mpz_t
__gen_e_acsl__11
;
__e_acsl_mpz_t
__gen_e_acsl_add_7
;
__gmpz_init_set_si
(
__gen_e_acsl__10
,(
long
)
m
.
k
);
__gmpz_init_set_si
(
__gen_e_acsl__11
,(
long
)
m
.
l
);
__gmpz_init
(
__gen_e_acsl_add_7
);
__gmpz_add
(
__gen_e_acsl_add_7
,
(
__e_acsl_mpz_struct
const
*
)(
__gen_e_acsl__10
),
(
__e_acsl_mpz_struct
const
*
)(
__gen_e_acsl__11
));
__gmpz_init_set
(
*
__retres_arg
,
(
__e_acsl_mpz_struct
const
*
)(
__gen_e_acsl_add_7
));
__gmpz_clear
(
__gen_e_acsl__10
);
__gmpz_clear
(
__gen_e_acsl__11
);
__gmpz_clear
(
__gen_e_acsl_add_7
);
return
;
}
int
__gen_e_acsl_k_pred
(
int
x
)
{
__e_acsl_mpz_t
__gen_e_acsl_x
;
__e_acsl_mpz_t
__gen_e_acsl_
;
int
__gen_e_acsl_gt
;
__gmpz_init_set_si
(
__gen_e_acsl_x
,(
long
)
x
);
__gmpz_init_set_si
(
__gen_e_acsl_
,
0L
);
__gen_e_acsl_gt
=
__gmpz_cmp
((
__e_acsl_mpz_struct
const
*
)(
__gen_e_acsl_x
),
(
__e_acsl_mpz_struct
const
*
)(
__gen_e_acsl_
));
int
__retres
=
__gen_e_acsl_gt
>
0
;
__gmpz_clear
(
__gen_e_acsl_x
);
__gmpz_clear
(
__gen_e_acsl_
);
return
__retres
;
}
double
__gen_e_acsl_f2
(
double
x
)
double
__gen_e_acsl_f2
(
double
x
)
{
{
__e_acsl_mpq_t
__gen_e_acsl__13
;
__e_acsl_mpq_t
__gen_e_acsl__13
;
...
...
This diff is collapsed.
Click to expand it.
Preview
0%
Loading
Try again
or
attach a new file
.
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Save comment
Cancel
Please
register
or
sign in
to comment