Frama-C/Codex Analysis results

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

Unproved alarms:

Proved 2/2 alarms

/	Name	Type	Value
Expr	x < 0	int	{0; 1}
Expr	x	int	[-1000..0x7FFFFFFF]
Lval	x	int
Expr	0	int	{0}
Lval	res	int
Expr	- x	int	[1..1000]
Expr	x	int	[-1000..-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