Skip to content
Snippets Groups Projects
Commit 349bf237 authored by Basile Desloges's avatar Basile Desloges
Browse files

[eacsl] Update tests

parent 82c54c10
No related branches found
No related tags found
No related merge requests found
/* run.config
COMMENT: frama-c/e-acsl#172, test for a term with two successive logic
coercion.
*/
double d2 = 11.;
int main() {
//@ assert (int)d2 > 10;
return 0;
}
/* Generated by Frama-C */
#include "stddef.h"
#include "stdio.h"
double d2 = 11.;
int main(void)
{
int __retres;
__e_acsl_assert(-2147483649. < d2,1,"RTE","main",
"float_to_int: -2147483649 < d2",
"tests/bts/issue-eacsl-172.c",7);
__e_acsl_assert(d2 < 2147483648.,1,"RTE","main",
"float_to_int: d2 < 2147483648",
"tests/bts/issue-eacsl-172.c",7);
__e_acsl_assert((int)d2 > 10,1,"Assertion","main","(int)d2 > 10",
"tests/bts/issue-eacsl-172.c",7);
/*@ assert (int)d2 > 10; */ ;
__retres = 0;
return __retres;
}
[e-acsl] beginning translation.
[e-acsl] translation done in project "e-acsl".
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