1#! /bin/sh 2 3# This file is dual-licensed. Choose whichever licence you want from 4# the two licences listed below. 5# 6# The first licence is a regular 2-clause BSD licence. The second licence 7# is the CC-0 from Creative Commons. It is intended to release Monocypher 8# to the public domain. The BSD licence serves as a fallback option. 9# 10# SPDX-License-Identifier: BSD-2-Clause OR CC0-1.0 11# 12# ------------------------------------------------------------------------ 13# 14# Copyright (c) 2017-2019, Loup Vaillant 15# All rights reserved. 16# 17# 18# Redistribution and use in source and binary forms, with or without 19# modification, are permitted provided that the following conditions are 20# met: 21# 22# 1. Redistributions of source code must retain the above copyright 23# notice, this list of conditions and the following disclaimer. 24# 25# 2. Redistributions in binary form must reproduce the above copyright 26# notice, this list of conditions and the following disclaimer in the 27# documentation and/or other materials provided with the 28# distribution. 29# 30# THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS 31# "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT 32# LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR 33# A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT 34# HOLDER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, 35# SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT 36# LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, 37# DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY 38# THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT 39# (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE 40# OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. 41# 42# ------------------------------------------------------------------------ 43# 44# Written in 2017-2019 by Loup Vaillant 45# 46# To the extent possible under law, the author(s) have dedicated all copyright 47# and related neighboring rights to this software to the public domain 48# worldwide. This software is distributed without any warranty. 49# 50# You should have received a copy of the CC0 Public Domain Dedication along 51# with this software. If not, see 52# <https://creativecommons.org/publicdomain/zero/1.0/> 53 54# Parses the source code 55frama-c tests/formal-analysis/*.c -save parsed.sav 56 57# Analyses the source code 58frama-c -load parsed.sav -val-builtins-auto -val -save value.sav -no-val-show-progress -memexec-all 59 60# Launches the Gui 61frama-c-gui -load value.sav 62