spec not grounding

[ftc]

For the specification:

SPEC FALSE[*] |- [CB] [t] void android.os.CountDownTimer.onFinish();
SPEC TRUE[*]; [CI] [t] android.os.CountDownTimer android.os.CountDownTimer.start() |+ [CB] [t] void android.os.CountDownTimer.onFinish()

And the trace

nocrashsequence.zip

running the verifier with the following arguments:

python driver.py -t nocrashsequence.out -m show-ground-specs -s countdowntimer.spec

The second rule does not ground the call to start to anything.

SPEC ((TRUE)[*]); (FALSE) |+ [CB] [32bded6e] void com.peilunzhang.contractiontimerdistilledfix.CountdownFragment$1.onFinish()

However start appears to be in the trace:

[3664] [CB] void com.peilunzhang.contractiontimerdistilledfix.CountdownFragment.onActivityCreated(android.os.Bundle) (36d95a75,NULL) 
  [3665] [CI] void android.app.Fragment.onActivityCreated(android.os.Bundle) (36d95a75,NULL) 
  [3667] [CI] android.view.View android.app.Fragment.getView() (36d95a75) 
  [3669] [CI] android.view.View android.view.View.findViewById(int) (328a72b9,2131427416) 
  [3671] [CI] void android.os.CountDownTimer.<init>(long,long) (3d23c199,10000,1000) 
  [3673] [CI] android.os.CountDownTimer android.os.CountDownTimer.start() (3d23c199)

[smover]

@ftc, cc @sllam: the specification for [CI] [t] android.os.CountDownTimer android.os.CountDownTimer.start() does not include the return value, while the start method in the trace actually does (it should be # = [CI] [t] android.os.CountDownTimer android.os.CountDownTimer.start() )

Now the tool does not look at the semantic of the return type (e.g. void or Int) in the name of the method, but it tests if the return value was used in the specification (i.e. a callin or a callback that does not have the return variable, [CB] [t] void method() instead of retval = [CB] [t] int method()) If there is no return value, then the method is assumed to not return a value (void).

If you change the spec in SPEC TRUE[*]; # = [CI] [t] android.os.CountDownTimer android.os.CountDownTimer.start() |+ [CB] [t] void android.os.CountDownTimer.onFinish() you get the expected result.

The question is, what is the most intuitive semantic if we just write [CB] [t] int method()?

1. Is it a void method? (as it is now, hence disregarding the semantic of "void", "int"...)
2. Is it a method that returns int, but the return value is not meaningful (e.g. it is implicitly # = [CB] [t] int method())?
3. Is it a malformed specification, since we did not specify what to do with the return value?

I would be inclined to adopt 3:

• it is the safest option (the tool yells at you if you did not specify something)
• we interpret the semantic of void, differently from 1
• as a disadvantage, the spec language is a bit more verbose than 1 and 2, but also less error prone.

[ftc]

Option 3 sounds good to me. I think 2 would be the behavior I would initially expect but perhaps we could have it throw an exception if you have a non void method which doesn't specify a return value?