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
57326b2b
Commit
57326b2b
authored
Feb 28, 2020
by
Virgile Prevosto
Committed by
Andre Maroneze
Mar 06, 2020
Browse files
[tests] E-ACSL oracle
parent
aace07d3
Changes
1
Hide whitespace changes
Inline
Side-by-side
src/plugins/e-acsl/tests/arith/oracle_ci/gen_rationals.c
View file @
57326b2b
...
...
@@ -20,8 +20,7 @@ int main(void)
{
int
__retres
;
__e_acsl_memory_init
((
int
*
)
0
,(
char
***
)
0
,(
size_t
)
8
);
__e_acsl_assert
(
3
.
!=
1
.
5
,(
char
*
)
"Assertion"
,(
char
*
)
"main"
,
(
char
*
)
"3 != 1.5"
,
12
);
__e_acsl_assert
(
1
,(
char
*
)
"Assertion"
,(
char
*
)
"main"
,(
char
*
)
"3 != 1.5"
,
12
);
/*@ assert 3 ≢ 1.5; */
;
{
__e_acsl_mpq_t
__gen_e_acsl_
;
...
...
@@ -61,7 +60,7 @@ int main(void)
__gmpq_clear
(
__gen_e_acsl__4
);
}
/*@ assert 0.1 ≡ 0.1; */
;
__e_acsl_assert
(
1
.
==
1
.
,(
char
*
)
"Assertion"
,(
char
*
)
"main"
,
__e_acsl_assert
(
1
,(
char
*
)
"Assertion"
,(
char
*
)
"main"
,
(
char
*
)
"(double)1.0 == 1.0"
,
15
);
/*@ assert (double)1.0 ≡ 1.0; */
;
{
...
...
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment