Commit 929ed1f1 authored by Andre Maroneze's avatar Andre Maroneze 💬
Browse files

Merge branch 'add-tsvc' into 'master'

[tsvc] new case study

See merge request !15
parents d65757b5 532a564e
Pipeline #34634 passed with stage
in 55 minutes and 39 seconds
......@@ -79,6 +79,7 @@ TARGETS=\
safestringlib \
semver \
solitaire \
tsvc \
tweetnacl-usable \
x509-parser \
......
......@@ -156,5 +156,6 @@ when available. We also summarize the license of each directory below.
- `safestringlib`: MIT
- `semver`: MIT
- `solitaire`: public domain, see `solitaire.c`
- `tsvc`: MIT, see `license.txt`
- `tweetnacl-usable`: public domain, see `LICENSE.txt`
- `x509-parser` : GPLv2 / BSD, see `LICENSE`
# Makefile template for Frama-C/Eva case studies.
# For details and usage information, see the Frama-C User Manual.
### Prologue. Do not modify this block. #######################################
-include path.mk
FRAMAC ?= frama-c
include $(shell $(FRAMAC)-config -print-share-path)/analysis-scripts/prologue.mk
###############################################################################
# Edit below as needed. Suggested flags are optional.
MACHDEP =
## Preprocessing flags (for -cpp-extra-args)
CPPFLAGS += \
## General flags
FCFLAGS += \
-add-symbolic-path=..:. \
-kernel-warn-key annot:missing-spec=abort \
-kernel-warn-key typing:implicit-function-declaration=abort \
-warn-special-float none \
## Eva-specific flags
EVAFLAGS += \
-eva-warn-key builtins:missing-spec=abort \
-eva-precision 1 \
## GUI-only flags
FCGUIFLAGS += \
## Analysis targets (suffixed with .eva)
TARGETS = tsvc.eva
### Each target <t>.eva needs a rule <t>.parse with source files as prerequisites
tsvc.parse: \
$(shell $(FRAMAC)-config -print-share-path)/libc/string.c \
../dummy.c \
../tsvc.c \
### Epilogue. Do not modify this block. #######################################
include $(shell $(FRAMAC)-config -print-share-path)/analysis-scripts/epilogue.mk
###############################################################################
# optional, for OSCS
-include ../../Makefile.common
../../path.mk
\ No newline at end of file
directory file line function property kind status property
. tsvc.c 107 set1ds mem_access Unknown \valid(arr + i)
. tsvc.c 115 set1ds mem_access Unknown \valid(arr + i_1)
. tsvc.c 1106 s118 index_bound Unknown 0 ≤ (int)((int)(i - j) - 1)
. tsvc.c 1228 s122 index_bound Unknown 0 ≤ (int)(32000 - k)
. tsvc.c 1259 s123 index_bound Unknown j < 32000
. tsvc.c 1262 s123 index_bound Unknown j < 32000
. tsvc.c 1294 s124 index_bound Unknown j < 32000
. tsvc.c 1297 s124 index_bound Unknown j < 32000
. tsvc.c 1328 s125 index_bound Unknown k < (int)(256 * 256)
. tsvc.c 1358 s126 index_bound Unknown (int)(k - 1) < (int)(256 * 256)
. tsvc.c 1361 s126 signed_overflow Unknown k + 1 ≤ 2147483647
. tsvc.c 1391 s127 index_bound Unknown j < 32000
. tsvc.c 1423 s128 signed_overflow Unknown j + 1 ≤ 2147483647
. tsvc.c 1424 s128 index_bound Unknown k < 32000
. tsvc.c 1512 s141 index_bound Unknown k < (int)(256 * 256)
. tsvc.c 3692 s318 precondition of abs Unknown abs_representable: j > -2147483647 - 1
. tsvc.c 3692 s318 float_to_int Unknown -2147483649 < a[k]
. tsvc.c 3692 s318 float_to_int Unknown a[k] < 2147483648
. tsvc.c 3692 s318 is_nan_or_infinite Unknown \is_finite((float)a[k])
. tsvc.c 3692 s318 index_bound Unknown k < 32000
. tsvc.c 3696 s318 precondition of abs Unknown abs_representable: j > -2147483647 - 1
. tsvc.c 3902 s3113 precondition of abs Unknown abs_representable: j > -2147483647 - 1
. tsvc.c 3902 s3113 float_to_int Unknown -2147483649 < a[i]
. tsvc.c 3902 s3113 float_to_int Unknown a[i] < 2147483648
. tsvc.c 3902 s3113 is_nan_or_infinite Unknown \is_finite((float)a[i])
. tsvc.c 3903 s3113 precondition of abs Unknown abs_representable: j > -2147483647 - 1
. tsvc.c 4100 s341 index_bound Unknown j < 32000
. tsvc.c 4133 s342 index_bound Unknown j < 32000
. tsvc.c 4167 s343 index_bound Unknown k < (int)(256 * 256)
. tsvc.c 4228 s1351 mem_access Unknown \valid(A)
. tsvc.c 4228 s1351 mem_access Unknown \valid_read(B)
. tsvc.c 4228 s1351 mem_access Unknown \valid_read(C)
. tsvc.c 4291 s353 initialization Unknown \initialized(ip + i)
. tsvc.c 4292 s353 initialization Unknown \initialized(ip + (int)(i + 1))
. tsvc.c 4293 s353 initialization Unknown \initialized(ip + (int)(i + 2))
. tsvc.c 4294 s353 initialization Unknown \initialized(ip + (int)(i + 3))
. tsvc.c 4295 s353 initialization Unknown \initialized(ip + (int)(i + 4))
. tsvc.c 4330 s421 initialization Unknown \initialized(yy + (int)(i + 1))
. tsvc.c 4339 s421 initialization Unknown \initialized(xx + i_0)
. tsvc.c 4816 s491 initialization Unknown \initialized(ip + i)
. tsvc.c 4843 s4112 initialization Unknown \initialized(ip + i)
. tsvc.c 4871 s4113 initialization Unknown \initialized(ip + i)
. tsvc.c 4900 s4114 initialization Unknown \initialized(ip + i)
. tsvc.c 4932 s4115 initialization Unknown \initialized(ip + i)
. tsvc.c 4965 s4116 initialization Unknown \initialized(ip + i)
. tsvc.c 4965 s4116 index_bound Unknown *(ip + i) < 256
. tsvc.c 5074 vag initialization Unknown \initialized(ip + i)
. tsvc.c 5102 vas initialization Unknown \initialized(ip + i)
FRAMAC_SHARE/libc stdlib.h 564 abs precondition Unknown abs_representable: j > -2147483647 - 1
[metrics] Eva coverage statistics
=======================
Syntactically reachable functions = 164 (out of 167)
Semantically reached functions = 164
Coverage estimation = 100.0%
[metrics] Statements analyzed by Eva
--------------------------
5478 stmts in analyzed functions, 5439 stmts analyzed (99.3%)
dummy: 2 stmts out of 2 (100.0%)
f__fc_inline: 2 stmts out of 2 (100.0%)
main: 160 stmts out of 160 (100.0%)
s000: 25 stmts out of 25 (100.0%)
s111: 25 stmts out of 25 (100.0%)
s1111: 25 stmts out of 25 (100.0%)
s1112: 25 stmts out of 25 (100.0%)
s1113: 25 stmts out of 25 (100.0%)
s1115: 31 stmts out of 31 (100.0%)
s1119: 31 stmts out of 31 (100.0%)
s112: 25 stmts out of 25 (100.0%)
s113: 25 stmts out of 25 (100.0%)
s114: 31 stmts out of 31 (100.0%)
s115: 31 stmts out of 31 (100.0%)
s116: 29 stmts out of 29 (100.0%)
s1161: 30 stmts out of 30 (100.0%)
s118: 31 stmts out of 31 (100.0%)
s119: 31 stmts out of 31 (100.0%)
s121: 26 stmts out of 26 (100.0%)
s1213: 26 stmts out of 26 (100.0%)
s122: 28 stmts out of 28 (100.0%)
s1221: 25 stmts out of 25 (100.0%)
s123: 30 stmts out of 30 (100.0%)
s1232: 31 stmts out of 31 (100.0%)
s124: 30 stmts out of 30 (100.0%)
s1244: 26 stmts out of 26 (100.0%)
s125: 33 stmts out of 33 (100.0%)
s1251: 27 stmts out of 27 (100.0%)
s126: 35 stmts out of 35 (100.0%)
s127: 29 stmts out of 29 (100.0%)
s1279: 27 stmts out of 27 (100.0%)
s128: 29 stmts out of 29 (100.0%)
s1281: 27 stmts out of 27 (100.0%)
s131: 26 stmts out of 26 (100.0%)
s13110: 37 stmts out of 37 (100.0%)
s132: 28 stmts out of 28 (100.0%)
s1351: 32 stmts out of 32 (100.0%)
s141: 34 stmts out of 34 (100.0%)
s1421: 36 stmts out of 36 (100.0%)
s151: 18 stmts out of 18 (100.0%)
s151s: 10 stmts out of 10 (100.0%)
s152: 26 stmts out of 26 (100.0%)
s152s: 3 stmts out of 3 (100.0%)
s161: 30 stmts out of 30 (100.0%)
s162: 25 stmts out of 25 (100.0%)
s171: 25 stmts out of 25 (100.0%)
s172: 25 stmts out of 25 (100.0%)
s173: 26 stmts out of 26 (100.0%)
s174: 25 stmts out of 25 (100.0%)
s175: 25 stmts out of 25 (100.0%)
s176: 32 stmts out of 32 (100.0%)
s2101: 25 stmts out of 25 (100.0%)
s2102: 33 stmts out of 33 (100.0%)
s211: 26 stmts out of 26 (100.0%)
s2111: 47 stmts out of 47 (100.0%)
s212: 26 stmts out of 26 (100.0%)
s221: 26 stmts out of 26 (100.0%)
s222: 27 stmts out of 27 (100.0%)
s2233: 40 stmts out of 40 (100.0%)
s2244: 26 stmts out of 26 (100.0%)
s2251: 28 stmts out of 28 (100.0%)
s2275: 33 stmts out of 33 (100.0%)
s231: 31 stmts out of 31 (100.0%)
s232: 31 stmts out of 31 (100.0%)
s233: 40 stmts out of 40 (100.0%)
s235: 33 stmts out of 33 (100.0%)
s241: 26 stmts out of 26 (100.0%)
s242: 25 stmts out of 25 (100.0%)
s243: 27 stmts out of 27 (100.0%)
s244: 27 stmts out of 27 (100.0%)
s251: 26 stmts out of 26 (100.0%)
s252: 28 stmts out of 28 (100.0%)
s253: 28 stmts out of 28 (100.0%)
s254: 27 stmts out of 27 (100.0%)
s255: 29 stmts out of 29 (100.0%)
s256: 32 stmts out of 32 (100.0%)
s257: 32 stmts out of 32 (100.0%)
s258: 29 stmts out of 29 (100.0%)
s261: 28 stmts out of 28 (100.0%)
s271: 26 stmts out of 26 (100.0%)
s2711: 26 stmts out of 26 (100.0%)
s2712: 26 stmts out of 26 (100.0%)
s272: 27 stmts out of 27 (100.0%)
s273: 28 stmts out of 28 (100.0%)
s274: 28 stmts out of 28 (100.0%)
s275: 32 stmts out of 32 (100.0%)
s276: 28 stmts out of 28 (100.0%)
s277: 31 stmts out of 31 (100.0%)
s278: 30 stmts out of 30 (100.0%)
s279: 33 stmts out of 33 (100.0%)
s281: 27 stmts out of 27 (100.0%)
s291: 27 stmts out of 27 (100.0%)
s292: 29 stmts out of 29 (100.0%)
s293: 25 stmts out of 25 (100.0%)
s311: 26 stmts out of 26 (100.0%)
s3110: 39 stmts out of 39 (100.0%)
s3111: 28 stmts out of 28 (100.0%)
s31111: 42 stmts out of 42 (100.0%)
s3112: 28 stmts out of 28 (100.0%)
s3113: 35 stmts out of 35 (100.0%)
s312: 27 stmts out of 27 (100.0%)
s313: 27 stmts out of 27 (100.0%)
s314: 28 stmts out of 28 (100.0%)
s315: 38 stmts out of 38 (100.0%)
s316: 28 stmts out of 28 (100.0%)
s317: 27 stmts out of 27 (100.0%)
s318: 42 stmts out of 42 (100.0%)
s319: 30 stmts out of 30 (100.0%)
s321: 25 stmts out of 25 (100.0%)
s322: 25 stmts out of 25 (100.0%)
s323: 26 stmts out of 26 (100.0%)
s3251: 27 stmts out of 27 (100.0%)
s331: 29 stmts out of 29 (100.0%)
s341: 29 stmts out of 29 (100.0%)
s342: 30 stmts out of 30 (100.0%)
s343: 35 stmts out of 35 (100.0%)
s351: 31 stmts out of 31 (100.0%)
s352: 28 stmts out of 28 (100.0%)
s353: 31 stmts out of 31 (100.0%)
s4112: 25 stmts out of 25 (100.0%)
s4113: 25 stmts out of 25 (100.0%)
s4114: 27 stmts out of 27 (100.0%)
s4115: 27 stmts out of 27 (100.0%)
s4116: 28 stmts out of 28 (100.0%)
s4117: 25 stmts out of 25 (100.0%)
s4121: 27 stmts out of 27 (100.0%)
s421: 36 stmts out of 36 (100.0%)
s422: 36 stmts out of 36 (100.0%)
s423: 37 stmts out of 37 (100.0%)
s424: 37 stmts out of 37 (100.0%)
s431: 28 stmts out of 28 (100.0%)
s441: 29 stmts out of 29 (100.0%)
s442: 37 stmts out of 37 (100.0%)
s443: 31 stmts out of 31 (100.0%)
s451: 28 stmts out of 28 (100.0%)
s452: 25 stmts out of 25 (100.0%)
s453: 27 stmts out of 27 (100.0%)
s471: 38 stmts out of 38 (100.0%)
s471s__fc_inline: 2 stmts out of 2 (100.0%)
s481: 27 stmts out of 27 (100.0%)
s482: 27 stmts out of 27 (100.0%)
s491: 25 stmts out of 25 (100.0%)
set: 37 stmts out of 37 (100.0%)
set1d: 25 stmts out of 25 (100.0%)
set2d: 43 stmts out of 43 (100.0%)
test: 9 stmts out of 9 (100.0%)
va: 25 stmts out of 25 (100.0%)
vag: 25 stmts out of 25 (100.0%)
vas: 25 stmts out of 25 (100.0%)
vbor: 44 stmts out of 44 (100.0%)
vdotr: 27 stmts out of 27 (100.0%)
vif: 26 stmts out of 26 (100.0%)
vpv: 25 stmts out of 25 (100.0%)
vpvpv: 25 stmts out of 25 (100.0%)
vpvts: 25 stmts out of 25 (100.0%)
vpvtv: 25 stmts out of 25 (100.0%)
vsumr: 26 stmts out of 26 (100.0%)
vtv: 25 stmts out of 25 (100.0%)
vtvtv: 25 stmts out of 25 (100.0%)
s332: 31 stmts out of 32 (96.9%)
init: 671 stmts out of 694 (96.7%)
s2710: 31 stmts out of 33 (93.9%)
check: 76 stmts out of 82 (92.7%)
set1ds: 18 stmts out of 25 (72.0%)
This diff is collapsed.
[metrics] Defined functions (167)
=======================
check (151 calls); dummy (151 calls); f__fc_inline (1 call);
init (151 calls); main (0 call); max (0 call); min (0 call); s000 (1 call);
s111 (1 call); s1111 (1 call); s1112 (1 call); s1113 (1 call);
s1115 (1 call); s1119 (1 call); s112 (1 call); s113 (1 call); s114 (1 call);
s115 (1 call); s116 (1 call); s1161 (1 call); s118 (1 call); s119 (1 call);
s121 (1 call); s1213 (1 call); s122 (1 call); s1221 (1 call); s123 (1 call);
s1232 (1 call); s124 (1 call); s1244 (1 call); s125 (1 call);
s1251 (1 call); s126 (1 call); s127 (1 call); s1279 (1 call); s128 (1 call);
s1281 (1 call); s131 (1 call); s13110 (1 call); s132 (1 call);
s1351 (1 call); s141 (1 call); s1421 (1 call); s151 (1 call);
s151s (1 call); s152 (1 call); s152s (1 call); s161 (1 call); s162 (1 call);
s171 (1 call); s172 (1 call); s173 (1 call); s174 (1 call); s175 (1 call);
s176 (1 call); s2101 (1 call); s2102 (1 call); s211 (1 call);
s2111 (1 call); s212 (1 call); s221 (1 call); s222 (1 call); s2233 (1 call);
s2244 (1 call); s2251 (1 call); s2275 (1 call); s231 (1 call);
s232 (1 call); s233 (1 call); s235 (1 call); s241 (1 call); s242 (1 call);
s243 (1 call); s244 (1 call); s251 (1 call); s252 (1 call); s253 (1 call);
s254 (1 call); s255 (1 call); s256 (1 call); s257 (1 call); s258 (1 call);
s261 (1 call); s271 (1 call); s2710 (1 call); s2711 (1 call);
s2712 (1 call); s272 (1 call); s273 (1 call); s274 (1 call); s275 (1 call);
s276 (1 call); s277 (1 call); s278 (1 call); s279 (1 call); s281 (1 call);
s291 (1 call); s292 (1 call); s293 (1 call); s311 (1 call); s3110 (1 call);
s3111 (1 call); s31111 (1 call); s3112 (1 call); s3113 (1 call);
s312 (1 call); s313 (1 call); s314 (1 call); s315 (1 call); s316 (1 call);
s317 (1 call); s318 (1 call); s319 (1 call); s321 (1 call); s322 (1 call);
s323 (1 call); s3251 (1 call); s331 (1 call); s332 (1 call); s341 (1 call);
s342 (1 call); s343 (1 call); s351 (1 call); s352 (1 call); s353 (1 call);
s4112 (1 call); s4113 (1 call); s4114 (1 call); s4115 (1 call);
s4116 (1 call); s4117 (1 call); s4121 (1 call); s421 (1 call);
s422 (1 call); s423 (1 call); s424 (1 call); s431 (1 call); s441 (1 call);
s442 (1 call); s443 (1 call); s451 (1 call); s452 (1 call); s453 (1 call);
s471 (1 call); s471s__fc_inline (1 call); s481 (1 call); s482 (1 call);
s491 (1 call); set (1 call); set1d (341 calls); set1ds (14 calls);
set2d (51 calls); sum1d (0 call); test (8 calls); va (1 call); vag (1 call);
vas (1 call); vbor (1 call); vdotr (1 call); vif (1 call); vpv (1 call);
vpvpv (1 call); vpvts (1 call); vpvtv (1 call); vsumr (1 call);
vtv (1 call); vtvtv (1 call);
Specified-only functions (0)
============================
Undefined and unspecified functions (0)
=======================================
'Extern' global variables (0)
=============================
Potential entry points (4)
==========================
main; max; min; sum1d;
Global metrics
==============
Sloc = 5499
Decision point = 572
Global variables = 21
If = 568
Loop = 359
Goto = 25
Assignment = 2125
Exit point = 167
Function = 167
Function call = 1652
Pointer dereferencing = 52
Cyclomatic complexity = 739
tsvc.c:228:[kernel:parser:decimal-float] warning: Floating-point constant .000001 is not represented exactly. Will use 0x1.0c6f7a0b5ed8dp-20.
(warn-once: no further messages from category 'parser:decimal-float' will be emitted)
#define LEN 30000
#define LEN2 256
int dummy(float a[LEN], float b[LEN], float c[LEN], float d[LEN], float e[LEN], float aa[LEN2][LEN2], float bb[LEN2][LEN2], float cc[LEN2][LEN2], float s){
// -- called in each loop to make all computations appear required
return 0;
}
Copyright (c) 2011 University of Illinois at Urbana-Champaign. All rights reserved.
Developed by: Polaris Research Group
University of Illinois at Urbana-Champaign
http://polaris.cs.uiuc.edu
Permission is hereby granted, free of charge, to any person obtaining a copy
of this software and associated documentation files (the "Software"), to
deal with the Software without restriction, including without limitation the
rights to use, copy, modify, merge, publish, distribute, sublicense, and/or
sell copies of the Software, and to permit persons to whom the Software is
furnished to do so, subject to the following conditions:
1. Redistributions of source code must retain the above copyright notice,
this list of conditions and the following disclaimers.
2. Redistributions in binary form must reproduce the above copyright
notice, this list of conditions and the following disclaimers in the
documentation and/or other materials provided with the distribution.
3. Neither the names of Polaris Research Group, University of Illinois at
Urbana-Champaign, nor the names of its contributors may be used to endorse
or promote products derived from this Software without specific prior
written permission.
THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
CONTRIBUTORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING
FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS
WITH THE SOFTWARE.
CC = gcc
flags = -std=c99 -O3 -fivopts -flax-vector-conversions -funsafe-math-optimizations -msse4.2 -Wall -Werror
vecflags = -ftree-vectorizer-verbose=1
novecflags = -fno-tree-vectorize
libs = -lm
noopt = -O0
all : runvec runnovec
runnovec : tscnovec.o dummy.o
$(CC) $(noopt) dummy.o tscnovec.o -o runnovec $(libs)
runvec : tscvec.o dummy.o
$(CC) $(noopt) dummy.o tscvec.o -o runvec $(libs)
tscvec.o : tsc.c
rm -f report.lst
$(CC) $(flags) $(vecflags) -c -o tscvec.o tsc.c 2> reportgcc.lst
tscnovec.o : tsc.c
$(CC) $(flags) $(novecflags) -c -o tscnovec.o tsc.c
tsc.s : tsc.c dummy.o
$(CC) $(flags) dummy.o tsc.c -S
dummy.o : dummy.c
$(CC) -c dummy.c
clean :
rm -f *.o runnovec runvec *.lst *.s
This diff is collapsed.
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment