Symbolic execution failed

596 views
Skip to first unread message

Zhenyu Zhou

unread,
Nov 17, 2015, 4:13:53 PM11/17/15
to Java™ Pathfinder
Hello,

I intend to do SE with JPF with jpf-core and jpf-symbc (I've compiled these two repos by `ant` with the default configuration. They should be the latest version because I fetched them just now). However, JPF throws exceptions when I run SE. Could anyone please help me?

In more detail, I get the following errors. The same error for command `java -jar ./build/RunJPF.jar  ~/jpf/test/Example.jpf`.

~/jpf/jpf-core$ ./bin/jpf ~/jpf/test/Example.jpf
JavaPathfinder core system v8.0 (rev 29) - (C) 2005-2014 United States Government. All rights reserved.


====================================================== system under test
Example.main()

====================================================== search started: 11/17/15 3:58 PM
First
[SEVERE] JPF exception, terminating: exception during searchFinished() notification
java.lang.NullPointerException
    at gov.nasa.jpf.symbc.SymbolicListener.publishFinished(SymbolicListener.java:613)
    at gov.nasa.jpf.report.Publisher.publishFinished(Publisher.java:344)
    at gov.nasa.jpf.report.ConsolePublisher.publishFinished(ConsolePublisher.java:126)
    at gov.nasa.jpf.report.Reporter.publishFinished(Reporter.java:248)
    at gov.nasa.jpf.report.Reporter.searchFinished(Reporter.java:295)
    at gov.nasa.jpf.search.Search.notifySearchFinished(Search.java:569)
    at gov.nasa.jpf.search.DFSearch.search(DFSearch.java:110)
    at gov.nasa.jpf.JPF.run(JPF.java:613)
    at gov.nasa.jpf.JPF.start(JPF.java:189)
    at sun.reflect.NativeMethodAccessorImpl.invoke0(Native Method)
    at sun.reflect.NativeMethodAccessorImpl.invoke(NativeMethodAccessorImpl.java:62)
    at sun.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:43)
    at java.lang.reflect.Method.invoke(Method.java:497)
    at gov.nasa.jpf.tool.Run.call(Run.java:80)
    at gov.nasa.jpf.tool.RunJPF.main(RunJPF.java:116)
---------------------- JPF error stack trace ---------------------
gov.nasa.jpf.JPFListenerException: exception during searchFinished() notification
    at gov.nasa.jpf.search.Search.notifySearchFinished(Search.java:572)
    at gov.nasa.jpf.search.DFSearch.search(DFSearch.java:110)
    at gov.nasa.jpf.JPF.run(JPF.java:613)
    at gov.nasa.jpf.JPF.start(JPF.java:189)
    at sun.reflect.NativeMethodAccessorImpl.invoke0(Native Method)
    at sun.reflect.NativeMethodAccessorImpl.invoke(NativeMethodAccessorImpl.java:62)
    at sun.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:43)
    at java.lang.reflect.Method.invoke(Method.java:497)
    at gov.nasa.jpf.tool.Run.call(Run.java:80)
    at gov.nasa.jpf.tool.RunJPF.main(RunJPF.java:116)
Caused by: java.lang.NullPointerException
    at gov.nasa.jpf.symbc.SymbolicListener.publishFinished(SymbolicListener.java:613)
    at gov.nasa.jpf.report.Publisher.publishFinished(Publisher.java:344)
    at gov.nasa.jpf.report.ConsolePublisher.publishFinished(ConsolePublisher.java:126)
    at gov.nasa.jpf.report.Reporter.publishFinished(Reporter.java:248)
    at gov.nasa.jpf.report.Reporter.searchFinished(Reporter.java:295)
    at gov.nasa.jpf.search.Search.notifySearchFinished(Search.java:569)
    ... 9 more

Attachments are my configuration and testing files. The path for them are:
~/.jpf/site.properties
~/jpf/test/Example.java
~/jpf/test/Example.jpf

I downloaded the Example.* from tutorial with slightly modification and I'm sure the .java file can be compiled and executed normally. And both jpf-core/ and jpf-symbc/ are under ~/jpf/:
~/jpf$ ls
jpf-core  jpf-symbc  test


Another concern is that I find this statement in Example.jpf:
symbolic.method= examples.Example.foo(sym#con)

This statement exist in the original tutorial file but I'm not sure what is "sym#con" here. Will the part after "#" be commented? However, if I remove "sym#con", problem remains. If I remove "(sym#con)", I got the exception as "index out of bound: -1".

Do I miss anything here (eg. missing configurations, wrong file location, etc.)? Any help would be appreciable.

Thanks!

Zhenyu



site.properties
Example.java
Example.jpf

Kasper Søe Luckow

unread,
Nov 17, 2015, 4:30:39 PM11/17/15
to java-pa...@googlegroups.com
Hi,

The NullPointerException seems to be because the decision procedure has not been set. Oddly, it should default to choco in SymbolicInstructionFactory, but could you try explicitly setting it in Example.jpf, i.e. put in there:
symbolic.dp=choco

Could you also verify that you have
jvm.insn_factory.class=gov.nasa.jpf.symbc.SymbolicInstructionFactory
in jpf.properties in jpf-symbc and that SymbolicInstructionFactory gets instantiated when you run the jpf file.

Regarding your second question:
In the specification of symbolic methods, '#' simply acts as a separator between the arguments. 'sym' means that the parameter is treated symbolically, while 'con' means that the parameter is treated concretely.

Kasper

--

---
You received this message because you are subscribed to the Google Groups "Java™ Pathfinder" group.
To unsubscribe from this group and stop receiving emails from it, send an email to java-pathfind...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

Quoc-Sang Phan

unread,
Nov 17, 2015, 4:35:40 PM11/17/15
to Java™ Pathfinder
Apart from Kasper's suggestion, you also forgot to modify the symbolic method when deleting the package:

symbolic.method= examples.Example.foo(sym#con)

==> should be changed to: symbolic.method= Example.foo(sym#con)

Zhenyu Zhou

unread,
Nov 17, 2015, 4:41:27 PM11/17/15
to Java™ Pathfinder
Hi Kasper,

Thanks for your reply! I just added "symbolic.dp=choco" to Example.jpf but the same problem still exists.

Also, I've checked and do find "jvm.insn_factory.class=gov.nasa.jpf.symbc.SymbolicInstructionFactory" in jpf.properties in jpf-symbc. But I'm not sure how to check whether it is instantiated. Any idea about that?

Zhenyu Zhou

unread,
Nov 17, 2015, 4:45:01 PM11/17/15
to Java™ Pathfinder
Hi Phan,

Oh sorry that's my bad. So now I removed the package in this statement (also with Kasper's suggested modification) and the exception changed as:

~/jpf/jpf-core$ ./bin/jpf ~/jpf/test/Example.jpf
JavaPathfinder core system v8.0 (rev 29) - (C) 2005-2014 United States Government. All rights reserved.


====================================================== system under test
Example.main()

====================================================== search started: 11/17/15 4:42 PM
[SEVERE] JPF exception, terminating: exception during instructionExecuted() notification
java.lang.RuntimeException: ERROR: you need to turn debug option on
    at gov.nasa.jpf.symbc.SymbolicListener.instructionExecuted(SymbolicListener.java:238)
    at gov.nasa.jpf.vm.VM.notifyInstructionExecuted(VM.java:808)
    at gov.nasa.jpf.vm.ThreadInfo.executeInstruction(ThreadInfo.java:1922)
    at gov.nasa.jpf.vm.ThreadInfo.executeTransition(ThreadInfo.java:1859)
    at gov.nasa.jpf.vm.SystemState.executeNextTransition(SystemState.java:765)
    at gov.nasa.jpf.vm.VM.forward(VM.java:1722)
    at gov.nasa.jpf.search.Search.forward(Search.java:579)
    at gov.nasa.jpf.search.DFSearch.search(DFSearch.java:79)

    at gov.nasa.jpf.JPF.run(JPF.java:613)
    at gov.nasa.jpf.JPF.start(JPF.java:189)
    at sun.reflect.NativeMethodAccessorImpl.invoke0(Native Method)
    at sun.reflect.NativeMethodAccessorImpl.invoke(NativeMethodAccessorImpl.java:62)
    at sun.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:43)
    at java.lang.reflect.Method.invoke(Method.java:497)
    at gov.nasa.jpf.tool.Run.call(Run.java:80)
    at gov.nasa.jpf.tool.RunJPF.main(RunJPF.java:116)
---------------------- JPF error stack trace ---------------------
gov.nasa.jpf.JPFListenerException: exception during instructionExecuted() notification
    at gov.nasa.jpf.vm.VM.notifyInstructionExecuted(VM.java:815)
    at gov.nasa.jpf.vm.ThreadInfo.executeInstruction(ThreadInfo.java:1922)
    at gov.nasa.jpf.vm.ThreadInfo.executeTransition(ThreadInfo.java:1859)
    at gov.nasa.jpf.vm.SystemState.executeNextTransition(SystemState.java:765)
    at gov.nasa.jpf.vm.VM.forward(VM.java:1722)
    at gov.nasa.jpf.search.Search.forward(Search.java:579)
    at gov.nasa.jpf.search.DFSearch.search(DFSearch.java:79)

    at gov.nasa.jpf.JPF.run(JPF.java:613)
    at gov.nasa.jpf.JPF.start(JPF.java:189)
    at sun.reflect.NativeMethodAccessorImpl.invoke0(Native Method)
    at sun.reflect.NativeMethodAccessorImpl.invoke(NativeMethodAccessorImpl.java:62)
    at sun.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:43)
    at java.lang.reflect.Method.invoke(Method.java:497)
    at gov.nasa.jpf.tool.Run.call(Run.java:80)
    at gov.nasa.jpf.tool.RunJPF.main(RunJPF.java:116)
Caused by: java.lang.RuntimeException: ERROR: you need to turn debug option on
    at gov.nasa.jpf.symbc.SymbolicListener.instructionExecuted(SymbolicListener.java:238)
    at gov.nasa.jpf.vm.VM.notifyInstructionExecuted(VM.java:808)
    ... 14 more

Kasper Søe Luckow

unread,
Nov 17, 2015, 4:48:56 PM11/17/15
to java-pa...@googlegroups.com
To solve that, your SUT needs be be compiled with the debug flag. If you are using ant, set debug="true" for the javac task.

Zhenyu Zhou

unread,
Nov 17, 2015, 4:56:33 PM11/17/15
to Java™ Pathfinder
I'm sorry that I didn't fully understand your answer. What do you mean by "SUT needs be be compiled with the debug flag"? Does SUT refer to Example.java in this example? If so, I only compile it with `javac Example.java`. Ant is used for compiling JPF itself. Do you mean to find some options (?) for javac in order to add the so called "debug flag"? 

Thanks!

Kasper Søe Luckow

unread,
Nov 17, 2015, 4:59:41 PM11/17/15
to java-pa...@googlegroups.com
I should have been more clear: The SUT (system under test) must be compiled with the debug flag to extract local variable names etc. Since you are compiling the SUT with javac, you can set the debug flag by adding "-g" to the command.

Zhenyu Zhou

unread,
Nov 17, 2015, 5:06:03 PM11/17/15
to Java™ Pathfinder
Sure. I compiled it with "javac -g Example.java" now. Unfortunately, the exception changes back to the first one, ie. NullPointerException.... All files are the same as my first attachment except for the suggested modification:
1. Add symbolic.dp=choco to Example.jpf
2. Remove the package in Example.jpf

Any more ideas to fix it?

Thanks!

Kasper Søe Luckow

unread,
Nov 17, 2015, 5:09:09 PM11/17/15
to java-pa...@googlegroups.com
I don't think that SymbolicInstructionFactory gets instantiated. Could you try just adding a print statement in the constructor and rerun your example. Even better you could use the debugger in, e.g., eclipse to see what is going on? jpf-symbc includes launch configurations for doing that.

Quoc-Sang Phan

unread,
Nov 17, 2015, 5:22:02 PM11/17/15
to Java™ Pathfinder
If you run JPF with the option "-show", it will print the whole configuration.

Zhenyu Zhou

unread,
Nov 17, 2015, 5:24:38 PM11/17/15
to Java™ Pathfinder
I got the following output:
----------- Config contents
branch_start = 1
cg.boolean.false_first = true
cg.break_single_choice = false
cg.enable_atomic = true
cg.enumerate_random = false
cg.max_processors = 1
cg.randomize_choices = NONE
cg.seed = 42
cg.threads.break_arrays = false
cg.threads.break_sleep = true
cg.threads.break_start = true
cg.threads.break_yield = true
classpath = /home/zzy/jpf/test
config = /home/zzy/jpf/test/Example.jpf
config_path = /home/zzy/jpf/test
extensions = /home/zzy/jpf/jpf-core,/home/zzy/jpf/jpf-symbc
jpf-core = /home/zzy/jpf/jpf-core
jpf-core.classpath = /home/zzy/jpf/jpf-core/build/jpf-classes.jar;/home/zzy/jpf/jpf-core/build/examples
jpf-core.native_classpath = /home/zzy/jpf/jpf-core/build/jpf.jar;/home/zzy/jpf/jpf-core/build/jpf-annotations.jar
jpf-core.peer_packages = gov.nasa.jpf.vm,<model>,<default>
jpf-core.sourcepath = /home/zzy/jpf/jpf-core/src/examples
jpf-core.test_classpath = /home/zzy/jpf/jpf-core/build/tests
jpf-symbc = /home/zzy/jpf/jpf-symbc
jpf-symbc.classpath = /home/zzy/jpf/jpf-symbc/build/jpf-symbc-classes.jar
jpf-symbc.native_classpath = /home/zzy/jpf/jpf-symbc/build/jpf-symbc.jar;/home/zzy/jpf/jpf-symbc/build/jpf-symbc-annotations.jar;/home/zzy/jpf/jpf-symbc/lib/choco-1_2_04.jar;/home/zzy/jpf/jpf-symbc/lib/choco-solver-2.1.1-20100709.142532-2.jar;/home/zzy/jpf/jpf-symbc/lib/STPJNI.jar;/home/zzy/jpf/jpf-symbc/lib/scale.jar;/home/zzy/jpf/jpf-symbc/lib/automaton.jar;/home/zzy/jpf/jpf-symbc/lib/iasolver.jar;/home/zzy/jpf/jpf-symbc/lib/string.jar;/home/zzy/jpf/jpf-symbc/lib/solver.jar;/home/zzy/jpf/jpf-symbc/lib/commons-lang-2.4.jar;/home/zzy/jpf/jpf-symbc/lib/commons-math-1.2.jar;/home/zzy/jpf/jpf-symbc/lib/coral.jar;/home/zzy/jpf/jpf-symbc/lib/opt4j-2.4.jar;/home/zzy/jpf/jpf-symbc/lib/libcvc3.jar;/home/zzy/jpf/jpf-symbc/lib/org.sat4j.core.jar;/home/zzy/jpf/jpf-symbc/lib/org.sat4j.pb.jar;/home/zzy/jpf/jpf-symbc/lib/aima-core.jar;/home/zzy/jpf/jpf-symbc/lib/yicesapijava.jar;/home/zzy/jpf/jpf-symbc/lib/PathConditionsReliability-0.0.1.jar;/home/zzy/jpf/jpf-symbc/lib/grappa.jar
jpf-symbc.test_classpath = build/tests
jpf.app = /home/zzy/jpf/test/Example.jpf
jpf.home = /home/zzy/jpf
jpf.print_exception_stack = true
jpf.site = /home/zzy/.jpf/site.properties
jvm.insn_factory.class = gov.nasa.jpf.jvm.bytecode.InstructionFactory
jvm.nested_init = false
jvm.nested_init.exclude = java.*,javax.*,sun.misc.*
listener = gov.nasa.jpf.symbc.SymbolicListener
listener.autoload = gov.nasa.jpf.NonNull,gov.nasa.jpf.Const
listener.gov.nasa.jpf.Const = gov.nasa.jpf.tools.ConstChecker
listener.gov.nasa.jpf.NonNull = gov.nasa.jpf.tools.NonNullChecker
log.handler.class = gov.nasa.jpf.util.LogHandler
log.level = warning
peer_packages = gov.nasa.jpf.symbc;
race.exclude = java.*,javax.*
report.class = gov.nasa.jpf.report.Reporter
report.console.class = gov.nasa.jpf.report.ConsolePublisher
report.console.constraint = constraint,snapshot
report.console.finished = result,statistics
report.console.probe = statistics
report.console.property_violation = error,snapshot
report.console.show_code = false
report.console.show_method = true
report.console.show_steps = true
report.console.start = jpf,sut
report.console.transition =
report.html.class = gov.nasa.jpf.report.HTMLPublisher
report.html.constraint = constraint
report.html.finished = result,statistics,error,snapshot,output
report.html.property_violation =
report.html.start = jpf,sut,platform,user,dtg,config
report.publisher = console
report.xml.class = gov.nasa.jpf.report.XMLPublisher
search.class = gov.nasa.jpf.search.DFSearch
search.heuristic.branch.count_early = true
search.heuristic.branch.no_branch_return = -1
search.heuristic.queue_limit = -1
search.match_depth = false
search.min_free = 1M
search.multiple_errors = true
search.properties = gov.nasa.jpf.vm.NotDeadlockedProperty,gov.nasa.jpf.vm.NoUncaughtExceptionsProperty
sourcepath = /home/zzy/jpf/test
symbolic.dp = choco
symbolic.method = Example.foo(sym#con)
target = Example
test.report.console.finished = result
vm.backtracker.class = gov.nasa.jpf.vm.DefaultBacktracker
vm.boot_classpath = <system>
vm.class = gov.nasa.jpf.vm.SingleProcessVM
vm.classloader.class = gov.nasa.jpf.jvm.JVMSystemClassLoaderInfo
vm.fields_factory.class = gov.nasa.jpf.vm.DefaultFieldsFactory
vm.finalize = false
vm.gc = true
vm.heap.class = gov.nasa.jpf.vm.OVHeap
vm.ignore_uncaught_handler = false
vm.max_alloc_gc = -1
vm.max_transition_length = 50000
vm.no_orphan_methods = false
vm.pass_uncaught_handler = true
vm.path_output = false
vm.process_finalizers = false
vm.restorer.class = .vm.DefaultMementoRestorer
vm.reuse_tid = false
vm.scheduler.class = gov.nasa.jpf.vm.DelegatingScheduler
vm.scheduler.sharedness.class = gov.nasa.jpf.vm.PathSharednessPolicy
vm.scheduler.sync.class = gov.nasa.jpf.vm.AllRunnablesSyncPolicy
vm.scheduler_factory.class = gov.nasa.jpf.vm.DefaultSchedulerFactory
vm.serializer.class = gov.nasa.jpf.vm.serialize.CFSerializer
vm.shared.break_on_exposure = true
vm.shared.never_break_fields = java.lang.Thread*.*,java.lang.System.*,java.lang.Runtime.*,java.lang.Boolean.*,java.lang.String.*,java.lang.*.TYPE,java.util.HashMap.EMPTY_TABLE,java.util.HashSet.PRESENT,java.util.concurrent.ThreadPoolExecutor*.*,java.util.concurrent.ThreadPoolExecutor*.*,java.util.concurrent.TimeUnit.*,java.util.concurrent.Exchanger.CANCEL,java.util.concurrent.Exchanger.NULL_ITEM,java.util.concurrent.Executors$DefaultThreadFactory.*,sun.misc.VM.*,sun.misc.SharedSecrets.*,sun.misc.Unsafe.theUnsafe,gov.nasa.jpf.util.test.TestJPF.*
vm.shared.never_break_methods = java.util.concurrent.ThreadPoolExecutor.processWorkerExit,java.util.concurrent.locks.Abstract*Synchronizer.*,java.util.concurrent.ThreadPoolExecutor.getTask,java.util.concurrent.atomic.Atomic*.*,java.util.concurrent.Exchanger.doExchange,java.util.concurrent.ThreadPoolExecutor.interruptIdleWorkers,java.util.concurrent.TimeUnit.*
vm.shared.never_break_types = java.util.concurrent.TimeUnit
vm.shared.skip_constructed_finals = false
vm.shared.skip_finals = true
vm.shared.skip_static_finals = false
vm.shared.sync_detection = true
vm.statics.class = gov.nasa.jpf.vm.OVStatics
vm.store_steps = false
vm.sysprop.source = SELECTED
vm.threadlist.class = gov.nasa.jpf.vm.ThreadList
vm.time.class = gov.nasa.jpf.vm.SystemTime
vm.tree_output = true
vm.untracked = true
vm.verify.ignore_path = true

JavaPathfinder core system v8.0 (rev 29) - (C) 2005-2014 United States Government. All rights reserved.
// null pointer exception below

Is it excepted?

Kasper Søe Luckow

unread,
Nov 17, 2015, 5:35:28 PM11/17/15
to java-pa...@googlegroups.com
The instruction factory is incorrectly set to:
jvm.insn_factory.class = gov.nasa.jpf.jvm.bytecode.InstructionFactory

Can you verify that you have
jvm.insn_factory.class=gov.nasa.jpf.symbc.SymbolicInstructionFactory
in jpf.properties in jpf-symbc

Did you make any changes to jpf.properties?

--

Zhenyu Zhou

unread,
Nov 17, 2015, 6:40:20 PM11/17/15
to Java™ Pathfinder
I double-checked it and it's indeed there (in jpf.properties of jpf-symbc):
jvm.insn_factory.class=gov.nasa.jpf.symbc.SymbolicInstructionFactory

It somehow isn't loaded... I didn't change anything with jpf.properties in both jpf-core and jpf-symbc after downloading them.

Another concern is that I run jpf inside jpf-core/ folder, is it correct? Should I run the bin/jpf in jpf-symbc instead?
If so, I got the following output (still not work):
~/jpf/jpf-symbc$ ./bin/jpf -show ~/jpf/test/Example.jpf
jvm.insn_factory.class = gov.nasa.jpf.symbc.SymbolicInstructionFactory
[SEVERE] JPF configuration error: error instantiating class gov.nasa.jpf.jvm.JVMSystemClassLoaderInfo for entry "vm.classloader.class":
> exception in gov.nasa.jpf.jvm.JVMSystemClassLoaderInfo(gov.nasa.jpf.vm.VM,int):
>> java.lang.NullPointerException
> used within "vm.class" instantiation of class gov.nasa.jpf.vm.SingleProcessVM
[SEVERE] JPF terminated

Kasper Søe Luckow

unread,
Nov 17, 2015, 6:46:17 PM11/17/15
to java-pa...@googlegroups.com
Yes, the jpf script uses the current dir for specifying the JPF_HOME variable (you can open the script and see what is going on -- it is quite simple). Actually, can you do:
~/jpf/jpf-symbc$ ../jpf-core/bin/jpf ~/jpf/test/Example.jpf

Zhenyu Zhou

unread,
Nov 17, 2015, 7:04:27 PM11/17/15
to Java™ Pathfinder
Great that works! Thank you! I've never thought I should use the jpf of one folder inside another folder....

So I get the following result:
====================================================== Method Summaries
Inputs: x_1_SYMINT,y_CONCRETE,

Example.foo(2,1)  --> Return Value: 2
Example.foo(-1000000,1)  --> Return Value: 1
Inputs: x_1_SYMINT,y_CONCRETE,

Example.foo(2,1)  --> Return Value: 2
Example.foo(-1000000,1)  --> Return Value: 1

Could you please kindly tell me what does "x_1_SYMINT,y_CONCRETE" mean? Is it the minimum int value and the given parameter "1"? Also, are there any special meanings of displaying this result twice?

Thanks!

Kasper Søe Luckow

unread,
Nov 17, 2015, 7:11:45 PM11/17/15
to java-pa...@googlegroups.com
Yes, unless you open that script, I agree, it is not clear. I missed that from your initial description of what you tried.
jpf-symbc applies a naming scheme to the symbolic variables -- x_1_SYMINT is simply the symbolic variable for argument x. The same applies for y, which has concrete execution semantics.
I haven't used the SymbolicListener much, so I cannot comment why the output is written twice -- I guess you can ignore that. The output:
Example.foo(2,1)  --> Return Value: 2
Example.foo(-1000000,1)  --> Return Value: 1

Are simply the two test cases produced as a result of exploring the program symbolically. x has been instantiated with two concrete values (2 and -1000000) corresponding to the solutions of the resulting path conditions.

Zhenyu Zhou

unread,
Nov 17, 2015, 7:18:08 PM11/17/15
to Java™ Pathfinder
OK I got it. Thank you so much!!
Reply all
Reply to author
Forward
0 new messages