2048/OSCS-README.txt

+Console version of the game 2048
+https://github.com/mevdschee/2048.c
+NO_DYN_ALLOC, NO_RECURSION, NO_FLOAT

2048/frama-c-path.mk

-../frama-c-path.mk
\ No newline at end of file

Makefile

 .ONESHELL:
+ROOT_DIR := $(dir $(realpath $(lastword $(MAKEFILE_LIST))))
 
 help::
 	@echo "*** PREPARATION TARGETS (first-time user)"
@@ -15,7 +16,15 @@ help::
 	@echo "- 'make clean': clean all analyses"
 	@echo ""
 	@echo "*** USAGE WITH FRAMA-C INSTALLED IN THE PATH"
-	@echo "- delete 'frama-c-path.mk' or comment its lines"
+	@echo "- delete 'path.mk' or comment its lines"
+	@echo ""
+	@echo "*** NON-FRAMA-C BUILD TARGETS"
+	@echo "- 'make build': build each case study, using its own Makefile,"
+	@echo "  CMake, Meson, etc. You can set BUILD_WRAPPER to a command"
+	@echo "  which will wrap the calls to the build tool."
+	@echo "  Note: this is highly system-dependent and requires several"
+	@echo "  libraries and tools. This target is only provided for "
+	@echo "  convenience, and cannot be relied upon for CI runs."
 
 # Note: if the user runs `make framac` before `make submodules`, the latter
 # will fail.
@@ -33,46 +42,55 @@ framac: frama-c/build/bin/frama-c
 # a submodule, it does not have a `.git` directory.
 # also, such dependency would prevent usage with FRAMAC=path/to/other/framac
 frama-c/build/bin/frama-c:
-	@echo "Compiling and installing local Frama-C..."
+	@echo "Compiling and (re)installing local Frama-C..."
 	mkdir -p frama-c/build
-	{
-	  cd frama-c
-	  echo "*** running autoconf..."
-	  autoconf -f >/dev/null 2>/dev/null
-	  echo "*** running configure..."
-	  ./configure --prefix=`pwd`/build --quiet >/dev/null
-	  $(MAKE) clean >/dev/null
-	  echo "*** running make..."
-	  $(MAKE) -j --quiet >/dev/null
-	  echo "*** running make install..."
-	  $(MAKE) install >/dev/null
-	};
+	echo "*** cleaning previous builds..."
+	$(MAKE) -C frama-c clean >/dev/null
+	echo "*** running make..."
+	$(MAKE) -C frama-c -j --quiet >/dev/null
+	echo "*** running make install..."
+	$(MAKE) -C frama-c install PREFIX=$(ROOT_DIR)/frama-c/build >/dev/null
 	echo "Local Frama-C (re-)installed."
 
 TARGETS=\
   2048 \
   basic-cwe-examples \
+  bench-moerman2018 \
+  c-testsuite \
+  c-utils \
   cerberus \
   chrony \
   debie1 \
+  genann \
+  gnugo \
   gzip124 \
   hiredis \
   icpc \
+  ioccc \
   itc-benchmarks \
   jsmn \
+  kgflags \
   khash \
   kilo \
   libmodbus \
   libspng \
+  libyaml \
+  line-following-robot \
   microstrain \
   mini-gmp \
+  miniz \
   monocypher \
   papabench \
   polarssl \
+  powerwindow \
   qlz \
+  safestringlib \
   semver \
   solitaire \
+  stmr \
+  tsvc \
   tweetnacl-usable \
+  verisec \
   x509-parser \
 
 help::
@@ -80,42 +98,71 @@ help::
 	@echo "Known targets:"
 	@echo "$(sort $(TARGETS))"
 
-# A target for "fast" analyses, used to speed up testing
-QUICK_TARGETS=$(filter-out polarssl gzip124 libmodbus monocypher chrony,$(TARGETS))
+# Targets sorted by "longest-running first"
+SLOW_TARGETS=monocypher chrony debie1 polarssl libmodbus
+
+QUICK_TARGETS=$(filter-out $(SLOW_TARGETS),$(TARGETS))
 
-all: $(TARGETS)
+# Start long-running targets first, to minimize overall wall-clock time
+# Note: we rely on the fact that GNU make tends to start running targets
+# in left-to-right order
+all: $(SLOW_TARGETS) $(QUICK_TARGETS)
+
+summary:
+	frama-c/share/analysis-scripts/summary.py
 
 $(TARGETS):
-	+$(MAKE) -C $@
+	+$(MAKE) -C $@/.frama-c
 
 quick: $(QUICK_TARGETS)
 
 %.clean:
-	$(MAKE) -C $* clean
+	$(MAKE) -C $*/.frama-c clean
 
 clean: $(addsuffix .clean,$(TARGETS))
 
 %.parse:
-	$(MAKE) -C $* parse
+	$(MAKE) -C $*/.frama-c parse
 
 parse: $(addsuffix .parse,$(TARGETS))
 
-%.stats:
-	$(MAKE) -C $* stats
+%.sarif:
+	$(MAKE) -C $*/.frama-c sarif
 
-stats: $(addsuffix .stats,$(TARGETS))
+sarif: $(addsuffix .sarif,$(TARGETS))
 
 display-targets:
 	@echo $(foreach target,$(TARGETS),\
 	        $(addprefix $(target)/,\
-	          $(shell $(MAKE) --quiet -C $(target) display-targets)))
+	          $(shell $(MAKE) --quiet -C $(target)/.frama-c display-targets)))
+
+%.eva: .FORCE
+	$(MAKE) -C $(dir $@) $(notdir $@)
+
+# For most case studies, 'make' is sufficient, but some of them require other
+# commands (which are overridden below).
+%.build:
+	$(BUILD_WRAPPER) $(MAKE) -C $*
+
+%.build.clean:
+	$(MAKE) -C $* clean
+
+build: $(addsuffix .build,$(TARGETS))
+
+build-clean: $(addsuffix .build.clean,$(TARGETS))
+
+cerberus.build:
+	@echo "Some Cerberus tests are not compilable (by design)"
+
+cerberus.build.clean:
+	@echo "Cerberus: nothing to clean"
+
+icpc.build:
+	$(BUILD_WRAPPER) $(MAKE) -C icpc/src
 
-.PHONY: $(TARGETS) frama-c/build/bin/frama-c clean-all help stats-all
+icpc.build.clean:
+	$(MAKE) -C icpc/src clean
 
-# for continuous integration: runs all tests, then uses git status and
-# git diff to check for unexpected differences
-ci-tests: all stats-all
-	git status --porcelain
-	git diff --exit-code
+.FORCE:
 
-ci-tests: export FCFLAGS=-value-verbose 0 -kernel-verbose 0
+.PHONY: $(TARGETS) frama-c/build/bin/frama-c help

Makefile.common

 # Makefile optionally included by each GNUmakefile in the target directories.
 # Note: it must be included at the end of the makefiles,
 # to ensure e.g. TARGETS and other variables are properly defined.
+
+### Extra targets for SARIF report
+# '-noautoload-plugins -load-module eva,markdown-report' minimize loading time
+# of several dozens of calls to Frama-C
+%.sarif: %.eva
+	$(FRAMAC) -no-autoload-plugins -load-module eva,markdown-report -load $^/framac.sav -mdr-gen sarif -mdr-no-print-libc -mdr-sarif-deterministic -mdr-out $@
+
+sarif: $(TARGETS:%.eva=%.sarif)

Makefile.single-target

+# This is a generic Makefile for directories containing a single target that
+# have do not already have a Makefile themselves.
+
+# This Makefile is NOT for running Frama-C, but for compiling the case study
+# itself.
+
+# Usage: `cd` to directory and `ln -s ../Makefile.single-target Makefile`
+
+TARGET = $(shell basename `pwd`)
+
+SOURCES := $(sort $(wildcard *.c))
+
+all: $(TARGET)
+
+# Some directories complement this Makefile with their own
+-include Makefile.own
+
+$(TARGET): $(SOURCES)
+	$(CC) $(CPPFLAGS) $(CFLAGS) -o $@ $^ $(LDFLAGS)
+
+clean:
+	rm -f $(TARGET)
+
+.PHONY: clean

README.md

+![Pipeline status badge](https://git.frama-c.com/pub/open-source-case-studies/badges/master/pipeline.svg)
+
 Open source case studies for Frama-C
 ====================================
 
@@ -12,7 +14,7 @@ A few contain sets of tests, benchmarks or tutorials.
 # Requirements
 
 - GNU Make >= 4.0;
-- (optional, for some scripts) Python >= 3.6.
+- (optional, for some scripts) Python >= 3.7.
 
 # Basic usage
 
@@ -20,17 +22,24 @@ A few contain sets of tests, benchmarks or tutorials.
 - (required once) `make framac`: prepares a git submodule with a clone
   of the public git of Frama-C, compiles it and installs it locally
   (in `frama-c/build/bin`);
-- `cd` to one of the case studies;
+- (required once) add the following alias to your shell:
+
+        alias fcmake='make -C .frama-c'
+
+  Each "case study" contains a `.frama-c` subdirectory with the Frama-C
+  Makefile. Running `fcmake` will run Frama-C related targets;
+  running `make` will run the case study's original Makefile (if it exists).
+- `cd` to the subdirectory of one of the case studies;
   We recommend `2048` for a short and fast analysis, or `debie1` for
   a finalized analysis.
-- Run `make` to parse and run Eva on the predefined targets.
+- Run `fcmake` to parse and run Eva on the predefined targets.
 
 ## Makefile targets
 
 The scripts provided with Frama-C create several Makefile targets,
 according to the intended usage. The main ones are:
 
-- `help`: lists the base targets
+- `display-targets`: lists the base targets
 - For each base target `t`, the following targets are generated:
   - `t.parse`: parse the sources;
   - `t.eva`: run Eva;
@@ -49,37 +58,40 @@ Other generated targets:
 
 - The output of `t.eva` is verbose, but you can ignore it;
   the important information (warnings and alarms) can be inspected via the GUI.
-- The result of each analysis is stored in a directory containing the full logs
-  and Frama-C save files; successive runs are copied into timestamped
-  directories, to allow comparing them (e.g. via `meld`);
+- The result of the analysis is stored inside `.frama-c`, in subdirectories
+  `t.parse` for parsing and `t.eva` for the Eva analysis.
+  Each subdirectory contains a few log files.
 - To try other parametrizations, simply edit variables
-  `CPPFLAGS/FCFLAGS/EVAFLAGS` in `GNUmakefile` and re-run `make`.
-- Technical remark: the default file used by GNU Make is `GNUmakefile`,
-  if it exists.
-  We use this to avoid renaming the original Makefile, if any. It also means
-  that, if you want to *compile* the code using its Makefile, you have to
-  explicitly name it (e.g. `make -f Makefile`).
-
+  `CPPFLAGS/FCFLAGS/EVAFLAGS` in `.frama-c/GNUmakefile` and re-run `fcmake`.
 
 # Notes
 
+A summary of the case studies, with a brief description, URL, number of Eva
+targets, etc, is available at [summary.md](summary.md).
+
 ## Source code modifications
 
-Only minor modifications were performed on each of these case studies:
-
-- File `GNUmakefile` is added to each case study, with Frama-C/Eva-specific
-  rules for parsing and running the analysis;
-- When necessary, syntactic modifications were performed to ensure better
-  C99-compliance and/or the inclusion of stubs to allow Frama-C to parse the
-  files;
-- In some cases, an `eva_main` function was added to provide a better initial
-  context for the analysis;
-- When recursive calls are present, the functions containing them need to be
-  replaced with specifications;
-- Some ACSL annotations were added to the sources
-  (to illustrate their usage, or to improve the analysis);
+We attempt to minimize changes to each case study, to keep the code close to
+the original. Here are the most common kinds of changes:
+
+- A `.frama-c` directory is added, with a `GNUmakefile` which defines the
+  Frama-C targets and parameters;
+- Some stubs file (e.g. `stubs.c`) are added to the `.frama-c` directory,
+  either to emulate an initial state with command-line arguments, or to provide
+  code/specifications for library functions, missing code, non-portable
+  features, etc.
+- When code modifications are needed (and cannot be moved to the stubs file,
+  e.g. when adding a specification to a `static` functions), we often
+  protect them by `#ifdef __FRAMAC__` guards, to ensure the code compiles
+  as before when not using Frama-C. Note that this is not always the case.
 - Some unnecessary files for the analysis (e.g. documentation, project setups
-  for IDEs, non-code resources) were removed.
+  for IDEs, non-code resources) are removed.
+- Some Makefiles were renamed `Makefile.original`, and a simplified
+  OSCS-related `Makefile` has been added. This enables compiling some targets
+  in a way that is useful for certain build tools.
+
+In case studies related to benchmarking, examples or test suites, we often
+apply modifications more liberally.
 
 ## Rationale
 
@@ -98,7 +110,7 @@ Only a few constitute "finalized" case studies.
 
 If you know of other open source code bases where Frama-C/Eva produces
 interesting results, please contribute with pull requests including the
-sources and the `GNUmakefile` that you have devised to run Frama-C.
+case study sources and your `.frama-c/GNUmakefile`.
 
 On the other hand, if you have some interesting open-source C software
 (ideally, C99-compatible) that you are unable to parse and/or run with
@@ -120,28 +132,75 @@ 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`
+- `c-utils` : MIT
+- `cerberus`: see `LICENSE`
 - `chrony`: GPL
 - `debie1`: distribution and use authorized by Patria Aviation Oy,
             Space Systems Finland Ltd. and Tidorum Ltd, see `README.txt`
             and `terms_of_use-2014-05.pdf`
+- `genann`: Zlib, see `LICENSE`
+- `gnugo`: GPL
 - `gzip124`: GPL
 - `hiredis`: Redis license (BSD-style), see `COPYING`
 - `icpc`: Unlicense
+- `ioccc`: Creative Commons Attribution-ShareAlike 3.0 Unported (CC BY-SA 3.0),
+           see `COPYING`
 - `itc-benchmarks`: BSD 2-clause, see `COPYING`
 - `jsmn`: MIT
+- `kgflags`: MIT, see `LICENSE`
 - `khash`: MIT
-- `kilo`: BSD 2-clause "Simplified"
-          (see https://github.com/antirez/kilo/blob/master/LICENSE)
+- `kilo`: BSD 2-clause "Simplified", see `LICENSE`
 - `libmodbus`: LGPL
 - `libspng`: BSD 2-clause, see `LICENSE`
-- `mibench`: several (see `LICENSE` file inside each subdirectory)
+- `libyaml`: MIT, see `License`
+- `line-following-robot`: MIT + modified BSD (for included `avr-libc`),
+                          see `LICENSE` and `avr-libc/include/LICENSE`
+- `mibench`: several, see `LICENSE` file inside each subdirectory
 - `mini-gmp`:  LGPL or GPL
+- `miniz`:  MIT
 - `microstrain`: GPL and others, see `LICENSE`
 - `monocypher`: see `README`
 - `papabench`: GPL
 - `polarssl`: GPL
+- `powerwindow`: GPL
 - `qlz`: GPL
+- `safestringlib`: MIT
 - `semver`: MIT
-- `solitaire`: public domain (see `solitaire.c`)
-- `tweetnacl-usable`: public domain (see `LICENSE.txt`)
-- `x509-parser` : GPLv2 / BSD (see `LICENSE`)
+- `solitaire`: public domain, see `solitaire.c`
+- `stmr`: MIT
+- `tsvc`: MIT, see `license.txt`
+- `tweetnacl-usable`: public domain, see `LICENSE.txt`
+- `verisec`: several, according to each app
+- `x509-parser` : GPLv2 / BSD, see `LICENSE`
+
+
+# Troubleshooting / Debugging
+
+(This section is mainly for Frama-C/plug-in developers who want to test OSCS
+with specific versions of Frama-C)
+
+OSCS can work in different modes:
+
+1. With a local Frama-C, installed via the Git submodule 'frama-c'
+   (after running `make framac`);
+2. With another, locally-installed Frama-C;
+3. With Frama-C installed in the PATH.
+
+This behavior is defined in `path.mk`. This file is included (as a symbolic
+link) in the `.frama-c` directory for each case study. Changing this file will
+change the behavior of all case studies.
+
+- Mode 1 (by default) is enabled as soon as `make framac` is executed.
+- To enable mode 2, modify the `FRAMAC_DIR=` line in `path.mk` to point to the
+  `bin` directory of your locally installed Frama-C.
+- To enable mode 3, simply comment the `FRAMAC_DIR=` line.
+
+If the value of `FRAMAC_DIR` is invalid (does not point to an existing
+directory), an error will be raised.
+
+If you need help debugging, consider adding messages such as
+`$(info FRAMAC_DIR is: $(FRAMAC_DIR))` to `path.mk`.
+When running one of the `make` targets, these messages might help understand
+if the path has been properly set.

basic-cwe-examples/.frama-c/GNUmakefile

+# 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-lib-path)/analysis-scripts/prologue.mk
+###############################################################################
+
+# Edit below as needed. Suggested flags are optional.
+
+MACHDEP = x86_64
+
+## 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 \
+
+## Eva-specific flags
+EVAFLAGS    += \
+  -eva-warn-key builtins:missing-spec=abort \
+
+## Analysis targets (suffixed with .eva)
+IMPRECISE_TARGETS = cwe20.eva cwe20-2.eva cwe119.eva cwe190.eva cwe416.eva cwe588.eva cwe761.eva cwe787.eva
+
+PRECISE_TARGETS = $(subst .eva,-precise.eva,$(IMPRECISE_TARGETS))
+
+OTHER_TARGETS = cwe190-unsigned.eva
+
+TARGETS = $(IMPRECISE_TARGETS) $(PRECISE_TARGETS) $(OTHER_TARGETS)
+
+### Each target <t>.eva needs a rule <t>.parse with source files as prerequisites
+cwe20.parse:  ../cwe20.c
+cwe20-2.parse:  ../cwe20-2.c
+cwe119.parse: ../cwe119.c
+cwe190.parse: ../cwe190.c
+cwe416.parse: ../cwe416.c
+cwe588.parse: ../cwe588.c
+cwe761.parse: ../cwe761.c
+cwe787.parse: ../cwe787.c
+
+cwe20-precise.parse:  ../cwe20.c
+cwe20-2-precise.parse:  ../cwe20-2.c
+cwe119-precise.parse: ../cwe119.c
+cwe190-precise.parse: ../cwe190.c
+cwe416-precise.parse: ../cwe416.c
+cwe588-precise.parse: ../cwe588.c
+cwe761-precise.parse: ../cwe761.c
+cwe787-precise.parse: ../cwe787.c
+
+cwe761-precise.parse: CPPFLAGS+=-DFC_EVA_PRECISE
+
+cwe190-unsigned.parse: ../cwe190-unsigned.c
+
+cwe20-precise.eva:   EVAFLAGS +=
+cwe20-2-precise.eva: EVAFLAGS += -eva-precision 5
+cwe119-precise.eva:  EVAFLAGS +=
+cwe190-precise.eva:  EVAFLAGS +=
+cwe416-precise.eva:  EVAFLAGS +=
+cwe588-precise.eva:  EVAFLAGS +=
+cwe761-precise.eva:  EVAFLAGS += -eva-precision 1
+cwe787-precise.eva:  EVAFLAGS += -eva-precision 2
+cwe190-unsigned.eva:  EVAFLAGS += -warn-unsigned-overflow
+
+### Epilogue. Do not modify this block. #######################################
+include $(shell $(FRAMAC)-config -print-lib-path)/analysis-scripts/epilogue.mk
+###############################################################################
+
+# optional, for OSCS
+-include ../../Makefile.common

basic-cwe-examples/.frama-c/cwe119-precise.eva/alarms.csv

+directory	file	line	function	property kind	status	property
+.	cwe119.c	28	my_strcmp	mem_access	Unknown	\valid_read(s1 + i)
+.	cwe119.c	28	my_strcmp	mem_access	Unknown	\valid_read(s2 + i)
+.	cwe119.c	65	host_lookup	precondition of strcpy	Invalid or unreachable	room_string: \valid(dest + (0 .. strlen(src)))
+FRAMAC_SHARE/libc	string.h	430	strcpy	precondition	Invalid or unreachable	room_string: \valid(dest + (0 .. strlen(src)))

basic-cwe-examples/.frama-c/cwe119-precise.eva/metrics.log

+[metrics] Eva coverage statistics
+=======================
+Syntactically reachable functions = 7 (out of 7)
+Semantically reached functions = 7
+Coverage estimation = 100.0%
+[metrics] Statements analyzed by Eva
+--------------------------
+54 stmts in analyzed functions, 48 stmts analyzed (88.9%)
+my_inet_addr: 10 stmts out of 10 (100.0%)
+my_strcmp: 12 stmts out of 12 (100.0%)
+nonzero_uint32_t: 9 stmts out of 9 (100.0%)
+validate_addr_form: 7 stmts out of 7 (100.0%)
+host_lookup: 4 stmts out of 5 (80.0%)
+my_gethostbyaddr: 4 stmts out of 5 (80.0%)
+main: 2 stmts out of 6 (33.3%)

basic-cwe-examples/.frama-c/cwe119-precise.eva/nonterm.log

+cwe119.c:65:[nonterm:stmt] warning: non-terminating function call
+stack: host_lookup :: cwe119.c:70 <- main
+cwe119.c:73:[nonterm:unreachable] warning: unreachable return

basic-cwe-examples/.frama-c/cwe119-precise.parse/framac.ast

+/* Generated by Frama-C */
+#include "errno.h"
+#include "inttypes.h"
+#include "netdb.h"
+#include "netinet/in.h"
+#include "signal.h"
+#include "stdarg.h"
+#include "stddef.h"
+#include "stdint.h"
+#include "stdio.h"
+#include "stdlib.h"
+#include "string.h"
+#include "strings.h"
+#include "sys/socket.h"
+#include "sys/uio.h"
+uint32_t volatile _rand;
+uint32_t nonzero_uint32_t(void)
+{
+  uint32_t __retres;
+  uint32_t r = _rand;
+  if (! r) {
+    __retres = 1U;
+    goto return_label;
+  }
+  else {
+    __retres = r;
+    goto return_label;
+  }
+  return_label: return __retres;
+}
+
+/*@ requires valid_read_string(format);
+    assigns \result, stream->__fc_FILE_data;
+    assigns \result
+      \from (indirect: stream->__fc_FILE_id),
+            (indirect: stream->__fc_FILE_data),
+            (indirect: *(format + (0 ..)));
+    assigns stream->__fc_FILE_data
+      \from (indirect: stream->__fc_FILE_id), stream->__fc_FILE_data,
+            (indirect: *(format + (0 ..)));
+ */
+int fprintf_va_1(FILE * restrict stream, char const * restrict format);
+
+static void validate_addr_form(char *v)
+{
+  size_t tmp;
+  size_t tmp_0;
+  tmp = strspn((char const *)v,
+               "ABCDEFGHIJKLMNOPQRSTUVWXYZabcdefghijklmnopqrstuvwxyz-0123456789.");
+  tmp_0 = strlen((char const *)v);
+  if (tmp < tmp_0) {
+    fprintf(__fc_stderr,"hostname contains invalid characters"); /* fprintf_va_1 */
+    exit(1);
+  }
+  return;
+}
+
+static int my_strcmp(char const *s1, char const *s2)
+{
+  int __retres;
+  size_t i;
+  i = (size_t)0;
+  while ((int)*(s1 + i) == (int)*(s2 + i)) {
+    if ((int)*(s1 + i) == 0) {
+      __retres = 0;
+      goto return_label;
+    }
+    i ++;
+  }
+  __retres = (int)*((unsigned char *)s1 + i) - (int)*((unsigned char *)s2 + i);
+  return_label: return __retres;
+}
+
+static in_addr_t my_inet_addr(char const *cp)
+{
+  in_addr_t __retres;
+  int tmp_0;
+  tmp_0 = my_strcmp(cp,"127.0.0.1");
+  if (tmp_0 == 0) {
+    __retres = (in_addr_t)0;
+    goto return_label;
+  }
+  else {
+    in_addr_t tmp;
+    tmp = nonzero_uint32_t();
+    __retres = tmp;
+    goto return_label;
+  }
+  return_label: return __retres;
+}
+
+static struct hostent my_gethostbyaddr_res;
+static struct hostent *my_gethostbyaddr(void const *addr, socklen_t len,
+                                        int type)
+{
+  struct hostent *__retres;
+  if ((in_addr_t *)addr == (in_addr_t *)0) my_gethostbyaddr_res.h_name = (char *)"www.example.com";
+  else my_gethostbyaddr_res.h_name = (char *)"hypermegagigaterasupercalifragilisticexpialidocious2.example.com";
+  __retres = & my_gethostbyaddr_res;
+  return __retres;
+}
+
+void host_lookup(char *user_supplied_addr)
+{
+  struct hostent *hp;
+  in_addr_t addr;
+  char hostname[64];
+  validate_addr_form(user_supplied_addr);
+  addr = my_inet_addr((char const *)user_supplied_addr);
+  hp = my_gethostbyaddr((void const *)(& addr),
+                        (socklen_t)sizeof(struct in_addr),2);
+  strcpy(hostname,(char const *)hp->h_name);
+  return;
+}
+
+int main(void)
+{
+  int __retres;
+  char *very_large_but_valid_hostname = (char *)"127.0.0.1";
+  host_lookup(very_large_but_valid_hostname);
+  char *overly_large_hostname = (char *)"127.0.0.2";
+  host_lookup(overly_large_hostname);
+  __retres = 0;
+  return __retres;
+}
+
+

basic-cwe-examples/.frama-c/cwe119-precise.parse/metrics.log

+[metrics] Defined functions (7)
+=====================
+ host_lookup (2 calls); main (0 call); my_gethostbyaddr (1 call);
+ my_inet_addr (1 call); my_strcmp (1 call); nonzero_uint32_t (1 call);
+ validate_addr_form (1 call); 
+
+Specified-only functions (0)
+============================
+ 
+
+Undefined and unspecified functions (0)
+=======================================
+ 
+
+'Extern' global variables (0)
+=============================
+ 
+
+Potential entry points (1)
+==========================
+ main; 
+
+Global metrics
+============== 
+Sloc = 54
+Decision point = 6
+Global variables = 2
+If = 6
+Loop = 1
+Goto = 5
+Assignment = 21
+Exit point = 7
+Function = 7
+Function call = 12
+Pointer dereferencing = 6
+Cyclomatic complexity = 13

basic-cwe-examples/.frama-c/cwe119.eva/alarms.csv

+directory	file	line	function	property kind	status	property
+.	cwe119.c	28	my_strcmp	mem_access	Unknown	\valid_read(s1 + i)
+.	cwe119.c	28	my_strcmp	mem_access	Unknown	\valid_read(s2 + i)
+.	cwe119.c	65	host_lookup	precondition of strcpy	Invalid or unreachable	room_string: \valid(dest + (0 .. strlen(src)))
+FRAMAC_SHARE/libc	string.h	430	strcpy	precondition	Invalid or unreachable	room_string: \valid(dest + (0 .. strlen(src)))

basic-cwe-examples/.frama-c/cwe119.eva/metrics.log

+[metrics] Eva coverage statistics
+=======================
+Syntactically reachable functions = 7 (out of 7)
+Semantically reached functions = 7
+Coverage estimation = 100.0%
+[metrics] Statements analyzed by Eva
+--------------------------
+54 stmts in analyzed functions, 48 stmts analyzed (88.9%)
+my_inet_addr: 10 stmts out of 10 (100.0%)
+my_strcmp: 12 stmts out of 12 (100.0%)
+nonzero_uint32_t: 9 stmts out of 9 (100.0%)
+validate_addr_form: 7 stmts out of 7 (100.0%)
+host_lookup: 4 stmts out of 5 (80.0%)
+my_gethostbyaddr: 4 stmts out of 5 (80.0%)
+main: 2 stmts out of 6 (33.3%)

basic-cwe-examples/.frama-c/cwe119.eva/nonterm.log

+cwe119.c:65:[nonterm:stmt] warning: non-terminating function call
+stack: host_lookup :: cwe119.c:70 <- main
+cwe119.c:73:[nonterm:unreachable] warning: unreachable return

basic-cwe-examples/.frama-c/cwe119.parse/framac.ast

+/* Generated by Frama-C */
+#include "errno.h"
+#include "inttypes.h"
+#include "netdb.h"
+#include "netinet/in.h"
+#include "signal.h"
+#include "stdarg.h"
+#include "stddef.h"
+#include "stdint.h"
+#include "stdio.h"
+#include "stdlib.h"
+#include "string.h"
+#include "strings.h"
+#include "sys/socket.h"
+#include "sys/uio.h"
+uint32_t volatile _rand;
+uint32_t nonzero_uint32_t(void)
+{
+  uint32_t __retres;
+  uint32_t r = _rand;
+  if (! r) {
+    __retres = 1U;
+    goto return_label;
+  }
+  else {
+    __retres = r;
+    goto return_label;
+  }
+  return_label: return __retres;
+}
+
+/*@ requires valid_read_string(format);
+    assigns \result, stream->__fc_FILE_data;
+    assigns \result
+      \from (indirect: stream->__fc_FILE_id),
+            (indirect: stream->__fc_FILE_data),
+            (indirect: *(format + (0 ..)));
+    assigns stream->__fc_FILE_data
+      \from (indirect: stream->__fc_FILE_id), stream->__fc_FILE_data,
+            (indirect: *(format + (0 ..)));
+ */
+int fprintf_va_1(FILE * restrict stream, char const * restrict format);
+
+static void validate_addr_form(char *v)
+{
+  size_t tmp;
+  size_t tmp_0;
+  tmp = strspn((char const *)v,
+               "ABCDEFGHIJKLMNOPQRSTUVWXYZabcdefghijklmnopqrstuvwxyz-0123456789.");
+  tmp_0 = strlen((char const *)v);
+  if (tmp < tmp_0) {
+    fprintf(__fc_stderr,"hostname contains invalid characters"); /* fprintf_va_1 */
+    exit(1);
+  }
+  return;
+}
+
+static int my_strcmp(char const *s1, char const *s2)
+{
+  int __retres;
+  size_t i;
+  i = (size_t)0;
+  while ((int)*(s1 + i) == (int)*(s2 + i)) {
+    if ((int)*(s1 + i) == 0) {
+      __retres = 0;
+      goto return_label;
+    }
+    i ++;
+  }
+  __retres = (int)*((unsigned char *)s1 + i) - (int)*((unsigned char *)s2 + i);
+  return_label: return __retres;
+}
+
+static in_addr_t my_inet_addr(char const *cp)
+{
+  in_addr_t __retres;
+  int tmp_0;
+  tmp_0 = my_strcmp(cp,"127.0.0.1");
+  if (tmp_0 == 0) {
+    __retres = (in_addr_t)0;
+    goto return_label;
+  }
+  else {
+    in_addr_t tmp;
+    tmp = nonzero_uint32_t();
+    __retres = tmp;
+    goto return_label;
+  }
+  return_label: return __retres;
+}
+
+static struct hostent my_gethostbyaddr_res;
+static struct hostent *my_gethostbyaddr(void const *addr, socklen_t len,
+                                        int type)
+{
+  struct hostent *__retres;
+  if ((in_addr_t *)addr == (in_addr_t *)0) my_gethostbyaddr_res.h_name = (char *)"www.example.com";
+  else my_gethostbyaddr_res.h_name = (char *)"hypermegagigaterasupercalifragilisticexpialidocious2.example.com";
+  __retres = & my_gethostbyaddr_res;
+  return __retres;
+}
+
+void host_lookup(char *user_supplied_addr)
+{
+  struct hostent *hp;
+  in_addr_t addr;
+  char hostname[64];
+  validate_addr_form(user_supplied_addr);
+  addr = my_inet_addr((char const *)user_supplied_addr);
+  hp = my_gethostbyaddr((void const *)(& addr),
+                        (socklen_t)sizeof(struct in_addr),2);
+  strcpy(hostname,(char const *)hp->h_name);
+  return;
+}
+
+int main(void)
+{
+  int __retres;
+  char *very_large_but_valid_hostname = (char *)"127.0.0.1";
+  host_lookup(very_large_but_valid_hostname);
+  char *overly_large_hostname = (char *)"127.0.0.2";
+  host_lookup(overly_large_hostname);
+  __retres = 0;
+  return __retres;
+}
+
+

basic-cwe-examples/.frama-c/cwe119.parse/metrics.log

+[metrics] Defined functions (7)
+=====================
+ host_lookup (2 calls); main (0 call); my_gethostbyaddr (1 call);
+ my_inet_addr (1 call); my_strcmp (1 call); nonzero_uint32_t (1 call);
+ validate_addr_form (1 call); 
+
+Specified-only functions (0)
+============================
+ 
+
+Undefined and unspecified functions (0)
+=======================================
+ 
+
+'Extern' global variables (0)
+=============================
+ 
+
+Potential entry points (1)
+==========================
+ main; 
+
+Global metrics
+============== 
+Sloc = 54
+Decision point = 6
+Global variables = 2
+If = 6
+Loop = 1
+Goto = 5
+Assignment = 21
+Exit point = 7
+Function = 7
+Function call = 12
+Pointer dereferencing = 6
+Cyclomatic complexity = 13