Skip to content
Snippets Groups Projects
Commit 3b19f39e authored by Virgile Prevosto's avatar Virgile Prevosto
Browse files

[tests] use better C++ expression for testing, avoiding a Clang warning

parent 42b1074a
No related branches found
No related tags found
No related merge requests found
[kernel] Parsing tests/specs/ternary_op_bts1532.cpp (external front-end) [kernel] Parsing tests/specs/ternary_op_bts1532.cpp (external front-end)
Now output intermediate result Now output intermediate result
/* Generated by Frama-C */ /* Generated by Frama-C */
/*@ ensures \result ≡ (1 ≢ 0? 2: 3); */ /*@ ensures \result ≡ (\old(x) ≢ 0? 0: 1); */
_Bool empty(void) _Bool empty(int x)
{ {
_Bool __retres; _Bool __retres;
__retres = (_Bool)1; int tmp;
if ((_Bool)(x != 0)) tmp = 0; else tmp = 1;
__retres = (_Bool)(tmp != 0);
return __retres; return __retres;
} }
......
//@ ensures \result == (1 ? 2 : 3); //@ ensures \result == (x ? 0 : 1);
bool empty() { return (1 ? 2 : 3); } bool empty(int x) { return (x ? 0 : 1); }
//@ logic integer min(integer x, integer y) = x < y ? x : y; //@ logic integer min(integer x, integer y) = x < y ? x : y;
......
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