[LFSC] Minor fixes/improvements

- Avoid mixing new/delete with malloc/free
- Remove reimplementation of strcmp
- Add assertions

diff --git a/proofs/lfsc_checker/check.cpp b/proofs/lfsc_checker/check.cpp
index 22e326cdae86a89f9ff4a8d685dfda61b31831d8..493b3ecc7c4ff888130ed310be28f5999772cb52 100644 (file)
--- 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 094a9060a6340ce22e0d61d6a3aa6bee9e016765..401fdb453b7b8fba763616ca232639a224f3b436 100644 (file)
--- 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();