[ltl2ba] Add -warning patch (bz 1037182).
Jerry James
jjames at fedoraproject.org
Mon Dec 9 17:31:39 UTC 2013
commit 33711ea22a533c8d5c202ac2c41c09725a53bc6f
Author: Jerry James <jamesjer at betterlinux.com>
Date: Mon Dec 9 10:31:35 2013 -0700
Add -warning patch (bz 1037182).
ltl2ba-warning.patch | 350 ++++++++++++++++++++++++++++++++++++++++++++++++++
ltl2ba.spec | 10 +-
2 files changed, 358 insertions(+), 2 deletions(-)
---
diff --git a/ltl2ba-warning.patch b/ltl2ba-warning.patch
new file mode 100644
index 0000000..4e48b40
--- /dev/null
+++ b/ltl2ba-warning.patch
@@ -0,0 +1,350 @@
+--- ./alternating.c.orig 2007-08-03 23:45:03.000000000 -0600
++++ ./alternating.c 2013-12-09 07:00:00.000000000 -0700
+@@ -146,7 +146,6 @@ int get_sym_id(char *s) /* finds the id
+ ATrans *boolean(Node *p) /* computes the transitions to boolean nodes -> next & init */
+ {
+ ATrans *t1, *t2, *lft, *rgt, *result = (ATrans *)0;
+- int id;
+ switch(p->ntyp) {
+ case TRUE:
+ result = emalloc_atrans();
+@@ -433,7 +432,7 @@ void mk_alternating(Node *p) /* generate
+ if(tl_stats) {
+ getrusage(RUSAGE_SELF, &tr_fin);
+ timeval_subtract (&t_diff, &tr_fin.ru_utime, &tr_debut.ru_utime);
+- fprintf(tl_out, "\nBuilding and simplification of the alternating automaton: %i.%06is",
++ fprintf(tl_out, "\nBuilding and simplification of the alternating automaton: %li.%06lis",
+ t_diff.tv_sec, t_diff.tv_usec);
+ fprintf(tl_out, "\n%i states, %i transitions\n", astate_count, atrans_count);
+ }
+--- ./buchi.c.orig 2007-08-03 23:44:54.000000000 -0600
++++ ./buchi.c 2013-12-09 07:00:00.000000000 -0700
+@@ -38,7 +38,6 @@ extern struct rusage tr_debut, tr_fin;
+ extern struct timeval t_diff;
+ extern int tl_verbose, tl_stats, tl_simp_diff, tl_simp_fly, tl_simp_scc,
+ init_size, *final;
+-extern void put_uform(void);
+
+ extern FILE *tl_out;
+ BState *bstack, *bstates, *bremoved;
+@@ -110,7 +109,7 @@ int simplify_btrans() /* simplifies the
+ if(tl_stats) {
+ getrusage(RUSAGE_SELF, &tr_fin);
+ timeval_subtract (&t_diff, &tr_fin.ru_utime, &tr_debut.ru_utime);
+- fprintf(tl_out, "\nSimplification of the Buchi automaton - transitions: %i.%06is",
++ fprintf(tl_out, "\nSimplification of the Buchi automaton - transitions: %li.%06lis",
+ t_diff.tv_sec, t_diff.tv_usec);
+ fprintf(tl_out, "\n%i transitions removed\n", changed);
+
+@@ -129,7 +128,6 @@ void remove_btrans(BState *to)
+ { /* redirects transitions before removing a state from the automaton */
+ BState *s;
+ BTrans *t;
+- int i;
+ for (s = bstates->nxt; s != bstates; s = s->nxt)
+ for (t = s->trans->nxt; t != s->trans; t = t->nxt)
+ if (t->to == to) { /* transition to a state with no transitions */
+@@ -225,7 +223,7 @@ int simplify_bstates() /* eliminates red
+ if(tl_stats) {
+ getrusage(RUSAGE_SELF, &tr_fin);
+ timeval_subtract (&t_diff, &tr_fin.ru_utime, &tr_debut.ru_utime);
+- fprintf(tl_out, "\nSimplification of the Buchi automaton - states: %i.%06is",
++ fprintf(tl_out, "\nSimplification of the Buchi automaton - states: %li.%06lis",
+ t_diff.tv_sec, t_diff.tv_usec);
+ fprintf(tl_out, "\n%i states removed\n", changed);
+ }
+@@ -465,7 +463,7 @@ void print_buchi(BState *s) /* dumps the
+ void print_spin_buchi() {
+ BTrans *t;
+ BState *s;
+- int accept_all = 0, init_count = 0;
++ int accept_all = 0;
+ if(bstates->nxt == bstates) { /* empty automaton */
+ fprintf(tl_out, "never { /* ");
+ put_uform();
+@@ -620,7 +618,7 @@ void mk_buchi()
+ if(tl_stats) {
+ getrusage(RUSAGE_SELF, &tr_fin);
+ timeval_subtract (&t_diff, &tr_fin.ru_utime, &tr_debut.ru_utime);
+- fprintf(tl_out, "\nBuilding the Buchi automaton : %i.%06is",
++ fprintf(tl_out, "\nBuilding the Buchi automaton : %li.%06lis",
+ t_diff.tv_sec, t_diff.tv_usec);
+ fprintf(tl_out, "\n%i states, %i transitions\n", bstate_count, btrans_count);
+ }
+--- ./cache.c.orig 2007-08-03 23:44:38.000000000 -0600
++++ ./cache.c 2013-12-09 07:00:00.000000000 -0700
+@@ -43,7 +43,6 @@ static Cache *stored = (Cache *) 0;
+ static unsigned long Caches, CacheHits;
+
+ static int ismatch(Node *, Node *);
+-extern void fatal(char *, char *);
+ int sameform(Node *, Node *);
+
+ void
+@@ -78,7 +77,7 @@ cached(Node *n)
+ Node *m;
+
+ if (!n) return n;
+- if (m = in_cache(n))
++ if ((m = in_cache(n)))
+ return m;
+
+ Caches++;
+@@ -215,7 +214,7 @@ sameform(Node *a, Node *b)
+ case FALSE:
+ return 1;
+ case PREDICATE:
+- if (!a->sym || !b->sym) fatal("sameform...", (char *) 0);
++ if (!a->sym || !b->sym) fatal("sameform...");
+ return !strcmp(a->sym->name, b->sym->name);
+
+ case NOT:
+@@ -237,7 +236,7 @@ sameform(Node *a, Node *b)
+
+ default:
+ printf("type: %d\n", a->ntyp);
+- fatal("cannot happen, sameform", (char *) 0);
++ fatal("cannot happen, sameform");
+ }
+
+ return 0;
+@@ -339,6 +338,6 @@ anywhere(int tok, Node *srch, Node *in)
+ case OR: return any_lor(srch, in);
+ case 0: return any_term(srch, in);
+ }
+- fatal("cannot happen, anywhere", (char *) 0);
++ fatal("cannot happen, anywhere");
+ return 0;
+ }
+--- ./generalized.c.orig 2007-08-03 23:45:16.000000000 -0600
++++ ./generalized.c 2013-12-09 07:00:00.000000000 -0700
+@@ -151,7 +151,7 @@ int simplify_gtrans() /* simplifies the
+ if(tl_stats) {
+ getrusage(RUSAGE_SELF, &tr_fin);
+ timeval_subtract (&t_diff, &tr_fin.ru_utime, &tr_debut.ru_utime);
+- fprintf(tl_out, "\nSimplification of the generalized Buchi automaton - transitions: %i.%06is",
++ fprintf(tl_out, "\nSimplification of the generalized Buchi automaton - transitions: %li.%06lis",
+ t_diff.tv_sec, t_diff.tv_usec);
+ fprintf(tl_out, "\n%i transitions removed\n", changed);
+ }
+@@ -244,7 +244,7 @@ int simplify_gstates() /* eliminates red
+ if(tl_stats) {
+ getrusage(RUSAGE_SELF, &tr_fin);
+ timeval_subtract (&t_diff, &tr_fin.ru_utime, &tr_debut.ru_utime);
+- fprintf(tl_out, "\nSimplification of the generalized Buchi automaton - states: %i.%06is",
++ fprintf(tl_out, "\nSimplification of the generalized Buchi automaton - states: %li.%06lis",
+ t_diff.tv_sec, t_diff.tv_usec);
+ fprintf(tl_out, "\n%i states removed\n", changed);
+ }
+@@ -389,8 +389,7 @@ GState *find_gstate(int *set, GState *s)
+ void make_gtrans(GState *s) { /* creates all the transitions from a state */
+ int i, *list, state_trans = 0, trans_exist = 1;
+ GState *s1;
+- GTrans *t;
+- ATrans *t1, *free;
++ ATrans *t1;
+ AProd *prod = (AProd *)tl_emalloc(sizeof(AProd)); /* initialization */
+ prod->nxt = prod;
+ prod->prv = prod;
+@@ -570,7 +569,6 @@ void mk_generalized()
+ { /* generates a generalized Buchi automaton from the alternating automaton */
+ ATrans *t;
+ GState *s;
+- int i;
+
+ if(tl_stats) getrusage(RUSAGE_SELF, &tr_debut);
+
+@@ -618,13 +616,13 @@ void mk_generalized()
+ if(tl_stats) {
+ getrusage(RUSAGE_SELF, &tr_fin);
+ timeval_subtract (&t_diff, &tr_fin.ru_utime, &tr_debut.ru_utime);
+- fprintf(tl_out, "\nBuilding the generalized Buchi automaton : %i.%06is",
++ fprintf(tl_out, "\nBuilding the generalized Buchi automaton : %li.%06lis",
+ t_diff.tv_sec, t_diff.tv_usec);
+ fprintf(tl_out, "\n%i states, %i transitions\n", gstate_count, gtrans_count);
+ }
+
+ tfree(gstack);
+- /*for(i = 0; i < node_id; i++) /* frees the data from the alternating automaton */
++ /*for(i = 0; i < node_id; i++) frees the data from the alternating automaton */
+ /*free_atrans(transition[i], 1);*/
+ free_all_atrans();
+ tfree(transition);
+--- ./ltl2ba.h.orig 2007-08-04 02:08:02.000000000 -0600
++++ ./ltl2ba.h 2013-12-09 07:00:00.000000000 -0700
+@@ -187,8 +187,8 @@ void addtrans(Graph *, char *, Node *, c
+ void cache_stats(void);
+ void dump(Node *);
+ void exit(int);
+-void Fatal(char *, char *);
+-void fatal(char *, char *);
++void Fatal(const char *) __attribute__((noreturn));
++void fatal(const char *) __attribute__((noreturn));
+ void fsm_print(void);
+ void releasenode(int, Node *);
+ void tfree(void *);
+@@ -227,6 +227,8 @@ int *list_set(int *, int);
+
+ int timeval_subtract (struct timeval *, struct timeval *, struct timeval *);
+
++void put_uform(void);
++
+ #define ZN (Node *)0
+ #define ZS (Symbol *)0
+ #define Nhash 255
+@@ -244,5 +246,5 @@ typedef Node *Nodeptr;
+ #define Explain(x) { if (tl_verbose) tl_explain(x); }
+
+ #define Assert(x, y) { if (!(x)) { tl_explain(y); \
+- Fatal(": assertion failed\n",(char *)0); } }
++ Fatal(": assertion failed\n"); } }
+ #define min(x,y) ((x<y)?x:y)
+--- ./main.c.orig 2007-08-03 23:36:49.000000000 -0600
++++ ./main.c 2013-12-09 07:00:00.000000000 -0700
+@@ -30,6 +30,7 @@
+ /* Some of the code in this file was taken from the Spin software */
+ /* Written by Gerard J. Holzmann, Bell Laboratories, U.S.A. */
+
++#include <unistd.h>
+ #include "ltl2ba.h"
+
+ FILE *tl_out;
+@@ -52,9 +53,9 @@ static char **add_ltl = (char **)0;
+ static char out1[64];
+
+ static void tl_endstats(void);
+-static void non_fatal(char *, char *);
++static void non_fatal(const char *);
+
+-void
++static __attribute__((noreturn)) void
+ alldone(int estatus)
+ {
+ if (strlen(out1) > 0)
+@@ -84,7 +85,7 @@ emalloc(int n)
+ { char *tmp;
+
+ if (!(tmp = (char *) malloc(n)))
+- fatal("not enough memory", (char *)0);
++ fatal("not enough memory");
+ memset(tmp, 0, n);
+ return tmp;
+ }
+@@ -110,7 +111,7 @@ tl_UnGetchar(void)
+ if (cnt > 0) cnt--;
+ }
+
+-void
++static __attribute__((noreturn)) void
+ usage(void)
+ {
+ printf("usage: ltl2ba [-flag] -f formula\n");
+@@ -193,18 +194,20 @@ main(int argc, char *argv[])
+ *ltl_file = (char *) formula;
+ }
+ if (argc > 1)
+- { char cmd[128], out2[64];
++ { char out2[64];
+ strcpy(out1, "_tmp1_");
+ strcpy(out2, "_tmp2_");
+ tl_out = cpyfile(argv[1], out2);
+- tl_main(2, add_ltl);
++ i = tl_main(2, add_ltl);
+ fclose(tl_out);
+ } else
+ {
+ if (argc > 0)
+- exit(tl_main(2, add_ltl));
+- usage();
++ i = tl_main(2, add_ltl);
++ else
++ usage();
+ }
++ return i;
+ }
+
+ /* Subtract the `struct timeval' values X and Y, storing the result X-Y in RESULT.
+@@ -229,7 +232,7 @@ struct timeval *result, *x, *y;
+
+ static void
+ tl_endstats(void)
+-{ extern int Stack_mx;
++{ /* extern int Stack_mx; */
+ printf("\ntotal memory used: %9ld\n", All_Mem);
+ /*printf("largest stack sze: %9d\n", Stack_mx);*/
+ /*cache_stats();*/
+@@ -311,15 +314,12 @@ tl_explain(int n)
+ }
+
+ static void
+-non_fatal(char *s1, char *s2)
++non_fatal(const char *s1)
+ { extern int tl_yychar;
+ int i;
+
+ printf("ltl2ba: ");
+- if (s2)
+- printf(s1, s2);
+- else
+- printf(s1);
++ fputs(s1, stdout);
+ if (tl_yychar != -1 && tl_yychar != 0)
+ { printf(", saw '");
+ tl_explain(tl_yychar);
+@@ -336,20 +336,20 @@ non_fatal(char *s1, char *s2)
+ void
+ tl_yyerror(char *s1)
+ {
+- Fatal(s1, (char *) 0);
++ Fatal(s1);
+ }
+
+ void
+-Fatal(char *s1, char *s2)
++Fatal(const char *s1)
+ {
+- non_fatal(s1, s2);
++ non_fatal(s1);
+ alldone(1);
+ }
+
+ void
+-fatal(char *s1, char *s2)
++fatal(const char *s1)
+ {
+- non_fatal(s1, s2);
++ non_fatal(s1);
+ alldone(1);
+ }
+
+--- ./mem.c.orig 2007-08-03 23:45:50.000000000 -0600
++++ ./mem.c 2013-12-09 07:00:00.000000000 -0700
+@@ -115,7 +115,7 @@ tfree(void *v)
+
+ --m;
+ if ((m->size&0xFF000000) != A_USER)
+- Fatal("releasing a free block", (char *)0);
++ Fatal("releasing a free block");
+
+ u = (m->size &= 0xFFFFFF);
+ if (u >= A_LARGE)
+--- ./rewrt.c.orig 2007-08-03 23:46:08.000000000 -0600
++++ ./rewrt.c 2013-12-09 07:00:00.000000000 -0700
+@@ -60,7 +60,7 @@ canonical(Node *n)
+ { Node *m; /* assumes input is right_linked */
+
+ if (!n) return n;
+- if (m = in_cache(n))
++ if ((m = in_cache(n)))
+ return m;
+
+ n->rgt = canonical(n->rgt);
+@@ -318,7 +318,7 @@ out:
+ #endif
+ if (!can)
+ { if (!dflt)
+- fatal("cannot happen, Canonical", (char *) 0);
++ fatal("cannot happen, Canonical");
+ return dflt;
+ }
+
diff --git a/ltl2ba.spec b/ltl2ba.spec
index 79c814d..6e524bf 100644
--- a/ltl2ba.spec
+++ b/ltl2ba.spec
@@ -1,12 +1,14 @@
Name: ltl2ba
Version: 1.1
-Release: 7%{?dist}
+Release: 8%{?dist}
Summary: Fast translation from LTL formulas to Buchi automata
Group: Applications/Engineering
License: GPLv2+
URL: http://www.lsv.ens-cachan.fr/~gastin/ltl2ba/
Source0: http://www.lsv.ens-cachan.fr/~gastin/ltl2ba/%{name}-%{version}.tar.gz
+# Fix gcc warnings and -Werror=format-security error
+Patch0: %{name}-warning.patch
%description
Translate from Linear temporal logic (LTL) formulas to Buchi automata.
@@ -25,9 +27,10 @@ presented at the CAV Conference, held in 2001, Paris, France 2001.
%prep
%setup -q
+%patch0
%build
-make %{?_smp_mflags} CFLAGS="%{optflags} -ansi -DNXT"
+make %{?_smp_mflags} CFLAGS="%{optflags} -DNXT"
iconv -f latin1 -t utf8 README > README.utf8
mv README.utf8 README
@@ -46,6 +49,9 @@ cp -p ltl2ba $RPM_BUILD_ROOT%{_bindir}
%changelog
+* Mon Dec 9 2013 Jerry James <loganjerry at gmail.com>
+- Add -warning patch (bz 1037182)
+
* Sat Aug 03 2013 Fedora Release Engineering <rel-eng at lists.fedoraproject.org> - 1.1-7
- Rebuilt for https://fedoraproject.org/wiki/Fedora_20_Mass_Rebuild
More information about the scm-commits
mailing list