From 8aa89be49173206bd988cbed3138cfad8e0fbe8f Mon Sep 17 00:00:00 2001 From: Norbert Manthey Date: Wed, 25 Jan 2017 09:18:32 +0100 Subject: [PATCH 1/6] build: introduce LIBSOLVER environment variable When building solvers.a while aiming at building CBMC with support for IPASIR solvers, all projects that need SAT checkers would require to link against the provided libipasir.a library. To make this library visible for all subprojects at the same time, but furthermore allow the user to choose which library to pick, the variable LIBSOLVER was introduced, which is set to an empty value by default. To get started with the default ipasir package, run the following commands in the root directory of the repository: make ipasir-build -C src make -C src IPASIR=../../ipasir LIBSOLVER=$(pwd)/ipasir/libipasir.a --- src/config.inc | 4 ++++ src/solvers/Makefile | 2 +- 2 files changed, 5 insertions(+), 1 deletion(-) diff --git a/src/config.inc b/src/config.inc index 5c276dc19c6..1d365cfabf5 100644 --- a/src/config.inc +++ b/src/config.inc @@ -26,6 +26,10 @@ MINISAT2 = ../../minisat-2.2.1 #GLUCOSE = ../../glucose-syrup #SMVSAT = +# Extra library for SAT solver. This should link to the archive file to be used +# when linking against an IPASIR solver. +LIBSOLVER = + ifneq ($(PRECOSAT),) CP_CXXFLAGS += -DSATCHECK_PRECOSAT endif diff --git a/src/solvers/Makefile b/src/solvers/Makefile index a3e7219db4d..361ce1aba14 100644 --- a/src/solvers/Makefile +++ b/src/solvers/Makefile @@ -222,4 +222,4 @@ endif solvers$(LIBEXT): $(OBJ) $(CHAFF_LIB) $(BOOLEFORCE_LIB) $(MINISAT_LIB) \ $(MINISAT2_LIB) $(SMVSAT_LIB) $(SQUOLEM2_LIB) $(CUDD_LIB) \ $(PRECOSAT_LIB) $(PICOSAT_LIB) $(LINGELING_LIB) $(GLUCOSE_LIB) - $(LINKLIB) + $(LINKLIB) $(LIBSOLVER) From 14419d272e3036c1c50182fddeb923332bfbf96d Mon Sep 17 00:00:00 2001 From: Norbert Manthey Date: Wed, 18 Jan 2017 00:32:26 +0100 Subject: [PATCH 2/6] solvers: add ipasir driver Add the necessary source changes to allow CBMC to use IPASIR solvers. --- src/solvers/Makefile | 10 ++ src/solvers/prop/literal.h | 3 + src/solvers/sat/satcheck.h | 47 ++++++- src/solvers/sat/satcheck_ipasir.cpp | 196 ++++++++++++++++++++++++++++ src/solvers/sat/satcheck_ipasir.h | 59 +++++++++ 5 files changed, 314 insertions(+), 1 deletion(-) create mode 100644 src/solvers/sat/satcheck_ipasir.cpp create mode 100644 src/solvers/sat/satcheck_ipasir.h diff --git a/src/solvers/Makefile b/src/solvers/Makefile index 361ce1aba14..c8cbebee1a6 100644 --- a/src/solvers/Makefile +++ b/src/solvers/Makefile @@ -21,6 +21,14 @@ ifneq ($(MINISAT2),) CP_CXXFLAGS += -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS endif +ifneq ($(IPASIR),) + IPASIR_SRC=sat/satcheck_ipasir.cpp + IPASIR_INCLUDE=-I $(IPASIR) + IPASIR_LIB=$(IPASIR)/ipasir.a + CP_CXXFLAGS += -DHAVE_IPASIR -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS + override CXXFLAGS := $(filter-out -pedantic, $(CXXFLAGS)) +endif + ifneq ($(GLUCOSE),) GLUCOSE_SRC=sat/satcheck_glucose.cpp GLUCOSE_INCLUDE=-I $(GLUCOSE) @@ -82,6 +90,7 @@ SRC = $(BOOLEFORCE_SRC) \ $(GLUCOSE_SRC) \ $(LINGELING_SRC) \ $(MINISAT2_SRC) \ + $(IPASIR_SRC) \ $(MINISAT_SRC) \ $(PICOSAT_SRC) \ $(PRECOSAT_SRC) \ @@ -198,6 +207,7 @@ SRC = $(BOOLEFORCE_SRC) \ INCLUDES += -I .. \ $(CHAFF_INCLUDE) $(BOOLEFORCE_INCLUDE) $(MINISAT_INCLUDE) $(MINISAT2_INCLUDE) \ + $(IPASIR_INCLUDE) \ $(SMVSAT_INCLUDE) $(SQUOLEM2_INC) $(CUDD_INCLUDE) $(GLUCOSE_INCLUDE) \ $(PRECOSAT_INCLUDE) $(PICOSAT_INCLUDE) $(LINGELING_INCLUDE) diff --git a/src/solvers/prop/literal.h b/src/solvers/prop/literal.h index 24e62ba599a..7e93efe052c 100644 --- a/src/solvers/prop/literal.h +++ b/src/solvers/prop/literal.h @@ -193,6 +193,9 @@ inline literalt neg(literalt a) { return !a; } inline literalt pos(literalt a) { return a; } +inline bool is_false (const literalt &l) { return (l.is_false()); } +inline bool is_true (const literalt &l) { return (l.is_true()); } + // bit-vectors typedef std::vector bvt; diff --git a/src/solvers/sat/satcheck.h b/src/solvers/sat/satcheck.h index 4905f3195ee..cc20e33476a 100644 --- a/src/solvers/sat/satcheck.h +++ b/src/solvers/sat/satcheck.h @@ -10,7 +10,9 @@ Author: Daniel Kroening, kroening@kroening.com #ifndef CPROVER_SOLVERS_SAT_SATCHECK_H #define CPROVER_SOLVERS_SAT_SATCHECK_H -// this picks the "default" SAT solver +// This sets a define for the SAT solver +// based on set flags that come via the compiler +// command line. // #define SATCHECK_ZCHAFF // #define SATCHECK_MINISAT1 @@ -21,6 +23,42 @@ Author: Daniel Kroening, kroening@kroening.com // #define SATCHECK_PICOSAT // #define SATCHECK_LINGELING +#if defined(HAVE_IPASIR) && !defined(SATCHECK_IPASIR) +#define SATCHECK_IPASIR +#endif + +#if defined(HAVE_ZCHAFF) && !defined(SATCHECK_ZCHAFF) +#define SATCHECK_ZCHAFF +#endif + +#if defined(HAVE_MINISAT1) && !defined(SATCHECK_MINISAT1) +#define SATCHECK_MINISAT1 +#endif + +#if defined(HAVE_MINISAT2) && !defined(SATCHECK_MINISAT2) +#define SATCHECK_MINISAT2 +#endif + +#if defined(HAVE_GLUCOSE) && !defined(SATCHECK_GLUCOSE) +#define SATCHECK_GLUCOSE +#endif + +#if defined(HAVE_BOOLEFORCE) && !defined(SATCHECK_BOOLEFORCE) +#define SATCHECK_BOOLEFORCE +#endif + +#if defined(HAVE_PRECOSAT) && !defined(SATCHECK_PRECOSAT) +#define SATCHECK_PRECOSAT +#endif + +#if defined(HAVE_PICOSAT) && !defined(SATCHECK_PICOSAT) +#define SATCHECK_PICOSAT +#endif + +#if defined(HAVE_LINGELING) && !defined(SATCHECK_LINGELING) +#define SATCHECK_LINGELING +#endif + #if defined SATCHECK_ZCHAFF #include "satcheck_zchaff.h" @@ -49,6 +87,13 @@ typedef satcheck_minisat1t satcheck_no_simplifiert; typedef satcheck_minisat_simplifiert satcheckt; typedef satcheck_minisat_no_simplifiert satcheck_no_simplifiert; +#elif defined SATCHECK_IPASIR + +#include "satcheck_ipasir.h" + +typedef satcheck_ipasirt satcheckt; +typedef satcheck_ipasirt satcheck_no_simplifiert; + #elif defined SATCHECK_PRECOSAT #include "satcheck_precosat.h" diff --git a/src/solvers/sat/satcheck_ipasir.cpp b/src/solvers/sat/satcheck_ipasir.cpp new file mode 100644 index 00000000000..6c91de27fa0 --- /dev/null +++ b/src/solvers/sat/satcheck_ipasir.cpp @@ -0,0 +1,196 @@ +/*******************************************************************\ + +Module: External SAT Solver Binding + +Author: Norbert Manthey, nmanthey@amazon.com + +\*******************************************************************/ + +#ifndef _MSC_VER +#include +#endif + +#include +#include +#include + +#include + +#include "satcheck_ipasir.h" + +#ifdef HAVE_IPASIR + +extern "C" +{ +#include +} + +/* + +Interface description: +https://github.com/biotomas/ipasir/blob/master/ipasir.h + +Representation: +Variables for a formula start with 1! 0 is used as termination symbol. + +*/ + +tvt satcheck_ipasirt::l_get(literalt a) const +{ + if(a.is_true()) + return tvt(true); + else if(a.is_false()) + return tvt(false); + + tvt result; + + // compare to internal no_variables number + if(a.var_no()>=(unsigned)no_variables()) + return tvt::unknown(); + + const int val=ipasir_val(solver, a.var_no()); + + if(val>0) + result=tvt(true); + else if(val<0) + result=tvt(false); + else + return tvt::unknown(); + + if(a.sign()) + result=!result; + + return result; +} + +const std::string satcheck_ipasirt::solver_text() +{ + return std::string(ipasir_signature()); +} + +void satcheck_ipasirt::lcnf(const bvt &bv) +{ + forall_literals(it, bv) + { + if(it->is_true()) + return; + else if(!it->is_false()) + INVARIANT(it->var_no()<(unsigned)no_variables(), + "reject out of bound variables"); + } + + forall_literals(it, bv) + { + if(!it->is_false()) + { + // add literal with correct sign + ipasir_add(solver, it->dimacs()); + } + } + ipasir_add(solver, 0); // terminate clause + + clause_counter++; +} + +propt::resultt satcheck_ipasirt::prop_solve() +{ + INVARIANT(status!=statust::ERROR, "there cannot be an error"); + + { + messaget::status() << + (no_variables()-1) << " variables, " << + clause_counter << " clauses" << eom; + } + + // use the internal representation, as ipasir does not support reporting the + // status + if(status==statust::UNSAT) + { + messaget::status() << + "SAT checker inconsistent: instance is UNSATISFIABLE" << eom; + } + else + { + // if assumptions contains false, we need this to be UNSAT + bvt::const_iterator it = std::find_if(assumptions.begin(), + assumptions.end(), is_false); + const bool has_false = it != assumptions.end(); + + if(has_false) + { + messaget::status() << + "got FALSE as assumption: instance is UNSATISFIABLE" << eom; + } + else + { + forall_literals(it, assumptions) + if(!it->is_false()) + ipasir_assume(solver, it->dimacs()); + + // solve the formula, and handle the return code (10=SAT, 20=UNSAT) + int solver_state=ipasir_solve(solver); + if(10==solver_state) + { + messaget::status() << + "SAT checker: instance is SATISFIABLE" << eom; + status=statust::SAT; + return resultt::P_SATISFIABLE; + } + else if(20==solver_state) + { + messaget::status() << + "SAT checker: instance is UNSATISFIABLE" << eom; + } + else + { + messaget::status() << + "SAT checker: solving returned without solution" << eom; + throw "solving inside IPASIR SAT solver has been interrupted"; + } + } + } + + status=statust::UNSAT; + return resultt::P_UNSATISFIABLE; +} + +void satcheck_ipasirt::set_assignment(literalt a, bool value) +{ + INVARIANT(!a.is_constant(), "cannot set an assignment for a constant"); + INVARIANT(false, "method not supported"); +} + +satcheck_ipasirt::satcheck_ipasirt() +: solver(nullptr) +{ + INVARIANT(!solver, "there cannot be a solver already"); + solver=ipasir_init(); +} + +satcheck_ipasirt::~satcheck_ipasirt() +{ + if(solver) + ipasir_release(solver); + solver=nullptr; +} + +bool satcheck_ipasirt::is_in_conflict(literalt a) const +{ + return ipasir_failed(solver, a.var_no()); +} + +void satcheck_ipasirt::set_assumptions(const bvt &bv) +{ + bvt::const_iterator it = std::find_if(bv.begin(), bv.end(), is_true); + const bool has_true = it != bv.end(); + + if(has_true) + { + assumptions.clear(); + return; + } + // only copy assertions, if there is no false in bt parameter + assumptions=bv; +} + +#endif diff --git a/src/solvers/sat/satcheck_ipasir.h b/src/solvers/sat/satcheck_ipasir.h new file mode 100644 index 00000000000..0536e535a87 --- /dev/null +++ b/src/solvers/sat/satcheck_ipasir.h @@ -0,0 +1,59 @@ +/*******************************************************************\ + +Module: + +Author: Norbert Manthey, nmanthey@amazon.com + +Sample compilation command: +(to be executed from base directory of project) + +make clean +make ipasir-build +CXXFLAGS=-g IPASIR=../../ipasir LIBSOLVER=$(pwd)/ipasir/libipasir.a \ + CFLAGS="-Wall -O2 -DSATCHECK_IPSAIR" LINKFLAGS="-static" \ + make -j 7 -C $(pwd)/src/; + +Note: Make sure, the LIBSOLVER variable is set in the environment! + The variable should point to the solver you actually want to + link against. + +\*******************************************************************/ + +#ifndef CPROVER_SOLVERS_SAT_SATCHECK_IPASIR_H +#define CPROVER_SOLVERS_SAT_SATCHECK_IPASIR_H + +#include "cnf.h" + +/// Interface for generic SAT solver interface IPASIR +class satcheck_ipasirt:public cnf_solvert +{ +public: + satcheck_ipasirt(); + virtual ~satcheck_ipasirt() override; + + /// This method returns the description produced by the linked SAT solver + virtual const std::string solver_text() override; + + virtual resultt prop_solve() override; + + /// This method returns the truth value for a literal of the current SAT model + virtual tvt l_get(literalt a) const override final; + + virtual void lcnf(const bvt &bv) override final; + + /* This method is not supported, and currently not called anywhere in CBMC */ + virtual void set_assignment(literalt a, bool value) override; + + virtual void set_assumptions(const bvt &_assumptions) override; + + virtual bool is_in_conflict(literalt a) const override; + virtual bool has_set_assumptions() const override final { return true; } + virtual bool has_is_in_conflict() const override final { return true; } + +protected: + void *solver; + + bvt assumptions; +}; + +#endif // CPROVER_SOLVERS_SAT_SATCHECK_IPASIR_H From 12a69173e568337c9bb49bce39fec9e672da8b6f Mon Sep 17 00:00:00 2001 From: Norbert Manthey Date: Wed, 18 Jan 2017 00:32:04 +0100 Subject: [PATCH 3/6] build: add ipasir solver support Add necessary steps to set variables for IPASIR Furthermore, allow to select SAT solver from make command line, for example by calling IPASIR=../../ipasir LIBSOLVER=$(pwd)/ipasir/libipasir.a make Note, to compile with a different SAT solver, e.g. GLUCOSE=../../glucose-syrup make it has to be ensured, that the solvers.a library is rebuild, and all components that link against this library are renewed as well. This can be achieved by touching the satcheck.h flie, i.e.: touch src/solvers/sat/satcheck.h --- src/Makefile | 15 ++++++++++++++- src/common | 42 ++++++++++++++++++++++++++++++++++++++++++ src/config.inc | 3 ++- 3 files changed, 58 insertions(+), 2 deletions(-) diff --git a/src/Makefile b/src/Makefile index 3f53a79fc32..365336893c7 100644 --- a/src/Makefile +++ b/src/Makefile @@ -93,4 +93,17 @@ cprover-jar-build: cd target; jar cf org.cprover.jar `find . -name "*.class"`; \ mv org.cprover.jar ../../../) -.PHONY: minisat2-download glucose-download cprover-jar-build +ipasir-download: + # get the 2016 version of the ipasir package, which contains a few solvers + @echo "Download ipasir 2016 package" + @(lwp-download http://baldur.iti.kit.edu/sat-competition-2016/downloads/ipasir.zip ../ipasir.zip) + @(cd ..; unzip -u ipasir.zip) + +ipasir-build: ipasir-download + # build libpicosat, and create a libipasir.a in ipasir directory + # make sure that the ipasir.h file is located there as well (ships with 2016 package) + @echo "Build Picosat 961 from ipasir 2016 package" + $(MAKE) -C ../ipasir/sat/picosat961 libipasirpicosat961.a + @(cd ../ipasir; ln -sf sat/picosat961/libipasirpicosat961.a libipasir.a) + +.PHONY: ipasir-build minisat2-download glucose-download cprover-jar-build diff --git a/src/common b/src/common index ad74f211928..fd093cc69af 100644 --- a/src/common +++ b/src/common @@ -155,6 +155,48 @@ else $(error Invalid setting for BUILD_ENV: $(BUILD_ENV_)) endif +# select default solver to be minisat2 if no other is specified +ifeq ($(BOOLEFORCE)$(CHAFF)$(GLUCOSE)$(IPASIR)$(LINGELING)$(MINISAT)$(MINISAT2)$(PICOSAT)$(PRECOSAT),) + MINISAT2 = ../../minisat-2.2.1 +endif + +ifneq ($(IPASIR),) + CP_CXXFLAGS += -DHAVE_IPASIR +endif + +ifneq ($(PRECOSAT),) + CP_CXXFLAGS += -DHAVE_PRECOSAT +endif + +ifneq ($(PICOSAT),) + CP_CXXFLAGS += -DHAVE_PICOSAT +endif + +ifneq ($(LINGELING),) + CP_CXXFLAGS += -DHAVE_LINGELING +endif + +ifneq ($(CHAFF),) + CP_CXXFLAGS += -DHAVE_CHAFF +endif + +ifneq ($(BOOLEFORCE),) + CP_CXXFLAGS += -DHAVE_BOOLEFORCE +endif + +ifneq ($(MINISAT),) + CP_CXXFLAGS += -DHAVE_MINISAT +endif + +ifneq ($(MINISAT2),) + CP_CXXFLAGS += -DHAVE_MINISAT2 +endif + +ifneq ($(GLUCOSE),) + CP_CXXFLAGS += -DHAVE_GLUCOSE +endif + + first_target: all diff --git a/src/config.inc b/src/config.inc index 1d365cfabf5..93b44e39a50 100644 --- a/src/config.inc +++ b/src/config.inc @@ -22,7 +22,8 @@ endif #CHAFF = ../../zChaff #BOOLEFORCE = ../../booleforce-0.4 #MINISAT = ../../MiniSat-p_v1.14 -MINISAT2 = ../../minisat-2.2.1 +#MINISAT2 = ../../minisat-2.2.1 +#IPASIR = ../../ipasir #GLUCOSE = ../../glucose-syrup #SMVSAT = From 751208d28edc6b5a9728efc86db31d65f554b303 Mon Sep 17 00:00:00 2001 From: Norbert Manthey Date: Wed, 4 Oct 2017 23:15:05 +0200 Subject: [PATCH 4/6] tests: drop number of iterations When checking for success or failure of a test, the number of iterations in the actual test should be irrelevant. As MiniSAT and PicoSAT seem to disagree on this number, do not check for it, so that the testis pass again. --- regression/cbmc-concurrency/pthread_join1/test.desc | 2 +- regression/cbmc-cover/mcdc1/test.desc | 2 +- regression/cbmc-cover/mcdc11/test.desc | 2 +- regression/cbmc-cover/mcdc12/test.desc | 2 +- regression/cbmc-cover/mcdc14/test.desc | 2 +- regression/cbmc-cover/mcdc3/test.desc | 2 +- regression/cbmc-cover/mcdc4/test.desc | 2 +- regression/cbmc-cover/mcdc6/test.desc | 2 +- regression/cbmc-cover/mcdc7/test.desc | 2 +- regression/cbmc-cover/mcdc8/test.desc | 2 +- regression/cbmc-cover/mcdc9/test.desc | 2 +- regression/cbmc-java/exceptions1/test.desc | 2 +- regression/cbmc-java/exceptions2/test.desc | 2 +- regression/cbmc-with-incr/Multi_Dimensional_Array6/test.desc | 2 +- regression/cbmc-with-incr/Pointer_byte_extract2/test.desc | 2 +- regression/cbmc-with-incr/Pointer_byte_extract5/test.desc | 2 +- regression/cbmc-with-incr/Pointer_byte_extract8/test.desc | 2 +- regression/cbmc-with-incr/pipe1/test.desc | 2 +- regression/cbmc/Malloc23/test.desc | 2 +- regression/cbmc/Multi_Dimensional_Array6/test.desc | 2 +- regression/cbmc/Pointer_byte_extract2/test.desc | 2 +- regression/cbmc/Pointer_byte_extract5/test.desc | 2 +- regression/cbmc/Pointer_byte_extract8/test.desc | 2 +- regression/cbmc/Quantifiers-assertion/test.desc | 2 +- regression/cbmc/Quantifiers-assignment/test.desc | 2 +- regression/cbmc/Quantifiers-if/test.desc | 2 +- regression/cbmc/Quantifiers-initialisation2/test.desc | 2 +- regression/cbmc/Quantifiers-not/test.desc | 2 +- regression/cbmc/Quantifiers-type/test.desc | 2 +- regression/cbmc/fgets1/test.desc | 2 +- regression/cbmc/memory_allocation1/test.desc | 2 +- regression/cbmc/memset1/test.desc | 2 +- regression/cbmc/pipe1/test.desc | 2 +- regression/cbmc/pointer-function-parameters-2/test.desc | 2 +- regression/cbmc/pointer-function-parameters/test.desc | 2 +- regression/strings/test_pass1/test.desc | 2 +- 36 files changed, 36 insertions(+), 36 deletions(-) diff --git a/regression/cbmc-concurrency/pthread_join1/test.desc b/regression/cbmc-concurrency/pthread_join1/test.desc index 41b36c525bf..bf4baf2d440 100644 --- a/regression/cbmc-concurrency/pthread_join1/test.desc +++ b/regression/cbmc-concurrency/pthread_join1/test.desc @@ -5,6 +5,6 @@ main.c ^SIGNAL=0$ ^\[main\.assertion\.1\] assertion i==1: FAILURE$ ^\[main\.assertion\.2\] assertion i==2: SUCCESS$ -^\*\* 1 of 2 failed \(2 iterations\)$ +^\*\* 1 of 2 failed -- ^warning: ignoring diff --git a/regression/cbmc-cover/mcdc1/test.desc b/regression/cbmc-cover/mcdc1/test.desc index d1779e15ce6..dbf4cb8d116 100644 --- a/regression/cbmc-cover/mcdc1/test.desc +++ b/regression/cbmc-cover/mcdc1/test.desc @@ -10,6 +10,6 @@ main.c ^\[main.coverage.5\] file main.c line 14 function main MC/DC independence condition `C && D && E && !A && B.*: SATISFIED$ ^\[main.coverage.6\] file main.c line 14 function main MC/DC independence condition `C && D && E && !A && !B.*: SATISFIED$ ^\*\* .* of .* covered \(100.0%\)$ -^\*\* Used 10 iterations$ +^\*\* Used -- ^warning: ignoring diff --git a/regression/cbmc-cover/mcdc11/test.desc b/regression/cbmc-cover/mcdc11/test.desc index 2358a5feb12..42ec4c2e750 100644 --- a/regression/cbmc-cover/mcdc11/test.desc +++ b/regression/cbmc-cover/mcdc11/test.desc @@ -10,6 +10,6 @@ main.c ^\[main.coverage.11\] file main.c line 12 function main MC/DC independence condition `!\(C != FALSE\) && D != FALSE.*: SATISFIED$ ^\[main.coverage.12\] file main.c line 12 function main MC/DC independence condition `!\(C != FALSE\) && !\(D != FALSE\).*: SATISFIED$ ^\*\* .* of .* covered \(100.0%\)$ -^\*\* Used 6 iterations$ +^\*\* Used -- ^warning: ignoring diff --git a/regression/cbmc-cover/mcdc12/test.desc b/regression/cbmc-cover/mcdc12/test.desc index 341ceb9da53..614ebbe3872 100644 --- a/regression/cbmc-cover/mcdc12/test.desc +++ b/regression/cbmc-cover/mcdc12/test.desc @@ -13,6 +13,6 @@ main.c ^\[main.coverage.20\] file main.c line 25 function main MC/DC independence condition `!\(E != FALSE\) && F != FALSE.*: SATISFIED$ ^\[main.coverage.21\] file main.c line 25 function main MC/DC independence condition `!\(E != FALSE\) && !\(F != FALSE\).*: SATISFIED$ ^\*\* .* of .* covered \(100.0%\)$ -^\*\* Used 10 iterations$ +^\*\* Used -- ^warning: ignoring diff --git a/regression/cbmc-cover/mcdc14/test.desc b/regression/cbmc-cover/mcdc14/test.desc index de3fd57033c..df4eaa08f1e 100644 --- a/regression/cbmc-cover/mcdc14/test.desc +++ b/regression/cbmc-cover/mcdc14/test.desc @@ -6,6 +6,6 @@ main.c ^\[main.coverage.1\] file main.c line 7 function main decision/condition `altitude > 2500.* SATISFIED$ ^\[main.coverage.2\] file main.c line 7 function main decision/condition `altitude > 2500.* SATISFIED$ ^\*\* .* of .* covered \(100.0%\)$ -^\*\* Used 2 iterations$ +^\*\* Used -- ^warning: ignoring diff --git a/regression/cbmc-cover/mcdc3/test.desc b/regression/cbmc-cover/mcdc3/test.desc index 0a531a3b9ba..8963f48b2da 100644 --- a/regression/cbmc-cover/mcdc3/test.desc +++ b/regression/cbmc-cover/mcdc3/test.desc @@ -7,6 +7,6 @@ main.c ^\[main.coverage.2\] file main.c line 8 function main MC/DC independence condition `y < \(unsigned int\)5 && !\(x > \(unsigned int\)3\).*: SATISFIED$ ^\[main.coverage.3\] file main.c line 8 function main MC/DC independence condition `y < \(unsigned int\)5 && x > \(unsigned int\)3.*: SATISFIED$ ^\*\* .* of .* covered \(100.0%\)$ -^\*\* Used 4 iterations$ +^\*\* Used -- ^warning: ignoring diff --git a/regression/cbmc-cover/mcdc4/test.desc b/regression/cbmc-cover/mcdc4/test.desc index 9ed8f0e7fce..a5d8e5a8e00 100644 --- a/regression/cbmc-cover/mcdc4/test.desc +++ b/regression/cbmc-cover/mcdc4/test.desc @@ -9,6 +9,6 @@ main.c ^\[main.coverage.4\] file main.c line 11 function main MC/DC independence condition `!C && D && A && !B.*: SATISFIED$ ^\[main.coverage.5\] file main.c line 11 function main MC/DC independence condition `!A && B && C && !D.*: SATISFIED$ ^\*\* .* of .* covered \(100.0%\)$ -^\*\* Used 9 iterations$ +^\*\* Used -- ^warning: ignoring diff --git a/regression/cbmc-cover/mcdc6/test.desc b/regression/cbmc-cover/mcdc6/test.desc index 7f5289c868d..7a33eb16b65 100644 --- a/regression/cbmc-cover/mcdc6/test.desc +++ b/regression/cbmc-cover/mcdc6/test.desc @@ -6,6 +6,6 @@ main.c ^\[main.coverage.1\] file main.c line 7 function main decision/condition `x < \(unsigned int\)3.* false: SATISFIED$ ^\[main.coverage.2\] file main.c line 7 function main decision/condition `x < \(unsigned int\)3.* true: SATISFIED$ ^\*\* .* of .* covered \(100.0%\)$ -^\*\* Used 2 iterations$ +^\*\* Used -- ^warning: ignoring diff --git a/regression/cbmc-cover/mcdc7/test.desc b/regression/cbmc-cover/mcdc7/test.desc index 7df603190cd..9c3858a3caf 100644 --- a/regression/cbmc-cover/mcdc7/test.desc +++ b/regression/cbmc-cover/mcdc7/test.desc @@ -8,6 +8,6 @@ main.c ^\[main.coverage.3\] file main.c line 8 function main decision/condition `x \* 123 < 0.* false: SATISFIED$ ^\[main.coverage.4\] file main.c line 8 function main decision/condition `x \* 123 < 0.* true: SATISFIED$ ^\*\* .* of .* covered \(100.0%\)$ -^\*\* Used 2 iterations$ +^\*\* Used -- ^warning: ignoring diff --git a/regression/cbmc-cover/mcdc8/test.desc b/regression/cbmc-cover/mcdc8/test.desc index f1711f5c8d1..cc12b098869 100644 --- a/regression/cbmc-cover/mcdc8/test.desc +++ b/regression/cbmc-cover/mcdc8/test.desc @@ -8,6 +8,6 @@ main.c ^\[main.coverage.3\] file main.c line 9 function main MC/DC independence condition `c != FALSE && !\(a != FALSE\) && !\(b != FALSE\).* SATISFIED$ ^\[main.coverage.4\] file main.c line 9 function main MC/DC independence condition `!\(c != FALSE\) && a != FALSE && !\(b != FALSE\).* SATISFIED$ ^\*\* .* of .* covered \(100.0%\)$ -^\*\* Used 6 iterations$ +^\*\* Used -- ^warning: ignoring diff --git a/regression/cbmc-cover/mcdc9/test.desc b/regression/cbmc-cover/mcdc9/test.desc index 3dbd096e9be..47045c120cd 100644 --- a/regression/cbmc-cover/mcdc9/test.desc +++ b/regression/cbmc-cover/mcdc9/test.desc @@ -9,6 +9,6 @@ main.c ^\[main.coverage.12\] file main.c line 16 function main MC/DC independence condition `!\(A != FALSE\) && B != FALSE && C != FALSE && !\(D != FALSE\).* SATISFIED$ ^\[main.coverage.13\] file main.c line 16 function main MC/DC independence condition `!\(A != FALSE\) && !\(B != FALSE\) && C != FALSE && !\(D != FALSE\).* SATISFIED$ ^\*\* .* of .* covered \(100.0%\)$ -^\*\* Used 8 iterations$ +^\*\* Used -- ^warning: ignoring diff --git a/regression/cbmc-java/exceptions1/test.desc b/regression/cbmc-java/exceptions1/test.desc index 1405444f649..bf588a879d5 100644 --- a/regression/cbmc-java/exceptions1/test.desc +++ b/regression/cbmc-java/exceptions1/test.desc @@ -4,7 +4,7 @@ test.class ^EXIT=10$ ^SIGNAL=0$ ^.*assertion at file test.java line 26 function.*: FAILURE$ -\*\* 1 of [0-9]* failed \(2 iterations\)$ +\*\* 1 of [0-9]* failed ^VERIFICATION FAILED$ -- ^warning: ignoring diff --git a/regression/cbmc-java/exceptions2/test.desc b/regression/cbmc-java/exceptions2/test.desc index 724e37b0677..85422de8707 100644 --- a/regression/cbmc-java/exceptions2/test.desc +++ b/regression/cbmc-java/exceptions2/test.desc @@ -4,7 +4,7 @@ test.class ^EXIT=10$ ^SIGNAL=0$ ^.*assertion at file test.java line 15 function.*: FAILURE$ -^\*\* 1 of [0-9]* failed \(2 iterations\)$ +^\*\* 1 of [0-9]* failed ^VERIFICATION FAILED$ -- ^warning: ignoring diff --git a/regression/cbmc-with-incr/Multi_Dimensional_Array6/test.desc b/regression/cbmc-with-incr/Multi_Dimensional_Array6/test.desc index d8033224594..c171dd49a18 100644 --- a/regression/cbmc-with-incr/Multi_Dimensional_Array6/test.desc +++ b/regression/cbmc-with-incr/Multi_Dimensional_Array6/test.desc @@ -5,6 +5,6 @@ main.c ^SIGNAL=0$ ^\[main\.assertion\.1\] assertion matriz\[\(signed long int\)j\]\[\(signed long int\)k\] <= maior: OK$ ^\[main\.assertion\.2\] assertion matriz\[\(signed long int\)0\]\[\(signed long int\)0\] < maior: FAILED$ -^\*\* 1 of 2 failed \(2 iterations\)$ +^\*\* 1 of 2 failed -- ^warning: ignoring diff --git a/regression/cbmc-with-incr/Pointer_byte_extract2/test.desc b/regression/cbmc-with-incr/Pointer_byte_extract2/test.desc index cf4a284351e..ad9c2b40bd5 100644 --- a/regression/cbmc-with-incr/Pointer_byte_extract2/test.desc +++ b/regression/cbmc-with-incr/Pointer_byte_extract2/test.desc @@ -4,6 +4,6 @@ main.c ^EXIT=10$ ^SIGNAL=0$ ^\[main\.assertion\.2\] .*: FAILED$ -^\*\* 1 of 2 failed \(2 iterations\)$ +^\*\* 1 of 2 failed -- ^warning: ignoring diff --git a/regression/cbmc-with-incr/Pointer_byte_extract5/test.desc b/regression/cbmc-with-incr/Pointer_byte_extract5/test.desc index b2bf0ea5879..47c1a75edbe 100644 --- a/regression/cbmc-with-incr/Pointer_byte_extract5/test.desc +++ b/regression/cbmc-with-incr/Pointer_byte_extract5/test.desc @@ -4,6 +4,6 @@ main.c ^EXIT=10$ ^SIGNAL=0$ ^\[main\.array_bounds\.5\] array.List upper bound in .*: FAILED$ -^\*\* 1 of 9 failed \(2 iterations\)$ +^\*\* 1 of 9 failed -- ^warning: ignoring diff --git a/regression/cbmc-with-incr/Pointer_byte_extract8/test.desc b/regression/cbmc-with-incr/Pointer_byte_extract8/test.desc index a2ae3807cab..a8688dd7116 100644 --- a/regression/cbmc-with-incr/Pointer_byte_extract8/test.desc +++ b/regression/cbmc-with-incr/Pointer_byte_extract8/test.desc @@ -4,6 +4,6 @@ main.c ^EXIT=0$ ^SIGNAL=0$ ^\[main\.array_bounds\.5\] array.List upper bound: FAILED$ -^\*\* 1 of 9 failed \(2 iterations\)$ +^\*\* 1 of 9 failed -- ^warning: ignoring diff --git a/regression/cbmc-with-incr/pipe1/test.desc b/regression/cbmc-with-incr/pipe1/test.desc index 95e607f531d..0d1e9fa0dba 100644 --- a/regression/cbmc-with-incr/pipe1/test.desc +++ b/regression/cbmc-with-incr/pipe1/test.desc @@ -4,6 +4,6 @@ main.c ^EXIT=10$ ^SIGNAL=0$ ^\[main\.assertion\.4\] assertion data\[1\]==31: FAILED$ -^\*\* 1 of 5 failed \(2 iterations\)$ +^\*\* 1 of 5 failed -- ^warning: ignoring diff --git a/regression/cbmc/Malloc23/test.desc b/regression/cbmc/Malloc23/test.desc index 4bd6cbdc141..4827431dc9c 100644 --- a/regression/cbmc/Malloc23/test.desc +++ b/regression/cbmc/Malloc23/test.desc @@ -7,6 +7,6 @@ pointer outside dynamic object bounds in \*p: FAILURE pointer outside dynamic object bounds in \*p: FAILURE pointer outside dynamic object bounds in p2\[.*1\]: FAILURE pointer outside dynamic object bounds in p2\[.*0\]: FAILURE -\*\* 4 of 36 failed \(3 iterations\) +\*\* 4 of 36 failed -- ^warning: ignoring diff --git a/regression/cbmc/Multi_Dimensional_Array6/test.desc b/regression/cbmc/Multi_Dimensional_Array6/test.desc index 101a4c0e3bf..a0a32880488 100644 --- a/regression/cbmc/Multi_Dimensional_Array6/test.desc +++ b/regression/cbmc/Multi_Dimensional_Array6/test.desc @@ -5,6 +5,6 @@ main.c ^SIGNAL=0$ ^\[main\.assertion\.1\] : SUCCESS$ ^\[main\.assertion\.2\] : FAILURE$ -^\*\* 1 of 2 failed \(2 iterations\)$ +^\*\* 1 of 2 failed -- ^warning: ignoring diff --git a/regression/cbmc/Pointer_byte_extract2/test.desc b/regression/cbmc/Pointer_byte_extract2/test.desc index 888430312a7..eb98d4f78ba 100644 --- a/regression/cbmc/Pointer_byte_extract2/test.desc +++ b/regression/cbmc/Pointer_byte_extract2/test.desc @@ -4,6 +4,6 @@ main.c ^EXIT=10$ ^SIGNAL=0$ ^\[main\.assertion\.2\] .*: FAILURE$ -^\*\* 1 of 2 failed \(2 iterations\)$ +^\*\* 1 of 2 failed -- ^warning: ignoring diff --git a/regression/cbmc/Pointer_byte_extract5/test.desc b/regression/cbmc/Pointer_byte_extract5/test.desc index 8c70c85ee47..fa59dbff9dc 100644 --- a/regression/cbmc/Pointer_byte_extract5/test.desc +++ b/regression/cbmc/Pointer_byte_extract5/test.desc @@ -4,6 +4,6 @@ main.c ^EXIT=10$ ^SIGNAL=0$ array\.List dynamic object upper bound in p->List\[2\]: FAILURE -\*\* 1 of 11 failed \(2 iterations\) +\*\* 1 of 11 failed -- ^warning: ignoring diff --git a/regression/cbmc/Pointer_byte_extract8/test.desc b/regression/cbmc/Pointer_byte_extract8/test.desc index 801d41ee41b..25368d1f99d 100644 --- a/regression/cbmc/Pointer_byte_extract8/test.desc +++ b/regression/cbmc/Pointer_byte_extract8/test.desc @@ -4,6 +4,6 @@ main.c ^EXIT=0$ ^SIGNAL=0$ ^\[main\.array_bounds\.5\] array.List upper bound: FAILED$ -^\*\* 1 of 9 failed \(2 iterations\)$ +^\*\* 1 of 9 failed -- ^warning: ignoring diff --git a/regression/cbmc/Quantifiers-assertion/test.desc b/regression/cbmc/Quantifiers-assertion/test.desc index df26ad98dbe..ccab2f3936c 100644 --- a/regression/cbmc/Quantifiers-assertion/test.desc +++ b/regression/cbmc/Quantifiers-assertion/test.desc @@ -8,5 +8,5 @@ main.c ^\[main.assertion.4\] NotExists-Forall: failed: FAILURE$ ^\[main.assertion.5\] NotForall-Forall: successful: SUCCESS$ ^\[main.assertion.6\] NotForall-NotForall: successful: SUCCESS$ -^\*\* 2 of 6 failed \(2 iterations\)$ +^\*\* 2 of 6 failed ^VERIFICATION FAILED$ diff --git a/regression/cbmc/Quantifiers-assignment/test.desc b/regression/cbmc/Quantifiers-assignment/test.desc index ca5f55d51a2..f9886ec28be 100644 --- a/regression/cbmc/Quantifiers-assignment/test.desc +++ b/regression/cbmc/Quantifiers-assignment/test.desc @@ -6,5 +6,5 @@ main.c ^\[main.assertion.2\] assertion y: FAILURE$ ^\[main.assertion.3\] assertion z1: SUCCESS$ ^\[main.assertion.4\] assertion z2: SUCCESS$ -^\*\* 1 of 4 failed \(2 iterations\)$ +^\*\* 1 of 4 failed ^VERIFICATION FAILED$ diff --git a/regression/cbmc/Quantifiers-if/test.desc b/regression/cbmc/Quantifiers-if/test.desc index 7685cf4284a..2f661c900ce 100644 --- a/regression/cbmc/Quantifiers-if/test.desc +++ b/regression/cbmc/Quantifiers-if/test.desc @@ -7,5 +7,5 @@ main.c ^\[main.assertion.3\] success 1: SUCCESS$ ^\[main.assertion.4\] failure 3: FAILURE$ ^\[main.assertion.5\] success 2: SUCCESS$ -^\*\* 3 of 5 failed \(2 iterations\)$ +^\*\* 3 of 5 failed ^VERIFICATION FAILED$ diff --git a/regression/cbmc/Quantifiers-initialisation2/test.desc b/regression/cbmc/Quantifiers-initialisation2/test.desc index 0f309d9332d..8e38bf5955b 100644 --- a/regression/cbmc/Quantifiers-initialisation2/test.desc +++ b/regression/cbmc/Quantifiers-initialisation2/test.desc @@ -7,5 +7,5 @@ main.c ^\[main.assertion.3\] assertion a\[.*\] > a\[.*\]: FAILURE$ ^\[main.assertion.4\] forall c\[\]: SUCCESS$ ^\[main.assertion.5\] assertion c\[.*\] >= c\[.*\]: SUCCESS$ -^\*\* 1 of 5 failed \(2 iterations\)$ +^\*\* 1 of 5 failed ^VERIFICATION FAILED$ diff --git a/regression/cbmc/Quantifiers-not/test.desc b/regression/cbmc/Quantifiers-not/test.desc index b22b6666f14..37843fe1472 100644 --- a/regression/cbmc/Quantifiers-not/test.desc +++ b/regression/cbmc/Quantifiers-not/test.desc @@ -7,5 +7,5 @@ main.c ^\[main.assertion.3\] failure 1: FAILURE$ ^\[main.assertion.4\] success 3: SUCCESS$ ^\[main.assertion.5\] failure 2: FAILURE$ -^\*\* 2 of 5 failed \(2 iterations\)$ +^\*\* 2 of 5 failed ^VERIFICATION FAILED$ diff --git a/regression/cbmc/Quantifiers-type/test.desc b/regression/cbmc/Quantifiers-type/test.desc index a3939c6a78a..d5e98684d0e 100644 --- a/regression/cbmc/Quantifiers-type/test.desc +++ b/regression/cbmc/Quantifiers-type/test.desc @@ -4,5 +4,5 @@ main.c ^\*\* Results:$ ^\[main.assertion.1\] assertion tmp_if_expr\$1: FAILURE$ ^\[main.assertion.2\] assertion tmp_if_expr\$2: SUCCESS$ -^\*\* 1 of 2 failed \(2 iterations\)$ +^\*\* 1 of 2 failed ^VERIFICATION FAILED$ diff --git a/regression/cbmc/fgets1/test.desc b/regression/cbmc/fgets1/test.desc index 1551462c520..3228a434a07 100644 --- a/regression/cbmc/fgets1/test.desc +++ b/regression/cbmc/fgets1/test.desc @@ -5,6 +5,6 @@ main.c ^SIGNAL=0$ ^VERIFICATION FAILED$ \[main.assertion.3\] assertion p\[1\]=='b': FAILURE -\*\* 1 of \d+ failed \(2 iterations\) +\*\* 1 of \d+ failed -- ^warning: ignoring diff --git a/regression/cbmc/memory_allocation1/test.desc b/regression/cbmc/memory_allocation1/test.desc index 218000c3650..f45db0953f4 100644 --- a/regression/cbmc/memory_allocation1/test.desc +++ b/regression/cbmc/memory_allocation1/test.desc @@ -7,6 +7,6 @@ main.c \[main.assertion.1\] assertion \*p==42: SUCCESS \[main.pointer_dereference.14\] dereference failure: pointer invalid in p\[.*1\]: FAILURE \[main.assertion.2\] assertion \*\(p\+1\)==42: SUCCESS -\*\* 12 of 26 failed \(2 iterations\) +\*\* 12 of 26 failed -- ^warning: ignoring diff --git a/regression/cbmc/memset1/test.desc b/regression/cbmc/memset1/test.desc index aef7e29d151..2473a80a95e 100644 --- a/regression/cbmc/memset1/test.desc +++ b/regression/cbmc/memset1/test.desc @@ -5,6 +5,6 @@ main.c ^SIGNAL=0$ ^VERIFICATION FAILED$ \[main.assertion.7\] assertion A\[1\]==0x01010111: FAILURE -\*\* 1 of 12 failed \(2 iterations\) +\*\* 1 of 12 failed -- ^warning: ignoring diff --git a/regression/cbmc/pipe1/test.desc b/regression/cbmc/pipe1/test.desc index 26a7b98287a..3c4aa9c5bc4 100644 --- a/regression/cbmc/pipe1/test.desc +++ b/regression/cbmc/pipe1/test.desc @@ -4,6 +4,6 @@ main.c ^EXIT=10$ ^SIGNAL=0$ ^\[main\.assertion\.4\] assertion data\[1\]==31: FAILURE$ -^\*\* 1 of 5 failed \(2 iterations\)$ +^\*\* 1 of 5 failed -- ^warning: ignoring diff --git a/regression/cbmc/pointer-function-parameters-2/test.desc b/regression/cbmc/pointer-function-parameters-2/test.desc index be81dbdc393..dddd7a6edcf 100644 --- a/regression/cbmc/pointer-function-parameters-2/test.desc +++ b/regression/cbmc/pointer-function-parameters-2/test.desc @@ -2,7 +2,7 @@ CORE main.c --function fun --cover branch ^\*\* 7 of 7 covered \(100.0%\)$ -^\*\* Used 4 iterations$ +^\*\* Used ^Test suite:$ ^a=\(\(signed int \*\*\)NULL\), tmp\$\d+=[^,]*, tmp\$\d+=[^,]*$ ^a=&tmp\$\d+!0, tmp\$\d+=\(\(signed int \*\)NULL\), tmp\$\d+=[^,]*$ diff --git a/regression/cbmc/pointer-function-parameters/test.desc b/regression/cbmc/pointer-function-parameters/test.desc index 89fbd70531a..00c63b0163a 100644 --- a/regression/cbmc/pointer-function-parameters/test.desc +++ b/regression/cbmc/pointer-function-parameters/test.desc @@ -2,7 +2,7 @@ CORE main.c --function fun --cover branch ^\*\* 5 of 5 covered \(100\.0%\)$ -^\*\* Used 3 iterations$ +^\*\* Used ^Test suite:$ ^a=\(\(signed int \*\)NULL\), tmp\$\d+=[^,]*$ ^a=&tmp\$\d+!0, tmp\$\d+=4$ diff --git a/regression/strings/test_pass1/test.desc b/regression/strings/test_pass1/test.desc index 77f0c2e7eb8..9cdafb87bed 100644 --- a/regression/strings/test_pass1/test.desc +++ b/regression/strings/test_pass1/test.desc @@ -5,4 +5,4 @@ test.c ^SIGNAL=0$ ^\[main.assertion.1\] assertion __CPROVER_uninterpreted_string_equal_func\(t, __CPROVER_uninterpreted_string_literal_func\(\"a\"\)): SUCCESS ^\[main.assertion.2\] assertion !__CPROVER_uninterpreted_string_equal_func\(t, __CPROVER_uninterpreted_string_literal_func\(\"a\"\)): FAILURE$ -^\*\* 1 of 2 failed \(2 iterations\)$ +^\*\* 1 of 2 failed From 900a0fcb8b45ea33abaf54f6e9c73e4fcfbe01f5 Mon Sep 17 00:00:00 2001 From: Norbert Manthey Date: Sun, 15 Oct 2017 13:58:51 +0200 Subject: [PATCH 5/6] tests: do not match iterations line During tests, the number of used iterations has been matched. When using different SAT solvers, these numbers differ. Without the numbers, the line is actually useless, so that we drop it completely. --- regression/cbmc-cover/mcdc1/test.desc | 1 - regression/cbmc-cover/mcdc11/test.desc | 1 - regression/cbmc-cover/mcdc12/test.desc | 1 - regression/cbmc-cover/mcdc14/test.desc | 1 - regression/cbmc-cover/mcdc3/test.desc | 1 - regression/cbmc-cover/mcdc4/test.desc | 1 - regression/cbmc-cover/mcdc6/test.desc | 1 - regression/cbmc-cover/mcdc7/test.desc | 1 - regression/cbmc-cover/mcdc8/test.desc | 1 - regression/cbmc-cover/mcdc9/test.desc | 1 - regression/cbmc/pointer-function-parameters-2/test.desc | 1 - regression/cbmc/pointer-function-parameters/test.desc | 1 - 12 files changed, 12 deletions(-) diff --git a/regression/cbmc-cover/mcdc1/test.desc b/regression/cbmc-cover/mcdc1/test.desc index dbf4cb8d116..6fe0cd3a5f0 100644 --- a/regression/cbmc-cover/mcdc1/test.desc +++ b/regression/cbmc-cover/mcdc1/test.desc @@ -10,6 +10,5 @@ main.c ^\[main.coverage.5\] file main.c line 14 function main MC/DC independence condition `C && D && E && !A && B.*: SATISFIED$ ^\[main.coverage.6\] file main.c line 14 function main MC/DC independence condition `C && D && E && !A && !B.*: SATISFIED$ ^\*\* .* of .* covered \(100.0%\)$ -^\*\* Used -- ^warning: ignoring diff --git a/regression/cbmc-cover/mcdc11/test.desc b/regression/cbmc-cover/mcdc11/test.desc index 42ec4c2e750..2027e1577be 100644 --- a/regression/cbmc-cover/mcdc11/test.desc +++ b/regression/cbmc-cover/mcdc11/test.desc @@ -10,6 +10,5 @@ main.c ^\[main.coverage.11\] file main.c line 12 function main MC/DC independence condition `!\(C != FALSE\) && D != FALSE.*: SATISFIED$ ^\[main.coverage.12\] file main.c line 12 function main MC/DC independence condition `!\(C != FALSE\) && !\(D != FALSE\).*: SATISFIED$ ^\*\* .* of .* covered \(100.0%\)$ -^\*\* Used -- ^warning: ignoring diff --git a/regression/cbmc-cover/mcdc12/test.desc b/regression/cbmc-cover/mcdc12/test.desc index 614ebbe3872..03a731e6d27 100644 --- a/regression/cbmc-cover/mcdc12/test.desc +++ b/regression/cbmc-cover/mcdc12/test.desc @@ -13,6 +13,5 @@ main.c ^\[main.coverage.20\] file main.c line 25 function main MC/DC independence condition `!\(E != FALSE\) && F != FALSE.*: SATISFIED$ ^\[main.coverage.21\] file main.c line 25 function main MC/DC independence condition `!\(E != FALSE\) && !\(F != FALSE\).*: SATISFIED$ ^\*\* .* of .* covered \(100.0%\)$ -^\*\* Used -- ^warning: ignoring diff --git a/regression/cbmc-cover/mcdc14/test.desc b/regression/cbmc-cover/mcdc14/test.desc index df4eaa08f1e..09cf68d35d2 100644 --- a/regression/cbmc-cover/mcdc14/test.desc +++ b/regression/cbmc-cover/mcdc14/test.desc @@ -6,6 +6,5 @@ main.c ^\[main.coverage.1\] file main.c line 7 function main decision/condition `altitude > 2500.* SATISFIED$ ^\[main.coverage.2\] file main.c line 7 function main decision/condition `altitude > 2500.* SATISFIED$ ^\*\* .* of .* covered \(100.0%\)$ -^\*\* Used -- ^warning: ignoring diff --git a/regression/cbmc-cover/mcdc3/test.desc b/regression/cbmc-cover/mcdc3/test.desc index 8963f48b2da..396c7cd5e0d 100644 --- a/regression/cbmc-cover/mcdc3/test.desc +++ b/regression/cbmc-cover/mcdc3/test.desc @@ -7,6 +7,5 @@ main.c ^\[main.coverage.2\] file main.c line 8 function main MC/DC independence condition `y < \(unsigned int\)5 && !\(x > \(unsigned int\)3\).*: SATISFIED$ ^\[main.coverage.3\] file main.c line 8 function main MC/DC independence condition `y < \(unsigned int\)5 && x > \(unsigned int\)3.*: SATISFIED$ ^\*\* .* of .* covered \(100.0%\)$ -^\*\* Used -- ^warning: ignoring diff --git a/regression/cbmc-cover/mcdc4/test.desc b/regression/cbmc-cover/mcdc4/test.desc index a5d8e5a8e00..1c469418a26 100644 --- a/regression/cbmc-cover/mcdc4/test.desc +++ b/regression/cbmc-cover/mcdc4/test.desc @@ -9,6 +9,5 @@ main.c ^\[main.coverage.4\] file main.c line 11 function main MC/DC independence condition `!C && D && A && !B.*: SATISFIED$ ^\[main.coverage.5\] file main.c line 11 function main MC/DC independence condition `!A && B && C && !D.*: SATISFIED$ ^\*\* .* of .* covered \(100.0%\)$ -^\*\* Used -- ^warning: ignoring diff --git a/regression/cbmc-cover/mcdc6/test.desc b/regression/cbmc-cover/mcdc6/test.desc index 7a33eb16b65..267488742c2 100644 --- a/regression/cbmc-cover/mcdc6/test.desc +++ b/regression/cbmc-cover/mcdc6/test.desc @@ -6,6 +6,5 @@ main.c ^\[main.coverage.1\] file main.c line 7 function main decision/condition `x < \(unsigned int\)3.* false: SATISFIED$ ^\[main.coverage.2\] file main.c line 7 function main decision/condition `x < \(unsigned int\)3.* true: SATISFIED$ ^\*\* .* of .* covered \(100.0%\)$ -^\*\* Used -- ^warning: ignoring diff --git a/regression/cbmc-cover/mcdc7/test.desc b/regression/cbmc-cover/mcdc7/test.desc index 9c3858a3caf..c288cbab0ce 100644 --- a/regression/cbmc-cover/mcdc7/test.desc +++ b/regression/cbmc-cover/mcdc7/test.desc @@ -8,6 +8,5 @@ main.c ^\[main.coverage.3\] file main.c line 8 function main decision/condition `x \* 123 < 0.* false: SATISFIED$ ^\[main.coverage.4\] file main.c line 8 function main decision/condition `x \* 123 < 0.* true: SATISFIED$ ^\*\* .* of .* covered \(100.0%\)$ -^\*\* Used -- ^warning: ignoring diff --git a/regression/cbmc-cover/mcdc8/test.desc b/regression/cbmc-cover/mcdc8/test.desc index cc12b098869..43a1b2ca741 100644 --- a/regression/cbmc-cover/mcdc8/test.desc +++ b/regression/cbmc-cover/mcdc8/test.desc @@ -8,6 +8,5 @@ main.c ^\[main.coverage.3\] file main.c line 9 function main MC/DC independence condition `c != FALSE && !\(a != FALSE\) && !\(b != FALSE\).* SATISFIED$ ^\[main.coverage.4\] file main.c line 9 function main MC/DC independence condition `!\(c != FALSE\) && a != FALSE && !\(b != FALSE\).* SATISFIED$ ^\*\* .* of .* covered \(100.0%\)$ -^\*\* Used -- ^warning: ignoring diff --git a/regression/cbmc-cover/mcdc9/test.desc b/regression/cbmc-cover/mcdc9/test.desc index 47045c120cd..199f3f14885 100644 --- a/regression/cbmc-cover/mcdc9/test.desc +++ b/regression/cbmc-cover/mcdc9/test.desc @@ -9,6 +9,5 @@ main.c ^\[main.coverage.12\] file main.c line 16 function main MC/DC independence condition `!\(A != FALSE\) && B != FALSE && C != FALSE && !\(D != FALSE\).* SATISFIED$ ^\[main.coverage.13\] file main.c line 16 function main MC/DC independence condition `!\(A != FALSE\) && !\(B != FALSE\) && C != FALSE && !\(D != FALSE\).* SATISFIED$ ^\*\* .* of .* covered \(100.0%\)$ -^\*\* Used -- ^warning: ignoring diff --git a/regression/cbmc/pointer-function-parameters-2/test.desc b/regression/cbmc/pointer-function-parameters-2/test.desc index dddd7a6edcf..584e452fc11 100644 --- a/regression/cbmc/pointer-function-parameters-2/test.desc +++ b/regression/cbmc/pointer-function-parameters-2/test.desc @@ -2,7 +2,6 @@ CORE main.c --function fun --cover branch ^\*\* 7 of 7 covered \(100.0%\)$ -^\*\* Used ^Test suite:$ ^a=\(\(signed int \*\*\)NULL\), tmp\$\d+=[^,]*, tmp\$\d+=[^,]*$ ^a=&tmp\$\d+!0, tmp\$\d+=\(\(signed int \*\)NULL\), tmp\$\d+=[^,]*$ diff --git a/regression/cbmc/pointer-function-parameters/test.desc b/regression/cbmc/pointer-function-parameters/test.desc index 00c63b0163a..809730ea5f1 100644 --- a/regression/cbmc/pointer-function-parameters/test.desc +++ b/regression/cbmc/pointer-function-parameters/test.desc @@ -2,7 +2,6 @@ CORE main.c --function fun --cover branch ^\*\* 5 of 5 covered \(100\.0%\)$ -^\*\* Used ^Test suite:$ ^a=\(\(signed int \*\)NULL\), tmp\$\d+=[^,]*$ ^a=&tmp\$\d+!0, tmp\$\d+=4$ From c3d527ca7a244792c108f52048f93b6040bd22c3 Mon Sep 17 00:00:00 2001 From: Norbert Manthey Date: Sun, 15 Oct 2017 14:07:15 +0200 Subject: [PATCH 6/6] compiling: add IPASIR notes for Linux Add the steps to link against an IPASIR solver to the COMPILING notes. --- COMPILING.md | 13 +++++++++++++ 1 file changed, 13 insertions(+) diff --git a/COMPILING.md b/COMPILING.md index 44760d2b26a..86ff874d556 100644 --- a/COMPILING.md +++ b/COMPILING.md @@ -46,6 +46,19 @@ We assume that you have a Debian/Ubuntu or Red Hat-like distribution. make ``` +4. Linking against an IPASIR SAT solver + + Get an IPASIR package and build picosat by default + ``` + make -C src ipasir-build + ``` + + Build CBMC with IPASIR and link against the ipasir solver library + Note: the LIBSOLVER variable could be pointed towards other solvers + ``` + make -C src IPASIR=../../ipasir LIBSOLVER=$(pwd)/ipasir/libipasir.a + ``` + # COMPILATION ON SOLARIS 11 1. As root, get the necessary development tools: