Verifying Fortran Intrinsic Function ABS

[udwuwenhao]

Hi,

I applied SMACK artifact (for tacas 19) on a Fortran example shown below:

! @expect verified

program main
use smack
implicit none
integer :: x
x = -1
x = ABS(x)
call assert(0 <= x)
end program main

and then SMACK reports an error (assertion failure) found in this program with following message:

SMACK program verifier version 1.9.1
/home/tacas20ae/Desktop/artifact/smack/share/smack/lib/smack.c(41,1): This assertion can fail
Execution trace:
/home/tacas20ae/Desktop/artifact/smack/share/smack/lib/smack.c(1451,3): Trace: Thread=1 (CALL $initialize, CALL _SMACK_static_init, .C283_MAIN = 0, RETURN from __SMACK_static_init , CALL __SMACK_init_func_memory_model)
/home/tacas20ae/Desktop/artifact/smack/share/smack/lib/smack.c(1451,3): Trace: Thread=1 ()
/home/tacas20ae/Desktop/artifact/smack/share/smack/lib/smack.c(1456,1): Trace: Thread=1 ()
abs.f90(3,1): Trace: Thread=1 (RETURN from SMACK_init_func_memory_model , RETURN from $initialize )
abs.f90(3,1): Trace: Thread=1 ()
abs.f90(3,1): Trace: Thread=1 (smack:entry:MAIN = -6195)
abs.f90(3,1): Trace: Thread=1 ()
abs.f90(3,1): Trace: Thread=1 (CALL $alloc)
abs.f90(3,1): Trace: Thread=1 (CALL $$alloc, RETURN from $$alloc , RETURN from $alloc )
abs.f90(3,1): Trace: Thread=1 ()
abs.f90(8,1): Trace: Thread=1 ()
abs.f90(8,1): Trace: Thread=1 (x = -1519)
abs.f90(9,1): Trace: Thread=1 ()
abs.f90(9,1): Trace: Thread=1 (CALL smack_assert)
/home/tacas20ae/Desktop/artifact/smack/share/smack/lib/smack.f90(35,1): Trace: Thread=1 ()
/home/tacas20ae/Desktop/artifact/smack/share/smack/lib/smack.f90(35,1): Trace: Thread=1 (cond_c = 0)
/home/tacas20ae/Desktop/artifact/smack/share/smack/lib/smack.f90(36,1): Trace: Thread=1 ()
/home/tacas20ae/Desktop/artifact/smack/share/smack/lib/smack.f90(36,1): Trace: Thread=1 (CALL __VERIFIER_assert)
/home/tacas20ae/Desktop/artifact/smack/share/smack/lib/smack.c(256,3): Trace: Thread=1 ()
/home/tacas20ae/Desktop/artifact/smack/share/smack/lib/smack.c(256,3): Trace: Thread=1 (__VERIFIER_assert:arg:x = 0)
/home/tacas20ae/Desktop/artifact/smack/share/smack/lib/smack.c(256,3): Trace: Thread=1 ()
/home/tacas20ae/Desktop/artifact/smack/share/smack/lib/smack.c(41,21): Trace: Thread=1 ()
/home/tacas20ae/Desktop/artifact/smack/share/smack/lib/smack.c(41,21): Trace: Thread=1 (ASSERTION FAILS assert $i0 != $0;
/home/tacas20ae/Desktop/artifact/smack/share/smack/lib/smack.f90(36,1): Trace: Thread=1 (RETURN from _VERIFIER_assert )
abs.f90(9,1): Trace: Thread=1 (RETURN from smack_assert )
abs.f90(9,1): Trace: Thread=1 (Done)

SMACK found an error.

May I ask how to change the example so that ABS function can be verified for always returning non-negative values?

Wenhao Wu
Lab. VSL
Dept. CIS
University of Delaware