Hello, thank you for your interest. My static analysis tool, F-IKOS, is continuously evolving and offers various options to support different levels of analysis precision.
I have tried the test case you provided and here are the analysis results. As I am currently writing my master’s thesis, I will update my README.md for one-click installation once I’m finished.
Currently, F-IKOS can also analyze Fortran projects; below, I will provide a few examples.
Example 1: change “y = x” to “y = x + 0.1”
real function cap(x)
implicit none
real, intent(in) :: x
real :: y
y = x + 0.1
! Cap the value of y based on certain conditions
if (10.0 > y) then
y = 10.0
else if (15.0 < y) then
y = 20.0
else
y = y / (y - x)
end if
cap = y
end function cap
program main
implicit none
real,external :: cap
real :: a
real :: x
x = 13.3
! Cap the value of x by calling the cap function
a = cap(x)
end program main
Output
$ ikos hello.ll --entry-point=MAIN_ -a='*,-sound,-upa' -fpd=apron-polka-polyhedra-f
[*] Running ikos preprocessor
[*] Running ikos analyzer
[*] Translating LLVM bitcode to AR
[*] Running liveness analysis
[*] Running widening hint analysis
[*] Running interprocedural value analysis
[*] Analyzing entry point 'MAIN_'
[*] Checking properties for entry point 'MAIN_'
# Time stats:
ikos-analyzer: 0.010 sec
ikos-pp : 0.007 sec
# Summary:
Total number of checks : 19
Total number of unreachable checks : 0
Total number of safe checks : 19
Total number of definite unsafe checks: 0
Total number of warnings : 0
The program is SAFE
# Results
No entries.
Example 2: change “y = x” to “y = x + 1.0e-10”
real function cap(x)
implicit none
real, intent(in) :: x
real :: y
y = x + 1.0e-10
! Cap the value of y based on certain conditions
if (10.0 > y) then
y = 10.0
else if (15.0 < y) then
y = 20.0
else
y = y / (y - x)
end if
cap = y
end function cap
program main
implicit none
real,external :: cap
real :: a
real :: x
x = 13.3
! Cap the value of x by calling the cap function
a = cap(x)
end program main
Output
$ ikos hello.ll --entry-point=MAIN_ -a='*,-sound,-upa' -fpd=apron-polka-polyhedra-f
[*] Running ikos preprocessor
[*] Running ikos analyzer
[*] Translating LLVM bitcode to AR
[*] Running liveness analysis
[*] Running widening hint analysis
[*] Running interprocedural value analysis
[*] Analyzing entry point 'MAIN_'
[*] Checking properties for entry point 'MAIN_'
# Time stats:
ikos-analyzer: 0.011 sec
ikos-pp : 0.007 sec
# Summary:
Total number of checks : 19
Total number of unreachable checks : 0
Total number of safe checks : 18
Total number of definite unsafe checks: 0
Total number of warnings : 1
The program is potentially UNSAFE
# Results
hello.f90: In function 'cap_':
hello.f90:12:1: warning: divisor might be zero ()
y = y / (y - x)
^
Example 3: Analyze runtime errors in Fortran project (this is preliminary work)
Structure of project
$ tree ./
./
├── configure
├── include
│ └── math_operations.h
├── main.f90
├── Makefile
└── math_operations.f90
1 directory, 5 files
Use f-ikos to detect runtime errors
$ ikos-scan ./configure
Nothing to analyze.
$ ikos-scan make
ikos-scan-fc -I./include -c main.f90 -o main.o
clang-14: warning: argument unused during compilation: '-Xflang -disable-O0-optnone' [-Wunused-command-line-argument]
ikos-scan-fc -I./include -c math_operations.f90 -o math_operations.o
clang-14: warning: argument unused during compilation: '-Xflang -disable-O0-optnone' [-Wunused-command-line-argument]
ikos-scan-fc main.o math_operations.o -o my_program
Analyze my_program? [Y/n] n
New structure of project: files produced by frontend ‘Flang’
$ tree ./
./
├── configure
├── include
│ └── math_operations.h
├── main.f90
├── main.o
├── main.o.bc
├── Makefile
├── math_operations.f90
├── math_operations.mod
├── math_operations.o
├── math_operations.o.bc
├── my_program
└── my_program.bc
1 directory, 12 files
Begin to analyze all files, and the output shows that
$ ikos main.o.bc --entry-point=MAIN_ -fpd=apron-polka-polyhedra-f -a='*,-sound,-upa'
[*] Running ikos preprocessor
[*] Running ikos analyzer
[*] Translating LLVM bitcode to AR
[*] Running liveness analysis
[*] Running widening hint analysis
[*] Running interprocedural value analysis
[*] Analyzing entry point 'MAIN_'
[*] Checking properties for entry point 'MAIN_'
# Time stats:
ikos-analyzer: 0.010 sec
ikos-pp : 0.009 sec
# Summary:
Total number of checks : 24
Total number of unreachable checks : 5
Total number of safe checks : 18
Total number of definite unsafe checks: 1
Total number of warnings : 0
The program is definitely UNSAFE
# Results
main.f90: In function 'MAIN_':
main.f90:18:1: error: division by zero
r = c / d
(among other codes).