Skip to content
Snippets Groups Projects
Select Git revision
  • master default protected
  • stable/zinc
  • 2699-wp-region-plugin-division-by-0-with-empty-region-node
  • stable/copper
  • stable/nickel
  • stable/cobalt
  • stable/iron
  • stable/manganese
  • stable/chromium
  • stable/vanadium
  • stable/titanium-backport
  • stable/titanium
  • stable/scandium
  • 30.0 protected
  • 30.0-beta protected
  • MIEL-2024-10 protected
  • 29.0 protected
  • 29.0-beta protected
  • 28.1 protected
  • 28.0 protected
  • MIEL-2023-10 protected
  • 28.0-beta protected
  • 27.1 protected
  • 27.0 protected
  • 27.0-beta protected
  • 26.1 protected
  • 26.0 protected
  • 26.0-beta protected
  • 25.0-r1 protected
  • pre-dune protected
  • 25.0 protected
  • 25.0-beta protected
  • 2022-03-23 protected
33 results
Blame Permalink
call_2.i 271 B
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17 






/* run.config*
   STDOPT: +"-warn-signed-overflow"
*/

void ff(float f, int i, int j){
  Frama_C_show_each(i, f, j);
}

void main(int i, int j, int c) {
  float f;
  int z;
  int *p = (int*)&f;
  *p = i;
  if (c) z = 1;
  ff(f, i+j, z); // Arguments with potential RTE
}