[修改] 增加freeRTOS

1. 版本FreeRTOSv202212.01，命名为kernel；

kernel/FreeRTOS-Plus/Source/AWS/device-shadow/test/cbmc/.gitignore

@@ -0,0 +1,24 @@
+# Emitted when running CBMC proofs
+proofs/**/logs
+proofs/**/gotos
+proofs/**/report
+proofs/**/html
+proofs/output
+
+# Emitted by CBMC Viewer
+TAGS-*
+
+# Emitted by Arpa
+arpa_cmake/
+arpa-validation-logs/
+Makefile.arpa
+
+# Emitted by litani
+.ninja_deps
+.ninja_log
+.litani_cache_dir
+
+# These files should be overwritten whenever prepare.py runs
+cbmc-batch.yaml
+
+__pycache__/

kernel/FreeRTOS-Plus/Source/AWS/device-shadow/test/cbmc/include/README.md

@@ -0,0 +1,6 @@
+CBMC proof include files
+========================
+
+This directory contains include files written for CBMC proof.  It is
+common to write some code to model aspects of the system under test,
+and the header files for this code go here.

kernel/FreeRTOS-Plus/Source/AWS/device-shadow/test/cbmc/proofs/Makefile-project-defines

@@ -0,0 +1,30 @@
+# -*- mode: makefile -*-
+# The first line sets the emacs major mode to Makefile
+
+################################################################
+# Use this file to give project-specific definitions of the command
+# line arguments to pass to CBMC tools like goto-cc to build the goto
+# binaries and cbmc to do the property and coverage checking.
+#
+# Use this file to override most default definitions of variables in
+# Makefile.common.
+################################################################
+
+# Flags to pass to goto-cc for compilation (typically those passed to gcc -c)
+COMPILE_FLAGS += -fPIC
+COMPILE_FLAGS += -std=gnu90
+
+LITANI ?= litani
+PROJECT_NAME = "FreeRTOS coreShadow"
+
+# Flags to pass to goto-cc for linking (typically those passed to gcc)
+# LINK_FLAGS =
+
+# Preprocessor include paths -I...
+INCLUDES += -I$(SRCDIR)/test/cbmc/include
+INCLUDES += -I$(SRCDIR)/source/include
+INCLUDES += -I$(SRCDIR)/source
+INCLUDES += -I$(SRCDIR)/test/include
+
+# Preprocessor definitions -D...
+DEFINES += -Dshadow_EXPORTS

kernel/FreeRTOS-Plus/Source/AWS/device-shadow/test/cbmc/proofs/Makefile-project-targets

@@ -0,0 +1,10 @@
+# -*- mode: makefile -*-
+# The first line sets the emacs major mode to Makefile
+
+# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+# SPDX-License-Identifier: MIT-0
+
+################################################################
+# Use this file to give project-specific targets, including targets
+# that may depend on targets defined in Makefile.common.
+################################################################

kernel/FreeRTOS-Plus/Source/AWS/device-shadow/test/cbmc/proofs/Makefile-project-testing

@@ -0,0 +1,11 @@
+# -*- mode: makefile -*-
+# The first line sets the emacs major mode to Makefile
+
+# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+# SPDX-License-Identifier: MIT-0
+
+################################################################
+# Use this file to define project-specific targets and definitions for
+# unit testing or continuous integration that may depend on targets
+# defined in Makefile.common
+################################################################

kernel/FreeRTOS-Plus/Source/AWS/device-shadow/test/cbmc/proofs/Makefile-template-defines

@@ -0,0 +1 @@
+SRCDIR ?= $(abspath $(PROOF_ROOT)/../../..)

kernel/FreeRTOS-Plus/Source/AWS/device-shadow/test/cbmc/proofs/Makefile.common

@@ -0,0 +1,999 @@
+# -*- mode: makefile -*-
+# The first line sets the emacs major mode to Makefile
+
+# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+# SPDX-License-Identifier: MIT-0
+
+CBMC_STARTER_KIT_VERSION = CBMC starter kit 2.5
+
+################################################################
+# The CBMC Starter Kit depends on the files Makefile.common and
+# run-cbmc-proofs.py.  They are installed by the setup script
+# cbmc-starter-kit-setup and updated to the latest version by the
+# update script cbmc-starter-kit-update.  For more information about
+# the starter kit and these files and these scripts, see
+# https://model-checking.github.io/cbmc-starter-kit
+#
+# Makefile.common implements what we consider to be some best
+# practices for using cbmc for software verification.
+#
+# Section I gives default values for a large number of Makefile
+# variables that control
+#   * how your code is built (include paths, etc),
+#   * what program transformations are applied to your code (loop
+#     unwinding, etc), and
+#   * what properties cbmc checks for in your code (memory safety, etc).
+#
+# These variables are defined below with definitions of the form
+#   VARIABLE ?= DEFAULT_VALUE
+# meaning VARIABLE is set to DEFAULT_VALUE if VARIABLE has not already
+# been given a value.
+#
+# For your project, you can override these default values with
+# project-specific definitions in Makefile-project-defines.
+#
+# For any individual proof, you can override these default values and
+# project-specific values with proof-specific definitions in the
+# Makefile for your proof.
+#
+# The definitions in the proof Makefile override definitions in the
+# project Makefile-project-defines which override definitions in this
+# Makefile.common.
+#
+# Section II uses the values defined in Section I to build your code, run
+# your proof, and build a report of your results.  You should not need
+# to modify or override anything in Section II, but you may want to
+# read it to understand how the values defined in Section I control
+# things.
+#
+# To use Makefile.common, set variables as described above as needed,
+# and then for each proof,
+#
+#   * Create a subdirectory <DIR>.
+#   * Write a proof harness (a function) with the name <HARNESS_ENTRY>
+#     in a file with the name <DIR>/<HARNESS_FILE>.c
+#   * Write a makefile with the name <DIR>/Makefile that looks
+#     something like
+#
+#     HARNESS_FILE=<HARNESS_FILE>
+#     HARNESS_ENTRY=<HARNESS_ENTRY>
+#     PROOF_UID=<PROOF_UID>
+#
+#     PROJECT_SOURCES += $(SRCDIR)/libraries/api_1.c
+#     PROJECT_SOURCES += $(SRCDIR)/libraries/api_2.c
+#
+#     PROOF_SOURCES += $(PROOFDIR)/harness.c
+#     PROOF_SOURCES += $(SRCDIR)/cbmc/proofs/stub_a.c
+#     PROOF_SOURCES += $(SRCDIR)/cbmc/proofs/stub_b.c
+#
+#     UNWINDSET += foo.0:3
+#     UNWINDSET += bar.1:6
+#
+#     REMOVE_FUNCTION_BODY += api_stub_a
+#     REMOVE_FUNCTION_BODY += api_stub_b
+#
+#     DEFINES = -DDEBUG=0
+#
+#     include ../Makefile.common
+#
+#   * Change directory to <DIR> and run make
+#
+# The proof setup script cbmc-starter-kit-setup-proof from the CBMC
+# Starter Kit will do most of this for, creating a directory and
+# writing a basic Makefile and proof harness into it that you can edit
+# as described above.
+#
+# Warning: If you get results that are hard to explain, consider
+# running "make clean" or "make veryclean" before "make" if you get
+# results that are hard to explain.  Dependency handling in this
+# Makefile.common may not be perfect.
+
+SHELL=/bin/bash
+
+default: report
+
+################################################################
+################################################################
+## Section I: This section gives common variable definitions.
+##
+## Override these definitions in Makefile-project-defines or
+## your proof Makefile.
+##
+## Remember that Makefile.common and Makefile-project-defines are
+## included into the proof Makefile in your proof directory, so all
+## relative pathnames defined there should be relative to your proof
+## directory.
+
+################################################################
+# Define the layout of the source tree and the proof subtree
+#
+# Generally speaking,
+#
+#   SRCDIR = the root of the repository
+#   CBMC_ROOT = /srcdir/cbmc
+#   PROOF_ROOT = /srcdir/cbmc/proofs
+#   PROOF_SOURCE = /srcdir/cbmc/sources
+#   PROOF_INCLUDE = /srcdir/cbmc/include
+#   PROOF_STUB = /srcdir/cbmc/stubs
+#   PROOFDIR = the directory containing the Makefile for your proof
+#
+# The path /srcdir/cbmc used in the example above is determined by the
+# setup script cbmc-starter-kit-setup.  Projects usually create a cbmc
+# directory somewhere in the source tree, and run the setup script in
+# that directory.  The value of CBMC_ROOT becomes the absolute path to
+# that directory.
+#
+# The location of that cbmc directory in the source tree affects the
+# definition of SRCDIR, which is defined in terms of the relative path
+# from a proof directory to the repository root.  The definition is
+# usually determined by the setup script cbmc-starter-kit-setup and
+# written to Makefile-template-defines, but you can override it for a
+# project in Makefile-project-defines and for a specific proof in the
+# Makefile for the proof.
+
+# Absolute path to the directory containing this Makefile.common
+# See https://ftp.gnu.org/old-gnu/Manuals/make-3.80/html_node/make_17.html
+#
+# Note: We compute the absolute paths to the makefiles in MAKEFILE_LIST
+# before we filter the list of makefiles for %/Makefile.common.
+# Otherwise an invocation of the form "make -f Makefile.common" will set
+# MAKEFILE_LIST to "Makefile.common" which will fail to match the
+# pattern %/Makefile.common.
+#
+MAKEFILE_PATHS = $(foreach makefile,$(MAKEFILE_LIST),$(abspath $(makefile)))
+PROOF_ROOT = $(dir $(filter %/Makefile.common,$(MAKEFILE_PATHS)))
+
+CBMC_ROOT = $(shell dirname $(PROOF_ROOT))
+PROOF_SOURCE = $(CBMC_ROOT)/sources
+PROOF_INCLUDE = $(CBMC_ROOT)/include
+PROOF_STUB = $(CBMC_ROOT)/stubs
+
+# Project-specific definitions to override default definitions below
+#   * Makefile-project-defines will never be overwritten
+#   * Makefile-template-defines may be overwritten when the starter
+#     kit is updated
+sinclude $(PROOF_ROOT)/Makefile-project-defines
+sinclude $(PROOF_ROOT)/Makefile-template-defines
+
+# SRCDIR is the path to the root of the source tree
+# This is a default definition that is frequently overridden in
+# another Makefile, see the discussion of SRCDIR above.
+SRCDIR ?= $(abspath ../..)
+
+# PROOFDIR is the path to the directory containing the proof harness
+PROOFDIR ?= $(abspath .)
+
+################################################################
+# Define how to run CBMC
+
+# Do property checking with the external SAT solver given by
+# EXTERNAL_SAT_SOLVER.  Do coverage checking with the default solver,
+# since coverage checking requires the use of an incremental solver.
+# The EXTERNAL_SAT_SOLVER variable is typically set (if it is at all)
+# as an environment variable or as a makefile variable in
+# Makefile-project-defines.
+#
+# For a particular proof, if the default solver is faster, do property
+# checking with the default solver by including this definition in the
+# proof Makefile:
+#         USE_EXTERNAL_SAT_SOLVER =
+#
+ifneq ($(strip $(EXTERNAL_SAT_SOLVER)),)
+   USE_EXTERNAL_SAT_SOLVER ?= --external-sat-solver $(EXTERNAL_SAT_SOLVER)
+endif
+CHECKFLAGS += $(USE_EXTERNAL_SAT_SOLVER)
+
+# Job pools
+# For version of Litani that are new enough (where `litani print-capabilities`
+# prints "pools"), proofs for which `EXPENSIVE = true` is set can be added to a
+# "job pool" that restricts how many expensive proofs are run at a time. All
+# other proofs will be built in parallel as usual.
+#
+# In more detail: all compilation, instrumentation, and report jobs are run with
+# full parallelism as usual, even for expensive proofs. The CBMC jobs for
+# non-expensive proofs are also run in parallel. The only difference is that the
+# CBMC safety checks and coverage checks for expensive proofs are run with a
+# restricted parallelism level. At any one time, only N of these jobs are run at
+# once, amongst all the proofs.
+#
+# To configure N, Litani needs to be initialized with a pool called "expensive".
+# For example, to only run two CBMC safety/coverage jobs at a time from amongst
+# all the proofs, you would initialize litani like
+#         litani init --pools expensive:2
+# The run-cbmc-proofs.py script takes care of this initialization through the
+# --expensive-jobs-parallelism flag.
+#
+# To enable this feature, set
+# the ENABLE_POOLS variable when running Make, like
+#         `make ENABLE_POOLS=true report`
+# The run-cbmc-proofs.py script takes care of this through the
+# --restrict-expensive-jobs flag.
+
+ifeq ($(strip $(ENABLE_POOLS)),)
+  POOL =
+else ifeq ($(strip $(EXPENSIVE)),)
+  POOL =
+else
+  POOL = --pool expensive
+endif
+
+# Similar to the pool feature above. If Litani is new enough, enable
+# profiling CBMC's memory use.
+ifeq ($(strip $(ENABLE_MEMORY_PROFILING)),)
+  MEMORY_PROFILING =
+else
+  MEMORY_PROFILING = --profile-memory
+endif
+
+# Property checking flags
+#
+# Each variable below controls a specific property checking flag
+# within CBMC. If desired, a property flag can be disabled within
+# a particular proof by nulling the corresponding variable. For
+# instance, the following line:
+#
+#     CHECK_FLAG_POINTER_CHECK =
+#
+# would disable the --pointer-check CBMC flag within:
+#   * an entire project when added to Makefile-project-defines
+#   * a specific proof when added to the harness Makefile
+
+CBMC_FLAG_MALLOC_MAY_FAIL ?= --malloc-may-fail
+CBMC_FLAG_MALLOC_FAIL_NULL ?= --malloc-fail-null
+CBMC_FLAG_BOUNDS_CHECK ?= --bounds-check
+CBMC_FLAG_CONVERSION_CHECK ?= --conversion-check
+CBMC_FLAG_DIV_BY_ZERO_CHECK ?= --div-by-zero-check
+CBMC_FLAG_FLOAT_OVERFLOW_CHECK ?= --float-overflow-check
+CBMC_FLAG_NAN_CHECK ?= --nan-check
+CBMC_FLAG_POINTER_CHECK ?= --pointer-check
+CBMC_FLAG_POINTER_OVERFLOW_CHECK ?= --pointer-overflow-check
+CBMC_FLAG_POINTER_PRIMITIVE_CHECK ?= --pointer-primitive-check
+CBMC_FLAG_SIGNED_OVERFLOW_CHECK ?= --signed-overflow-check
+CBMC_FLAG_UNDEFINED_SHIFT_CHECK ?= --undefined-shift-check
+CBMC_FLAG_UNSIGNED_OVERFLOW_CHECK ?= --unsigned-overflow-check
+CBMC_FLAG_UNWINDING_ASSERTIONS ?= --unwinding-assertions
+CBMC_FLAG_UNWIND ?= --unwind 1
+CBMC_FLAG_FLUSH ?= --flush
+
+# CBMC flags used for property checking and coverage checking
+
+CBMCFLAGS += $(CBMC_FLAG_UNWIND) $(CBMC_UNWINDSET) $(CBMC_FLAG_FLUSH)
+
+# CBMC flags used for property checking
+
+CHECKFLAGS += $(CBMC_FLAG_MALLOC_MAY_FAIL)
+CHECKFLAGS += $(CBMC_FLAG_MALLOC_FAIL_NULL)
+CHECKFLAGS += $(CBMC_FLAG_BOUNDS_CHECK)
+CHECKFLAGS += $(CBMC_FLAG_CONVERSION_CHECK)
+CHECKFLAGS += $(CBMC_FLAG_DIV_BY_ZERO_CHECK)
+CHECKFLAGS += $(CBMC_FLAG_FLOAT_OVERFLOW_CHECK)
+CHECKFLAGS += $(CBMC_FLAG_NAN_CHECK)
+CHECKFLAGS += $(CBMC_FLAG_POINTER_CHECK)
+CHECKFLAGS += $(CBMC_FLAG_POINTER_OVERFLOW_CHECK)
+CHECKFLAGS += $(CBMC_FLAG_POINTER_PRIMITIVE_CHECK)
+CHECKFLAGS += $(CBMC_FLAG_SIGNED_OVERFLOW_CHECK)
+CHECKFLAGS += $(CBMC_FLAG_UNDEFINED_SHIFT_CHECK)
+CHECKFLAGS += $(CBMC_FLAG_UNSIGNED_OVERFLOW_CHECK)
+CHECKFLAGS += $(CBMC_FLAG_UNWINDING_ASSERTIONS)
+
+# CBMC flags used for coverage checking
+
+COVERFLAGS += $(CBMC_FLAG_MALLOC_MAY_FAIL)
+COVERFLAGS += $(CBMC_FLAG_MALLOC_FAIL_NULL)
+
+# Additional CBMC flag to CBMC control verbosity.
+#
+# Meaningful values are
+# 0 none
+# 1 only errors
+# 2 + warnings
+# 4 + results
+# 6 + status/phase information
+# 8 + statistical information
+# 9 + progress information
+# 10 + debug info
+#
+# Uncomment the following line or set in Makefile-project-defines
+# CBMC_VERBOSITY ?= --verbosity 4
+
+# Additional CBMC flag to control how CBMC treats static variables.
+#
+# NONDET_STATIC is a list of flags of the form --nondet-static
+# and --nondet-static-exclude VAR.  The --nondet-static flag causes
+# CBMC to initialize static variables with unconstrained value
+# (ignoring initializers and default zero-initialization).  The
+# --nondet-static-exclude VAR excludes VAR for the variables
+# initialized with unconstrained values.
+NONDET_STATIC ?=
+
+# Flags to pass to goto-cc for compilation and linking
+COMPILE_FLAGS ?= -Wall
+LINK_FLAGS ?= -Wall
+EXPORT_FILE_LOCAL_SYMBOLS ?= --export-file-local-symbols
+
+# Preprocessor include paths -I...
+INCLUDES ?=
+
+# Preprocessor definitions -D...
+DEFINES ?=
+
+# CBMC object model
+#
+# CBMC_OBJECT_BITS is the number of bits in a pointer CBMC uses for
+# the id of the object to which a pointer is pointing.  CBMC uses 8
+# bits for the object id by default. The remaining bits in the pointer
+# are used for offset into the object.  This limits the size of the
+# objects that CBMC can model.  This Makefile defines this bound on
+# object size to be CBMC_MAX_OBJECT_SIZE.  You are likely to get
+# unexpected results if you try to malloc an object larger than this
+# bound.
+CBMC_OBJECT_BITS ?= 8
+
+# CBMC loop unwinding (Normally set in the proof Makefile)
+#
+# UNWINDSET is a list of pairs of the form foo.1:4 meaning that
+# CBMC should unwind loop 1 in function foo no more than 4 times.
+# For historical reasons, the number 4 is one more than the number
+# of times CBMC actually unwinds the loop.
+UNWINDSET ?=
+
+# CBMC early loop unwinding (Normally set in the proof Makefile)
+#
+# Most users can ignore this variable.
+#
+# This variable exists to support the use of loop and function
+# contracts, two features under development for CBMC.  Checking the
+# assigns clause for function contracts and loop invariants currently
+# assumes loop-free bodies for loops and functions with contracts
+# (possibly after replacing nested loops with their own loop
+# contracts).  To satisfy this requirement, it may be necessary to
+# unwind some loops before the function contract and loop invariant
+# transformations are applied to the goto program.  This variable
+# EARLY_UNWINDSET is identical to UNWINDSET, and we assume that the
+# loops mentioned in EARLY_UNWINDSET and UNWINDSET are disjoint.
+EARLY_UNWINDSET ?=
+
+# CBMC function removal (Normally set set in the proof Makefile)
+#
+# REMOVE_FUNCTION_BODY is a list of function names.  CBMC will "undefine"
+# the function, and CBMC will treat the function as having no side effects
+# and returning an unconstrained value of the appropriate return type.
+# The list should include the names of functions being stubbed out.
+REMOVE_FUNCTION_BODY ?=
+
+# CBMC function pointer restriction (Normally set in the proof Makefile)
+#
+# RESTRICT_FUNCTION_POINTER is a list of function pointer restriction
+# instructions of the form:
+#
+#    <fun_id>.function_pointer_call.<N>/<fun_id>[,<fun_id>]*
+#
+# The function pointer call number <N> in the specified function gets
+# rewritten to a case switch over a finite list of functions.
+# If some possible target functions are omitted from the list a counter
+# example trace will be found by CBMC, i.e. the transformation is sound.
+# If the target functions are file-local symbols, then mangled names must
+# be used.
+RESTRICT_FUNCTION_POINTER ?=
+
+# The project source files (Normally set set in the proof Makefile)
+#
+# PROJECT_SOURCES is the list of project source files to compile,
+# including the source file defining the function under test.
+PROJECT_SOURCES ?=
+
+# The proof source files (Normally set in the proof Makefile)
+#
+# PROOF_SOURCES is the list of proof source files to compile, including
+# the proof harness, and including any function stubs being used.
+PROOF_SOURCES ?=
+
+# The number of seconds that CBMC should be allowed to run for before
+# being forcefully terminated. Currently, this is set to be less than
+# the time limit for a CodeBuild job, which is eight hours. If a proof
+# run takes longer than the time limit of the CI environment, the
+# environment will halt the proof run without updating the Litani
+# report, making the proof run appear to "hang".
+CBMC_TIMEOUT ?= 21600
+
+# Proof writers could add function contracts in their source code.
+# These contracts are ignored by default, but may be enabled in two distinct
+# contexts using the following two variables:
+# 1. To check whether one or more function contracts are sound with respect to
+#    the function implementation, CHECK_FUNCTION_CONTRACTS should be a list of
+#    function names.
+# 2. To replace calls to certain functions with their correspondent function
+#    contracts, USE_FUNCTION_CONTRACTS should be a list of function names.
+#    One must check separately whether a function contract is sound before
+#    replacing it in calling contexts.
+CHECK_FUNCTION_CONTRACTS ?=
+CBMC_CHECK_FUNCTION_CONTRACTS := $(patsubst %,--enforce-contract %, $(CHECK_FUNCTION_CONTRACTS))
+
+USE_FUNCTION_CONTRACTS ?=
+CBMC_USE_FUNCTION_CONTRACTS := $(patsubst %,--replace-call-with-contract %, $(USE_FUNCTION_CONTRACTS))
+
+# Similarly, proof writers could also add loop contracts in their source code
+# to obtain unbounded correctness proofs. Unlike function contracts, loop
+# contracts are not reusable and thus are checked and used simultaneously.
+# These contracts are also ignored by default, but may be enabled by setting
+# the APPLY_LOOP_CONTRACTS variable to 1.
+APPLY_LOOP_CONTRACTS ?= 0
+ifeq ($(APPLY_LOOP_CONTRACTS),1)
+  CBMC_APPLY_LOOP_CONTRACTS ?= --apply-loop-contracts
+endif
+
+# Silence makefile output (eg, long litani commands) unless VERBOSE is set.
+ifndef VERBOSE
+    MAKEFLAGS := $(MAKEFLAGS) -s
+endif
+
+################################################################
+################################################################
+## Section II: This section defines the process of running a proof
+##
+## There should be no reason to edit anything below this line.
+
+################################################################
+# Paths
+
+CBMC ?= cbmc
+GOTO_ANALYZER ?= goto-analyzer
+GOTO_CC ?= goto-cc
+GOTO_INSTRUMENT ?= goto-instrument
+CRANGLER ?= crangler
+VIEWER ?= cbmc-viewer
+MAKE_SOURCE ?= make-source
+VIEWER2 ?= cbmc-viewer
+CMAKE ?= cmake
+
+GOTODIR ?= $(PROOFDIR)/gotos
+LOGDIR ?= $(PROOFDIR)/logs
+
+PROJECT ?= project
+PROOF ?= proof
+
+HARNESS_GOTO ?= $(GOTODIR)/$(HARNESS_FILE)
+PROJECT_GOTO ?= $(GOTODIR)/$(PROJECT)
+PROOF_GOTO ?= $(GOTODIR)/$(PROOF)
+
+################################################################
+# Useful macros for values that are hard to reference
+SPACE :=$() $()
+COMMA :=,
+
+################################################################
+# Set C compiler defines
+
+CBMCFLAGS += --object-bits $(CBMC_OBJECT_BITS)
+COMPILE_FLAGS += --object-bits $(CBMC_OBJECT_BITS)
+
+DEFINES += -DCBMC=1
+DEFINES += -DCBMC_OBJECT_BITS=$(CBMC_OBJECT_BITS)
+DEFINES += -DCBMC_MAX_OBJECT_SIZE="(SIZE_MAX>>(CBMC_OBJECT_BITS+1))"
+
+# CI currently assumes cbmc invocation has at most one --unwindset
+ifdef UNWINDSET
+  ifneq ($(strip $(UNWINDSET)),"")
+    CBMC_UNWINDSET := --unwindset $(subst $(SPACE),$(COMMA),$(strip $(UNWINDSET)))
+  endif
+endif
+ifdef EARLY_UNWINDSET
+  ifneq ($(strip $(EARLY_UNWINDSET)),"")
+    CBMC_EARLY_UNWINDSET := --unwindset $(subst $(SPACE),$(COMMA),$(strip $(EARLY_UNWINDSET)))
+  endif
+endif
+
+CBMC_REMOVE_FUNCTION_BODY := $(patsubst %,--remove-function-body %, $(REMOVE_FUNCTION_BODY))
+CBMC_RESTRICT_FUNCTION_POINTER := $(patsubst %,--restrict-function-pointer %, $(RESTRICT_FUNCTION_POINTER))
+
+################################################################
+# Targets for rewriting source files with crangler
+
+# Construct crangler configuration files
+#
+# REWRITTEN_SOURCES is a list of crangler output files source.i.
+# This target assumes that for each source.i
+#   * source.i_SOURCE is the path to a source file,
+#   * source.i_FUNCTIONS is a list of functions (may be empty)
+#   * source.i_OBJECTS is a list of variables (may be empty)
+# This target constructs the crangler configuration file source.i.json
+# of the form
+#   {
+#     "sources":   [ "/proj/code.c" ],
+#     "includes":  [ "/proj/include" ],
+#     "defines":   [ "VAR=1" ],
+#     "functions": [ {"function_name": ["remove static"]} ],
+#     "objects":   [ {"variable_name": ["remove static"]} ],
+#     "output":    "source.i"
+#   }
+# to remove the static attribute from function_name and variable_name
+# in the source file source.c and write the result to source.i.
+#
+# This target assumes that filenames include no spaces and that
+# the INCLUDES and DEFINES variables include no spaces after -I
+# and -D.  For example, use "-DVAR=1" and not "-D VAR=1".
+#
+# Define *_SOURCE, *_FUNCTIONS, and *_OBJECTS in the proof Makefile.
+# The string source.i is usually an absolute path $(PROOFDIR)/code.i
+# to a file in the proof directory that contains the proof Makefile.
+# The proof Makefile usually includes the definitions
+#   $(PROOFDIR)/code.i_SOURCE = /proj/code.c
+#   $(PROOFDIR)/code.i_FUNCTIONS = function_name
+#   $(PROOFDIR)/code.i_OBJECTS = variable_name
+# Because these definitions refer to PROOFDIR that is defined in this
+# Makefile.common, these definitions must appear after the inclusion
+# of Makefile.common in the proof Makefile.
+#
+$(foreach rs,$(REWRITTEN_SOURCES),$(eval $(rs).json: $($(rs)_SOURCE)))
+$(foreach rs,$(REWRITTEN_SOURCES),$(rs).json):
+	echo '{'\
+	  '"sources": ['\
+	  '"$($(@:.json=)_SOURCE)"'\
+	  '],'\
+	  '"includes": ['\
+	    '$(subst $(SPACE),$(COMMA),$(patsubst -I%,"%",$(strip $(INCLUDES))))' \
+	  '],'\
+	  '"defines": ['\
+	    '$(subst $(SPACE),$(COMMA),$(patsubst -D%,"%",$(subst ",\",$(strip $(DEFINES)))))' \
+	  '],'\
+	  '"functions": ['\
+	    '{'\
+	      '$(subst ~, ,$(subst $(SPACE),$(COMMA),$(patsubst %,"%":["remove~static"],$($(@:.json=)_FUNCTIONS))))' \
+	    '}'\
+	  '],'\
+	  '"objects": ['\
+	    '{'\
+	      '$(subst ~, ,$(subst $(SPACE),$(COMMA),$(patsubst %,"%":["remove~static"],$($(@:.json=)_OBJECTS))))' \
+	    '}'\
+	  '],'\
+	  '"output": "$(@:.json=)"'\
+	'}' > $@
+
+# Rewrite source files with crangler
+#
+$(foreach rs,$(REWRITTEN_SOURCES),$(eval $(rs): $(rs).json))
+$(REWRITTEN_SOURCES):
+	$(LITANI) add-job \
+	  --command \
+	  '$(CRANGLER) $@.json' \
+	  --inputs $($@_SOURCE) \
+	  --outputs $@ \
+	  --stdout-file $(LOGDIR)/crangler-$(subst /,_,$(subst .,_,$@))-log.txt \
+	  --interleave-stdout-stderr \
+	  --pipeline-name "$(PROOF_UID)" \
+	  --ci-stage build \
+	  --description "$(PROOF_UID): removing static"
+
+################################################################
+# Build targets that make the relevant .goto files
+
+# Compile project sources
+$(PROJECT_GOTO)1.goto: $(PROJECT_SOURCES) $(REWRITTEN_SOURCES)
+	$(LITANI) add-job \
+	  --command \
+	    '$(GOTO_CC) $(CBMC_VERBOSITY) $(COMPILE_FLAGS) $(EXPORT_FILE_LOCAL_SYMBOLS) $(INCLUDES) $(DEFINES) $^ -o $@' \
+	  --inputs $^ \
+	  --outputs $@ \
+	  --stdout-file $(LOGDIR)/project_sources-log.txt \
+	  --pipeline-name "$(PROOF_UID)" \
+	  --ci-stage build \
+	  --description "$(PROOF_UID): building project binary"
+
+# Compile proof sources
+$(PROOF_GOTO)1.goto: $(PROOF_SOURCES)
+	$(LITANI) add-job \
+	  --command \
+	    '$(GOTO_CC) $(CBMC_VERBOSITY) $(COMPILE_FLAGS) $(EXPORT_FILE_LOCAL_SYMBOLS) $(INCLUDES) $(DEFINES) $^ -o $@' \
+	  --inputs $^ \
+	  --outputs $@ \
+	  --stdout-file $(LOGDIR)/proof_sources-log.txt \
+	  --pipeline-name "$(PROOF_UID)" \
+	  --ci-stage build \
+	  --description "$(PROOF_UID): building proof binary"
+
+# Remove function bodies from project sources
+$(PROJECT_GOTO)2.goto: $(PROJECT_GOTO)1.goto
+	$(LITANI) add-job \
+	  --command \
+	    '$(GOTO_INSTRUMENT) $(CBMC_VERBOSITY) $(CBMC_REMOVE_FUNCTION_BODY) $^ $@' \
+	  --inputs $^ \
+	  --outputs $@ \
+	  --stdout-file $(LOGDIR)/remove_function_body-log.txt \
+	  --pipeline-name "$(PROOF_UID)" \
+	  --ci-stage build \
+	  --description "$(PROOF_UID): removing function bodies from project sources"
+
+# Link project and proof sources into the proof harness
+$(HARNESS_GOTO)1.goto: $(PROOF_GOTO)1.goto $(PROJECT_GOTO)2.goto
+	$(LITANI) add-job \
+	  --command '$(GOTO_CC) $(CBMC_VERBOSITY) --function $(HARNESS_ENTRY) $^ $(LINK_FLAGS) -o $@' \
+	  --inputs $^ \
+	  --outputs $@ \
+	  --stdout-file $(LOGDIR)/link_proof_project-log.txt \
+	  --pipeline-name "$(PROOF_UID)" \
+	  --ci-stage build \
+	  --description "$(PROOF_UID): linking project to proof"
+
+# Restrict function pointers
+$(HARNESS_GOTO)2.goto: $(HARNESS_GOTO)1.goto
+	$(LITANI) add-job \
+	  --command \
+	    '$(GOTO_INSTRUMENT) $(CBMC_VERBOSITY) $(CBMC_RESTRICT_FUNCTION_POINTER) $^ $@' \
+	  --inputs $^ \
+	  --outputs $@ \
+	  --stdout-file $(LOGDIR)/restrict_function_pointer-log.txt \
+	  --pipeline-name "$(PROOF_UID)" \
+	  --ci-stage build \
+	  --description "$(PROOF_UID): restricting function pointers in project sources"
+
+# Fill static variable with unconstrained values
+$(HARNESS_GOTO)3.goto: $(HARNESS_GOTO)2.goto
+	$(LITANI) add-job \
+	  --command \
+	    '$(GOTO_INSTRUMENT) $(CBMC_VERBOSITY) $(NONDET_STATIC) $^ $@' \
+	  --inputs $^ \
+	  --outputs $@ \
+	  --stdout-file $(LOGDIR)/nondet_static-log.txt \
+	  --pipeline-name "$(PROOF_UID)" \
+	  --ci-stage build \
+	  --description "$(PROOF_UID): setting static variables to nondet"
+
+# Omit unused functions (sharpens coverage calculations)
+$(HARNESS_GOTO)4.goto: $(HARNESS_GOTO)3.goto
+	$(LITANI) add-job \
+	  --command \
+	    '$(GOTO_INSTRUMENT) $(CBMC_VERBOSITY) --drop-unused-functions $^ $@' \
+	  --inputs $^ \
+	  --outputs $@ \
+	  --stdout-file $(LOGDIR)/drop_unused_functions-log.txt \
+	  --pipeline-name "$(PROOF_UID)" \
+	  --ci-stage build \
+	  --description "$(PROOF_UID): dropping unused functions"
+
+# Omit initialization of unused global variables (reduces problem size)
+$(HARNESS_GOTO)5.goto: $(HARNESS_GOTO)4.goto
+	$(LITANI) add-job \
+	  --command \
+	    '$(GOTO_INSTRUMENT) $(CBMC_VERBOSITY) --slice-global-inits $^ $@' \
+	  --inputs $^ \
+	  --outputs $@ \
+	  --stdout-file $(LOGDIR)/slice_global_inits-log.txt \
+	  --pipeline-name "$(PROOF_UID)" \
+	  --ci-stage build \
+	  --description "$(PROOF_UID): slicing global initializations"
+
+# Replace function calls with function contracts
+# This must be done before enforcing function contracts,
+# since contract enforcement inlines all function calls.
+$(HARNESS_GOTO)6.goto: $(HARNESS_GOTO)5.goto
+	$(LITANI) add-job \
+	  --command \
+	    '$(GOTO_INSTRUMENT) $(CBMC_VERBOSITY) $(CBMC_USE_FUNCTION_CONTRACTS) $^ $@' \
+	  --inputs $^ \
+	  --outputs $@ \
+	  --stdout-file $(LOGDIR)/use_function_contracts-log.txt \
+	  --pipeline-name "$(PROOF_UID)" \
+	  --ci-stage build \
+	  --description "$(PROOF_UID): replacing function calls with function contracts"
+
+# Unwind loops for loop and function contracts
+$(HARNESS_GOTO)7.goto: $(HARNESS_GOTO)6.goto
+	$(LITANI) add-job \
+	  --command \
+	    '$(GOTO_INSTRUMENT) $(CBMC_VERBOSITY) $(CBMC_EARLY_UNWINDSET) $(CBMC_FLAG_UNWINDING_ASSERTIONS) $^ $@' \
+	  --inputs $^ \
+	  --outputs $@ \
+	  --stdout-file $(LOGDIR)/unwind_loops-log.txt \
+	  --pipeline-name "$(PROOF_UID)" \
+	  --ci-stage build \
+	  --description "$(PROOF_UID): unwinding loops"
+
+# Apply loop contracts
+$(HARNESS_GOTO)8.goto: $(HARNESS_GOTO)7.goto
+	$(LITANI) add-job \
+	  --command \
+	    '$(GOTO_INSTRUMENT) $(CBMC_VERBOSITY) $(CBMC_APPLY_LOOP_CONTRACTS) $^ $@' \
+	  --inputs $^ \
+	  --outputs $@ \
+	  --stdout-file $(LOGDIR)/apply_loop_contracts-log.txt \
+	  --pipeline-name "$(PROOF_UID)" \
+	  --ci-stage build \
+	  --description "$(PROOF_UID): applying loop contracts"
+
+# Check function contracts
+$(HARNESS_GOTO)9.goto: $(HARNESS_GOTO)8.goto
+	$(LITANI) add-job \
+	  --command \
+	    '$(GOTO_INSTRUMENT) $(CBMC_VERBOSITY) $(CBMC_CHECK_FUNCTION_CONTRACTS) $^ $@' \
+	  --inputs $^ \
+	  --outputs $@ \
+	  --stdout-file $(LOGDIR)/check_function_contracts-log.txt \
+	  --pipeline-name "$(PROOF_UID)" \
+	  --ci-stage build \
+	  --description "$(PROOF_UID): checking function contracts"
+
+# Final name for proof harness
+$(HARNESS_GOTO).goto: $(HARNESS_GOTO)9.goto
+	$(LITANI) add-job \
+	  --command 'cp $< $@' \
+	  --inputs $^ \
+	  --outputs $@ \
+	  --pipeline-name "$(PROOF_UID)" \
+	  --ci-stage build \
+	  --description "$(PROOF_UID): copying final goto-binary"
+
+################################################################
+# Targets to run the analysis commands
+
+$(LOGDIR)/result.txt: $(HARNESS_GOTO).goto
+	$(LITANI) add-job \
+	  $(POOL) \
+	  --command \
+	    '$(CBMC) $(CBMC_VERBOSITY) $(CBMCFLAGS) $(CBMC_FLAG_UNWINDING_ASSERTIONS) $(CHECKFLAGS) --trace $<' \
+	  --inputs $^ \
+	  --outputs $@ \
+	  --ci-stage test \
+	  --stdout-file $@ \
+	  $(MEMORY_PROFILING) \
+	  --ignore-returns 10 \
+	  --timeout $(CBMC_TIMEOUT) \
+	  --pipeline-name "$(PROOF_UID)" \
+	  --tags "stats-group:safety checks" \
+	  --stderr-file $(LOGDIR)/result-err-log.txt \
+	  --description "$(PROOF_UID): checking safety properties"
+
+$(LOGDIR)/result.xml: $(HARNESS_GOTO).goto
+	$(LITANI) add-job \
+	  $(POOL) \
+	  --command \
+	    '$(CBMC) $(CBMC_VERBOSITY) $(CBMCFLAGS) $(CBMC_FLAG_UNWINDING_ASSERTIONS) $(CHECKFLAGS) --trace --xml-ui $<' \
+	  --inputs $^ \
+	  --outputs $@ \
+	  --ci-stage test \
+	  --stdout-file $@ \
+	  $(MEMORY_PROFILING) \
+	  --ignore-returns 10 \
+	  --timeout $(CBMC_TIMEOUT) \
+	  --pipeline-name "$(PROOF_UID)" \
+	  --tags "stats-group:safety checks" \
+	  --stderr-file $(LOGDIR)/result-err-log.txt \
+	  --description "$(PROOF_UID): checking safety properties"
+
+$(LOGDIR)/property.xml: $(HARNESS_GOTO).goto
+	$(LITANI) add-job \
+	  --command \
+	    '$(CBMC) $(CBMC_VERBOSITY) $(CBMCFLAGS) $(CBMC_FLAG_UNWINDING_ASSERTIONS) $(CHECKFLAGS) --show-properties --xml-ui $<' \
+	  --inputs $^ \
+	  --outputs $@ \
+	  --ci-stage test \
+	  --stdout-file $@ \
+	  --ignore-returns 10 \
+	  --pipeline-name "$(PROOF_UID)" \
+	  --stderr-file $(LOGDIR)/property-err-log.txt \
+	  --description "$(PROOF_UID): printing safety properties"
+
+$(LOGDIR)/coverage.xml: $(HARNESS_GOTO).goto
+	$(LITANI) add-job \
+	  $(POOL) \
+	  --command \
+	    '$(CBMC) $(CBMC_VERBOSITY) $(CBMCFLAGS) $(COVERFLAGS) --cover location --xml-ui $<' \
+	  --inputs $^ \
+	  --outputs $@ \
+	  --ci-stage test \
+	  --stdout-file $@ \
+	  $(MEMORY_PROFILING) \
+	  --ignore-returns 10 \
+	  --timeout $(CBMC_TIMEOUT) \
+	  --pipeline-name "$(PROOF_UID)" \
+	  --tags "stats-group:coverage computation" \
+	  --stderr-file $(LOGDIR)/coverage-err-log.txt \
+	  --description "$(PROOF_UID): calculating coverage"
+
+define VIEWER_CMD
+  $(VIEWER) \
+    --result $(LOGDIR)/result.txt \
+    --block $(LOGDIR)/coverage.xml \
+    --property $(LOGDIR)/property.xml \
+    --srcdir $(SRCDIR) \
+    --goto $(HARNESS_GOTO).goto \
+    --htmldir $(PROOFDIR)/html
+endef
+export VIEWER_CMD
+
+$(PROOFDIR)/html: $(LOGDIR)/result.txt $(LOGDIR)/property.xml $(LOGDIR)/coverage.xml
+	$(LITANI) add-job \
+	  --command "$$VIEWER_CMD" \
+	  --inputs $^ \
+	  --outputs $(PROOFDIR)/html \
+	  --pipeline-name "$(PROOF_UID)" \
+	  --ci-stage report \
+	  --stdout-file $(LOGDIR)/viewer-log.txt \
+	  --description "$(PROOF_UID): generating report"
+
+
+# Caution: run make-source before running property and coverage checking
+# The current make-source script removes the goto binary
+$(LOGDIR)/source.json:
+	mkdir -p $(dir $@)
+	$(RM) -r $(GOTODIR)
+	$(MAKE_SOURCE) --srcdir $(SRCDIR) --wkdir $(PROOFDIR) > $@
+	$(RM) -r $(GOTODIR)
+
+define VIEWER2_CMD
+  $(VIEWER2) \
+    --result $(LOGDIR)/result.xml \
+    --coverage $(LOGDIR)/coverage.xml \
+    --property $(LOGDIR)/property.xml \
+    --srcdir $(SRCDIR) \
+    --goto $(HARNESS_GOTO).goto \
+    --reportdir $(PROOFDIR)/report \
+    --config $(PROOFDIR)/cbmc-viewer.json
+endef
+export VIEWER2_CMD
+
+# Omit logs/source.json from report generation until make-sources
+# works correctly with Makefiles that invoke the compiler with
+# mutliple source files at once.
+$(PROOFDIR)/report: $(LOGDIR)/result.xml $(LOGDIR)/property.xml $(LOGDIR)/coverage.xml
+	$(LITANI) add-job \
+	  --command "$$VIEWER2_CMD" \
+	  --inputs $^ \
+	  --outputs $(PROOFDIR)/report \
+	  --pipeline-name "$(PROOF_UID)" \
+	  --stdout-file $(LOGDIR)/viewer-log.txt \
+	  --ci-stage report \
+	  --description "$(PROOF_UID): generating report"
+
+litani-path:
+	@echo $(LITANI)
+
+# ##############################################################
+# Phony Rules
+#
+#	These rules provide a convenient way to run a single proof up to a
+#	certain stage. Users can browse into a proof directory and run
+#	"make -Bj 3 report" to generate a report for just that proof, or
+#	"make goto" to build the goto binary. Under the hood, this runs litani
+#	for just that proof.
+
+_goto: $(HARNESS_GOTO).goto
+goto:
+	@ echo Running 'litani init'
+	$(LITANI) init --project $(PROJECT_NAME)
+	@ echo Running 'litani add-job'
+	$(MAKE) -B _goto
+	@ echo Running 'litani build'
+	$(LITANI) run-build
+
+_result: $(LOGDIR)/result.txt
+result:
+	@ echo Running 'litani init'
+	$(LITANI) init --project $(PROJECT_NAME)
+	@ echo Running 'litani add-job'
+	$(MAKE) -B _result
+	@ echo Running 'litani build'
+	$(LITANI) run-build
+
+_property: $(LOGDIR)/property.xml
+property:
+	@ echo Running 'litani init'
+	$(LITANI) init --project $(PROJECT_NAME)
+	@ echo Running 'litani add-job'
+	$(MAKE) -B _property
+	@ echo Running 'litani build'
+	$(LITANI) run-build
+
+_coverage: $(LOGDIR)/coverage.xml
+coverage:
+	@ echo Running 'litani init'
+	$(LITANI) init --project $(PROJECT_NAME)
+	@ echo Running 'litani add-job'
+	$(MAKE) -B _coverage
+	@ echo Running 'litani build'
+	$(LITANI) run-build
+
+# Choose the invocation of cbmc-viewer depending on which version of
+# cbmc-viewer is installed.  The --version flag is not implemented in
+# version 1 --- it is an "unrecognized argument" --- but it is
+# implemented in version 2.
+_report1: $(PROOFDIR)/html
+_report2: $(PROOFDIR)/report
+_report:
+	(cbmc-viewer --version 2>&1 | grep "unrecognized argument" > /dev/null) && \
+		$(MAKE) -B _report1 || $(MAKE) -B _report2
+
+report report1 report2:
+	@ echo Running 'litani init'
+	$(LITANI) init --project $(PROJECT_NAME)
+	@ echo Running 'litani add-job'
+	$(MAKE) -B _report
+	@ echo Running 'litani build'
+	$(LITANI) run-build
+
+################################################################
+# Targets to clean up after ourselves
+clean:
+	-$(RM) $(DEPENDENT_GOTOS)
+	-$(RM) TAGS*
+	-$(RM) *~ \#*
+	-$(RM) $(REWRITTEN_SOURCES) $(foreach rs,$(REWRITTEN_SOURCES),$(rs).json)
+
+veryclean: clean
+	-$(RM) -r html report
+	-$(RM) -r $(LOGDIR) $(GOTODIR)
+
+.PHONY: \
+  _coverage \
+  _goto \
+  _property \
+  _report \
+  _report2 \
+  _result \
+  clean \
+  coverage \
+  goto \
+  litani-path \
+  property \
+  report \
+  report2 \
+  result \
+  setup_dependencies \
+  testdeps \
+  veryclean \
+  #
+
+################################################################
+
+# Rule for generating cbmc-batch.yaml, used by the CI at
+# https://github.com/awslabs/aws-batch-cbmc/
+
+JOB_OS ?= ubuntu16
+JOB_MEMORY ?= 32000
+
+# Proofs that are expected to fail should set EXPECTED to
+# "FAILED" in their Makefile. Values other than SUCCESSFUL
+# or FAILED will cause a CI error.
+EXPECTED ?= SUCCESSFUL
+
+define yaml_encode_options
+	"$(shell echo $(1) | sed 's/ ,/ /g' | sed 's/ /;/g')"
+endef
+
+CI_FLAGS = $(CBMCFLAGS) $(CHECKFLAGS) $(COVERFLAGS)
+
+cbmc-batch.yaml:
+	@$(RM) $@
+	@echo 'build_memory: $(JOB_MEMORY)' > $@
+	@echo 'cbmcflags: $(strip $(call yaml_encode_options,$(CI_FLAGS)))' >> $@
+	@echo 'coverage_memory: $(JOB_MEMORY)' >> $@
+	@echo 'expected: $(EXPECTED)' >> $@
+	@echo 'goto: $(HARNESS_GOTO).goto' >> $@
+	@echo 'jobos: $(JOB_OS)' >> $@
+	@echo 'property_memory: $(JOB_MEMORY)' >> $@
+	@echo 'report_memory: $(JOB_MEMORY)' >> $@
+
+.PHONY: cbmc-batch.yaml
+
+################################################################
+
+# Run "make echo-proof-uid" to print the proof ID of a proof. This can be
+# used by scripts to ensure that every proof has an ID, that there are
+# no duplicates, etc.
+
+.PHONY: echo-proof-uid
+echo-proof-uid:
+	@echo $(PROOF_UID)
+
+.PHONY: echo-project-name
+echo-project-name:
+	@echo $(PROJECT_NAME)
+
+################################################################
+
+# Project-specific targets requiring values defined above
+sinclude $(PROOF_ROOT)/Makefile-project-targets
+
+# CI-specific targets to drive cbmc in CI
+sinclude $(PROOF_ROOT)/Makefile-project-testing
+
+################################################################

kernel/FreeRTOS-Plus/Source/AWS/device-shadow/test/cbmc/proofs/README.md

@@ -0,0 +1,27 @@
+CBMC proofs
+===========
+
+This directory contains the CBMC proofs.  Each proof is in its own
+directory.
+
+This directory includes four Makefiles.
+
+One Makefile describes the basic workflow for building and running proofs:
+
+* Makefile.common:
+    * make: builds the goto binary, does the cbmc property checking
+	  and coverage checking, and builds the final report.
+	* make goto: builds the goto binary
+	* make result: does cbmc property checking
+	* make coverage: does cbmc coverage checking
+	* make report: builds the final report
+
+Three included Makefiles describe project-specific settings and can override
+definitions in Makefile.common:
+
+* Makefile-project-defines: definitions like compiler flags
+  required to build the goto binaries, and definitions to override
+  definitions in Makefile.common.
+* Makefile-project-targets: other make targets needed for the project
+* Makefile-project-testing: other definitions and targets needed for
+  unit testing or continuous integration.

kernel/FreeRTOS-Plus/Source/AWS/device-shadow/test/cbmc/proofs/Shadow_AssembleTopicString/Makefile

@@ -0,0 +1,34 @@
+#
+# Copyright (C) 2020 Amazon.com, Inc. or its affiliates.  All Rights Reserved.
+#
+# Permission is hereby granted, free of charge, to any person obtaining a copy of
+# this software and associated documentation files (the "Software"), to deal in
+# 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:
+#
+# The above copyright notice and this permission notice shall be included in all
+# copies or substantial portions of the Software.
+#
+# 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 AUTHORS 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 IN THE SOFTWARE.
+#
+
+HARNESS_ENTRY=harness
+HARNESS_FILE=Shadow_AssembleTopicString_harness
+PROOF_UID = Shadow_AssembleTopicString
+
+DEFINES +=
+INCLUDES +=
+
+REMOVE_FUNCTION_BODY +=
+
+PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
+PROJECT_SOURCES += $(SRCDIR)/source/shadow.c
+
+include ../Makefile.common

kernel/FreeRTOS-Plus/Source/AWS/device-shadow/test/cbmc/proofs/Shadow_AssembleTopicString/README.md

@@ -0,0 +1,10 @@
+Shadow_AssembleTopicString proof
+==============
+
+This directory contains a memory safety proof for Shadow_AssembleTopicString.
+
+To run the proof.
+* Add cbmc, goto-cc, goto-instrument, goto-analyzer, and cbmc-viewer
+  to your path.
+* Run "make".
+* Open html/index.html in a web browser.

kernel/FreeRTOS-Plus/Source/AWS/device-shadow/test/cbmc/proofs/Shadow_AssembleTopicString/Shadow_AssembleTopicString_harness.c

@@ -0,0 +1,58 @@
+/*
+ * AWS IoT Device Shadow v1.3.0
+ * Copyright (C) 2020 Amazon.com, Inc. or its affiliates.  All Rights Reserved.
+ *
+ * SPDX-License-Identifier: MIT
+ *
+ * Permission is hereby granted, free of charge, to any person obtaining a copy of
+ * this software and associated documentation files (the "Software"), to deal in
+ * 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:
+ *
+ * The above copyright notice and this permission notice shall be included in all
+ * copies or substantial portions of the Software.
+ *
+ * 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 AUTHORS 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 IN THE SOFTWARE.
+ */
+
+/**
+ * @file Shadow_AssembleTopicString_harness.c
+ * @brief Implements the proof harness for Shadow_AssembleTopicString function.
+ */
+
+#include "shadow.h"
+
+#include <stdlib.h>
+
+void harness()
+{
+    char * topicBuffer;
+    uint16_t bufferSize;
+    uint16_t * pOutLength;
+    char * pThingName;
+    uint8_t thingNameLength;
+    char * pShadowName;
+    uint8_t shadowNameLength;
+    uint8_t topicType;
+
+    topicBuffer = malloc( bufferSize );
+    pOutLength = malloc( sizeof( *pOutLength ) );
+    pThingName = malloc( thingNameLength );
+    pShadowName = malloc( shadowNameLength );
+
+    Shadow_AssembleTopicString( topicType,
+                                pThingName,
+                                thingNameLength,
+                                pShadowName,
+                                shadowNameLength,
+                                topicBuffer,
+                                bufferSize,
+                                pOutLength );
+}

kernel/FreeRTOS-Plus/Source/AWS/device-shadow/test/cbmc/proofs/Shadow_AssembleTopicString/cbmc-proof.txt

@@ -0,0 +1 @@
+# This file marks this directory as containing a CBMC proof.

kernel/FreeRTOS-Plus/Source/AWS/device-shadow/test/cbmc/proofs/Shadow_AssembleTopicString/cbmc-viewer.json

@@ -0,0 +1,7 @@
+{ "expected-missing-functions":
+  [
+
+  ],
+  "proof-name": "Shadow_AssembleTopicString",
+  "proof-root": "../cbmc/proofs"
+}

kernel/FreeRTOS-Plus/Source/AWS/device-shadow/test/cbmc/proofs/Shadow_MatchTopic/Makefile

@@ -0,0 +1,52 @@
+#
+# Copyright (C) 2021 Amazon.com, Inc. or its affiliates.  All Rights Reserved.
+#
+# Permission is hereby granted, free of charge, to any person obtaining a copy of
+# this software and associated documentation files (the "Software"), to deal in
+# 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:
+#
+# The above copyright notice and this permission notice shall be included in all
+# copies or substantial portions of the Software.
+#
+# 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 AUTHORS 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 IN THE SOFTWARE.
+#
+
+HARNESS_ENTRY=harness
+HARNESS_FILE=Shadow_MatchTopic_harness
+PROOF_UID = Shadow_MatchTopic
+
+# The topic length is bounded to reduce the proof run time. This length bounds
+# the time to look for the thing name in the topic string. The minimum length
+# of the topic string is the length of the SHADOW_PREFIX ("$aws/things/")
+# plus the maximum Shadow Message Type length ("/shadow/update/documents")
+# plus the minimum Thing name length (1 byte). Memory safety on the buffer
+# holding the topic string can be proven within a reasonable bound. It adds
+# no value to the proof to input the largest possible topic string accepted
+# by AWS (64KB). The reasonable bound for topic length is chosen as 50 bytes,
+# which is higher than the minimum (38 bytes) topic length and provides a good
+# allowance for the variable Thing name length (13 bytes).
+TOPIC_STRING_LENGTH_MAX=50
+
+DEFINES += -DTOPIC_STRING_LENGTH_MAX=$(TOPIC_STRING_LENGTH_MAX)
+INCLUDES +=
+
+# The maximum length of the message type ( /shadow/update/documents ) is 24.
+UNWINDSET += strncmp.0:25
+
+UNWINDSET += __CPROVER_file_local_shadow_c_validateName.0:$(TOPIC_STRING_LENGTH_MAX)
+
+# The number of message types is 8.
+UNWINDSET += __CPROVER_file_local_shadow_c_extractShadowMessageType.0:9
+
+PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
+PROJECT_SOURCES += $(SRCDIR)/source/shadow.c
+
+include ../Makefile.common

kernel/FreeRTOS-Plus/Source/AWS/device-shadow/test/cbmc/proofs/Shadow_MatchTopic/README.md

@@ -0,0 +1,10 @@
+Shadow_MatchTopic proof
+==============
+
+This directory contains a memory safety proof for Shadow_MatchTopic.
+
+To run the proof.
+* Add cbmc, goto-cc, goto-instrument, goto-analyzer, and cbmc-viewer
+  to your path.
+* Run "make".
+* Open html/index.html in a web browser.

kernel/FreeRTOS-Plus/Source/AWS/device-shadow/test/cbmc/proofs/Shadow_MatchTopic/Shadow_MatchTopic_harness.c

@@ -0,0 +1,55 @@
+/*
+ * AWS IoT Device Shadow v1.3.0
+ * Copyright (C) 2021 Amazon.com, Inc. or its affiliates.  All Rights Reserved.
+ *
+ * SPDX-License-Identifier: MIT
+ *
+ * Permission is hereby granted, free of charge, to any person obtaining a copy of
+ * this software and associated documentation files (the "Software"), to deal in
+ * 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:
+ *
+ * The above copyright notice and this permission notice shall be included in all
+ * copies or substantial portions of the Software.
+ *
+ * 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 AUTHORS 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 IN THE SOFTWARE.
+ */
+
+/**
+ * @file Shadow_MatchTopic_harness.c
+ * @brief Implements the proof harness for Shadow_MatchTopic function.
+ */
+
+#include "shadow.h"
+
+#include <stdlib.h>
+
+void harness()
+{
+    const char * pTopicName;
+    uint16_t topicNameLength;
+    ShadowMessageType_t * pMessageType;
+    const char ** pThingName;
+    uint16_t * pThingNameLength;
+
+    __CPROVER_assume( topicNameLength < TOPIC_STRING_LENGTH_MAX );
+    pTopicName = malloc( topicNameLength );
+
+    pMessageType = malloc( sizeof( *pMessageType ) );
+
+    pThingName = malloc( sizeof( *pThingName ) );
+    pThingNameLength = malloc( sizeof( *pThingNameLength ) );
+
+    Shadow_MatchTopic( pTopicName,
+                       topicNameLength,
+                       pMessageType,
+                       pThingName,
+                       pThingNameLength );
+}

kernel/FreeRTOS-Plus/Source/AWS/device-shadow/test/cbmc/proofs/Shadow_MatchTopic/cbmc-proof.txt

@@ -0,0 +1 @@
+# This file marks this directory as containing a CBMC proof.

kernel/FreeRTOS-Plus/Source/AWS/device-shadow/test/cbmc/proofs/Shadow_MatchTopic/cbmc-viewer.json

@@ -0,0 +1,7 @@
+{ "expected-missing-functions":
+  [
+
+  ],
+  "proof-name": "Shadow_MatchTopic",
+  "proof-root": "../cbmc/proofs"
+}

kernel/FreeRTOS-Plus/Source/AWS/device-shadow/test/cbmc/proofs/Shadow_MatchTopicString/Makefile

@@ -0,0 +1,50 @@
+#
+# Copyright (C) 2020 Amazon.com, Inc. or its affiliates.  All Rights Reserved.
+#
+# Permission is hereby granted, free of charge, to any person obtaining a copy of
+# this software and associated documentation files (the "Software"), to deal in
+# 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:
+#
+# The above copyright notice and this permission notice shall be included in all
+# copies or substantial portions of the Software.
+#
+# 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 AUTHORS 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 IN THE SOFTWARE.
+#
+
+HARNESS_ENTRY=harness
+HARNESS_FILE=Shadow_MatchTopicString_harness
+PROOF_UID = Shadow_MatchTopicString
+
+# The topic length is bounded to reduce the proof run time. This length bounds
+# the time to look for the thing and shadow names in the topic string. It adds
+# no value to the proof to input the largest possible topic string accepted by
+# AWS (64KB). We allow for a the longest named shadow topic, but with only
+# reasonable allowance for typical Thing and Shadow names.
+# $aws/things/thingName/shadow/name/shadowName/update/documents
+TOPIC_STRING_LENGTH_MAX=65
+
+DEFINES += -DTOPIC_STRING_LENGTH_MAX=$(TOPIC_STRING_LENGTH_MAX)
+INCLUDES +=
+
+# The maximum length of the message type ( /update/documents ) is 17.
+UNWINDSET += strncmp.0:18
+
+# Allow for the longest possible Shadow name
+UNWINDSET += __CPROVER_file_local_shadow_c_validateName.0:64
+
+# The number of message types is 8.
+UNWINDSET += __CPROVER_file_local_shadow_c_extractShadowMessageType.0:9
+
+
+PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
+PROJECT_SOURCES += $(SRCDIR)/source/shadow.c
+
+include ../Makefile.common

kernel/FreeRTOS-Plus/Source/AWS/device-shadow/test/cbmc/proofs/Shadow_MatchTopicString/README.md

@@ -0,0 +1,10 @@
+Shadow_MatchTopicString proof
+==============
+
+This directory contains a memory safety proof for Shadow_MatchTopicString.
+
+To run the proof.
+* Add cbmc, goto-cc, goto-instrument, goto-analyzer, and cbmc-viewer
+  to your path.
+* Run "make".
+* Open html/index.html in a web browser.

kernel/FreeRTOS-Plus/Source/AWS/device-shadow/test/cbmc/proofs/Shadow_MatchTopicString/Shadow_MatchTopicString_harness.c

@@ -0,0 +1,62 @@
+/*
+ * AWS IoT Device Shadow v1.3.0
+ * Copyright (C) 2020 Amazon.com, Inc. or its affiliates.  All Rights Reserved.
+ *
+ * SPDX-License-Identifier: MIT
+ *
+ * Permission is hereby granted, free of charge, to any person obtaining a copy of
+ * this software and associated documentation files (the "Software"), to deal in
+ * 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:
+ *
+ * The above copyright notice and this permission notice shall be included in all
+ * copies or substantial portions of the Software.
+ *
+ * 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 AUTHORS 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 IN THE SOFTWARE.
+ */
+
+/**
+ * @file Shadow_MatchTopicString_harness.c
+ * @brief Implements the proof harness for Shadow_MatchTopicString function.
+ */
+
+#include "shadow.h"
+
+#include <stdlib.h>
+
+void harness()
+{
+    const char * pTopicName;
+    uint16_t topicNameLength;
+    ShadowMessageType_t * pMessageType;
+    const char ** pThingName;
+    uint16_t * pThingNameLength;
+    const char ** pShadowName;
+    uint16_t * pShadowNameLength;
+
+    __CPROVER_assume( topicNameLength < TOPIC_STRING_LENGTH_MAX );
+    pTopicName = malloc( topicNameLength );
+
+    pMessageType = malloc( sizeof( *pMessageType ) );
+
+    pThingName = malloc( sizeof( *pThingName ) );
+    pThingNameLength = malloc( sizeof( *pThingNameLength ) );
+
+    pShadowName = malloc( sizeof( *pShadowName ) );
+    pShadowNameLength = malloc( sizeof( *pShadowNameLength ) );
+
+    Shadow_MatchTopicString( pTopicName,
+                             topicNameLength,
+                             pMessageType,
+                             pThingName,
+                             pThingNameLength,
+                             pShadowName,
+                             pShadowNameLength );
+}

kernel/FreeRTOS-Plus/Source/AWS/device-shadow/test/cbmc/proofs/Shadow_MatchTopicString/cbmc-proof.txt

@@ -0,0 +1 @@
+# This file marks this directory as containing a CBMC proof.

kernel/FreeRTOS-Plus/Source/AWS/device-shadow/test/cbmc/proofs/Shadow_MatchTopicString/cbmc-viewer.json

@@ -0,0 +1,7 @@
+{ "expected-missing-functions":
+  [
+
+  ],
+  "proof-name": "Shadow_MatchTopicString",
+  "proof-root": "../cbmc/proofs"
+}

kernel/FreeRTOS-Plus/Source/AWS/device-shadow/test/cbmc/proofs/lib/summarize.py

@@ -0,0 +1,92 @@
+# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+# SPDX-License-Identifier: MIT-0
+
+import json
+import logging
+
+
+def _get_max_length_per_column_list(data):
+    ret = [len(item) + 1 for item in data[0]]
+    for row in data[1:]:
+        for idx, item in enumerate(row):
+            ret[idx] = max(ret[idx], len(item) + 1)
+    return ret
+
+
+def _get_table_header_separator(max_length_per_column_list):
+    line_sep = ""
+    for max_length_of_word_in_col in max_length_per_column_list:
+        line_sep += "|" + "-" * (max_length_of_word_in_col + 1)
+    line_sep += "|\n"
+    return line_sep
+
+
+def _get_entries(max_length_per_column_list, row_data):
+    entries = []
+    for row in row_data:
+        entry = ""
+        for idx, word in enumerate(row):
+            max_length_of_word_in_col = max_length_per_column_list[idx]
+            space_formatted_word = (max_length_of_word_in_col - len(word)) * " "
+            entry += "| " + word + space_formatted_word
+        entry += "|\n"
+        entries.append(entry)
+    return entries
+
+
+def _get_rendered_table(data):
+    table = []
+    max_length_per_column_list = _get_max_length_per_column_list(data)
+    entries = _get_entries(max_length_per_column_list, data)
+    for idx, entry in enumerate(entries):
+        if idx == 1:
+            line_sep = _get_table_header_separator(max_length_per_column_list)
+            table.append(line_sep)
+        table.append(entry)
+    table.append("\n")
+    return "".join(table)
+
+
+def _get_status_and_proof_summaries(run_dict):
+    """Parse a dict representing a Litani run and create lists summarizing the
+    proof results.
+
+    Parameters
+    ----------
+    run_dict
+        A dictionary representing a Litani run.
+
+    Returns
+    -------
+    A list of 2 lists.
+    The first sub-list maps a status to the number of proofs with that status.
+    The second sub-list maps each proof to its status.
+    """
+    count_statuses = {}
+    proofs = [["Proof", "Status"]]
+    for proof_pipeline in run_dict["pipelines"]:
+        status_pretty_name = proof_pipeline["status"].title().replace("_", " ")
+        try:
+            count_statuses[status_pretty_name] += 1
+        except KeyError:
+            count_statuses[status_pretty_name] = 1
+        proof = proof_pipeline["name"]
+        proofs.append([proof, status_pretty_name])
+    statuses = [["Status", "Count"]]
+    for status, count in count_statuses.items():
+        statuses.append([status, str(count)])
+    return [statuses, proofs]
+
+
+def print_proof_results(out_file):
+    """
+    Print 2 strings that summarize the proof results.
+    When printing, each string will render as a GitHub flavored Markdown table.
+    """
+    try:
+        with open(out_file, encoding='utf-8') as run_json:
+            run_dict = json.load(run_json)
+            for summary in _get_status_and_proof_summaries(run_dict):
+                print(_get_rendered_table(summary))
+    except Exception as ex: # pylint: disable=broad-except
+        logging.critical("Could not print results. Exception: %s", str(ex))

kernel/FreeRTOS-Plus/Source/AWS/device-shadow/test/cbmc/proofs/run-cbmc-proofs.py

@@ -0,0 +1,414 @@
+#!/usr/bin/env python3
+#
+# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+# SPDX-License-Identifier: MIT-0
+
+
+import argparse
+import asyncio
+import json
+import logging
+import math
+import os
+import pathlib
+import re
+import subprocess
+import sys
+import tempfile
+
+from lib.summarize import print_proof_results
+
+
+DESCRIPTION = "Configure and run all CBMC proofs in parallel"
+
+# Keep the epilog hard-wrapped at 70 characters, as it gets printed
+# verbatim in the terminal. 70 characters stops here --------------> |
+EPILOG = """
+This tool automates the process of running `make report` in each of
+the CBMC proof directories. The tool calculates the dependency graph
+of all tasks needed to build, run, and report on all the proofs, and
+executes these tasks in parallel.
+
+The tool is roughly equivalent to doing this:
+
+        litani init --project "my-cool-project";
+
+        find . -name cbmc-proof.txt | while read -r proof; do
+            pushd $(dirname ${proof});
+
+            # The `make _report` rule adds a single proof to litani
+            # without running it
+            make _report;
+
+            popd;
+        done
+
+        litani run-build;
+
+except that it is much faster and provides some convenience options.
+The CBMC CI runs this script with no arguments to build and run all
+proofs in parallel. The value of "my-cool-project" is taken from the
+PROJECT_NAME variable in Makefile-project-defines.
+
+The --no-standalone argument omits the `litani init` and `litani
+run-build`; use it when you want to add additional proof jobs, not
+just the CBMC ones. In that case, you would run `litani init`
+yourself; then run `run-cbmc-proofs --no-standalone`; add any
+additional jobs that you want to execute with `litani add-job`; and
+finally run `litani run-build`.
+
+The litani dashboard will be written under the `output` directory; the
+cbmc-viewer reports remain in the `$PROOF_DIR/report` directory. The
+HTML dashboard from the latest Litani run will always be symlinked to
+`output/latest/html/index.html`, so you can keep that page open in
+your browser and reload the page whenever you re-run this script.
+"""
+# 70 characters stops here ----------------------------------------> |
+
+
+def get_project_name():
+    cmd = [
+        "make",
+        "--no-print-directory",
+        "-f", "Makefile.common",
+        "echo-project-name",
+    ]
+    logging.debug(" ".join(cmd))
+    proc = subprocess.run(cmd, universal_newlines=True, stdout=subprocess.PIPE, check=False)
+    if proc.returncode:
+        logging.critical("could not run make to determine project name")
+        sys.exit(1)
+    if not proc.stdout.strip():
+        logging.warning(
+            "project name has not been set; using generic name instead. "
+            "Set the PROJECT_NAME value in Makefile-project-defines to "
+            "remove this warning")
+        return "<PROJECT NAME HERE>"
+    return proc.stdout.strip()
+
+
+def get_args():
+    pars = argparse.ArgumentParser(
+        description=DESCRIPTION, epilog=EPILOG,
+        formatter_class=argparse.RawDescriptionHelpFormatter)
+    for arg in [{
+            "flags": ["-j", "--parallel-jobs"],
+            "type": int,
+            "metavar": "N",
+            "help": "run at most N proof jobs in parallel",
+    }, {
+            "flags": ["--fail-on-proof-failure"],
+            "action": "store_true",
+            "help": "exit with return code `10' if any proof failed"
+                    " (default: exit 0)",
+    }, {
+            "flags": ["--no-standalone"],
+            "action": "store_true",
+            "help": "only configure proofs: do not initialize nor run",
+    }, {
+            "flags": ["-p", "--proofs"],
+            "nargs": "+",
+            "metavar": "DIR",
+            "help": "only run proof in directory DIR (can pass more than one)",
+    }, {
+            "flags": ["--project-name"],
+            "metavar": "NAME",
+            "default": get_project_name(),
+            "help": "project name for report. Default: %(default)s",
+    }, {
+            "flags": ["--marker-file"],
+            "metavar": "FILE",
+            "default": "cbmc-proof.txt",
+            "help": (
+                "name of file that marks proof directories. Default: "
+                "%(default)s"),
+    }, {
+            "flags": ["--no-memory-profile"],
+            "action": "store_true",
+            "help": "disable memory profiling, even if Litani supports it"
+    }, {
+            "flags": ["--no-expensive-limit"],
+            "action": "store_true",
+            "help": "do not limit parallelism of 'EXPENSIVE' jobs",
+    }, {
+            "flags": ["--expensive-jobs-parallelism"],
+            "metavar": "N",
+            "default": 1,
+            "type": int,
+            "help": (
+                "how many proof jobs marked 'EXPENSIVE' to run in parallel. "
+                "Default: %(default)s"),
+    }, {
+            "flags": ["--verbose"],
+            "action": "store_true",
+            "help": "verbose output",
+    }, {
+            "flags": ["--debug"],
+            "action": "store_true",
+            "help": "debug output",
+    }, {
+            "flags": ["--summarize"],
+            "action": "store_true",
+            "help": "summarize proof results with two tables on stdout",
+    }, {
+            "flags": ["--version"],
+            "action": "version",
+            "version": "CBMC starter kit 2.5",
+            "help": "display version and exit"
+    }]:
+        flags = arg.pop("flags")
+        pars.add_argument(*flags, **arg)
+    return pars.parse_args()
+
+
+def set_up_logging(verbose):
+    if verbose:
+        level = logging.DEBUG
+    else:
+        level = logging.WARNING
+    logging.basicConfig(
+        format="run-cbmc-proofs: %(message)s", level=level)
+
+
+def task_pool_size():
+    ret = os.cpu_count()
+    if ret is None or ret < 3:
+        return 1
+    return ret - 2
+
+
+def print_counter(counter):
+    # pylint: disable=consider-using-f-string
+    print("\rConfiguring CBMC proofs: "
+          "{complete:{width}} / {total:{width}}".format(**counter), end="", file=sys.stderr)
+
+
+def get_proof_dirs(proof_root, proof_list, marker_file):
+    if proof_list is not None:
+        proofs_remaining = list(proof_list)
+    else:
+        proofs_remaining = []
+
+    for root, _, fyles in os.walk(proof_root):
+        proof_name = str(pathlib.Path(root).name)
+        if root != str(proof_root) and ".litani_cache_dir" in fyles:
+            pathlib.Path(f"{root}/.litani_cache_dir").unlink()
+        if proof_list and proof_name not in proof_list:
+            continue
+        if proof_list and proof_name in proofs_remaining:
+            proofs_remaining.remove(proof_name)
+        if marker_file in fyles:
+            yield root
+
+    if proofs_remaining:
+        logging.critical(
+            "The following proofs were not found: %s",
+            ", ".join(proofs_remaining))
+        sys.exit(1)
+
+
+def run_build(litani, jobs, fail_on_proof_failure, summarize):
+    cmd = [str(litani), "run-build"]
+    if jobs:
+        cmd.extend(["-j", str(jobs)])
+    if fail_on_proof_failure:
+        cmd.append("--fail-on-pipeline-failure")
+    if summarize:
+        out_file = pathlib.Path(tempfile.gettempdir(), "run.json").resolve()
+        cmd.extend(["--out-file", str(out_file)])
+
+    logging.debug(" ".join(cmd))
+    proc = subprocess.run(cmd, check=False)
+
+    if proc.returncode and not fail_on_proof_failure:
+        logging.critical("Failed to run litani run-build")
+        sys.exit(1)
+
+    if summarize:
+        print_proof_results(out_file)
+        out_file.unlink()
+
+    if proc.returncode:
+        logging.error("One or more proofs failed")
+        sys.exit(10)
+
+def get_litani_path(proof_root):
+    cmd = [
+        "make",
+        "--no-print-directory",
+        f"PROOF_ROOT={proof_root}",
+        "-f", "Makefile.common",
+        "litani-path",
+    ]
+    logging.debug(" ".join(cmd))
+    proc = subprocess.run(cmd, universal_newlines=True, stdout=subprocess.PIPE, check=False)
+    if proc.returncode:
+        logging.critical("Could not determine path to litani")
+        sys.exit(1)
+    return proc.stdout.strip()
+
+
+def get_litani_capabilities(litani_path):
+    cmd = [litani_path, "print-capabilities"]
+    proc = subprocess.run(
+        cmd, text=True, stdout=subprocess.PIPE, stderr=subprocess.DEVNULL, check=False)
+    if proc.returncode:
+        return []
+    try:
+        return json.loads(proc.stdout)
+    except RuntimeError:
+        logging.warning("Could not load litani capabilities: '%s'", proc.stdout)
+        return []
+
+
+def check_uid_uniqueness(proof_dir, proof_uids):
+    with (pathlib.Path(proof_dir) / "Makefile").open() as handle:
+        for line in handle:
+            match = re.match(r"^PROOF_UID\s*=\s*(?P<uid>\w+)", line)
+            if not match:
+                continue
+            if match["uid"] not in proof_uids:
+                proof_uids[match["uid"]] = proof_dir
+                return
+
+            logging.critical(
+                "The Makefile in directory '%s' should have a different "
+                "PROOF_UID than the Makefile in directory '%s'",
+                proof_dir, proof_uids[match["uid"]])
+            sys.exit(1)
+
+    logging.critical(
+        "The Makefile in directory '%s' should contain a line like", proof_dir)
+    logging.critical("PROOF_UID = ...")
+    logging.critical("with a unique identifier for the proof.")
+    sys.exit(1)
+
+
+def should_enable_memory_profiling(litani_caps, args):
+    if args.no_memory_profile:
+        return False
+    return "memory_profile" in litani_caps
+
+
+def should_enable_pools(litani_caps, args):
+    if args.no_expensive_limit:
+        return False
+    return "pools" in litani_caps
+
+
+async def configure_proof_dirs( # pylint: disable=too-many-arguments
+    queue, counter, proof_uids, enable_pools, enable_memory_profiling, debug):
+    while True:
+        print_counter(counter)
+        path = str(await queue.get())
+
+        check_uid_uniqueness(path, proof_uids)
+
+        pools = ["ENABLE_POOLS=true"] if enable_pools else []
+        profiling = [
+            "ENABLE_MEMORY_PROFILING=true"] if enable_memory_profiling else []
+
+        # Allow interactive tasks to preempt proof configuration
+        proc = await asyncio.create_subprocess_exec(
+            "nice", "-n", "15", "make", *pools,
+            *profiling, "-B", "_report", "" if debug else "--quiet", cwd=path,
+            stdout=asyncio.subprocess.PIPE, stderr=asyncio.subprocess.PIPE)
+        stdout, stderr = await proc.communicate()
+        logging.debug("returncode: %s", str(proc.returncode))
+        logging.debug("stdout:")
+        for line in stdout.decode().splitlines():
+            logging.debug(line)
+        logging.debug("stderr:")
+        for line in stderr.decode().splitlines():
+            logging.debug(line)
+
+        counter["fail" if proc.returncode else "pass"].append(path)
+        counter["complete"] += 1
+
+        print_counter(counter)
+        queue.task_done()
+
+
+async def main(): # pylint: disable=too-many-locals
+    args = get_args()
+    set_up_logging(args.verbose)
+
+    proof_root = pathlib.Path(os.getcwd())
+    litani = get_litani_path(proof_root)
+
+    litani_caps = get_litani_capabilities(litani)
+    enable_pools = should_enable_pools(litani_caps, args)
+    init_pools = [
+        "--pools", f"expensive:{args.expensive_jobs_parallelism}"
+    ] if enable_pools else []
+
+    if not args.no_standalone:
+        cmd = [
+            str(litani), "init", *init_pools, "--project", args.project_name,
+            "--no-print-out-dir",
+        ]
+
+        if "output_directory_flags" in litani_caps:
+            out_prefix = proof_root / "output"
+            out_symlink = out_prefix / "latest"
+            out_index = out_symlink / "html" / "index.html"
+            cmd.extend([
+                "--output-prefix", str(out_prefix),
+                "--output-symlink", str(out_symlink),
+            ])
+            print(
+                "\nFor your convenience, the output of this run will be symbolically linked to ",
+                out_index, "\n")
+
+        logging.debug(" ".join(cmd))
+        proc = subprocess.run(cmd, check=False)
+        if proc.returncode:
+            logging.critical("Failed to run litani init")
+            sys.exit(1)
+
+    proof_dirs = list(get_proof_dirs(
+        proof_root, args.proofs, args.marker_file))
+    if not proof_dirs:
+        logging.critical("No proof directories found")
+        sys.exit(1)
+
+    proof_queue = asyncio.Queue()
+    for proof_dir in proof_dirs:
+        proof_queue.put_nowait(proof_dir)
+
+    counter = {
+        "pass": [],
+        "fail": [],
+        "complete": 0,
+        "total": len(proof_dirs),
+        "width": int(math.log10(len(proof_dirs))) + 1
+    }
+
+    proof_uids = {}
+    tasks = []
+
+    enable_memory_profiling = should_enable_memory_profiling(litani_caps, args)
+
+    for _ in range(task_pool_size()):
+        task = asyncio.create_task(configure_proof_dirs(
+            proof_queue, counter, proof_uids, enable_pools,
+            enable_memory_profiling, args.debug))
+        tasks.append(task)
+
+    await proof_queue.join()
+
+    print_counter(counter)
+    print("", file=sys.stderr)
+
+    if counter["fail"]:
+        logging.critical(
+            "Failed to configure the following proofs:\n%s", "\n".join(
+                [str(f) for f in counter["fail"]]))
+        sys.exit(1)
+
+    if not args.no_standalone:
+        run_build(litani, args.parallel_jobs, args.fail_on_proof_failure, args.summarize)
+
+
+if __name__ == "__main__":
+    asyncio.run(main())

kernel/FreeRTOS-Plus/Source/AWS/device-shadow/test/cbmc/sources/README.md

@@ -0,0 +1,6 @@
+CBMC proof source code
+======================
+
+This directory contains source code written for CBMC proofs.  It is
+common to write some code to model aspects of the system under test,
+and this code goes here.

kernel/FreeRTOS-Plus/Source/AWS/device-shadow/test/cbmc/stubs/README.md

@@ -0,0 +1,6 @@
+CBMC proof stubs
+======================
+
+This directory contains the stubs written for CBMC proofs.  It is
+common to stub out functionality like network send and receive methods
+when writing a CBMC proof, and the code for these stubs goes here.