| commit | 3586101e0bd2194834c04f764fa8c2cf560e9d9d | [log] [tgz] |
|---|---|---|
| author | Nico Huber <nico.huber@secunet.com> | Tue Mar 14 13:29:48 2017 +0100 |
| committer | Nico Huber <nico.h@gmx.de> | Sat Jun 03 15:32:09 2017 +0200 |
| tree | ce9f19fbf8fc3c0e9a991f1966239e5e234f1362 | |
| parent | 1c3b9285ceb3ff7bbb6dab8d9805ca3bda9d0ff3 [diff] |
gma: Juggle with types of a precondition Using the same type (Pos64) as in the actual calculation below, helps current SPARK Pro to prove absence of overflows (SPARK GPL 2016 still works too ofc). Change-Id: Ifde556f9201f3333be0eb8566bf69b7f9df11277 Signed-off-by: Nico Huber <nico.huber@secunet.com> Reviewed-on: https://review.coreboot.org/18809 Tested-by: Nico Huber <nico.h@gmx.de> Reviewed-by: Arthur Heymans <arthur@aheymans.xyz>