Merge branch 'master' of ssh://cremersc@buckleburg.inf.ethz.ch/home/cremersc/repos/scyther

protocols/misc/tls/tls-paulson-avispa.spdl

@@ -15,7 +15,9 @@ secret unkeygen: Function;
 inversekeys(keygen, unkeygen);
 
 const pa,pb: Params;
+const Alice,Bob: Agent;
 const Terence: Agent;
+const Sally: Agent;
 const false,true: Bool;
 
 

src/compiler.c

@@ -2213,8 +2213,10 @@ preprocess (const System sys)
   /*
    * Check well-formedness
    */
+  /* TODO Temporarily disabled wellformedness check (well-formedness) after Simon bug reporting.
   if (sys->knowledgedefined)
     {
       checkWellFormed (sys);
     }
+  */
 }

src/intruderknowledge.c

@@ -115,6 +115,13 @@ anySubTerm (Term t, Termlist sublist)
 void
 initialIntruderKnowledge (const System sys)
 {
+  /*
+  TODO this is buggy and leads to a segfault with Simon's example (bug report for wellformedness check)
+  Disabled for now.
+  ./scyther-linux simple-challenge-SEGFAULT.spdl
+  */
+  return;
+
   /*
    * display initial role knowledge
    */