smackers
Verifying Fortran Intrinsic Function ABS
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
