diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2017-01-04 12:21:52 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2017-01-04 12:21:52 -0600 |
commit | a3094c713b73c6941f1f564bab33110927466526 (patch) | |
tree | 1fc232dc5fb9eae0616589f9b8d239b4f272ca83 /proofs | |
parent | 8c99adc0fab8e482023750628431fe28ef49438b (diff) | |
parent | 27b9bd8cad995180f466e440df7c2b4db26ad6e1 (diff) |
Merge pull request #122 from 4tXJ7f/fix_lfsc_str
[LFSC] Minor fixes/improvements
Diffstat (limited to 'proofs')
-rw-r--r-- | proofs/lfsc_checker/check.cpp | 32 | ||||
-rw-r--r-- | proofs/lfsc_checker/trie.h | 18 |
2 files changed, 20 insertions, 30 deletions
diff --git a/proofs/lfsc_checker/check.cpp b/proofs/lfsc_checker/check.cpp index 222c10615..e100efa69 100644 --- a/proofs/lfsc_checker/check.cpp +++ b/proofs/lfsc_checker/check.cpp @@ -941,15 +941,14 @@ void check_file(const char *_filename, args a, sccwriter* scw, libwriter* lw) { run_scc = a.run_scc; tail_calls = !a.no_tail_calls; - - char *f; + std::string f; if (strcmp(_filename,"stdin") == 0) { curfile = stdin; - f = strdup(_filename); + f = std::string(_filename); } else { if (prev_curfile) { - f = strdup(prev_filename); + f = std::string(prev_filename); #ifdef _MSC_VER std::string str( f ); for( int n=str.length(); n>=0; n-- ){ @@ -960,26 +959,24 @@ void check_file(const char *_filename, args a, sccwriter* scw, libwriter* lw) { } char *tmp = (char*)str.c_str(); #else - char *tmp = dirname(f); + // Note: dirname may modify its argument, so we create a non-const copy. + char *f_copy = strdup(f.c_str()); + std::string str = std::string(dirname(f_copy)); + free(f_copy); #endif - delete f; - f = new char[strlen(tmp) + 10 + strlen(_filename)]; - strcpy(f,tmp); - strcat(f,"/"); - strcat(f,_filename); + f = str + std::string("/") + std::string(_filename); + } else { + f = std::string(_filename); } - else - f = strdup(_filename); - curfile = fopen(f,"r"); + curfile = fopen(f.c_str(), "r"); if (!curfile) - report_error(string("Could not open file \"") - + string(f) - + string("\" for reading.\n")); + report_error(string("Could not open file \"") + f + + string("\" for reading.\n")); } linenum = 1; colnum = 1; - filename = f; + filename = f.c_str(); char c; while ((c = non_ws()) && c!=EOF ) { @@ -1286,7 +1283,6 @@ void check_file(const char *_filename, args a, sccwriter* scw, libwriter* lw) { } } } - free(f); if (curfile != stdin) fclose(curfile); linenum = prev_linenum; diff --git a/proofs/lfsc_checker/trie.h b/proofs/lfsc_checker/trie.h index 094a9060a..401fdb453 100644 --- a/proofs/lfsc_checker/trie.h +++ b/proofs/lfsc_checker/trie.h @@ -1,9 +1,10 @@ #ifndef sc2__trie_h #define sc2__trie_h -#include <vector> -#include <string.h> +#include <assert.h> #include <stdlib.h> +#include <string.h> +#include <vector> template<class Data> class Trie { @@ -15,6 +16,7 @@ protected: // s is assumed to be non-empty (and non-null) Data insert_next(const char *s, const Data &x) { + assert(s != NULL && s[0] != '\0'); unsigned c = s[0]; if (c >= next.size()) { using_next = true; @@ -29,6 +31,7 @@ protected: // s is assumed to be non-empty (and non-null) Data get_next(const char *s) { + assert(s != NULL && s[0] != '\0'); unsigned c = s[0]; if (c >= next.size()) return Data(); @@ -51,19 +54,10 @@ public: static Cleaner *cleaner; - bool eqstr(const char *s1, const char *s2) { - while (*s1 && *s2) { - if (*s1++ != *s2++) - return false; - } - return (*s1 == *s2); - } - Data get(const char *s) { if (!s[0] && (!str || !str[0])) return d; - if (str && eqstr(str,s)) - return d; + if (str && strcmp(str, s) == 0) return d; if (using_next) return get_next(s); return Data(); |