diff --git a/latte-umbrella/src/main/java/examples/MyStackTest.java b/latte-umbrella/src/main/java/examples/MyStackTest.java index c405da0..3a1bc2f 100644 --- a/latte-umbrella/src/main/java/examples/MyStackTest.java +++ b/latte-umbrella/src/main/java/examples/MyStackTest.java @@ -1,186 +1,59 @@ package examples; -import java.io.BufferedReader; -import java.io.InputStream; -import java.io.InputStreamReader; -import java.util.ArrayList; -import specification.Borrowed; -import specification.Free; -import specification.Shared; -import specification.Unique; +public class MyStackTest { -import java.io.UnsupportedEncodingException; + public static void main(String[] args) { -public class MyStackTest { -} + // Define and initialize queues + LinkedList qev1, qev2, qcv1, qcv2; + qev1 = new LinkedList<>(); + qev2 = new LinkedList<>(); + qcv1 = new LinkedList<>(); + qcv2 = new LinkedList<>(); + qev1.add(100); + qev1.add(200); + qev1.add(300); + qev1.add(300); + qev1.add(300); + qev1.add(300); -class Test { - public static void test(HttpResponse r) throws UnsupportedEncodingException { - HttpResponse response = r; - InputStream in = response.getEntity().getContent(); - BufferedReader reader = new BufferedReader( - new InputStreamReader( - response.getEntity().getContent(), "UTF-8")); // Second call to getEntity() + // Get an iterator for the queue + Iterator iterator = qev1.iterator(); - //Cannot call getContent twice if the entity is not repeatable. There is a method isRepeatable() to check - } -} + try { + iterator.remove(); // Error no call to next before remove + } + catch(UnsupportedOperationException e) { + System.out.println("Calling Iterator.remove() and throwing exception."); + } -class HttpResponse { - // TODO: STUB METHOD - public HttpEntity getEntity() { - return new HttpEntity(); } + } -class HttpEntity { - // TODO: STUB METHOD - public InputStream getContent() { - return (InputStream) new Object(); - } +// @ExternalRefinementsFor("java.util.Iterator") +// @StateSet({"start", "ready", "inNext"}) +class Iterator { + + // @StateRefinement(to = "start(this)") + public Iterator(){} + + // @StateRefinement(to = "ready(this)") + public boolean hasNext(){return true;} + + // @StateRefinement(from = "ready(this)", to = "inNext(this)") + public Object next(){return null;} + + // @StateRefinement(from = "inNext(this)", to = "start(this)") + public void remove(){} } +// @ExternalRefinementsFor("java.util.LinkedList") +class LinkedList { + public Iterator iterator(){return null;} -// class Box { -// @Unique int value; -// void add(@Owned int delta) { -// // ERROR: RHS and LHS are not separately unique -// this.value = this.value + this.delta; -// } -// void test() { -// int x = 123; -// Box b1 = new Box(x); -// // ERROR: ‘x‘ is consumed since ‘value‘ is unique, -// // thus it is unaccessible -// Box b2 = new Box(x); -// } -// void makeBox2() { -// // ERROR: ‘this.value‘ is unique, thus cannot be -// // passed to a shared parameter -// return new Box2(this.value); -// } -// } -// class Box2 { @Shared int value; } - - - -// HttpResponse response = r; -// InputStream in = response.getEntity().getContent(); -// BufferedReader reader = new BufferedReader( -// new InputStreamReader( -// response.getEntity().getContent(), "UTF-8")); // Second call to getEntity() - - - -// @Unique Node root; - -// public MyStack(@Free Node root) { -// this.root = root; -// } - - -// void push( @Free Object value) { -// Node r; -// Node n; - -// r = this.root; // save root in r -// this.root = null; //nullify root -// n = new Node(value, r); //create new root -// this.root = n; //replace root -// } - - -// @Free Object pop (){ -// Object value; - -// if (this.root == null) { -// value = null; -// } else { -// Node r = root; -// value = r.value; -// Node n; -// n = r.next; -// r.next = null; -// r.value = null; -// this.root = n; -// } -// return value; -// } - -// // public @Unique Object dequeue() { -// // Node r = this.root; -// // //r : alias(this.root) -// // if (r == null || r.next == null) { -// // // In an empty or single-element stack, dequeue and pop -// // // are equivalent -// // return pop(); -// // } else { - -// // // `this` and `this.root` are effectively alias, thus -// // // we cannot pass `this.root` to `this.dequeue` without -// // // doing a destructive read -// // this.root = null; -// // // r : unique - -// // Object value = dequeueHelper(r); -// // // value : unique - -// // // Since `dequeue` only detaches the next node of the one -// // // passed to it, it will never need to detach `root`, so -// // // we can just restore it back to the original value. -// // this.root = r; -// // // r : alias(this.root) - -// // return value; -// // } -// // } - -// // private @Free Object dequeueHelper(@Borrowed Node n) { -// // // Look ahead two steps so that we can disconnect the *next* -// // // node by mutating the node that will remain in the stack. - -// // Node nn = n.next; -// // // nn : alias(n.next) - -// // if (nn.next == null) { -// // n.next = null; -// // // nn : unique - -// // Object value = nn.value; -// // // value : alias(nn.value) - -// // nn.value = null; -// // // value : unique - -// // return value; -// // } else { -// // return dequeueHelper(n.next); -// // } -// // } -// } - -// /** -// * Node class for the stack example -// * Uses @Unique annotations to specify that the value and next fields are unique -// * in the scope of the Node class -// * @author catarina gamboa -// * -// */ -// class Node { - -// @Unique Object value; -// @Unique Node next; - -// /** -// * Constructor for the Node class using @Free value and next nodes -// * @param value -// * @param next -// */ -// public Node (@Free Object value, @Free Node next) { -// this.value = value; -// this.next = next; -// } -// } + public void add(T t){} +} \ No newline at end of file diff --git a/latte-umbrella/src/test/examples/ResultSetForwardOnly.java b/latte-umbrella/src/test/examples/searching_state_space/ResultSetForwardOnly.java similarity index 100% rename from latte-umbrella/src/test/examples/ResultSetForwardOnly.java rename to latte-umbrella/src/test/examples/searching_state_space/ResultSetForwardOnly.java diff --git a/latte-umbrella/src/test/examples/ResultSetNoNext.java b/latte-umbrella/src/test/examples/searching_state_space/ResultSetNoNext.java similarity index 88% rename from latte-umbrella/src/test/examples/ResultSetNoNext.java rename to latte-umbrella/src/test/examples/searching_state_space/ResultSetNoNext.java index daf205b..cfc135b 100644 --- a/latte-umbrella/src/test/examples/ResultSetNoNext.java +++ b/latte-umbrella/src/test/examples/searching_state_space/ResultSetNoNext.java @@ -5,7 +5,7 @@ import specification.Free; import specification.Unique; -public class ResultSetNoNext { +public class SSSResultSetNoNext { /* @@ -42,19 +42,19 @@ public PreparedStatement prepareStatement(String s) { // prepareStatement​(String sql, int resultSetType, int resultSetConcurrency){} } - class PreparedStatement{ void setString(int index, String s){} - // @StateRefinement(return, to="TYPE_FORWARD_ONLY, col == -1") + // @ReturnState( to="TYPE_FORWARD_ONLY, beforeRow") ResultSet executeQuery(String s){return null;} } + //@StateSet({"beforeRow", "onRow"}) class ResultSet{ - // @StateRefinement(this, col > 0) + // @StateRefinement( from = "onRow") float getFloat(String s){return 0;} - // @StateRefinement(this, col == old(col) + 1) + // @StateRefinement( to="onRow") void next(){} } diff --git a/latte-umbrella/src/test/examples/TimerTaskCannotReschedule.java b/latte-umbrella/src/test/examples/searching_state_space/TimerTaskCannotReschedule.java similarity index 85% rename from latte-umbrella/src/test/examples/TimerTaskCannotReschedule.java rename to latte-umbrella/src/test/examples/searching_state_space/TimerTaskCannotReschedule.java index cdb64d8..4aa2d6e 100644 --- a/latte-umbrella/src/test/examples/TimerTaskCannotReschedule.java +++ b/latte-umbrella/src/test/examples/searching_state_space/TimerTaskCannotReschedule.java @@ -3,7 +3,7 @@ import specification.Borrowed; import specification.Free; -public class TimerTaskCannotReschedule { +public class SSSTimerTaskCannotReschedule { /* * Error cannot reschedule a timer @@ -47,12 +47,12 @@ public void schedule(TimerTask task, /* delay > 0 */int delay) {} // timer.cancel(); // // Step 3) Schedule a new task for this timer -> ERROR Cannot reschedule a Timer -// timer.schedule(new TimerTask() { -// @Override -// public void run() { -// System.out.println("Timer task completed."); -// } -// }, 1000); + // timer.schedule(new TimerTask() { + // @Override + // public void run() { + // System.out.println("Timer task completed."); + // } + // }, 1000); // } diff --git a/latte-umbrella/src/test/examples/URLConnectionReuseConnection.java b/latte-umbrella/src/test/examples/searching_state_space/URLConnectionReuseConnection.java similarity index 97% rename from latte-umbrella/src/test/examples/URLConnectionReuseConnection.java rename to latte-umbrella/src/test/examples/searching_state_space/URLConnectionReuseConnection.java index 32b3e87..f43398a 100644 --- a/latte-umbrella/src/test/examples/URLConnectionReuseConnection.java +++ b/latte-umbrella/src/test/examples/searching_state_space/URLConnectionReuseConnection.java @@ -1,7 +1,7 @@ import specification.Borrowed; import specification.Unique; -public class URLConnectionReuseConnection { +public class SSSURLConnectionReuseConnection { public static void example4278917(@Borrowed URL address) { diff --git a/latte-umbrella/src/test/examples/URLConnectionSetProperty1.java b/latte-umbrella/src/test/examples/searching_state_space/URLConnectionSetProperty1.java similarity index 93% rename from latte-umbrella/src/test/examples/URLConnectionSetProperty1.java rename to latte-umbrella/src/test/examples/searching_state_space/URLConnectionSetProperty1.java index e3467d6..adf909f 100644 --- a/latte-umbrella/src/test/examples/URLConnectionSetProperty1.java +++ b/latte-umbrella/src/test/examples/searching_state_space/URLConnectionSetProperty1.java @@ -3,7 +3,7 @@ import java.io.IOException; import java.io.InputStream; -public class URLConnectionSetProperty1 { +public class SSSURLConnectionSetProperty1 { public static void example331538(@Borrowed URL address) { try { @@ -14,8 +14,7 @@ public static void example331538(@Borrowed URL address) { // Step 2) Setup parameters and connection properties cnx.setAllowUserInteraction(false); // Step 2) cnx.setDoOutput(true); - cnx.addRequestProperty("User-Agent", - "Mozilla/4.0 (compatible; MSIE 6.0; Windows NT 5.0)"); + cnx.addRequestProperty("User-Agent", "Mozilla/4.0 (compatible; MSIE 6.0; Windows NT 5.0)"); // Step 3) diff --git a/latte-umbrella/src/test/examples/URLConnectionSetPropertyMultipleComplete.java b/latte-umbrella/src/test/examples/searching_state_space/URLConnectionSetPropertyMultipleComplete.java similarity index 98% rename from latte-umbrella/src/test/examples/URLConnectionSetPropertyMultipleComplete.java rename to latte-umbrella/src/test/examples/searching_state_space/URLConnectionSetPropertyMultipleComplete.java index a50dd0a..ba94f96 100644 --- a/latte-umbrella/src/test/examples/URLConnectionSetPropertyMultipleComplete.java +++ b/latte-umbrella/src/test/examples/searching_state_space/URLConnectionSetPropertyMultipleComplete.java @@ -6,7 +6,7 @@ import specification.Shared; import specification.Unique; -public class URLConnectionSetPropertyMultipleComplete { +public class SSSURLConnectionSetPropertyMultipleComplete { String sessionId = "1234"; public void example5368535(@Borrowed URL address, String content) { diff --git a/latte-umbrella/src/test/examples/URLConnectionSetPropertyMultipleShort.java b/latte-umbrella/src/test/examples/searching_state_space/URLConnectionSetPropertyMultipleShort.java similarity index 98% rename from latte-umbrella/src/test/examples/URLConnectionSetPropertyMultipleShort.java rename to latte-umbrella/src/test/examples/searching_state_space/URLConnectionSetPropertyMultipleShort.java index 3a2792d..f465657 100644 --- a/latte-umbrella/src/test/examples/URLConnectionSetPropertyMultipleShort.java +++ b/latte-umbrella/src/test/examples/searching_state_space/URLConnectionSetPropertyMultipleShort.java @@ -6,7 +6,7 @@ import specification.Shared; import specification.Unique; -public class URLConnectionSetPropertyMultipleShort { +public class SSSURLConnectionSetPropertyMultipleShort { String sessionId = "1234"; public void example5368535(@Borrowed URL address, String content) { diff --git a/latte-umbrella/src/test/examples/stack_overflow/Iterator.java b/latte-umbrella/src/test/examples/stack_overflow/Iterator.java new file mode 100644 index 0000000..6f521ea --- /dev/null +++ b/latte-umbrella/src/test/examples/stack_overflow/Iterator.java @@ -0,0 +1,5 @@ +public class Iterator { + + + +} diff --git a/latte-umbrella/src/test/examples/stack_overflow/MediaRecord.java b/latte-umbrella/src/test/examples/stack_overflow/MediaRecord.java new file mode 100644 index 0000000..391aede --- /dev/null +++ b/latte-umbrella/src/test/examples/stack_overflow/MediaRecord.java @@ -0,0 +1,70 @@ +package examples; +import java.util.TimerTask; + +import specification.Borrowed; +import specification.Free; +import specification.Unique; + +public class MediaRecord { + + public static void test( boolean isChecked) { + MediaRecorder recorder = new MediaRecorder(); + + recorder.setAudioSource(); + recorder.setOutputFormat(); + recorder.setAudioEncoder(); + recorder.setOutputFile(); + + while (isChecked) { // While loop will make it start and stop multiple times + recorder.start(); // here it were it throws + //... + recorder.stop(); + } + + } + + + public static void test2( boolean isChecked) { + MediaRecorder recorder = new MediaRecorder(); + + recorder.setAudioSource(); + recorder.setVideoSource(); + recorder.setOutputFormat(); + recorder.setProfile(); // setProfile error + // From stackoverflow - setProfile() tries to setOutputFormat but cannot because it is already explicitly set - which makes it redundant + // From documentation - setProfile() should be done after setAudioSource and setVideoSource and after should be setOutputFile - however, it does not appear in the SM + } + +} +// From website - https://developer.android.com/reference/android/media/MediaRecorder +//@StateSet(initial, initialized, dataSourceConfigured, prepared, recording, released, error) + class MediaRecorder { + + public static final String AudioSource = null; + + // @StateRefinement(from="prepared", to="recording") + public void start() {} + + // @StateRefinement(from="recording", to="initial") + public void stop() {} + + // @StateRefinement(from="initial", to="initialized") + public void setAudioSource() {} + + // @StateRefinement(from="initialized", to="dataSourceConfigured") + public void setOutputFormat() {} + + // @StateRefinement(from="dataSourceConfigured") + public void setAudioEncoder() {} + + // @StateRefinement(from="dataSourceConfigured") + public void setOutputFile() {} + + // @StateRefinement(from="dataSourceConfigured") + public void setVideoSource() {} + + // Not in the SM but seems to be this + // @StateRefinement(from="initialized", to="dataSourceConfigured") + public void setProfile() {} + +} diff --git a/latte-umbrella/src/test/java/latte/latte_umbrella/AppTest.java b/latte-umbrella/src/test/java/latte/latte_umbrella/AppTest.java index 23a861a..65329eb 100644 --- a/latte-umbrella/src/test/java/latte/latte_umbrella/AppTest.java +++ b/latte-umbrella/src/test/java/latte/latte_umbrella/AppTest.java @@ -92,7 +92,7 @@ public void testHttpEntityNoAnnotations(){ @Test public void testURLConnectionReuseConnection(){ try { - App.launcher("src/test/examples/URLConnectionReuseConnection.java"); + App.launcher("src/test/examples/searching_state_space/URLConnectionReuseConnection.java"); } catch (Exception e) { e.printStackTrace(); assert(false); @@ -102,7 +102,7 @@ public void testURLConnectionReuseConnection(){ @Test public void testURLConnectionSetProperty1(){ try { - App.launcher("src/test/examples/URLConnectionSetProperty1.java"); + App.launcher("src/test/examples/searching_state_space/URLConnectionSetProperty1.java"); } catch (Exception e) { e.printStackTrace(); assert(false); @@ -112,7 +112,7 @@ public void testURLConnectionSetProperty1(){ @Test public void testURLConnectionSetPropertyMultipleShort(){ try { - App.launcher("src/test/examples/URLConnectionSetPropertyMultipleShort.java"); + App.launcher("src/test/examples/searching_state_space/URLConnectionSetPropertyMultipleShort.java"); } catch (Exception e) { e.printStackTrace(); assert(false); @@ -122,7 +122,7 @@ public void testURLConnectionSetPropertyMultipleShort(){ @Test public void testTimerTaskCannotReschedule(){ try { - App.launcher("src/test/examples/TimerTaskCannotReschedule.java"); + App.launcher("src/test/examples/searching_state_space/TimerTaskCannotReschedule.java"); } catch (Exception e) { e.printStackTrace(); assert(false); @@ -132,7 +132,7 @@ public void testTimerTaskCannotReschedule(){ @Test public void testResultSetNoNext(){ try { - App.launcher("src/test/examples/ResultSetNoNext.java"); + App.launcher("src/test/examples/searching_state_space/ResultSetNoNext.java"); } catch (Exception e) { e.printStackTrace(); assert(false); @@ -142,13 +142,23 @@ public void testResultSetNoNext(){ @Test public void testResultSetForwardOnly(){ try { - App.launcher("src/test/examples/ResultSetForwardOnly.java"); + App.launcher("src/test/examples/searching_state_space/ResultSetForwardOnly.java"); } catch (Exception e) { e.printStackTrace(); assert(false); } } - + + @Test + public void testSOSMediaRecord(){ + try { + App.launcher("src/test/examples/stack_overflow/MediaRecord.java"); + } catch (Exception e) { + e.printStackTrace(); + assert(false); + } + } + /* * Incorrect Examples */