Frama-C/Codex Analysis results

int abs(int x)
{
  int res;
  if (x < 0) res = - x; else res = x;
  return res;
}

Unproved alarms:

abs.c:4: Signed_overflow(- x <=
2147483647) {true;false}

Proved 1/2 alarms

/	Name	Type	Value
Expr	x < 0	int	{0; 1}
Expr	x	int	[--..--]
Lval	x	int
Expr	0	int	{0}
Lval	res	int
Expr	- x	int	[1..0x7FFFFFFF]
Expr	x	int	[-0x80000000..-1]
Lval	x	int
Lval	res	int
Expr	x	int	[0..0x7FFFFFFF]
Lval	x	int
Expr	res	int	[0..0x7FFFFFFF]
Lval	res	int
Func	abs	undefined ctype