Commit 559566da authored by ISWB Prasetya's avatar ISWB Prasetya
Browse files

fixing some bug with tracking of _spec() method; it causes both m and m_spec()...

fixing some bug with tracking of _spec() method; it causes both m and m_spec() to be included in the scope.
parent 4f61ded4
......@@ -22,5 +22,7 @@ public class CONSTANTS {
public static final String T3loggerName = "T3" ;
public static final String auxField_prefix = "AUX__" ;
public static final String classinv_name = "classinv__" ;
public static final String specmethod_suffix = "_spec" ;
}
package Sequenic.T3.Examples;
public class CobaClassWithSpecs {
private boolean classinv__() {
System.out.println(">>>> classinv()") ;
return x==0 ;
}
public CobaClassWithSpecs() {}
int x = 0 ;
public int m(){
System.out.println(">>>> m()") ;
x++ ;
return 999 ;
}
private boolean pre() {
System.out.println(">>>> checking pre-cond") ; return true ;
}
private boolean post() {
System.out.println(">>>> checking post-cond") ; return true ;
}
public int m_spec() {
System.out.println(">>>> invoking m_spec()") ;
assert pre() : "PRE" ;
int v = m() ;
assert post() ;
System.out.println(">>>> leaving m_spec()") ;
return v ;
}
}
......@@ -26,7 +26,7 @@ public class SimpleSortedList implements Serializable {
* This class invariant only specifies that the max-pointer points
* to some element in the list, if it is not empty.
*/
private boolean classinv() {
private boolean classinv__() {
return s.isEmpty() || s.contains(max);
}
......
......@@ -130,6 +130,11 @@ public class TestingScope {
}
else methods.add(M) ;
}
//System.out.println("### Included in the scope:") ;
//for (Method M : methods) {
// System.out.println("### " + M.getName()) ;
//}
// get the fields in scope (static fields are already excluded)
for (Field F : getAccessibleFields()) {
fields.add(F) ;
......@@ -387,7 +392,28 @@ public class TestingScope {
continue;
if (isVisible(M.getDeclaringClass(),M.getModifiers())) methods.add(M) ;
}
return methods ;
// if m_spec() is present, remove m()
List<Method> specs = new LinkedList<Method>();
for (Method M : methods) {
if (M.getName().endsWith(CONSTANTS.specmethod_suffix)) {
//System.out.println("### adding spec " + M.getName()) ;
specs.add(M) ;
}
}
List<Method> methods_ = new LinkedList<Method>();
for (Method M : methods) {
String name = M.getName() ;
boolean hasSpec = false ;
for (Method S : specs) {
String specname = S.getName() ;
String name2 = specname.substring(0,specname.length() - CONSTANTS.specmethod_suffix.length()) ;
// System.out.println("### comparing " + name + " vs " + name2) ;
if (name.equals(name2)) { hasSpec = true ; break ; }
}
if (!hasSpec) methods_.add(M) ;
}
return methods_ ;
}
private boolean isVisible(Class declaringClass, int modifier) {
......
import Sequenic.T3.T3Cmd;
public class Test_T3_incode_spec_checking {
static public void main(String[] args) throws Exception {
T3Cmd.main("-ms 1 -pl 1 -sl 0 -sex -d . -sd ./bin Sequenic.T3.Examples.CobaClassWithSpecs");
}
}
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment