jjames pushed to cbmc (master). "New upstream release. Drop upstreamed -messaget patch."
notifications at fedoraproject.org
notifications at fedoraproject.org
Thu May 14 03:15:22 UTC 2015
From 400f15b0215dff25d4c1a252fcdb4e148975367f Mon Sep 17 00:00:00 2001
From: Jerry James <loganjerry at gmail.com>
Date: Wed, 13 May 2015 21:14:51 -0600
Subject: New upstream release. Drop upstreamed -messaget patch.
diff --git a/.gitignore b/.gitignore
index e0d72e0..32ee5af 100644
--- a/.gitignore
+++ b/.gitignore
@@ -1 +1,2 @@
/cbmc-5.0.tar.xz
+/cbmc-5.1.tar.xz
diff --git a/cbmc-5.0-fix-build.patch b/cbmc-5.0-fix-build.patch
deleted file mode 100644
index afbf92d..0000000
--- a/cbmc-5.0-fix-build.patch
+++ /dev/null
@@ -1,96 +0,0 @@
-Index: src/cbmc/Makefile
-===================================================================
---- src/cbmc/Makefile (revision 5150)
-+++ src/cbmc/Makefile (working copy)
-@@ -23,7 +23,7 @@
-
- INCLUDES= -I ..
-
--LIBS =
-+LIBS = -lminisat -lcuddobj -lcudd -lmtr -lcuddst -lcuddutil -lepd -ldddmp
-
- include ../config.inc
- include ../common
-Index: src/common
-===================================================================
---- src/common (revision 5150)
-+++ src/common (working copy)
-@@ -69,7 +69,7 @@
- endif
- else
- LINKLIB = ar rcT $@ $^
-- LINKBIN = $(CXX) $(LINKFLAGS) -o $@ -Wl,--start-group $^ -Wl,--end-group $(LIBS)
-+ LINKBIN = $(CXX) $(LINKFLAGS) -o $@ -Wl,--start-group $^ -Wl,--end-group $(LDFLAGS) $(LIBS)
- LINKNATIVE = $(HOSTCXX) -o $@ $^
- ifeq ($(origin CC),default)
- CC = gcc
-Index: src/config.inc
-===================================================================
---- src/config.inc (revision 5150)
-+++ src/config.inc (working copy)
-@@ -4,18 +4,22 @@
- # Variables you may want to override
- #CXXFLAGS = -Wall -O0 -g -Werror -Wno-long-long -Wno-sign-compare -Wno-parentheses -Wno-strict-aliasing -pedantic
- #CXXFLAGS = -std=c++11
-+CFLAGS = @RPM_OPT_FLAGS@
-+CXXFLAGS = @RPM_OPT_FLAGS@
-+LDFLAGS = @RPM_LD_FLAGS@
-
- # If GLPK is available; this is used by goto-instrument and musketeer.
--#LIB_GLPK = -lglpk
-+LIB_GLPK = -lglpk
-
- # SAT-solvers we have
- #PRECOSAT = ../../precosat-576-7e5e66f-120112
- #PICOSAT = ../../picosat-959
-+CUDD = /usr
- #LINGELING = ../../lingeling-587f-4882048-110513
- #CHAFF = ../../zChaff
- #BOOLEFORCE = ../../booleforce-0.4
- #MINISAT = ../../MiniSat-p_v1.14
--MINISAT2 = ../../minisat-2.2.0
-+MINISAT2 = /usr/include/minisat
- #GLUCOSE = ../../glucose2.2
- #SMVSAT =
-
-Index: src/goto-instrument/Makefile
-===================================================================
---- src/goto-instrument/Makefile (revision 5150)
-+++ src/goto-instrument/Makefile (working copy)
-@@ -39,7 +39,7 @@
-
- INCLUDES= -I ..
-
--LIBS =
-+LIBS = -lminisat -lcuddobj -lcudd -lmtr -lcuddst -lcuddutil -lepd -ldddmp
-
- CLEANFILES = goto-instrument$(EXEEXT)
-
-Index: src/solvers/Makefile
-===================================================================
---- src/solvers/Makefile (revision 5150)
-+++ src/solvers/Makefile (working copy)
-@@ -17,7 +17,7 @@
- ifneq ($(MINISAT2),)
- MINISAT2_SRC=sat/satcheck_minisat2.cpp
- MINISAT2_INCLUDE=-I $(MINISAT2)
-- MINISAT2_LIB=$(MINISAT2)/simp/SimpSolver$(OBJEXT) $(MINISAT2)/core/Solver$(OBJEXT)
-+# MINISAT2_LIB=$(MINISAT2)/simp/SimpSolver$(OBJEXT) $(MINISAT2)/core/Solver$(OBJEXT)
- CP_CXXFLAGS += -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS
- override CXXFLAGS := $(filter-out -pedantic, $(CXXFLAGS))
- endif
-@@ -44,10 +44,10 @@
-
- ifneq ($(CUDD),)
- CUDD_SRC=qbf/qbf_bdd_core.cpp qbf/qbf_skizzo_core.cpp
-- CUDD_INCLUDE=-I $(CUDD)/include
-- CUDD_LIB=-L $(CUDD)/cudd -L $(CUDD)/util -L $(CUDD)/mtr \
-- -L $(CUDD)/st -L $(CUDD)/obj -L $(CUDD)/dddmp \
-- -L $(CUDD)/epd -lobj -lcudd -lmtr -lst -lutil -lepd -ldddmp
-+ CUDD_INCLUDE=-I $(CUDD)/include/cudd
-+# CUDD_LIB=-L $(CUDD)/cudd -L $(CUDD)/util -L $(CUDD)/mtr \
-+# -L $(CUDD)/st -L $(CUDD)/obj -L $(CUDD)/dddmp \
-+# -L $(CUDD)/epd -lobj -lcudd -lmtr -lst -lutil -lepd -ldddmp
- endif
-
- ifneq ($(PRECOSAT),)
diff --git a/cbmc-5.0-messaget.patch b/cbmc-5.0-messaget.patch
deleted file mode 100644
index 3c71f49..0000000
--- a/cbmc-5.0-messaget.patch
+++ /dev/null
@@ -1,349 +0,0 @@
-Index: src/solvers/qbf/qbf_bdd_core.cpp
-===================================================================
---- src/solvers/qbf/qbf_bdd_core.cpp (revision 5150)
-+++ src/solvers/qbf/qbf_bdd_core.cpp (working copy)
-@@ -194,7 +194,7 @@
- solver_text() + ": "+
- i2string(no_variables())+" variables, "+
- i2string(matrix->nodeCount())+" nodes";
-- messaget::status(msg);
-+ messaget::status() << msg << messaget::eom;
- }
-
- model_bdds.resize(no_variables()+1, NULL);
-@@ -419,7 +419,7 @@
-
- void qbf_bdd_coret::compress_certificate(void)
- {
-- status("Compressing Certificate");
-+ status() << "Compressing Certificate" << eom;
-
- for(quantifierst::const_iterator it=quantifiers.begin();
- it!=quantifiers.end();
-Index: src/solvers/qbf/qbf_skizzo_core.cpp
-===================================================================
---- src/solvers/qbf/qbf_skizzo_core.cpp (revision 5150)
-+++ src/solvers/qbf/qbf_skizzo_core.cpp (working copy)
-@@ -104,7 +104,7 @@
- "Skizzo: "+
- i2string(no_variables())+" variables, "+
- i2string(no_clauses())+" clauses";
-- messaget::status(msg);
-+ messaget::status() << msg << messaget::eom;
- }
-
- std::string result_tmp_file="sKizzo.out";
-@@ -156,7 +156,7 @@
-
- if(!result_found)
- {
-- messaget::error("Skizzo failed: unknown result");
-+ messaget::error() << "Skizzo failed: unknown result" << messaget::eom;
- return P_ERROR;
- }
- }
-@@ -166,7 +166,7 @@
-
- if(result)
- {
-- messaget::status("Skizzo: TRUE");
-+ messaget::status() << "Skizzo: TRUE" << messaget::eom;
-
- if(get_certificate())
- return P_ERROR;
-@@ -175,7 +175,7 @@
- }
- else
- {
-- messaget::status("Skizzo: FALSE");
-+ messaget::status() << "Skizzo: FALSE" << messaget::eom;
- return P_UNSATISFIABLE;
- }
- }
-@@ -260,7 +260,7 @@
-
- if(!result)
- {
-- messaget::error("Skizzo failed: unknown result");
-+ messaget::error() << "Skizzo failed: unknown result" << messaget::eom;
- return true;
- }
-
-Index: src/solvers/qbf/qbf_squolem.cpp
-===================================================================
---- src/solvers/qbf/qbf_squolem.cpp (revision 5150)
-+++ src/solvers/qbf/qbf_squolem.cpp (working copy)
-@@ -96,7 +96,7 @@
- "Squolem: "+
- i2string(no_variables())+" variables, "+
- i2string(no_clauses())+" clauses";
-- messaget::status(msg);
-+ messaget::status() << msg << messaget::eom;
- }
-
- if(early_decision) return P_UNSATISFIABLE;
-@@ -113,12 +113,12 @@
-
- if(result)
- {
-- messaget::status("Squolem: VALID");
-+ messaget::status() << "Squolem: VALID" << messaget::eom;
- return P_SATISFIABLE;
- }
- else
- {
-- messaget::status("Squolem: INVALID");
-+ messaget::status() << "Squolem: INVALID" << messaget::eom;
- return P_UNSATISFIABLE;
- }
-
-Index: src/solvers/qbf/qbf_squolem_core.cpp
-===================================================================
---- src/solvers/qbf/qbf_squolem_core.cpp (revision 5150)
-+++ src/solvers/qbf/qbf_squolem_core.cpp (working copy)
-@@ -168,7 +168,7 @@
- "Squolem: "+
- i2string(no_variables())+" variables, "+
- i2string(no_clauses())+" clauses";
-- messaget::status(msg);
-+ messaget::status() << msg << messaget::eom;
- }
-
- squolem->endOfOriginals();
-@@ -176,12 +176,12 @@
-
- if(result)
- {
-- messaget::status("Squolem: VALID");
-+ messaget::status() << "Squolem: VALID" << messaget::eom;
- return P_SATISFIABLE;
- }
- else
- {
-- messaget::status("Squolem: INVALID");
-+ messaget::status() << "Squolem: INVALID" << messaget::eom;
- return P_UNSATISFIABLE;
- }
-
-Index: src/solvers/sat/satcheck_booleforce.cpp
-===================================================================
---- src/solvers/sat/satcheck_booleforce.cpp (revision 5150)
-+++ src/solvers/sat/satcheck_booleforce.cpp (working copy)
-@@ -188,7 +188,7 @@
- break;
- }
-
-- messaget::status(msg);
-+ messaget::status() << msg << messaget::eom;
- }
-
- if(result==BOOLEFORCE_UNSATISFIABLE)
-Index: src/solvers/sat/satcheck_glucose.cpp
-===================================================================
---- src/solvers/sat/satcheck_glucose.cpp (revision 5150)
-+++ src/solvers/sat/satcheck_glucose.cpp (working copy)
-@@ -203,7 +203,7 @@
- std::string msg=
- i2string(_no_variables)+" variables, "+
- i2string(solver->nClauses())+" clauses";
-- messaget::status(msg);
-+ messaget::status() << msg << messaget::eom;
- }
-
- add_variables();
-@@ -213,12 +213,12 @@
- if(empty_clause_added)
- {
- msg="empty clause: negated claim is UNSATISFIABLE, i.e., holds";
-- messaget::status(msg);
-+ messaget::status() << msg << messaget::eom
- }
- else if(!solver->okay())
- {
- msg="SAT checker inconsistent: negated claim is UNSATISFIABLE, i.e., holds";
-- messaget::status(msg);
-+ messaget::status() << msg << messaget::eom;
- }
- else
- {
-@@ -228,7 +228,7 @@
- if(solver->solve(solver_assumptions))
- {
- msg="SAT checker: negated claim is SATISFIABLE, i.e., does not hold";
-- messaget::status(msg);
-+ messaget::status() << msg << messaget::eom;
- assert(solver->model.size()!=0);
- status=SAT;
- return P_SATISFIABLE;
-@@ -236,7 +236,7 @@
- else
- {
- msg="SAT checker: negated claim is UNSATISFIABLE, i.e., holds";
-- messaget::status(msg);
-+ messaget::status() << msg << messaget::eom;
- }
- }
-
-Index: src/solvers/sat/satcheck_limmat.cpp
-===================================================================
---- src/solvers/sat/satcheck_limmat.cpp (revision 5150)
-+++ src/solvers/sat/satcheck_limmat.cpp (working copy)
-@@ -158,7 +158,7 @@
- std::string msg=
- i2string(maxvar_Limmat(solver))+" variables, "+
- i2string(clauses_Limmat(solver))+" clauses";
-- messaget::status(msg);
-+ messaget::status() << msg << messaget::eom;
- }
-
- int status=sat_Limmat(solver, -1);
-@@ -181,7 +181,7 @@
- break;
- }
-
-- messaget::status(msg);
-+ messaget::status() << msg << messaget::eom;
- }
-
- if(status==0)
-Index: src/solvers/sat/satcheck_lingeling.cpp
-===================================================================
---- src/solvers/sat/satcheck_lingeling.cpp (revision 5150)
-+++ src/solvers/sat/satcheck_lingeling.cpp (working copy)
-@@ -118,7 +118,7 @@
- std::string msg=
- i2string(_no_variables)+" variables, "+
- i2string(clause_counter)+" clauses";
-- messaget::status(msg);
-+ messaget::status() << msg << messaget::eom;
- }
-
- std::string msg;
-@@ -130,7 +130,7 @@
- if(res==10)
- {
- msg="SAT checker: negated claim is SATISFIABLE, i.e., does not hold";
-- messaget::status(msg);
-+ messaget::status() << msg << messaget::eom;
- status=SAT;
- return P_SATISFIABLE;
- }
-@@ -138,7 +138,7 @@
- {
- assert(res==20);
- msg="SAT checker: negated claim is UNSATISFIABLE, i.e., holds";
-- messaget::status(msg);
-+ messaget::status() << msg << messaget::eom;
- }
-
- status=UNSAT;
-Index: src/solvers/sat/satcheck_picosat.cpp
-===================================================================
---- src/solvers/sat/satcheck_picosat.cpp (revision 5150)
-+++ src/solvers/sat/satcheck_picosat.cpp (working copy)
-@@ -120,7 +120,7 @@
- std::string msg=
- i2string(_no_variables)+" variables, "+
- i2string(picosat_added_original_clauses(picosat))+" clauses";
-- messaget::status(msg);
-+ messaget::status() << msg << messaget::eom;
- }
-
- std::string msg;
-@@ -132,7 +132,7 @@
- if(res==PICOSAT_SATISFIABLE)
- {
- msg="SAT checker: negated claim is SATISFIABLE, i.e., does not hold";
-- messaget::status(msg);
-+ messaget::status() << msg << messaget::eom;
- status=SAT;
- return P_SATISFIABLE;
- }
-@@ -140,7 +140,7 @@
- {
- assert(res==PICOSAT_UNSATISFIABLE);
- msg="SAT checker: negated claim is UNSATISFIABLE, i.e., holds";
-- messaget::status(msg);
-+ messaget::status() << msg << messaget::eom;
- }
-
- status=UNSAT;
-Index: src/solvers/sat/satcheck_precosat.cpp
-===================================================================
---- src/solvers/sat/satcheck_precosat.cpp (revision 5150)
-+++ src/solvers/sat/satcheck_precosat.cpp (working copy)
-@@ -118,7 +118,7 @@
- std::string msg=
- i2string(_no_variables)+" variables, "+
- i2string(solver->getAddedOrigClauses())+" clauses";
-- messaget::status(msg);
-+ messaget::status() << msg << messaget::eom;
- }
-
- std::string msg;
-@@ -127,7 +127,7 @@
- if(res==1)
- {
- msg="SAT checker: negated claim is SATISFIABLE, i.e., does not hold";
-- messaget::status(msg);
-+ messaget::status() << msg << messaget::eom;
- status=SAT;
- return P_SATISFIABLE;
- }
-@@ -135,7 +135,7 @@
- {
- assert(res==-1);
- msg="SAT checker: negated claim is UNSATISFIABLE, i.e., holds";
-- messaget::status(msg);
-+ messaget::status() << msg << messaget::eom;
- }
-
- status=UNSAT;
-Index: src/solvers/sat/satcheck_smvsat.cpp
-===================================================================
---- src/solvers/sat/satcheck_smvsat.cpp (revision 5150)
-+++ src/solvers/sat/satcheck_smvsat.cpp (working copy)
-@@ -188,7 +188,7 @@
- break;
- }
-
-- messaget::status(msg);
-+ messaget::status() << msg << messaget::eom;
- }
-
- if(result==0)
-Index: src/solvers/sat/satcheck_zchaff.cpp
-===================================================================
---- src/solvers/sat/satcheck_zchaff.cpp (revision 5150)
-+++ src/solvers/sat/satcheck_zchaff.cpp (working copy)
-@@ -153,7 +153,7 @@
- std::string msg=
- i2string(solver->num_variables())+" variables, "+
- i2string(solver->clauses().size())+" clauses";
-- messaget::status(msg);
-+ messaget::status() << msg << messaget::eom;
- }
-
- SAT_StatusT result=(SAT_StatusT)solver->solve();
-@@ -192,7 +192,7 @@
- break;
- }
-
-- messaget::status(msg);
-+ messaget::status() << msg << messaget::eom;
- }
-
- if(result==SATISFIABLE)
-Index: src/solvers/sat/satcheck_zcore.cpp
-===================================================================
---- src/solvers/sat/satcheck_zcore.cpp (revision 5150)
-+++ src/solvers/sat/satcheck_zcore.cpp (working copy)
-@@ -101,7 +101,7 @@
- std::string msg=
- i2string(no_variables())+" variables, "+
- i2string(no_clauses())+" clauses";
-- messaget::status(msg);
-+ messaget::status() << msg << messaget::eom;
- }
-
- // get the core
diff --git a/cbmc-5.1-fix-build.patch b/cbmc-5.1-fix-build.patch
new file mode 100644
index 0000000..fd4d274
--- /dev/null
+++ b/cbmc-5.1-fix-build.patch
@@ -0,0 +1,96 @@
+Index: src/cbmc/Makefile
+===================================================================
+--- src/cbmc/Makefile (revision 5391)
++++ src/cbmc/Makefile (working copy)
+@@ -23,7 +23,7 @@
+
+ INCLUDES= -I ..
+
+-LIBS =
++LIBS = -lminisat -lcuddobj -lcudd -lmtr -lcuddst -lcuddutil -lepd -ldddmp
+
+ include ../config.inc
+ include ../common
+Index: src/common
+===================================================================
+--- src/common (revision 5391)
++++ src/common (working copy)
+@@ -69,7 +69,7 @@
+ endif
+ else
+ LINKLIB = ar rcT $@ $^
+- LINKBIN = $(CXX) $(LINKFLAGS) -o $@ -Wl,--start-group $^ -Wl,--end-group $(LIBS)
++ LINKBIN = $(CXX) $(LINKFLAGS) -o $@ -Wl,--start-group $^ -Wl,--end-group $(LDFLAGS) $(LIBS)
+ LINKNATIVE = $(HOSTCXX) -o $@ $^
+ ifeq ($(origin CC),default)
+ CC = gcc
+Index: src/config.inc
+===================================================================
+--- src/config.inc (revision 5391)
++++ src/config.inc (working copy)
+@@ -4,18 +4,22 @@
+ # Variables you may want to override
+ #CXXFLAGS = -Wall -O0 -g -Werror -Wno-long-long -Wno-sign-compare -Wno-parentheses -Wno-strict-aliasing -pedantic
+ #CXXFLAGS = -std=c++11
++CFLAGS = @RPM_OPT_FLAGS@
++CXXFLAGS = @RPM_OPT_FLAGS@
++LDFLAGS = @RPM_LD_FLAGS@
+
+ # If GLPK is available; this is used by goto-instrument and musketeer.
+-#LIB_GLPK = -lglpk
++LIB_GLPK = -lglpk
+
+ # SAT-solvers we have
+ #PRECOSAT = ../../precosat-576-7e5e66f-120112
+ #PICOSAT = ../../picosat-959
++CUDD = /usr
+ #LINGELING = ../../lingeling-587f-4882048-110513
+ #CHAFF = ../../zChaff
+ #BOOLEFORCE = ../../booleforce-0.4
+ #MINISAT = ../../MiniSat-p_v1.14
+-MINISAT2 = ../../minisat-2.2.0
++MINISAT2 = /usr/include/minisat
+ #GLUCOSE = ../../glucose2.2
+ #SMVSAT =
+
+Index: src/goto-instrument/Makefile
+===================================================================
+--- src/goto-instrument/Makefile (revision 5391)
++++ src/goto-instrument/Makefile (working copy)
+@@ -39,7 +39,7 @@
+
+ INCLUDES= -I ..
+
+-LIBS =
++LIBS = -lminisat -lcuddobj -lcudd -lmtr -lcuddst -lcuddutil -lepd -ldddmp
+
+ CLEANFILES = goto-instrument$(EXEEXT)
+
+Index: src/solvers/Makefile
+===================================================================
+--- src/solvers/Makefile (revision 5391)
++++ src/solvers/Makefile (working copy)
+@@ -17,7 +17,7 @@
+ ifneq ($(MINISAT2),)
+ MINISAT2_SRC=sat/satcheck_minisat2.cpp
+ MINISAT2_INCLUDE=-I $(MINISAT2)
+- MINISAT2_LIB=$(MINISAT2)/simp/SimpSolver$(OBJEXT) $(MINISAT2)/core/Solver$(OBJEXT)
++# MINISAT2_LIB=$(MINISAT2)/simp/SimpSolver$(OBJEXT) $(MINISAT2)/core/Solver$(OBJEXT)
+ CP_CXXFLAGS += -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS
+ override CXXFLAGS := $(filter-out -pedantic, $(CXXFLAGS))
+ endif
+@@ -44,10 +44,10 @@
+
+ ifneq ($(CUDD),)
+ CUDD_SRC=qbf/qbf_bdd_core.cpp qbf/qbf_skizzo_core.cpp
+- CUDD_INCLUDE=-I $(CUDD)/include
+- CUDD_LIB=-L $(CUDD)/cudd -L $(CUDD)/util -L $(CUDD)/mtr \
+- -L $(CUDD)/st -L $(CUDD)/obj -L $(CUDD)/dddmp \
+- -L $(CUDD)/epd -lobj -lcudd -lmtr -lst -lutil -lepd -ldddmp
++ CUDD_INCLUDE=-I $(CUDD)/include/cudd
++# CUDD_LIB=-L $(CUDD)/cudd -L $(CUDD)/util -L $(CUDD)/mtr \
++# -L $(CUDD)/st -L $(CUDD)/obj -L $(CUDD)/dddmp \
++# -L $(CUDD)/epd -lobj -lcudd -lmtr -lst -lutil -lepd -ldddmp
+ endif
+
+ ifneq ($(PRECOSAT),)
diff --git a/cbmc.spec b/cbmc.spec
index 0b81b88..4b21fb0 100644
--- a/cbmc.spec
+++ b/cbmc.spec
@@ -1,6 +1,6 @@
Name: cbmc
-Version: 5.0
-Release: 2%{?dist}
+Version: 5.1
+Release: 1%{?dist}
Summary: Bounded Model Checker for ANSI-C and C++ programs
License: BSD with advertising
@@ -14,9 +14,7 @@ Source0: %{name}-%{version}.tar.xz
# Man page link for goto-cc and goto-instrument
Source1: goto-cc.1
# Fedora-specific patch: set up our build options
-Patch0: %{name}-5.0-fix-build.patch
-# Finish applying an incomplete API change; sent upstream 2 Feb 2015
-Patch1: %{name}-5.0-messaget.patch
+Patch0: %{name}-5.1-fix-build.patch
BuildRequires: bison
BuildRequires: cudd-devel
@@ -36,7 +34,6 @@ iterations.
%prep
%setup -q
%patch0
-%patch1
# Use the right build flags
sed -e "s|@RPM_OPT_FLAGS@|$RPM_OPT_FLAGS|" \
@@ -76,6 +73,10 @@ make -C regression
%{_mandir}/man1/*
%changelog
+* Wed May 13 2015 Jerry James <loganjerry at gmail.com> - 5.1-1
+- New upstream release
+- Drop upstreamed -messaget patch
+
* Sat May 02 2015 Kalev Lember <kalevlember at gmail.com> - 5.0-2
- Rebuilt for GCC 5 C++11 ABI change
diff --git a/sources b/sources
index 0110a9f..a14ca06 100644
--- a/sources
+++ b/sources
@@ -1 +1 @@
-5ca51f52407714e41bf3497e053bf798 cbmc-5.0.tar.xz
+3e148706b27f07850aac995b459b2330 cbmc-5.1.tar.xz
--
cgit v0.10.2
http://pkgs.fedoraproject.org/cgit/cbmc.git/commit/?h=master&id=400f15b0215dff25d4c1a252fcdb4e148975367f
More information about the scm-commits
mailing list