From aad9547029ec8dbe2c62666f3a8f7034deca5095 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Dominic=20H=C3=B6glinger?= <dominic@hoeglinger.eu>
Date: Sun, 20 Nov 2022 22:44:06 +0100
Subject: [PATCH] added comment capability

---
 analyze.py    | 26 +++++++++++++--
 model_bad.smv | 30 ++++++++++++++++++
 test_bad.c    | 87 +++++++++++++++++++++++++++++++++++++++++++++++++++
 3 files changed, 140 insertions(+), 3 deletions(-)
 create mode 100644 model_bad.smv
 create mode 100644 test_bad.c

diff --git a/analyze.py b/analyze.py
index 00483a7..4eeadcf 100644
--- a/analyze.py
+++ b/analyze.py
@@ -1,7 +1,8 @@
 from __future__ import print_function
 import argparse
 import sys
-from pycparser import parse_file, c_ast
+import re
+from pycparser import parse_file, c_ast, CParser
 import graphviz as gv
 
 from modelbuilder import *
@@ -168,10 +169,22 @@ class SwitchCaseCodePropertyVisitor(c_ast.NodeVisitor):
             scpv.visit(block)
             self.properties += scpv.properties
 
+def comment_remover(text):
+    def replacer(match):
+        s = match.group(0)
+        if s.startswith('/'):
+            return ""
+        else:
+            return s
+    pattern = re.compile(
+        r'//.*?$|/\*.*?\*/|\'(?:\\.|[^\\\'])*\'|"(?:\\.|[^\\"])*"',
+        re.DOTALL | re.MULTILINE
+    )
+    return re.sub(pattern, replacer, text)
+
 if __name__ == "__main__":
     argparser = argparse.ArgumentParser('Create a Kripke Structure Model from C Code')
     argparser.add_argument('filename',
-                           default='examples/c_files/basic.c',
                            nargs='?',
                            help='name of file to parse')
     argparser.add_argument('--coord', help='show coordinates in the dump',
@@ -185,7 +198,14 @@ if __name__ == "__main__":
     argparser.add_argument('--dot', help='output dot file')
     args = argparser.parse_args()
 
-    ast = parse_file(args.filename, use_cpp=False)
+    source = ""
+    with open(args.filename, "r") as f:     
+        #read whole file to a string
+        source = f.read()
+    
+    parser = CParser()
+    ast = parser.parse(comment_remover(source))
+    #ast = parse_file(args.filename, use_cpp=False)
 
     fdv = FuncDefVisitor()
     fdv.visit(ast)
diff --git a/model_bad.smv b/model_bad.smv
new file mode 100644
index 0000000..b3670ff
--- /dev/null
+++ b/model_bad.smv
@@ -0,0 +1,30 @@
+
+------------------------------------------------------------------------
+-- Generated using Kripkomat
+------------------------------------------------------------------------
+MODULE main
+VAR
+state : { STATE_I,STATE_C,STATE_D,STATE_A,STATE_B };
+ASSIGN
+    init(state) := STATE_I;
+    next(state) :=
+        case
+            state = STATE_I : {STATE_A,STATE_B};
+            state = STATE_C : {STATE_A};
+            state = STATE_D : {STATE_B};
+            state = STATE_A : {STATE_C,STATE_D};
+            state = STATE_B : {STATE_C};
+        esac;
+DEFINE
+    -- Property "p_fsm->m_b<=true"
+    a := state = STATE_C | state = STATE_B;
+
+    -- Property "p_fsm->m_a<=true"
+    b := state = STATE_B;
+
+LTLSPEC
+    X b;
+LTLSPEC
+    F a;
+LTLSPEC
+    G( a -> F(b));
diff --git a/test_bad.c b/test_bad.c
new file mode 100644
index 0000000..c21b395
--- /dev/null
+++ b/test_bad.c
@@ -0,0 +1,87 @@
+/* 
+ * Test Bad
+ * Bad example.
+ */
+
+typedef char bool;
+
+typedef enum
+{
+    STATE_I = 0,
+    STATE_A,
+    STATE_B,
+    STATE_C,
+    STATE_D
+}
+testfsm_state_t;
+
+typedef struct
+{
+    testfsm_state_t m_state;
+    bool m_a;
+    bool m_b;
+} testfsm_t;
+
+void process(testfsm_t *p_fsm, const bool input)
+{
+    testfsm_state_t nextState = p_fsm->m_state;
+
+    p_fsm->m_a = false;
+    p_fsm->m_b = false;
+
+    switch(p_fsm->m_state)
+    {
+        case STATE_I:
+            if (!input)
+                nextState = STATE_A;
+            else
+                nextState = STATE_B;
+            break;
+        case STATE_A:
+            //p_fsm->m_a = true; //oops
+            if (!input)
+                nextState = STATE_D;
+            else
+                nextState = STATE_C;
+            break;
+        case STATE_B:
+            p_fsm->m_a = true;
+            p_fsm->m_b = true;
+            nextState = STATE_C;
+            break;
+        case STATE_C:
+            p_fsm->m_b = true;
+            nextState = STATE_A;
+            break;
+        case STATE_D:
+            nextState = STATE_B;
+            break;
+    }
+
+    p_fsm->m_state = nextState;
+}
+
+bool randbool(int throws)
+{
+    bool stillTrue = true;
+    for (int i = 0; i < throws; ++i)
+    {
+        stillTrue &= rand() & 1;
+    }
+    return stillTrue;
+}
+
+int main()
+{
+    testfsm_t fsm = { .m_state = STATE_I, .m_a = false, .m_b = false };
+    bool input = false;
+
+    srand(0);
+    for (int j = 0; j < 100; ++j)
+    {
+        input = randbool(1);
+        process(&fsm, input);
+    }
+
+    return 0;
+}