[Jcontractor-user] JInstrument is not working

[thomas r. <rou...@gm...>]

Hello,

I'm a newbie in java and i try to use jcontractor.
Unfortunately, when i call Jinstrument, the instrumentation is not
correclty working.

You can see below my environment and i hope you will find my mistake…

My java version is 1.6.0_65 (on mac osX)

----------------------------------------------
public class Operations
{
   public double sqrt(double value)
   {
      return Math.sqrt(value);
   }
}

----------------------------------------------
public class Operations_CONTRACT
{
   protected boolean _Invariant()
   {
      System.out.println("=== Invariant ===");
      return true;
   }

   protected boolean sqrt_Precondition (double value)
   {
      System.out.println("=== Precondition ===");
      return value > 0;
   }
}

----------------------------------------------
public class main_with_problem
{
   /**
   * @param args
   */
   public static void main(String[] args)
   {
      @SuppressWarnings("unused")
      double result = 0;
      Operations Op = new Operations();

     System.out.println("=== Call sqrt ===");

      result = Op.sqrt(-1.0); // Precondition is not correct
      System.out.println("=== exit of sqrt ===");
      System.out.println(result);
   }
}


i perform the following script to compile, instrum and run :

----------------------------------------------
#!/bin/bash

jcontractor_file_path="jcontractor/jcontractor.jar"
without_contracts_dir="without_contracts_dir"
with_contracts_dir="with_contracts_dir"
main_dir="main_dir"

rm -rf $without_contracts_dir
rm -rf $with_contracts_dir
rm -rf $main_dir

mkdir $without_contracts_dir
mkdir $with_contracts_dir
mkdir $main_dir

echo "============ ls -R ========="
ls -R

echo "============ COMPILE ========="
javac Operations.java                     -d $without_contracts_dir
javac Operations_CONTRACT.java -d $without_contracts_dir

echo "============ ls -R ========="
ls -R

echo "============ INSTRUM ========="
cmdline="-classpath $without_contracts_dir:$jcontractor_file_path
jInstrument -v -pre -d $with_contracts_dir
$without_contracts_dir/Operations.class"
echo $cmdline
java $cmdline

echo "============ ls -R ========="
ls -R

echo "============ COMPILE MAIN ========="
cmdline_main="-classpath .:$with_contracts_dir:$without_contracts_dir
-d $main_dir main_with_problem.java"
echo $cmdline_main
javac $cmdline_main

echo "============ ls -R ========="
ls -R

echo "==========RUN MAIN =========="
cd $main_dir
exe_cmd=" -classpath .:../$with_contracts_dir main_with_problem"
echo $exe_cmd
java $exe_cmd


And the output is :
./run.sh
============ ls -R =========
Operations.java          Operations_CONTRACT.java jcontractor
    main_dir                 main_with_problem.java   run.sh
        with_contracts_dir       without_contracts_dir

./jcontractor:
jcontractor.jar

./main_dir:

./with_contracts_dir:

./without_contracts_dir:
============ COMPILE =========
============ ls -R =========
Operations.java          Operations_CONTRACT.java jcontractor
    main_dir                 main_with_problem.java   run.sh
        with_contracts_dir       without_contracts_dir

./jcontractor:
jcontractor.jar

./main_dir:

./with_contracts_dir:

./without_contracts_dir:
Operations.class          Operations_CONTRACT.class
============ INSTRUM =========
-classpath without_contracts_dir:jcontractor/jcontractor.jar
jInstrument -v -pre -d with_contracts_dir
without_contracts_dir/Operations.class
============ ls -R =========
Operations.java          Operations_CONTRACT.java jcontractor
    main_dir                 main_with_problem.java   run.sh
        with_contracts_dir       without_contracts_dir

./jcontractor:
jcontractor.jar

./main_dir:

./with_contracts_dir:
Operations.class

./without_contracts_dir:
Operations.class          Operations_CONTRACT.class
============ COMPILE MAIN =========
-classpath .:with_contracts_dir:without_contracts_dir -d main_dir
main_with_problem.java
============ ls -R =========
Operations.java          Operations_CONTRACT.java jcontractor
    main_dir                 main_with_problem.java   run.sh
        with_contracts_dir       without_contracts_dir

./jcontractor:
jcontractor.jar

./main_dir:
main_with_problem.class

./with_contracts_dir:
Operations.class

./without_contracts_dir:
Operations.class          Operations_CONTRACT.class
==========RUN MAIN ==========
-classpath .:../with_contracts_dir main_with_problem
=== Call sqrt ===
=== exit of sqrt ===
NaN



So we can see precondition function is not called ;-(
i really don't understand…

Thanks a lot for your help !
Regards,
Thomas