synchronised stmt

Author: laurayuwen

src/common/stmt-syntax.k

@@ -63,12 +63,8 @@ syntax BreakStmt ::= "break" K ";" [klabel('Break)]
 syntax ReturnStmt ::= "return" K ";" [klabel('Return)]
 
 syntax SynchronizedStmt ::= "synchronized" "(" Exp ")" Block [strict(1),klabel('Synchronized)]
-//todo
+//todo: replace Exp with StmtExp
 syntax ExprStmt ::= Exp ";"  [strict, klabel('ExprStm)]
-//syntax InternalUse ::= TypedVal ";"
-
-
-
 
 endmodule
 

src/exec/api-threads.k

@@ -43,22 +43,13 @@ when
     Class ==K class String2Id("java.lang.Thread") andBool Id2String(MethodName) ==String "startImpl"
 
 //@ \subsection{Synchronized statement}
-// 'Synchronized(objectRef(...)::_,, Block)
-//syntax KLabel ::= "'Synchronized"
-//evaluate the expression
-//context 'Synchronized(HOLE,, _)
 
 rule [Synchronized-first-time]:
     <k>
-      'Synchronized(objectRef(OId:Int,_)::_,, Block:K)
-      => 'Try(Block,, [.KList],, releaseLock(OId))
-      ...
+          synchronized (objectRef(OId:Int,_)::_) Block:Block
+          => try Block [.KList] finally releaseLock(OId)
+          ...
     </k>
-//    <k>
-//          synchronized (objectRef(OId:Int,_)::_) Block:Block
-//          => 'Try(Block,, [.KList],, releaseLock(OId))
-//          ...
-//        </k>
     <holds>... (. => OId |-> 1) ...</holds>
     <busy> Busy:Set (. => SetItem(OId)) </busy>
 when
@@ -67,15 +58,15 @@ when
 
 rule [Synchronized-nested]:
     <k>
-      'Synchronized(objectRef(OId:Int,_)::_,, Block:K)
-      => 'Try(Block,, [.KList],, releaseLock(OId))
+            synchronized (objectRef(OId:Int,_)::_) Block:Block
+            => try Block [.KList] finally releaseLock(OId)
       ...
     </k>
     <holds>... OId |-> (Level:Int => Level +Int 1) ...</holds>
         [transition-threading, transition-sync]
 
 rule [Synchronized-on-null]:
-    'Synchronized(null::_,,_) => throw new classNullPointerException(null::classString);
+    synchronized (null::_) _ => throw new classNullPointerException(null::classString);
 
 /*@Release one level of lock for the given object.*/
 syntax KItem ::=  releaseLock ( Int )