Merge branch 'add-c-testsuite' into 'master'

[c-testsuite] add new case study

See merge request !13

Makefile

@@ -53,6 +53,7 @@ TARGETS=\
   2048 \
   basic-cwe-examples \
   bench-moerman2018 \
+  c-testsuite \
   cerberus \
   chrony \
   debie1 \

README.md

@@ -127,6 +127,8 @@ when available. We also summarize the license of each directory below.
 - `2048`: MIT
 - `basic-cwe-examples`: see `LICENSE`
 - `bench-moerman2018`: MIT
+- `c-testsuite`: see `LICENSE` and `LICENSE-tests`
+- `cerberus`: see `LICENSE`
 - `chrony`: GPL
 - `debie1`: distribution and use authorized by Patria Aviation Oy,
             Space Systems Finland Ltd. and Tidorum Ltd, see `README.txt`

c-testsuite/.frama-c/00001.eva/alarms.csv

+directory	file	line	function	property kind	status	property

c-testsuite/.frama-c/00001.eva/metrics.log

+[metrics] Eva coverage statistics
+=======================
+Syntactically reachable functions = 1 (out of 1)
+Semantically reached functions = 1
+Coverage estimation = 100.0%
+[metrics] Statements analyzed by Eva
+--------------------------
+2 stmts in analyzed functions, 2 stmts analyzed (100.0%)
+main: 2 stmts out of 2 (100.0%)

c-testsuite/.frama-c/00001.parse/framac.ast

+/* Generated by Frama-C */
+int main(void)
+{
+  int __retres;
+  __retres = 0;
+  return __retres;
+}
+
+

c-testsuite/.frama-c/00001.parse/metrics.log

+[metrics] Defined functions (1)
+=====================
+ main (0 call); 
+
+Specified-only functions (0)
+============================
+ 
+
+Undefined and unspecified functions (0)
+=======================================
+ 
+
+'Extern' global variables (0)
+=============================
+ 
+
+Potential entry points (1)
+==========================
+ main; 
+
+Global metrics
+============== 
+Sloc = 2
+Decision point = 0
+Global variables = 0
+If = 0
+Loop = 0
+Goto = 0
+Assignment = 1
+Exit point = 1
+Function = 1
+Function call = 0
+Pointer dereferencing = 0
+Cyclomatic complexity = 1

c-testsuite/.frama-c/00002.eva/alarms.csv

+directory	file	line	function	property kind	status	property

c-testsuite/.frama-c/00002.eva/metrics.log

+[metrics] Eva coverage statistics
+=======================
+Syntactically reachable functions = 1 (out of 1)
+Semantically reached functions = 1
+Coverage estimation = 100.0%
+[metrics] Statements analyzed by Eva
+--------------------------
+2 stmts in analyzed functions, 2 stmts analyzed (100.0%)
+main: 2 stmts out of 2 (100.0%)

c-testsuite/.frama-c/00002.parse/framac.ast

+/* Generated by Frama-C */
+int main(void)
+{
+  int __retres;
+  __retres = 3 - 3;
+  return __retres;
+}
+
+

c-testsuite/.frama-c/00002.parse/metrics.log

+[metrics] Defined functions (1)
+=====================
+ main (0 call); 
+
+Specified-only functions (0)
+============================
+ 
+
+Undefined and unspecified functions (0)
+=======================================
+ 
+
+'Extern' global variables (0)
+=============================
+ 
+
+Potential entry points (1)
+==========================
+ main; 
+
+Global metrics
+============== 
+Sloc = 2
+Decision point = 0
+Global variables = 0
+If = 0
+Loop = 0
+Goto = 0
+Assignment = 1
+Exit point = 1
+Function = 1
+Function call = 0
+Pointer dereferencing = 0
+Cyclomatic complexity = 1

c-testsuite/.frama-c/00003.eva/alarms.csv

+directory	file	line	function	property kind	status	property

c-testsuite/.frama-c/00003.eva/metrics.log

+[metrics] Eva coverage statistics
+=======================
+Syntactically reachable functions = 1 (out of 1)
+Semantically reached functions = 1
+Coverage estimation = 100.0%
+[metrics] Statements analyzed by Eva
+--------------------------
+3 stmts in analyzed functions, 3 stmts analyzed (100.0%)
+main: 3 stmts out of 3 (100.0%)