Skip to content
Snippets Groups Projects
Commit 88668f6b authored by Patrick Baudin's avatar Patrick Baudin
Browse files

[ACSL] fixes casts to unsigned short int (add test file)

parent 2653a4e6
No related branches found
No related tags found
No related merge requests found
unsigned short int toto;
/*@ensures toto==(unsigned short int)param;*/
int F(int param){
return 0;
}
[kernel] Parsing tests/spec/cast_int.i (no preprocessing)
/* Generated by Frama-C */
unsigned short toto;
/*@ ensures toto ≡ (unsigned short)\old(param); */
int F(int param)
{
int __retres;
__retres = 0;
return __retres;
}
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