From 2df34ccb1f712c68910011349a629c5af93428d2 Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Wed, 12 Feb 2025 11:32:02 +0000 Subject: [PATCH 1/4] add example for urlconnection reuse --- .../ResultSetForwardOnly.java | 94 +++++++++++++++ .../ResultSetNoNext.java | 64 ++++++++++ .../TimerTaskCannotReschedule.java | 59 +++++++++ .../URLConnectionReuseConnection.java | 57 +++++++++ .../URLConnectionSetProperty1.java | 78 ++++++++++++ ...ConnectionSetPropertyMultipleComplete.java | 114 ++++++++++++++++++ ...URLConnectionSetPropertyMultipleShort.java | 103 ++++++++++++++++ .../examples/stack_overflow/Iterator.java | 5 + .../examples/stack_overflow/MediaRecord.java | 70 +++++++++++ 9 files changed, 644 insertions(+) create mode 100644 latte-umbrella/src/test/examples/searching_state_space/ResultSetForwardOnly.java create mode 100644 latte-umbrella/src/test/examples/searching_state_space/ResultSetNoNext.java create mode 100644 latte-umbrella/src/test/examples/searching_state_space/TimerTaskCannotReschedule.java create mode 100644 latte-umbrella/src/test/examples/searching_state_space/URLConnectionReuseConnection.java create mode 100644 latte-umbrella/src/test/examples/searching_state_space/URLConnectionSetProperty1.java create mode 100644 latte-umbrella/src/test/examples/searching_state_space/URLConnectionSetPropertyMultipleComplete.java create mode 100644 latte-umbrella/src/test/examples/searching_state_space/URLConnectionSetPropertyMultipleShort.java create mode 100644 latte-umbrella/src/test/examples/stack_overflow/Iterator.java create mode 100644 latte-umbrella/src/test/examples/stack_overflow/MediaRecord.java diff --git a/latte-umbrella/src/test/examples/searching_state_space/ResultSetForwardOnly.java b/latte-umbrella/src/test/examples/searching_state_space/ResultSetForwardOnly.java new file mode 100644 index 0000000..5a9c115 --- /dev/null +++ b/latte-umbrella/src/test/examples/searching_state_space/ResultSetForwardOnly.java @@ -0,0 +1,94 @@ +package examples; + + +import java.util.TimerTask; + +import specification.Borrowed; +import specification.Free; +import specification.Unique; + +public class ResultSetForwardOnly { + /* + * Error ResultSet is FORWARD_ONLY and we try to get a value before + */ + public static void example6367737(Connection con, String username, String password ) throws Exception { + + // Step 1) Prepare the statement + PreparedStatement pstat = + con.prepareStatement("select typeid from users where username=? and password=?"); + + // Step 2) Set parameters for the statement + pstat.setString(1, username); + pstat.setString(2, password); + + // Step 3) Execute the query + ResultSet rs = pstat.executeQuery(); + + // Step 4) Process the result + int rowCount=0; + while(rs.next()){ + rowCount++; + } + + // ERROR! because it is FORWARD_ONLY, we cannot go back and check beforeFirst + rs.beforeFirst(); + + int typeID = 0; // ... + + // To be correct we need to change the resultset to be scrollable + /*PreparedStatement pstat = + con.prepareStatement("select typeid from users where username=? and password=?", + ResultSet.TYPE_SCROLL_SENSITIVE, + ResultSet.CONCUR_UPDATABLE); + */ + } + + + class Connection{ + + // Result sets created using the returned PreparedStatement object will by default be type TYPE_FORWARD_ONLY + // and have a concurrency level of CONCUR_READ_ONLY. + @Unique // @StateRefinement (return, to="TYPE_FORWARD_ONLY, CONCUR_READ_ONLY") + public PreparedStatement prepareStatement(String s) { + return new PreparedStatement(); + } + + @Unique // @StateRefinement (return, to="type == resultSetType") + public PreparedStatement prepareStatement​(String sql, int resultSetType, int resultSetConcurrency){ + return new PreparedStatement(); + + } + } + + // @Ghost("type") + class PreparedStatement{ + + void setString(int index, String s){} + + // @StateRefinement(return, to="type != TYPE_FORWARD_ONLY, col == -1") + ResultSet executeQuery(String s){return null;} + + // @StateRefinement(return, to="type, col == -1") + ResultSet executeQuery(){return null;} + } + + // @Ghost("type") + class ResultSet{ + + // @StateRefinement(this, type == ) + void beforeFirst(){} + + // @StateRefinement(this, col > 0) + float getFloat(String s){return 0;} + + // @StateRefinement(this, col > 0) + int getInt(int s){return 0;} + + // @StateRefinement(this, col == old(col) + 1) + boolean next(){return true;} + } + + +} + + diff --git a/latte-umbrella/src/test/examples/searching_state_space/ResultSetNoNext.java b/latte-umbrella/src/test/examples/searching_state_space/ResultSetNoNext.java new file mode 100644 index 0000000..cfc135b --- /dev/null +++ b/latte-umbrella/src/test/examples/searching_state_space/ResultSetNoNext.java @@ -0,0 +1,64 @@ + +import java.util.TimerTask; + +import specification.Borrowed; +import specification.Free; +import specification.Unique; + +public class SSSResultSetNoNext { + + + /* + * Error - in ResultSet, after executing the query we need to call next() before getting a value + */ + public static void example6367737(@Borrowed Connection con, String username, String password ) throws Exception { + + // Step 1 Prepare the statement + PreparedStatement pstat = + con.prepareStatement("select typeid from users where username=? and password=?"); + + // Step 2 Set parameters for the statement + pstat.setString(1, username); + pstat.setString(2, password); + + // Step 3 Execute the query + ResultSet parentMessage = pstat.executeQuery("SELECT SUM(IMPORTANCE) AS IMPAVG FROM MAIL"); + + float avgsum = parentMessage.getFloat("IMPAVG"); // Error because we are trying to get a value before next + // To be correct we need to call next() before the getter + } + + + class Connection{ + + // Result sets created using the returned PreparedStatement object will by default be type TYPE_FORWARD_ONLY + // and have a concurrency level of CONCUR_READ_ONLY. + @Unique // @StateRefinement (return, to="TYPE_FORWARD_ONLY, CONCUR_READ_ONLY") + public PreparedStatement prepareStatement(String s) { + return new PreparedStatement(); + } + + // To change resultSetType + // prepareStatement​(String sql, int resultSetType, int resultSetConcurrency){} + } + + class PreparedStatement{ + void setString(int index, String s){} + + // @ReturnState( to="TYPE_FORWARD_ONLY, beforeRow") + ResultSet executeQuery(String s){return null;} + } + + //@StateSet({"beforeRow", "onRow"}) + class ResultSet{ + // @StateRefinement( from = "onRow") + float getFloat(String s){return 0;} + + // @StateRefinement( to="onRow") + void next(){} + } + + +} + + diff --git a/latte-umbrella/src/test/examples/searching_state_space/TimerTaskCannotReschedule.java b/latte-umbrella/src/test/examples/searching_state_space/TimerTaskCannotReschedule.java new file mode 100644 index 0000000..4aa2d6e --- /dev/null +++ b/latte-umbrella/src/test/examples/searching_state_space/TimerTaskCannotReschedule.java @@ -0,0 +1,59 @@ +import java.util.TimerTask; + +import specification.Borrowed; +import specification.Free; + +public class SSSTimerTaskCannotReschedule { + + /* + * Error cannot reschedule a timer + */ + public static void example1801324_simplified( @Borrowed Timer timer, String sessionKey, @Free TimerTask tt) { + + // Step 2) Cancel the timer + timer.cancel(); + + // Step 3 Schedule a new task for this timer -> ERROR Cannot reschedule a Timer + timer.schedule(tt , 1000); + } + +} + +/* + * [If the timer is cancelled] any further attempt to schedule a task on the timer will result in an IllegalStateException + * + * START --- schedule() ----> [SCHEDULED]--------> + * ----------------------------------------> cancel() -----> [CANCELLED] (no further scheduling allowed) + */ +class Timer{ + //@StateRefinement(this, to="cancelled") + public void cancel() { } + + // @StateRefinement(this, from="start", to="scheduled") + public void schedule(TimerTask task, /* delay > 0 */int delay) {} + +} + + +// /* +// * Error cannot reschedule a timer +// */ +// public static void example1801324( Map timers, String sessionKey) { + +// // Step 1) Get the timer +// Timer timer = timers.get(sessionKey); + +// // Step 2) Cancel the timer +// 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); +// } + + + diff --git a/latte-umbrella/src/test/examples/searching_state_space/URLConnectionReuseConnection.java b/latte-umbrella/src/test/examples/searching_state_space/URLConnectionReuseConnection.java new file mode 100644 index 0000000..f43398a --- /dev/null +++ b/latte-umbrella/src/test/examples/searching_state_space/URLConnectionReuseConnection.java @@ -0,0 +1,57 @@ +import specification.Borrowed; +import specification.Unique; + +public class SSSURLConnectionReuseConnection { + + public static void example4278917(@Borrowed URL address) { + + try { + // Step 1) Open the connection + URLConnection connection = address.openConnection(); // returns a unique object + + // Step 2) Connect + connection.connect(); + + /* Other code in original question */ + + // Step 3) Setup parameters and connection properties after connection == ERROR + connection.setAllowUserInteraction(true); + connection.addRequestProperty("AUTHENTICATION_REQUEST_PROPERTY", "authorizationRequest"); + connection.getHeaderFields(); + + } catch (IOException e) { + // Handle exceptions related to network or stream issues + System.err.println("Error: " + e.getMessage()); + } + } +} + +class URL{ + @Unique // @StateRefinement (return, to="manipulate") + public URLConnection openConnection() { + return new URLConnection(); + } +} + + +/** + * --- openConnection() ----> [MANIPULATE PARAMS] ------> connect() -----> [INTERACT] + * setAllowUserInteraction() getContent() + * addRequestProperty()... getHeaderFields()... + */ +// @StateSet({"manipulate", "interact"}) +class URLConnection{ + + //@StateRefinement(this, from="manipulate") + void setAllowUserInteraction(boolean b){} + + //@StateRefinement(this, from="manipulate") + void addRequestProperty(String s1, String s2){} + + //@StateRefinement(this, from="interact") + void getHeaderFields(){} + + //@StateRefinement(this, from="manipulate", to="interact") + void connect() throws IOException {} +} + diff --git a/latte-umbrella/src/test/examples/searching_state_space/URLConnectionSetProperty1.java b/latte-umbrella/src/test/examples/searching_state_space/URLConnectionSetProperty1.java new file mode 100644 index 0000000..adf909f --- /dev/null +++ b/latte-umbrella/src/test/examples/searching_state_space/URLConnectionSetProperty1.java @@ -0,0 +1,78 @@ +import specification.Borrowed; +import specification.Unique; +import java.io.IOException; +import java.io.InputStream; + +public class SSSURLConnectionSetProperty1 { + + public static void example331538(@Borrowed URL address) { + try { + + // Step 1) Open the connection + URLConnection cnx = address.openConnection(); + + // 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)"); + + + // Step 3) + cnx.connect(); + + // Step 4) + cnx.getContent(); + + // Get the input stream and process it + InputStream is = cnx.getInputStream(); + System.out.println("Successfully opened input stream."); + + // Ensure to close the InputStream after use + is.close(); + + } catch (IOException e) { + // Handle exceptions related to network or stream issues + System.err.println("Error: " + e.getMessage()); + } + } +} + + + + +class URL{ + @Unique // @StateRefinement (return, to="manipulate") + public URLConnection openConnection() { + return new URLConnection(); + } +} + +/** + * --- openConnection() ----> [MANIPULATE PARAMS] ------> connect() -----> [INTERACT] + * setAllowUserInteraction() getContent() + * addRequestProperty()... getHeaderFields()... + */ +// @StateSet({"manipulate", "interact"}) +class URLConnection{ + + //@StateRefinement(this, from="manipulate") + void setAllowUserInteraction(boolean b){} + + //@StateRefinement(this, from="manipulate") + void setDoOutput(boolean b){} + + //@StateRefinement(this, from="manipulate") + void addRequestProperty(String s1, String s2){} + + //@StateRefinement(this, from="manipulate", to="interact") + void connect() throws IOException {} + + //@StateRefinement(this, from="interact") + void getContent(){} + + + //@StateRefinement(this, from="interact") + @Unique //????? Not sure: Returns an input stream that reads from this open connection. + InputStream getInputStream(){ return null;} + +} \ No newline at end of file diff --git a/latte-umbrella/src/test/examples/searching_state_space/URLConnectionSetPropertyMultipleComplete.java b/latte-umbrella/src/test/examples/searching_state_space/URLConnectionSetPropertyMultipleComplete.java new file mode 100644 index 0000000..ba94f96 --- /dev/null +++ b/latte-umbrella/src/test/examples/searching_state_space/URLConnectionSetPropertyMultipleComplete.java @@ -0,0 +1,114 @@ +import java.io.IOException; +import java.io.InputStream; +import java.io.OutputStream; + +import specification.Borrowed; +import specification.Shared; +import specification.Unique; + +public class SSSURLConnectionSetPropertyMultipleComplete { + + String sessionId = "1234"; + public void example5368535(@Borrowed URL address, String content) { + try { + URLConnection con = openConnection(address, true, true, "POST"); + + //ERROR write before set + writeToOutput(con, content); // writeOutput calls cnx.getOutputStream() + setCookies(con); // writeOutput calls cnx.setRequestProperty + + con.connect(); + + System.out.println("Request completed successfully."); + } catch (IOException e) { + // Handle exceptions related to network or stream issues + System.err.println("Error: " + e.getMessage()); + } + } + + // Exactly from the original code + @Unique + public URLConnection openConnection(@Borrowed URL url, boolean in, boolean out, String requestMethode) throws IOException{ + URLConnection con = url.openConnection(); + con.setDoInput(in); + con.setDoOutput (out); + con.setRequestMethod(requestMethode); + con.setRequestProperty ("Content-Type", "application/x-www-form-urlencoded"); + return con; + } + + // Set cookies + private void setCookies(@Borrowed URLConnection cnx) { + if (sessionId != null) { + cnx.setRequestProperty("Cookie", sessionId); + System.out.println("Cookie set: " + sessionId); + } + } + + // Write content + private void writeToOutput(@Borrowed URLConnection cnx, String content) throws IOException { + try { + OutputStream os = cnx.getOutputStream() ; + os.write(content.getBytes()); + os.flush(); + os.close(); + } catch (IOException e) { + System.err.println("Error writing content: " + e.getMessage()); + throw e; + } + } + +} + + +class URL{ + @Unique // @StateRefinement (return, to="manipulate") + public URLConnection openConnection() { + return new URLConnection(); + } +} + + +/** + * --- openConnection() ----> [MANIPULATE PARAMS] ------> connect() -----> [INTERACT] + * setAllowUserInteraction() getContent() + * addRequestProperty()... getHeaderFields()... + */ +// @StateSet({"manipulate", "interact"}) +class URLConnection{ + + //@StateRefinement(this, from="manipulate") + void setAllowUserInteraction(boolean b){} + + //@StateRefinement(this, from="manipulate") + void setDoOutput(boolean b){} + + //@StateRefinement(this, from="manipulate") + void setRequestProperty(String a, String b){} + + //@StateRefinement(this, from="manipulate") + void setRequestMethod(String a){} + + //@StateRefinement(this, from="manipulate") + void setDoInput(boolean b){} + + //@StateRefinement(this, from="manipulate") + void addRequestProperty(String s1, String s2){} + + //@StateRefinement(this, from="manipulate", to="interact") + void connect() throws IOException {} + + //@StateRefinement(this, from="interact") + void getContent(){} + + + //@StateRefinement(this, from="interact") + @Unique //????? Not sure: Returns an input stream that reads from this open connection. + InputStream getInputStream(){ return null;} + + + //@StateRefinement(this, from="interact") + @Shared //????? Not sure: Returns an output stream that writes to this connection. + OutputStream getOutputStream(){ return null;} + +} \ No newline at end of file diff --git a/latte-umbrella/src/test/examples/searching_state_space/URLConnectionSetPropertyMultipleShort.java b/latte-umbrella/src/test/examples/searching_state_space/URLConnectionSetPropertyMultipleShort.java new file mode 100644 index 0000000..f465657 --- /dev/null +++ b/latte-umbrella/src/test/examples/searching_state_space/URLConnectionSetPropertyMultipleShort.java @@ -0,0 +1,103 @@ +import java.io.IOException; +import java.io.InputStream; +import java.io.OutputStream; + +import specification.Borrowed; +import specification.Shared; +import specification.Unique; + +public class SSSURLConnectionSetPropertyMultipleShort { + + String sessionId = "1234"; + public void example5368535(@Borrowed URL address, String content) { + try { + URLConnection con = openConnection(address, true, true, "POST"); + + //ERROR write before set + writeToOutput(con, content); // writeOutput calls cnx.getOutputStream() + setCookies(con); // writeOutput calls cnx.setRequestProperty + + con.connect(); + + System.out.println("Request completed successfully."); + } catch (IOException e) { + // Handle exceptions related to network or stream issues + System.err.println("Error: " + e.getMessage()); + } + } + + // Setters + @Unique // @StateRefinement(return, to="manipulate") + public URLConnection openConnection(@Borrowed URL url, boolean in, boolean out, + String requestMethode) throws IOException { + URLConnection con = url.openConnection(); + con.setDoInput(in); + con.setDoOutput (out); + return con; + } + + // Set cookies + // @StateRefinement(cnx, from="manipulate") + private void setCookies(@Borrowed URLConnection cnx) { + cnx.setRequestProperty("Cookie", sessionId); + } + + // Write content + // @StateRefinement(cnx, from="interact") + private void writeToOutput(@Borrowed URLConnection cnx, String content) throws IOException { + cnx.getOutputStream(); + } +} + + +class URL{ + @Unique // @StateRefinement (return, to="manipulate") + public URLConnection openConnection() { + return new URLConnection(); + } +} + + +/** + * --- openConnection() ----> [MANIPULATE PARAMS] ------> connect() -----> [INTERACT] + * setAllowUserInteraction() getContent() + * addRequestProperty()... getHeaderFields()... + */ +// @StateSet({"manipulate", "interact"}) +class URLConnection{ + + //@StateRefinement(this, from="manipulate") + void setAllowUserInteraction(boolean b){} + + //@StateRefinement(this, from="manipulate") + void setDoOutput(boolean b){} + + //@StateRefinement(this, from="manipulate") + void setRequestProperty(String a, String b){} + + //@StateRefinement(this, from="manipulate") + void setRequestMethod(String a){} + + //@StateRefinement(this, from="manipulate") + void setDoInput(boolean b){} + + //@StateRefinement(this, from="manipulate") + void addRequestProperty(String s1, String s2){} + + //@StateRefinement(this, from="manipulate", to="interact") + void connect() throws IOException {} + + //@StateRefinement(this, from="interact") + void getContent(){} + + + //@StateRefinement(this, from="interact") + @Unique //????? Not sure: Returns an input stream that reads from this open connection. + InputStream getInputStream(){ return null;} + + + //@StateRefinement(this, from="interact") + @Shared //????? Not sure: Returns an output stream that writes to this connection. + OutputStream getOutputStream(){ return null;} + +} 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() {} + +} From d9a15b3d93468711767e210e55552de79417e0bb Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Wed, 12 Feb 2025 13:49:49 +0000 Subject: [PATCH 2/4] add examples urlconnection property with several methods --- latte-umbrella/src/test/java/latte/latte_umbrella/AppTest.java | 3 +++ 1 file changed, 3 insertions(+) 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..7cdae47 100644 --- a/latte-umbrella/src/test/java/latte/latte_umbrella/AppTest.java +++ b/latte-umbrella/src/test/java/latte/latte_umbrella/AppTest.java @@ -118,6 +118,7 @@ public void testURLConnectionSetPropertyMultipleShort(){ assert(false); } } +<<<<<<< HEAD @Test public void testTimerTaskCannotReschedule(){ @@ -148,6 +149,8 @@ public void testResultSetForwardOnly(){ assert(false); } } +======= +>>>>>>> 4ba1475 (add examples urlconnection property with several methods) /* * Incorrect Examples From 89594941cf9547b58577aaee1bbbe1058c2cc13b Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Wed, 12 Feb 2025 14:19:20 +0000 Subject: [PATCH 3/4] add example for timertask --- .../src/test/java/latte/latte_umbrella/AppTest.java | 5 +---- 1 file changed, 1 insertion(+), 4 deletions(-) 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 7cdae47..946d30a 100644 --- a/latte-umbrella/src/test/java/latte/latte_umbrella/AppTest.java +++ b/latte-umbrella/src/test/java/latte/latte_umbrella/AppTest.java @@ -118,7 +118,6 @@ public void testURLConnectionSetPropertyMultipleShort(){ assert(false); } } -<<<<<<< HEAD @Test public void testTimerTaskCannotReschedule(){ @@ -149,9 +148,7 @@ public void testResultSetForwardOnly(){ assert(false); } } -======= ->>>>>>> 4ba1475 (add examples urlconnection property with several methods) - + /* * Incorrect Examples */ From 78225c3f6f8074a02a1fc09f22428599d7a33f16 Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Tue, 15 Apr 2025 17:34:54 +0100 Subject: [PATCH 4/4] add examples --- .../src/main/java/examples/MyStackTest.java | 213 ++++-------------- .../test/examples/ResultSetForwardOnly.java | 94 -------- .../src/test/examples/ResultSetNoNext.java | 64 ------ .../examples/TimerTaskCannotReschedule.java | 59 ----- .../URLConnectionReuseConnection.java | 57 ----- .../examples/URLConnectionSetProperty1.java | 79 ------- ...ConnectionSetPropertyMultipleComplete.java | 114 ---------- ...URLConnectionSetPropertyMultipleShort.java | 103 --------- .../java/latte/latte_umbrella/AppTest.java | 22 +- 9 files changed, 59 insertions(+), 746 deletions(-) delete mode 100644 latte-umbrella/src/test/examples/ResultSetForwardOnly.java delete mode 100644 latte-umbrella/src/test/examples/ResultSetNoNext.java delete mode 100644 latte-umbrella/src/test/examples/TimerTaskCannotReschedule.java delete mode 100644 latte-umbrella/src/test/examples/URLConnectionReuseConnection.java delete mode 100644 latte-umbrella/src/test/examples/URLConnectionSetProperty1.java delete mode 100644 latte-umbrella/src/test/examples/URLConnectionSetPropertyMultipleComplete.java delete mode 100644 latte-umbrella/src/test/examples/URLConnectionSetPropertyMultipleShort.java 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/ResultSetForwardOnly.java deleted file mode 100644 index 5a9c115..0000000 --- a/latte-umbrella/src/test/examples/ResultSetForwardOnly.java +++ /dev/null @@ -1,94 +0,0 @@ -package examples; - - -import java.util.TimerTask; - -import specification.Borrowed; -import specification.Free; -import specification.Unique; - -public class ResultSetForwardOnly { - /* - * Error ResultSet is FORWARD_ONLY and we try to get a value before - */ - public static void example6367737(Connection con, String username, String password ) throws Exception { - - // Step 1) Prepare the statement - PreparedStatement pstat = - con.prepareStatement("select typeid from users where username=? and password=?"); - - // Step 2) Set parameters for the statement - pstat.setString(1, username); - pstat.setString(2, password); - - // Step 3) Execute the query - ResultSet rs = pstat.executeQuery(); - - // Step 4) Process the result - int rowCount=0; - while(rs.next()){ - rowCount++; - } - - // ERROR! because it is FORWARD_ONLY, we cannot go back and check beforeFirst - rs.beforeFirst(); - - int typeID = 0; // ... - - // To be correct we need to change the resultset to be scrollable - /*PreparedStatement pstat = - con.prepareStatement("select typeid from users where username=? and password=?", - ResultSet.TYPE_SCROLL_SENSITIVE, - ResultSet.CONCUR_UPDATABLE); - */ - } - - - class Connection{ - - // Result sets created using the returned PreparedStatement object will by default be type TYPE_FORWARD_ONLY - // and have a concurrency level of CONCUR_READ_ONLY. - @Unique // @StateRefinement (return, to="TYPE_FORWARD_ONLY, CONCUR_READ_ONLY") - public PreparedStatement prepareStatement(String s) { - return new PreparedStatement(); - } - - @Unique // @StateRefinement (return, to="type == resultSetType") - public PreparedStatement prepareStatement​(String sql, int resultSetType, int resultSetConcurrency){ - return new PreparedStatement(); - - } - } - - // @Ghost("type") - class PreparedStatement{ - - void setString(int index, String s){} - - // @StateRefinement(return, to="type != TYPE_FORWARD_ONLY, col == -1") - ResultSet executeQuery(String s){return null;} - - // @StateRefinement(return, to="type, col == -1") - ResultSet executeQuery(){return null;} - } - - // @Ghost("type") - class ResultSet{ - - // @StateRefinement(this, type == ) - void beforeFirst(){} - - // @StateRefinement(this, col > 0) - float getFloat(String s){return 0;} - - // @StateRefinement(this, col > 0) - int getInt(int s){return 0;} - - // @StateRefinement(this, col == old(col) + 1) - boolean next(){return true;} - } - - -} - - diff --git a/latte-umbrella/src/test/examples/ResultSetNoNext.java b/latte-umbrella/src/test/examples/ResultSetNoNext.java deleted file mode 100644 index daf205b..0000000 --- a/latte-umbrella/src/test/examples/ResultSetNoNext.java +++ /dev/null @@ -1,64 +0,0 @@ - -import java.util.TimerTask; - -import specification.Borrowed; -import specification.Free; -import specification.Unique; - -public class ResultSetNoNext { - - - /* - * Error - in ResultSet, after executing the query we need to call next() before getting a value - */ - public static void example6367737(@Borrowed Connection con, String username, String password ) throws Exception { - - // Step 1 Prepare the statement - PreparedStatement pstat = - con.prepareStatement("select typeid from users where username=? and password=?"); - - // Step 2 Set parameters for the statement - pstat.setString(1, username); - pstat.setString(2, password); - - // Step 3 Execute the query - ResultSet parentMessage = pstat.executeQuery("SELECT SUM(IMPORTANCE) AS IMPAVG FROM MAIL"); - - float avgsum = parentMessage.getFloat("IMPAVG"); // Error because we are trying to get a value before next - // To be correct we need to call next() before the getter - } - - - class Connection{ - - // Result sets created using the returned PreparedStatement object will by default be type TYPE_FORWARD_ONLY - // and have a concurrency level of CONCUR_READ_ONLY. - @Unique // @StateRefinement (return, to="TYPE_FORWARD_ONLY, CONCUR_READ_ONLY") - public PreparedStatement prepareStatement(String s) { - return new PreparedStatement(); - } - - // To change resultSetType - // prepareStatement​(String sql, int resultSetType, int resultSetConcurrency){} - } - - - class PreparedStatement{ - void setString(int index, String s){} - - // @StateRefinement(return, to="TYPE_FORWARD_ONLY, col == -1") - ResultSet executeQuery(String s){return null;} - } - - class ResultSet{ - // @StateRefinement(this, col > 0) - float getFloat(String s){return 0;} - - // @StateRefinement(this, col == old(col) + 1) - void next(){} - } - - -} - - diff --git a/latte-umbrella/src/test/examples/TimerTaskCannotReschedule.java b/latte-umbrella/src/test/examples/TimerTaskCannotReschedule.java deleted file mode 100644 index cdb64d8..0000000 --- a/latte-umbrella/src/test/examples/TimerTaskCannotReschedule.java +++ /dev/null @@ -1,59 +0,0 @@ -import java.util.TimerTask; - -import specification.Borrowed; -import specification.Free; - -public class TimerTaskCannotReschedule { - - /* - * Error cannot reschedule a timer - */ - public static void example1801324_simplified( @Borrowed Timer timer, String sessionKey, @Free TimerTask tt) { - - // Step 2) Cancel the timer - timer.cancel(); - - // Step 3 Schedule a new task for this timer -> ERROR Cannot reschedule a Timer - timer.schedule(tt , 1000); - } - -} - -/* - * [If the timer is cancelled] any further attempt to schedule a task on the timer will result in an IllegalStateException - * - * START --- schedule() ----> [SCHEDULED]--------> - * ----------------------------------------> cancel() -----> [CANCELLED] (no further scheduling allowed) - */ -class Timer{ - //@StateRefinement(this, to="cancelled") - public void cancel() { } - - // @StateRefinement(this, from="start", to="scheduled") - public void schedule(TimerTask task, /* delay > 0 */int delay) {} - -} - - -// /* -// * Error cannot reschedule a timer -// */ -// public static void example1801324( Map timers, String sessionKey) { - -// // Step 1) Get the timer -// Timer timer = timers.get(sessionKey); - -// // Step 2) Cancel the timer -// 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); -// } - - - diff --git a/latte-umbrella/src/test/examples/URLConnectionReuseConnection.java b/latte-umbrella/src/test/examples/URLConnectionReuseConnection.java deleted file mode 100644 index 32b3e87..0000000 --- a/latte-umbrella/src/test/examples/URLConnectionReuseConnection.java +++ /dev/null @@ -1,57 +0,0 @@ -import specification.Borrowed; -import specification.Unique; - -public class URLConnectionReuseConnection { - - public static void example4278917(@Borrowed URL address) { - - try { - // Step 1) Open the connection - URLConnection connection = address.openConnection(); // returns a unique object - - // Step 2) Connect - connection.connect(); - - /* Other code in original question */ - - // Step 3) Setup parameters and connection properties after connection == ERROR - connection.setAllowUserInteraction(true); - connection.addRequestProperty("AUTHENTICATION_REQUEST_PROPERTY", "authorizationRequest"); - connection.getHeaderFields(); - - } catch (IOException e) { - // Handle exceptions related to network or stream issues - System.err.println("Error: " + e.getMessage()); - } - } -} - -class URL{ - @Unique // @StateRefinement (return, to="manipulate") - public URLConnection openConnection() { - return new URLConnection(); - } -} - - -/** - * --- openConnection() ----> [MANIPULATE PARAMS] ------> connect() -----> [INTERACT] - * setAllowUserInteraction() getContent() - * addRequestProperty()... getHeaderFields()... - */ -// @StateSet({"manipulate", "interact"}) -class URLConnection{ - - //@StateRefinement(this, from="manipulate") - void setAllowUserInteraction(boolean b){} - - //@StateRefinement(this, from="manipulate") - void addRequestProperty(String s1, String s2){} - - //@StateRefinement(this, from="interact") - void getHeaderFields(){} - - //@StateRefinement(this, from="manipulate", to="interact") - void connect() throws IOException {} -} - diff --git a/latte-umbrella/src/test/examples/URLConnectionSetProperty1.java b/latte-umbrella/src/test/examples/URLConnectionSetProperty1.java deleted file mode 100644 index e3467d6..0000000 --- a/latte-umbrella/src/test/examples/URLConnectionSetProperty1.java +++ /dev/null @@ -1,79 +0,0 @@ -import specification.Borrowed; -import specification.Unique; -import java.io.IOException; -import java.io.InputStream; - -public class URLConnectionSetProperty1 { - - public static void example331538(@Borrowed URL address) { - try { - - // Step 1) Open the connection - URLConnection cnx = address.openConnection(); - - // 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)"); - - - // Step 3) - cnx.connect(); - - // Step 4) - cnx.getContent(); - - // Get the input stream and process it - InputStream is = cnx.getInputStream(); - System.out.println("Successfully opened input stream."); - - // Ensure to close the InputStream after use - is.close(); - - } catch (IOException e) { - // Handle exceptions related to network or stream issues - System.err.println("Error: " + e.getMessage()); - } - } -} - - - - -class URL{ - @Unique // @StateRefinement (return, to="manipulate") - public URLConnection openConnection() { - return new URLConnection(); - } -} - -/** - * --- openConnection() ----> [MANIPULATE PARAMS] ------> connect() -----> [INTERACT] - * setAllowUserInteraction() getContent() - * addRequestProperty()... getHeaderFields()... - */ -// @StateSet({"manipulate", "interact"}) -class URLConnection{ - - //@StateRefinement(this, from="manipulate") - void setAllowUserInteraction(boolean b){} - - //@StateRefinement(this, from="manipulate") - void setDoOutput(boolean b){} - - //@StateRefinement(this, from="manipulate") - void addRequestProperty(String s1, String s2){} - - //@StateRefinement(this, from="manipulate", to="interact") - void connect() throws IOException {} - - //@StateRefinement(this, from="interact") - void getContent(){} - - - //@StateRefinement(this, from="interact") - @Unique //????? Not sure: Returns an input stream that reads from this open connection. - InputStream getInputStream(){ return null;} - -} \ No newline at end of file diff --git a/latte-umbrella/src/test/examples/URLConnectionSetPropertyMultipleComplete.java b/latte-umbrella/src/test/examples/URLConnectionSetPropertyMultipleComplete.java deleted file mode 100644 index a50dd0a..0000000 --- a/latte-umbrella/src/test/examples/URLConnectionSetPropertyMultipleComplete.java +++ /dev/null @@ -1,114 +0,0 @@ -import java.io.IOException; -import java.io.InputStream; -import java.io.OutputStream; - -import specification.Borrowed; -import specification.Shared; -import specification.Unique; - -public class URLConnectionSetPropertyMultipleComplete { - - String sessionId = "1234"; - public void example5368535(@Borrowed URL address, String content) { - try { - URLConnection con = openConnection(address, true, true, "POST"); - - //ERROR write before set - writeToOutput(con, content); // writeOutput calls cnx.getOutputStream() - setCookies(con); // writeOutput calls cnx.setRequestProperty - - con.connect(); - - System.out.println("Request completed successfully."); - } catch (IOException e) { - // Handle exceptions related to network or stream issues - System.err.println("Error: " + e.getMessage()); - } - } - - // Exactly from the original code - @Unique - public URLConnection openConnection(@Borrowed URL url, boolean in, boolean out, String requestMethode) throws IOException{ - URLConnection con = url.openConnection(); - con.setDoInput(in); - con.setDoOutput (out); - con.setRequestMethod(requestMethode); - con.setRequestProperty ("Content-Type", "application/x-www-form-urlencoded"); - return con; - } - - // Set cookies - private void setCookies(@Borrowed URLConnection cnx) { - if (sessionId != null) { - cnx.setRequestProperty("Cookie", sessionId); - System.out.println("Cookie set: " + sessionId); - } - } - - // Write content - private void writeToOutput(@Borrowed URLConnection cnx, String content) throws IOException { - try { - OutputStream os = cnx.getOutputStream() ; - os.write(content.getBytes()); - os.flush(); - os.close(); - } catch (IOException e) { - System.err.println("Error writing content: " + e.getMessage()); - throw e; - } - } - -} - - -class URL{ - @Unique // @StateRefinement (return, to="manipulate") - public URLConnection openConnection() { - return new URLConnection(); - } -} - - -/** - * --- openConnection() ----> [MANIPULATE PARAMS] ------> connect() -----> [INTERACT] - * setAllowUserInteraction() getContent() - * addRequestProperty()... getHeaderFields()... - */ -// @StateSet({"manipulate", "interact"}) -class URLConnection{ - - //@StateRefinement(this, from="manipulate") - void setAllowUserInteraction(boolean b){} - - //@StateRefinement(this, from="manipulate") - void setDoOutput(boolean b){} - - //@StateRefinement(this, from="manipulate") - void setRequestProperty(String a, String b){} - - //@StateRefinement(this, from="manipulate") - void setRequestMethod(String a){} - - //@StateRefinement(this, from="manipulate") - void setDoInput(boolean b){} - - //@StateRefinement(this, from="manipulate") - void addRequestProperty(String s1, String s2){} - - //@StateRefinement(this, from="manipulate", to="interact") - void connect() throws IOException {} - - //@StateRefinement(this, from="interact") - void getContent(){} - - - //@StateRefinement(this, from="interact") - @Unique //????? Not sure: Returns an input stream that reads from this open connection. - InputStream getInputStream(){ return null;} - - - //@StateRefinement(this, from="interact") - @Shared //????? Not sure: Returns an output stream that writes to this connection. - OutputStream getOutputStream(){ return null;} - -} \ No newline at end of file diff --git a/latte-umbrella/src/test/examples/URLConnectionSetPropertyMultipleShort.java b/latte-umbrella/src/test/examples/URLConnectionSetPropertyMultipleShort.java deleted file mode 100644 index 3a2792d..0000000 --- a/latte-umbrella/src/test/examples/URLConnectionSetPropertyMultipleShort.java +++ /dev/null @@ -1,103 +0,0 @@ -import java.io.IOException; -import java.io.InputStream; -import java.io.OutputStream; - -import specification.Borrowed; -import specification.Shared; -import specification.Unique; - -public class URLConnectionSetPropertyMultipleShort { - - String sessionId = "1234"; - public void example5368535(@Borrowed URL address, String content) { - try { - URLConnection con = openConnection(address, true, true, "POST"); - - //ERROR write before set - writeToOutput(con, content); // writeOutput calls cnx.getOutputStream() - setCookies(con); // writeOutput calls cnx.setRequestProperty - - con.connect(); - - System.out.println("Request completed successfully."); - } catch (IOException e) { - // Handle exceptions related to network or stream issues - System.err.println("Error: " + e.getMessage()); - } - } - - // Setters - @Unique // @StateRefinement(return, to="manipulate") - public URLConnection openConnection(@Borrowed URL url, boolean in, boolean out, - String requestMethode) throws IOException { - URLConnection con = url.openConnection(); - con.setDoInput(in); - con.setDoOutput (out); - return con; - } - - // Set cookies - // @StateRefinement(cnx, from="manipulate") - private void setCookies(@Borrowed URLConnection cnx) { - cnx.setRequestProperty("Cookie", sessionId); - } - - // Write content - // @StateRefinement(cnx, from="interact") - private void writeToOutput(@Borrowed URLConnection cnx, String content) throws IOException { - cnx.getOutputStream(); - } -} - - -class URL{ - @Unique // @StateRefinement (return, to="manipulate") - public URLConnection openConnection() { - return new URLConnection(); - } -} - - -/** - * --- openConnection() ----> [MANIPULATE PARAMS] ------> connect() -----> [INTERACT] - * setAllowUserInteraction() getContent() - * addRequestProperty()... getHeaderFields()... - */ -// @StateSet({"manipulate", "interact"}) -class URLConnection{ - - //@StateRefinement(this, from="manipulate") - void setAllowUserInteraction(boolean b){} - - //@StateRefinement(this, from="manipulate") - void setDoOutput(boolean b){} - - //@StateRefinement(this, from="manipulate") - void setRequestProperty(String a, String b){} - - //@StateRefinement(this, from="manipulate") - void setRequestMethod(String a){} - - //@StateRefinement(this, from="manipulate") - void setDoInput(boolean b){} - - //@StateRefinement(this, from="manipulate") - void addRequestProperty(String s1, String s2){} - - //@StateRefinement(this, from="manipulate", to="interact") - void connect() throws IOException {} - - //@StateRefinement(this, from="interact") - void getContent(){} - - - //@StateRefinement(this, from="interact") - @Unique //????? Not sure: Returns an input stream that reads from this open connection. - InputStream getInputStream(){ return null;} - - - //@StateRefinement(this, from="interact") - @Shared //????? Not sure: Returns an output stream that writes to this connection. - OutputStream getOutputStream(){ return null;} - -} 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 946d30a..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,7 +142,17 @@ 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);